اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدComputing with Classical Real Numbers
187
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN library from Nijmegen defines constructively valid real numbers. Unfortunately, this means results about one structure cannot easily be used in the other structure. We present a way interfacing these two libraries by showing that their real number structures are isomorphic assuming the classical axioms already present in the standard library reals. This allows us to use OConnors decision procedure for solving ground inequalities present in CoRN to solve inequalities about the reals from the Coq standard library, and it allows theorems from the Coq standard library to apply to problem about the CoRN reals.
قيم البحث
اقرأ أيضاً
We study a variant of the Ackermann encoding $mathbb{N}(x) := sum_{yin x}2^{mathbb{N}(y)}$ of the hereditarily finite sets by the natural numbers, applicable to the larger collection $mathsf{HF}^{1/2}$ of the hereditarily finite hypersets. The propos
ed variation is obtained by simply placing a `minus sign before each exponent in the definition of $mathbb{N}$, resulting in the expression $mathbb{R}(x) := sum_{yin x}2^{-mathbb{R}(y)}$. By a careful analysis, we prove that the encoding $mathbb{R}_{A}$ is well-defined over the whole collection $mathsf{HF}^{1/2}$, as it allows one to univocally assign a real-valued code to each hereditarily finite hyperset. We also address some preliminary cases of the injectivity problem for $mathbb{R}_{A}$.
Floating point arithmetic allows us to use a finite machine, the digital computer, to reach conclusions about models based on continuous mathematics. In this article we work in the other direction, that is, we present examples in which continuous mat
hematics leads to sharp, simple and new results about the evaluation of sums, square roots and dot products in floating point arithmetic.
Quantum devices may overcome limitations of classical computers in studies of nuclear structure functions and parton Wigner distributions of protons and nuclei. In this talk, we discuss a worldline approach to compute nuclear structure functions in t
he high energy Regge limit of QCD using a hybrid quantum computer, by expressing the fermion determinant in the QCD path integral as a quantum mechanical path integral over $0+1$-dimensional fermionic and bosonic world-lines in background gauge fields. Our simplest example of computing the well-known dipole model result for the structure function $F_2$ in the high energy Regge limit is feasible with NISQ era technology using few qubits and shallow circuits. This example can be scaled up in complexity and extended in scope to compute structure functions, scattering amplitudes and other real-time correlation functions in QCD, relevant for example to describe non-equilibrium transport of quarks and gluons in a Quark-Gluon-Plasma.
A perfect number is a positive integer n such that n equals the sum of all positive integer divisors of n that are less than n. That is, although n is a divisor of n, n is excluded from this sum. Thus 6 = 1 + 2 + 3 is perfect, but 12 < 1 + 2 + 3 + 4
+ 6 is not perfect. An ACL2 theory of perfect numbers is developed and used to prove, in ACL2(r), this bit of mathematical folklore: Even if there are infinitely many perfect numbers the series of the reciprocals of all perfect numbers converges.
Inspired by a mathematical riddle involving fuses, we define the fusible numbers as follows: $0$ is fusible, and whenever $x,y$ are fusible with $|y-x|<1$, the number $(x+y+1)/2$ is also fusible. We prove that the set of fusible numbers, ordered by t
he usual order on $mathbb R$, is well-ordered, with order type $varepsilon_0$. Furthermore, we prove that the density of the fusible numbers along the real line grows at an incredibly fast rate: Letting $g(n)$ be the largest gap between consecutive fusible numbers in the interval $[n,infty)$, we have $g(n)^{-1} ge F_{varepsilon_0}(n-c)$ for some constant $c$, where $F_alpha$ denotes the fast-growing hierarchy. Finally, we derive some true statements that can be formulated but not proven in Peano Arithmetic, of a different flavor than previously known such statements: PA cannot prove the true statement For every natural number $n$ there exists a smallest fusible number larger than $n$. Also, consider the algorithm $M(x)$: if $x<0$ return $-x$, else return $M(x-M(x-1))/2$. Then $M$ terminates on real inputs, although PA cannot prove the statement $M$ terminates on all natural inputs.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
