3
$\begingroup$

In Ralph Loader's lecture notes on lambda calculus (section 3.3), he states that a combinatorial proof of the SN of simply typed lambda calculus uses a technique that is "in essence that used by Gentzen to prove cut-elimination for LK, the classical sequent calculus."

The proof proceeds as follows. We first define a set of normalizing terms that are generated by a set of rules, dubbed "inductively normalizing (IN)". We then define applicative types, as the types such that whenever $t,r$ are IN and $r$ is in an applicative type, $(tr)$ is also IN, if suitably typed. The substitutive types are the types such that if $t, r$ are IN and $r$ is in a substitutive type, then $t[r/x]$ is in IN. Then we can prove that substitutive types are all applicative types. At last, we finish the proof by noting that every type can be decomposed $\sigma = \sigma_1 \to \sigma_2 \to \dots \to \sigma_n \to o$, and do induction to prove that all types are substitutive.

The question: What is the connection between this proof and the proof of Gentzen of cut-elimination for LK? As far as I know, the main technique of Gentzen's proof is the introduction of the mix rule. Is this what Loader is referring to? I would be grateful if anyone sheds light on this matter.

Improve this question
$\endgroup$
3
  • $\begingroup$ That's a curious comment, since in general I would expect SN of STLC to be most closely connected to cut-elimination for intuitionistic sequent calculus. $\endgroup$
    – Mike Shulman
    Commented Jun 22, 2021 at 18:37
  • $\begingroup$ I think Loader is just referring loosely to Gentzen's proof of cut-elimination, for which arguably the "main technique" is a nested induction on formulas and derivations. Gentzen actually proved cut-elimination for both LK and LJ in one go: he gave a cut-elimination procedure for LK, then observed that it preserves the property of being an LJ-derivation (i.e., having at most one formula on the RHS of every sequent). $\endgroup$
    – Noam Zeilberger
    Commented Jun 22, 2021 at 20:27
  • 1
    $\begingroup$ as an aside, it is perhaps worth mentioning that Gentzen also gave a direct proof of normalization for first-order intuitionistic natural deduction. Surprisingly, Gentzen's manuscript was only discovered relatively recently by von Plato, who discusses it in this 2008 article: jstor.org/stable/pdf/20059973.pdf $\endgroup$
    – Noam Zeilberger
    Commented Jun 24, 2021 at 5:58

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .