<p>My first advice is to take a look at chapter 15 of Girard, Lafont &amp; Taylor <a href="http://www.paultaylor.eu/stable/prot.pdf" rel="nofollow">Proofs &amp; Types</a>. In it, a weaker theorem is proved, but the basic ideas are quite similar, and the exposition should be simpler.</p>

<p>Second: Provably type correct is a bit of a misnomer. The property looks more like <em>definability</em> or <em>accessibility</em>. In a nutshell it expresses</p>

<p>$$ \forall t_1,\ldots t_n,\ \mathrm{Ind}(t_1) \wedge \ldots\wedge\mathrm{Ind}(t_n) \Rightarrow \mathrm{Ind}(f(t_1,\ldots, t_n))$$
where $\mathrm{Ind}(t)$ means the term $t$ is <em>inductive</em>, that is, built up from constructors. Being inductive is essentially being defined as an element of the inductive type, which makes the above property a statement about definability.</p>

<p>Third: You are correct, if $B$ proves that $f$ is type correct, then $[B]$ is the definition of $f$. Work through an example first: If $\mathrm{add}: \mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$, then the statement of type correctness is:</p>

<p>$$ \forall x\ y,\ \mathrm{Ind}_{\mathbb{N}}(x)\rightarrow\mathrm{Ind}_{\mathbb{N}}\rightarrow \mathrm{Ind}_{\mathbb{N}}(\mathrm{add}(x, y))$$
in $\lambda\mathrm{PRED}_2$, which, erased, gives
$$ \mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N}$$
in $\lambda_2$ (with $\mathrm{N}=\Pi X:*.X\rightarrow(X\rightarrow X)\rightarrow X$) which is exactly the right type for $\mathrm{add}$! So at least the types add up. Checking that the proof of type correctness of $\mathrm{add}$ gives you a good definition is more tedious, but Leivant gives the details.</p>

<p>Fourth: you are correct that (1 way of seeing) the converse requires examining the proofs of strong normalization. For each function definition in $\lambda_2$, you can "decorate" it into a proof of type correctness in $\lambda\mathrm{PRED}_2$, essentially using the "theorem for free" that comes with the type. A really nice exposition is Wadler, <a href="http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf" rel="nofollow">The Girard-Reynolds isomorphism</a>, which is a highly suggested read for anyone in the field.</p>

<p>Fifth: I think you are correct in your correction of 5.4.39.</p>

<hr>

<p><strong>Edit</strong>: Elaboration on the 4th point:</p>

<p>Wadler defines, among other things, the <em>Reynolds embedding</em> from $\lambda_2$ to $\lambda\mathrm{PRED}_2$ with higher-order functions (Figure 4). This embeding sends a type to a proposition (the <em>parametricity theorem</em>) and sends a well tyepd term to a proof of parametricity of that same term.</p>

<p>The theorem you get implies "type correctness" of the defined function rather trivially. In fact I think Wadler treats this in detail in Section 5, and treats the $\mathrm{add}$ example in the appendix. The only subtle point is that the function is not directly defined over the inductive type, rather it takes the type and constructors as <em>arguments</em>.</p>

<p>At this point I really have to suggest you work through some examples.</p>

CC BY-SA 3.0
2014-07-07T02:55:22.050Z
Is it possible for you to elaborate on the fourth point on the converse?  I don't understand what part of the Wadler's work you introduced to me gives the result.
Pteromys
CC BY-SA 3.0
2014-07-07T20:15:07.950Z
I edited my answer to try to elaborate.
cody
CC BY-SA 3.0
2014-07-06T23:50:32.450Z
2014-07-07T16:19:56.540Z
2014-07-07T16:19:56.540Z
cody
<p>I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's <em>Lambda calculi with types</em> (1992), a chapter in Handbook in logic in computer science. (I'm referring to the <a href="http://ttic.uchicago.edu/~dreyer/course/.../barendregt.pdf" rel="nofollow">PostScript version</a> available on the Web.)</p>

<p>The theorem states that a function is $\lambda$2-definable iff it is HG (Herbrand-Goedel) computable and provably type correct in $\lambda$PRED2.  The author delegates the proof to a proceeding in FOCS, i.e., <em>Reasoning about functional programs and complexity associated with type disciplines</em> (1983) by Leivant.  The corresponding theorem in the proceeding is Theorem 3.1 and Corollary 3.2, although they are stated in terms of provable type-correctness in $\lambda$2, not in $\lambda$PRED2.</p>

<p>The first problem I'm running into is that the definition of HG computability by Barendregt doesn't make sense.  IMHO, the equation in Definition 5.4.39.1 should be replaced by
$$
\mathit{HG} \vdash p:(f_n(t^\sim) =_L (f(t))^\sim).
$$</p>

<p>Assuming this, I tried to prove the equivalent of Theorem 3.1 (Leivant) in terms of $\lambda$PRED2, but in vain.  Leivant's proof is informal and I have hard times formalizing it. (By using Barendregt's notation, I'm pretty sure that if $B$ is the proof of $f$'s type correctness then $[B]$ is a $\lambda$2-term that represents $f$, but I am unable to prove this.)  Besides, his proof deals with only one direction of the equivalence (provably type correct $\Rightarrow$ $\lambda$2-definable) and the rest is left unstated.  I suppose the opposite direction involves the formalization of SN, but I am unsure.</p>

<p>I would be the most grateful for detailed explanation of Theorem 5.4.40.3 by Barendregt.</p>

CC BY-SA 3.0
2014-07-06T22:16:07.820Z
I'm not finding a theorem 3.4.40.3. Care to give a page number?
cody
CC BY-SA 3.0
2014-07-06T22:36:44.587Z
@cody Thank you for pointing out the typo; it's actually 5.4.40.3, on page 163 (in the PostScript file).
Pteromys
<lo.logic><pl.programming-languages><computability><type-theory><lambda-calculus>
A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2
Pteromys
# A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

(Asked by: username_0 on 2014-07-06)

I'm having a problem regarding Theorem 5.4.40.3 of Barendregt's *Lambda calculi with types* (1992), a chapter in Handbook in logic in computer science. (I'm referring to the [PostScript version](http://ttic.uchicago.edu/~dreyer/course/.../barendregt.pdf) available on the Web.)

The theorem states that a function is $\lambda$2-definable iff it is HG (Herbrand-Goedel) computable and provably type correct in $\lambda$PRED2. The author delegates the proof to a proceeding in FOCS, i.e., *Reasoning about functional programs and complexity associated with type disciplines* (1983) by Leivant. The corresponding theorem in the proceeding is Theorem 3.1 and Corollary 3.2, although they are stated in terms of provable type-correctness in $\lambda$2, not in $\lambda$PRED2.

The first problem I'm running into is that the definition of HG computability by Barendregt doesn't make sense. IMHO, the equation in Definition 5.4.39.1 should be replaced by
$$
\mathit{HG} \vdash p:(f\_n(t^\sim) =\_L (f(t))^\sim).
$$

Assuming this, I tried to prove the equivalent of Theorem 3.1 (Leivant) in terms of $\lambda$PRED2, but in vain. Leivant's proof is informal and I have hard times formalizing it. (By using Barendregt's notation, I'm pretty sure that if $B$ is the proof of $f$'s type correctness then $[B]$ is a $\lambda$2-term that represents $f$, but I am unable to prove this.) Besides, his proof deals with only one direction of the equivalence (provably type correct $\Rightarrow$ $\lambda$2-definable) and the rest is left unstated. I suppose the opposite direction involves the formalization of SN, but I am unsure.

I would be the most grateful for detailed explanation of Theorem 5.4.40.3 by Barendregt.

**Tags:** lo.logic, pl.programming-languages, computability, type-theory, lambda-calculus
> **Comments:**
> **username_1**: I'm not finding a theorem 3.4.40.3. Care to give a page number?  
> **username_0**: @cody Thank you for pointing out the typo; it's actually 5.4.40.3, on page 163 (in the PostScript file).  

---

## 1 answers

### Answer by username_1 on 2014-07-06. Score: 7 | Accepted answer

My first advice is to take a look at chapter 15 of Girard, Lafont & Taylor [Proofs & Types](http://www.paultaylor.eu/stable/prot.pdf). In it, a weaker theorem is proved, but the basic ideas are quite similar, and the exposition should be simpler.

Second: Provably type correct is a bit of a misnomer. The property looks more like *definability* or *accessibility*. In a nutshell it expresses

$$ \forall t\_1,\ldots t\_n,\ \mathrm{Ind}(t\_1) \wedge \ldots\wedge\mathrm{Ind}(t\_n) \Rightarrow \mathrm{Ind}(f(t\_1,\ldots, t\_n))$$
where $\mathrm{Ind}(t)$ means the term $t$ is *inductive*, that is, built up from constructors. Being inductive is essentially being defined as an element of the inductive type, which makes the above property a statement about definability.

Third: You are correct, if $B$ proves that $f$ is type correct, then $[B]$ is the definition of $f$. Work through an example first: If $\mathrm{add}: \mathbb{N}\rightarrow\mathbb{N}\rightarrow\mathbb{N}$, then the statement of type correctness is:

$$ \forall x\ y,\ \mathrm{Ind}\_{\mathbb{N}}(x)\rightarrow\mathrm{Ind}\_{\mathbb{N}}\rightarrow \mathrm{Ind}\_{\mathbb{N}}(\mathrm{add}(x, y))$$
in $\lambda\mathrm{PRED}\_2$, which, erased, gives
$$ \mathrm{N}\rightarrow\mathrm{N}\rightarrow\mathrm{N}$$
in $\lambda\_2$ (with $\mathrm{N}=\Pi X:\*.X\rightarrow(X\rightarrow X)\rightarrow X$) which is exactly the right type for $\mathrm{add}$! So at least the types add up. Checking that the proof of type correctness of $\mathrm{add}$ gives you a good definition is more tedious, but Leivant gives the details.

Fourth: you are correct that (1 way of seeing) the converse requires examining the proofs of strong normalization. For each function definition in $\lambda\_2$, you can "decorate" it into a proof of type correctness in $\lambda\mathrm{PRED}\_2$, essentially using the "theorem for free" that comes with the type. A really nice exposition is Wadler, [The Girard-Reynolds isomorphism](http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf), which is a highly suggested read for anyone in the field.

Fifth: I think you are correct in your correction of 5.4.39.

---

**Edit**: Elaboration on the 4th point:

Wadler defines, among other things, the *Reynolds embedding* from $\lambda\_2$ to $\lambda\mathrm{PRED}\_2$ with higher-order functions (Figure 4). This embeding sends a type to a proposition (the *parametricity theorem*) and sends a well tyepd term to a proof of parametricity of that same term.

The theorem you get implies "type correctness" of the defined function rather trivially. In fact I think Wadler treats this in detail in Section 5, and treats the $\mathrm{add}$ example in the appendix. The only subtle point is that the function is not directly defined over the inductive type, rather it takes the type and constructors as *arguments*.

At this point I really have to suggest you work through some examples.

> **Comments:**
> **username_0**: Is it possible for you to elaborate on the fourth point on the converse?  I don't understand what part of the Wadler's work you introduced to me gives the result.  
> **username_1**: I edited my answer to try to elaborate.  

---

