A function is lambda-2-definable iff it is HG computable and provably type correct in lambda-PRED2

Question

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 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.

Answer 1

My first advice is to take a look at chapter 15 of Girard, Lafont & Taylor Proofs & Types. 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, 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.