17

I work in real-number computation, and I wish I knew the real answer. But I can speculate. It's a sociological problem, I think. The community of people who work on exact real arithmetic consists of theoreticians who are not used to developing software. So they usually relegate the task of implementation to students (a notable exception is Norbert Müller's ...


15

This is not a research-level question, but since the general level of interest seems high, here is an answer. I cannot guess from your question whether you're shooting for something that will result in the usual computable numbers, or you're trying to surpass that. First we have Turing's definition of computable real number, and it is the one others have ...


15

A nice example is given by Godelization: in lambda calculus, the only thing you can do with a function is to apply it. As a result, there is no way to write a closed function of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, which takes a function argument and returns a Godel code for it. Adding this as an axiom to Heyting arithmetic is usually called "...


13

I am not exactly sure what the question is here, but I can try to say a bit to clean up possible misunderstandings. First of all, if we are talking about complexity of a map $f : \mathbb{R} \to \mathbb{R}$, it makes no sense to ask "What is a good representation for $\sqrt{2}$?" Instead, you have to ask "What is a good representation for all inputs of $f$?"....


11

The simplest answer is given by the fact that typed lambda calculi correspond to logics (simply typed lambda calculus -> predicate logic; system f -> second-order logic) and consistent logics cannot prove their own consistency. So let's say that you have natural numbers (or a Church encoding of natural numbers) in your typed lambda calculus. It's possible ...


10

In general, people always care about floating point errors. However I disagree with Andrej, and I do not think that floats are preferred to arbitrary precision reals (for the most part) because of sociological reasons. I believe the main argument against exact computation of reals is one of performance. So the short answer is, whenever performance is more ...


10

The untyped $\lambda$-calculus posseses general recursion in the form of the $Y$ combinator. Simply-typed $\lambda$-calculus does not. Thus, any function that requires general recursion is a candidate, for example the Ackermann function. (I am skipping some details on how precisely we represent the natural numbers in each system, but essentially any ...


9

You are touching on some very interesting basic questions about mathematics in general. Do we construct mathematical objects and later discover their structure, or do we construct objects with a specific structure in mind? I think the answer is not simple. Sometimes we "design" structures to order, and sometimes we discover them. I believe the quarternions ...


8

Kristoffer's solution can be used to show that, assuming reals are represented so that we can compute limits of sequences of reals which are computably Cauchy. Recall that a sequence $(a_n)_n$ is computably Cauchy if there is a computable map $f$ such that, given any $k$ we have $|a_{m} - a_{n}| < 2^{-k}$ for all $m, n \geq f(k)$. The standard ...


7

No, it is not decidable. A good heuristic to answer such questions is the following: every computable map is continuous. If you could decide whether $f(x) = 0$ for all $x \in \mathbb{C}$, then the characteristic map $d$ of such a decision procedure, namely $$d : f \mapsto \begin{cases} 1 & \text{if $\forall x \in \mathbb{C} . f(x) = 0$}\\ 0 & \text{...


6

The simply-typed lambda calculus is actually surprisingly weak. For example, it can't recognize the regular language $\mathtt{a}^*$. I've never found a precise characterization of the set of languages that STLC can recognize, though.


5

Given a Turing machine $M$, define a Turing machine $M'$ representing a number as follows: On input $i$ run $M$ for $i$ steps on the empty input. If $M$ halted, output $0$. Otherwise output the $i$th bit of $\pi$.


4

One vision of the limits of strongly normalizing calculi I like is the computability angle. In a strongly normalizing typed calculus, such as the core simply-typed lambda calculus, System F, or Calculus of Constructions, you have a proof that all terms eventually terminate. If this proof is constructive, you get a fixed algorithm to evaluate all terms with ...


4

Computing an 'infinite' object is usually defined based on Turing machines with one-way output tape; cmp. Section 2.1 in [Weihrauch'00]. This also asserts closure under composition. [Turing'36] first defined computability of real numbers based on their binary (historically actually: decimal) and in [Turing'37] corrected himself to consider sequences of ...


3

How about, $x\in[0,1]$ is computable if there is a TM $M$ which, on input $n\in\mathbb{N}$, prints the first $n$ digits of the decimal expansion of $x$ and then halts.


3

The standard solution is to require write only tape if you want to use TTE. Obviously you can have RW work tapes. Another solution is information theoretic (domain theory) and says that you get better and better approximations approximation to the real number as internals and the limit is a single number. Also keep in mind that decimal representation of ...


3

You can (without too much work) find a number $K$ such that if $|x| > K$ then $|a_n x^n| > \sum_{k<n} |a_k x^k|$, and so all roots are inside $(-K,K)$ and the distance between them is smaller than $2K$.


3

Another model possibly to explore, is that of the Feasible RAM model. This is a modified real RAM model for Real computation, Feasible RAM, or a modified RAM model which uses both the discrete, and real valued arithmetic operations. This model allows for real, and discrete operations, and the Turing model, is interchangeable with it. The Feasible RAM model ...


3

To turn my comment into an answer... Andrej Bauer in this post makes the parenthetical claim An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic. He never explicitly defines acceptable or cites the theorem. I assume the OPs question is the following. What theorem is Andrej Bauer ...


3

No, it is undecidable. Imagine a TM that outputs a sequence $0.1111\ldots$ that may be finite or not. If it is finite, the conversion algorithm should give some fraction like $\frac{11\ldots11}{10\ldots000}$. If it is infinite (the TM doesn't halt) then the output should be $\frac{1}{9}$. Any program that converts between the $TM$ representation of a number ...


2

The first theorem of the form you are asking about was proved by Y. Moschovakis in Notation systems and recursive ordered fields, Compositio Mathematica 17:40–71 (1965). Then in the context of Type Two Effectivity a similar theorem was proved by P. Hertling, see A real number structure that is effectively categorical, Mathematical Logic Quarterly, 45(2):147–...


2

I think it's undecidable, but I don't have a proof. Intuitively, if $s\neq qr+p$ for all $p,q\in\mathbb{Q}$ (i.e. if the answer is "NO"), then you will be always looking for a "next" pair $(q,p)$ such that $|s-(qr+p)|$ is smaller than before. You don't really have an argument to decide when to stop and return "NO" because, for all you know, there is a better ...


2

One solution is what Radu GRIGore suggested, namely requiring that every digit becomes fixed after some (finite) number of steps. Of course, this comes with the practical issue that you never know whether a digit is already fixed. For defining computability, this is seems to be fine since the Turing machine is never actually used in practice by someone who ...


1

I guess I have an alternative solution. Let $f :\subseteq \Sigma^{\omega} \to \Sigma^{\omega}$ be computable. Define $$ h(u) = v \mbox{ iff } f(u\Sigma^{\omega}) = \{v\} \mbox{ with $u$ minimal} $$ and let $h(u)$ diverge otherwise. Then $\mbox{dom}(h)$ is prefix-free for if $h(u) = v$ then $f(u\Sigma^{\omega}) = \{v\}$ as the machine behaves the same when ...


1

The set of transcendentals is not open in $\mathbf R$ (in particular, it is dense and codense in $\mathbf R$. Hence it is undecidable.


Only top voted, non community-wiki answers of a minimum length are eligible