2
$\begingroup$

In Proof and Types by Girard et alii. Section 7.4.2, I think that the authors want to show that:

(1) The set of functions definable in System T coincides with the set of recursive functions whose termination is provable in Peano arithmetic

I don't understand the arguments given to support this thesis.

In particular, if t is a closed term of type $Int \to Int$ of T, it induces a function $|t|:\mathbb{N} \to \mathbb{N}$ defined by:

$|t|(n) = m$ iff $t \overline{n} \leadsto \overline{m}$ $[\ldots]$

The functions $|t|$ are clearly calculable: the normalization algorithm gives $|t|(n)$ as a function of $n$. So those functions representable in T are recursive. Can we characterize the class of such functions?

This is how I read this parragraph:

  1. Regarding calculability of $|t|$: using the iff one computes $|t|(n)$ by computing $t \overline{n} \leadsto \overline{m}$. Then $\overline{m}$ syntax can be more complex that an integer and in order to obtain $m$ one has to rewrite it into a normal form (which should be an integer by the term's type).

  2. Regarding recursivity: I believe that they stress that the normalization begins with term $t \overline{n}$ and thus $|t|$ is indirectly "recursive" in its argument.

The next parragraph seems to confirm this view:

$[\ldots]$ Seen as a partial algorithm, $|t|$ amounts to looking for the normal form, and, in the case where this succeeds, writing it. The normalization theorem is thus a proof of program guaranteeing termination of all algorithms obtained from $T$.

From here I get the idea that every function written in $T$ is terminating. The next parragraph comes as a surprise though:

Now, what are the mathematical principles necessary to prove the reducibility of a fixed term t?

  • to be able to express the reducibility of t and of its subterms: one must be able to write a finite number of reducibilities, which can be done in Peano arithmetic (PA)

  • to be able to reason by mathematical induction on this finite number of reduciblity predicates; that can again be done in PA, modulo some awful coding without significant interest (Godel numbering).

Summing up, the termination is provable in arithmetic: we say that $|t|$ is provably total in PA.

If every function was terminating in System T why would one want to prove in PA specifically?

My question is if you can solve the doubts I presented or if you have your own way of showing statement (1)?

$\endgroup$
  • $\begingroup$ The syntax of $\overline{m}$ is not "more complicated". The notation $\overline{m}$ means "numeral $m$", so the statement is that in fact when we normalize $t \overline{n}$ we get a numeral. And this is not a research-level question, it belongs on cs.stackexchange.com. $\endgroup$ – Andrej Bauer Jul 30 '18 at 4:26
6
$\begingroup$

If every term in system T terminates, then $t\overline{n}\leadsto\overline{m}$ for every numeral $n$, and it is easy to show that a normal form $\overline{m}$ in the empty context is a numeral as well (and cannot be more complex!). In addition, it is easy to show, if the term $t\overline{n}$ is normalizing, that computing the normal form $\overline{m}$ can be done by a Turing machine, which is to say that the function $|t|$ is recursive (the terminology is slightly confusing here). This is what is meant by the first paragraph you have quoted.

Furthermore, every fact stated above can be easily proven in $\mathrm{PA}$, except the normalization of an arbitrary term of system T. They go on to show that each individual term $t$ can be shown to be normalizing in $\mathrm{PA}$ wich they suggest implies that every term $t$ defines a function in $\mathrm{PA}$: for every term $t:\mathrm{Int}\rightarrow\mathrm{Int}$, there is a proposition $\phi_t(x,y)$ such that $$\mathrm{PA}\vdash \forall x\exists! y\phi_t(x,y)$$

and

$$\mathrm{PA}\vdash\phi_t(\overline{n},\overline{m})$$ iff $$|t|(n)=m$$

As the following pages explain, the other direction is provable as well, that is to every $\phi$ with the first property, there is some term $t$ in system T that corresponds to it.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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