<p>This just appeared on arxive.org and may be of some help.</p>

<blockquote>
  <p><a href="http://arxiv.org/abs/1011.6353"><em>The definability of functionals in Gödel's theory T</em></a></p>
  
  <p>Matthew P. Szudzik (Carnegie Mellon)</p>
  
  <p>Gödel's theory T can be understood as a theory of the simply-typed lambda calculus that is extended to include the constant 0, the successor function $S$, and the operator $R_\tau$ for primitive recursion on objects of type $\tau$. It is known that the functions from non-negative integers to non-negative integers that can be defined in this theory are exactly the $\epsilon$-recursive functions of non-negative integers. But it is not well-known which functionals of arbitrary type can be defined in T.
  We show that when the domain and codomain are restricted to pure closed normal forms, the functionals of arbitrary type that are definable in T are exactly those functionals that can be encoded as $\epsilon$-recursive functions of non-negative integers. This result has many interesting consequences, including a new characterization of T.</p>
</blockquote>

CC BY-SA 2.5
2010-11-30T20:05:13.917Z
2010-11-30T20:05:13.917Z
Andrej Bauer
<p>My intuition would be that the length of the Collatz sequence is not definable in System F. That is, we cannot compute the length of the Collatz sequence starting with a given <span class="math-container">$n$</span>.</p>
<p>My reasoning is that System F can perform loops but only if the total number of iterations is known in advance. For instance, one can compute <span class="math-container">$f(f(f(...(f(x))...)))$</span> where the number of applications of <span class="math-container">$f$</span> is given. But a program in System F cannot keep repeating a computation until some condition is met. We cannot keep applying <span class="math-container">$f(f(f(...)))$</span> until the result becomes equal to <span class="math-container">$1$</span>. But that kind of loop is required to compute the length of the Collatz sequence.</p>

CC BY-SA 4.0
2024-11-03T07:59:06.773Z
We *currently* do not know any better algorithm other than the one here, because we do not know much of anything about properties of this function, and in particular, we do not know even know whether it is *total*. This is a requirement in the question, as non-total computable functions cannot be defined in System T, and examples of these are well known and easy to find. It is possible, and indeed very likely, that once someone proves that this function is total (= the Collatz conjecture), they will also prove the lengths of the sequences are bounded by a simple function such as iterated ...
Emil Jeřábek
CC BY-SA 4.0
2024-11-03T07:59:12.693Z
...  exponential, making it definable in System T. Also, the question is about System T, whereas your answer is about System F (though this does not really make a difference, as the reasoning applies to any computably enumerable system of total computable functions).
Emil Jeřábek
CC BY-SA 4.0
2024-11-03T08:56:33.590Z
@EmilJeřábek OK I see, thank you for explanations!
winitzki
CC BY-SA 4.0
2024-11-02T19:45:51.080Z
2024-11-03T06:44:46.673Z
2024-11-03T06:44:46.673Z
winitzki
<p>Interpreters for T are not definable in T, thanks to the incompleteness theorem. </p>

<p>Concretely, fix a Godel encoding, and then let $f$ be the function which takes a pair consisting of a Godel-encoding of a closed term of type $\mathbb{N} \to \mathbb{N}$, and a natural number in $\mathbb{N}$, and returns the value of the application. This function is not definable in T. It's a worthwhile exercise to work out how you can use a self-interpreter to define an infinitely looping program.</p>

CC BY-SA 4.0
2024-11-01T19:03:50.173Z
10 years later, here's a counterexample: take the Gödel encoding which takes a term $t$ of T, and encodes it as the "usual" (using, say the one detailed [here](https://en.wikipedia.org/wiki/G%C3%B6del_numbering#G%C3%B6del's_encoding)) encoding of the pair $\langle t, v\rangle$ of $t$ and the *normal form* $v$ of $t$. This is computable and bijective, but given this encoding, system $T$ easily can compute the value $v$ (by second projection). So one must, as usual, either give an explicit encoding or somehow define "reasonable" ones.
cody
CC BY-SA 4.0
2024-11-03T07:42:15.677Z
@cody: This appears in Theorem 3.2 of [On self-interpreters for System T and other $\lambda$-calculi](https://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/) in 2016. I should have callled that note "Much ado about nothing". But more importantly, how is your idea a counter-example to Neel's?
Andrej Bauer
CC BY-SA 4.0
2024-11-04T18:36:55.027Z
I know Neel is aware of this, but as written, if "Gödel encoding" is taken to mean "*any* computable map from terms (or strings) to natural numbers" then the theorem stated in the answer is false. But maybe that's a bit disingenuous, since usually "Gödel encoding" has some "reasonableness" condition associated to it. It's the usual "encodings are important" argument that pops up everywhere in these sorts of discussions.
cody
CC BY-SA 2.5
2010-11-29T23:00:49.850Z
2010-11-29T23:00:49.850Z
Neel Krishnaswami
<p>Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks. </p>

CC BY-SA 2.5
2010-11-30T21:25:57.360Z
I think this needs to be edited. "nat ⨯ nat → nat" does not make sense. Did you mean $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$?
Sadeq Dousti
<computability><lo.logic><type-theory>
An example of a totally computable function that is not definable in system T?
day
# An example of a totally computable function that is not definable in system T?

(Asked by: username_0 on 2010-11-29)

Could you give me an example of a totally computable function of type N × N → N that is not definable in System T? Thanks.

**Tags:** computability, lo.logic, type-theory

> **Comments:**
> **username_1**: I think this needs to be edited. "nat ⨯ nat → nat" does not make sense. Did you mean $\mathbb{N} \times \mathbb{N} \to \mathbb{N}$?  

---

## 3 answers

### Answer by username_5 on 2010-11-29. Score: 11 | Accepted answer

Interpreters for T are not definable in T, thanks to the incompleteness theorem.

Concretely, fix a Godel encoding, and then let $f$ be the function which takes a pair consisting of a Godel-encoding of a closed term of type $\mathbb{N} \to \mathbb{N}$, and a natural number in $\mathbb{N}$, and returns the value of the application. This function is not definable in T. It's a worthwhile exercise to work out how you can use a self-interpreter to define an infinitely looping program.

> **Comments:**
> **username_6**: 10 years later, here's a counterexample: take the Gödel encoding which takes a term $t$ of T, and encodes it as the "usual" (using, say the one detailed [here](https://en.wikipedia.org/wiki/G%C3%B6del_numbering#G%C3%B6del's_encoding)) encoding of the pair $\langle t, v\rangle$ of $t$ and the *normal form* $v$ of $t$. This is computable and bijective, but given this encoding, system $T$ easily can compute the value $v$ (by second projection). So one must, as usual, either give an explicit encoding or somehow define "reasonable" ones.  
> **username_2**: @username_6: This appears in Theorem 3.2 of [On self-interpreters for System T and other $\lambda$-calculi](https://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/) in 2016. I should have callled that note "Much ado about nothing". But more importantly, how is your idea a counter-example to Neel's?  
> **username_6**: I know Neel is aware of this, but as written, if "Gödel encoding" is taken to mean "*any* computable map from terms (or strings) to natural numbers" then the theorem stated in the answer is false. But maybe that's a bit disingenuous, since usually "Gödel encoding" has some "reasonableness" condition associated to it. It's the usual "encodings are important" argument that pops up everywhere in these sorts of discussions.  

---

### Answer by username_2 on 2010-11-30. Score: 9

This just appeared on arxive.org and may be of some help.

> [*The definability of functionals in Gödel's theory T*](http://arxiv.org/abs/1011.6353)
>
> Matthew P. Szudzik (Carnegie Mellon)
>
> Gödel's theory T can be understood as a theory of the simply-typed lambda calculus that is extended to include the constant 0, the successor function $S$, and the operator $R\_\tau$ for primitive recursion on objects of type $\tau$. It is known that the functions from non-negative integers to non-negative integers that can be defined in this theory are exactly the $\epsilon$-recursive functions of non-negative integers. But it is not well-known which functionals of arbitrary type can be defined in T.
> We show that when the domain and codomain are restricted to pure closed normal forms, the functionals of arbitrary type that are definable in T are exactly those functionals that can be encoded as $\epsilon$-recursive functions of non-negative integers. This result has many interesting consequences, including a new characterization of T.


---

### Answer by username_3 on 2024-11-02. Score: -2

My intuition would be that the length of the Collatz sequence is not definable in System F. That is, we cannot compute the length of the Collatz sequence starting with a given $n$.

My reasoning is that System F can perform loops but only if the total number of iterations is known in advance. For instance, one can compute $f(f(f(...(f(x))...)))$ where the number of applications of $f$ is given. But a program in System F cannot keep repeating a computation until some condition is met. We cannot keep applying $f(f(f(...)))$ until the result becomes equal to $1$. But that kind of loop is required to compute the length of the Collatz sequence.

> **Comments:**
> **username_4**: We *currently* do not know any better algorithm other than the one here, because we do not know much of anything about properties of this function, and in particular, we do not know even know whether it is *total*. This is a requirement in the question, as non-total computable functions cannot be defined in System T, and examples of these are well known and easy to find. It is possible, and indeed very likely, that once someone proves that this function is total (= the Collatz conjecture), they will also prove the lengths of the sequences are bounded by a simple function such as iterated ...  
> **username_4**: ...  exponential, making it definable in System T. Also, the question is about System T, whereas your answer is about System F (though this does not really make a difference, as the reasoning applies to any computably enumerable system of total computable functions).  
> **username_3**: @EmilJeřábek OK I see, thank you for explanations!  

---

