10
$\begingroup$

I'm reading Girard's Proofs and Types, and in section 4.4 he writes:

Lemma: t is strongly normalisable iff there is a number ν(t) which bounds the length of every normalisation sequence beginning with t.

He later uses this lemma in his proof that the STLC is strongly normalizing in section 6.2.3:

(CR 3) Let t be neutral and suppose all the t' one step from t are reducible. Let u be a reducible term of type U; we want to show that t u is reducible. By induction hypothesis (CR 1) for U, we know that u is strongly normalisable; so we can reason by induction on ν(u).

The lemma uses a version of Konig's Lemma which IIUC is not provable constructively. Is there a constructive proof of strong normalization for the simply typed lambda calculus? Specifically something I can (try to) translate into Agda?

$\endgroup$
0

2 Answers 2

17
$\begingroup$

As Dan Doel says in the comments, the reason Kőnig's lemma is used is that Girard's definition of strong normalization is constructively too weak. It's defined as the non-existence of infinite reduction sequences.

We can use the following definition instead: a term is strongly normalizing if every one-step reduct of it is strongly normalizing (inductively). In Agda:

data SN {Γ A} (t : Tm Γ A) : Set where
  sn : (∀ {t'} → t ~> t' → SN t') → SN t

Note that if a term is normal then it has no one-step reduct so SN t holds vacuously.

This is also called accessibility of t with respect to ~>. I believe it originates from Aczel's An Introduction to Inductive Definitions. This is a common SN definition in formalizations. The oldest formalized example that I know is in Altenkirch's thesis.

The advantage of SN t is that we can do induction on it. Operationally, we can make a "recursive call" on any one-step reduct of a strongly normalizing term. You could also look at my Agda formalization of Girard's Chapter 6, which uses this SN.

$\endgroup$
3
  • $\begingroup$ I updated my question to be more specific about where Girard uses the lemma in the strong normalization proof. I'll have to look carefully at your code to see how you got around it. $\endgroup$ Mar 23, 2022 at 20:25
  • 3
    $\begingroup$ The difference (I think) is that Girard's use of Kőnig's lemma is only necessary because "strongly normalizable" is defined weakly. It is one of the classically equivalent ways to say, "reduction is well-founded." The Agda defines this in the constructively appropriate way, where a proof that a value is "accessible" justifies induction over its predecessors. Kőnig's lemma is used to recover a natural number to justify the same induction, but this is unnecessary if you set things up appropriately. $\endgroup$
    – Dan Doel
    Mar 23, 2022 at 21:47
  • $\begingroup$ You're both right. I updated my answer. $\endgroup$ Mar 24, 2022 at 7:30
7
$\begingroup$

For a modern take on the proof, you can have a look at POPLmark Reloaded.

The paper's appendix explains in great details what the (sometimes technical) proofs are. The paper comes with various formalisations in Agda, Beluga, Coq, F*, and Lean 3. The Agda formalisation uses sized types which are now marked as unsafe so a new version of the formalisation seen to be safe by a recent version of Agda would be a welcomed addition!

$\endgroup$
1
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$
    – JNat
    Mar 28, 2022 at 10:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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