Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userComputing with Classical Real Numbers
224
0
0.0
(
0
)
Added by
Russell O'Connor
Publication date
2008
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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 proposed 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 mathematics 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 the 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 the 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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
