0
$\begingroup$

In type theory, all computable functions must terminate, however, numbers like Pi are non-terminating real numbers, hence a non-terminating function is required to compute this number, even though one would never compute the full sequence.

How does type theory view/deal with such non-terminating numbers/object?

$\endgroup$
2
  • 1
    $\begingroup$ en.wikipedia.org/wiki/Computable_number $\endgroup$
    – D.W.
    Commented Apr 23, 2021 at 7:37
  • $\begingroup$ Forget about type theory for a second. What do you mean by "non-terminating function required to compute this number"? If your function generates an infinite sequence of digits approximating your number with arbitrary precision, then the type is trivial $seq<int>$ (or e.g. $seq<bool>$ for binary digits). $\endgroup$
    – user114966
    Commented Apr 23, 2021 at 7:42

1 Answer 1

4
$\begingroup$

If by "non-terminating real number" you mean to say that the digit expansion of the number is an infinite sequence, then that is not saying much, because every real number is "non-terminating" in this sense, even the real number 42, for its digit expansion is

$$41.999999999999999999999999999999....$$

In any case, nobody suggests that the digits must somehow be computed all at once, although that is a common misconception that arises in the study of computability of reals. We just need a method which computes any digit we desire – but we never desire all the digits at once.

A sequence of digits is a function $f : \mathbb{N} \to \mathbb{N}$, and such functions can be perfectly managed by type theory. In fact, the correct way to represent a real number by a sequence is to use positive and negative digits, or else you can't compute certain operations (such as $+$). So in reality, in type theory or in any other setting a real number may be represented by a sequence of digits $f : \mathbb{N} \to \{-9, -8, \ldots, 8, 9\}$. Even better but equivalent is the representation by which a real number is represented by a map $g : \mathbb{N} \to \mathbb{Q}$ satisfying the condition $\forall m, n \in \mathbb{N} \,.\, |g(m) - g(n)| < 2^{-\min(m,n)-1}$. Such a map represents the number $\lim_n g(n)$.

All of the above can be stated in type theory: $$ \Sigma (g : \mathbb{N} \to \mathbb{Q}) \, \Pi (m, n : \mathbb{N}) \; \mathrm{Id}_\mathbb{Q}(1, \max(|g(m) - g(n)| \cdot 2^{1 + \min(m, n)}, 1)) $$ The inner $\mathrm{Id}$-type says $$\max(|g(m) - g(n)| \cdot 2^{1 + \min(m, n)}, 1) = 1$$ which is just a fancy way of stating $$|g(m) - g(n)| \cdot 2^{1 + \min(m, n)} \leq 1.$$

$\endgroup$
3
  • $\begingroup$ This question deals with a slightly simpler notion. I am not concerned with notions such as 0.9... = 1, or even any equality. What I am interested in is the following: In type theory all lambda terms are formed such that they are guaranteed to terminate. A constant such as Pi has many algorithms, non terminating. How does one define Pi in Type theory (0-arity, non-terminating). I understand that once we "use" Pi in some calculation, somehow it will be limited to an finite number of steps, in order to give an approximation, but before that, how do you reason about Pi in type theory? $\endgroup$
    – RFV
    Commented Apr 26, 2021 at 2:33
  • $\begingroup$ It is false that $\pi$ has "non-terminating algorithms". You need to understand this point first. Also, I wrote out explicitly the type of (representations of) reals in type theory, above. There is going to be a term of that type which represents $\pi$. $\endgroup$ Commented Apr 26, 2021 at 8:02
  • $\begingroup$ Once again: $\pi$ is represented by a function of type $\mathbb{N} \to \mathbb{N}$. There is nothing "non-terminating" about that, unless you think that every such function is somehow non-terminating (in which case you have to clear that up first). $\endgroup$ Commented Apr 26, 2021 at 8:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.