9
$\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

3 Answers 3

14
$\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 at 20:25
  • 2
    $\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 at 21:47
  • $\begingroup$ You're both right. I updated my answer. $\endgroup$ Mar 24 at 7:30
8
$\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 at 10:27
4
$\begingroup$

There are already translations into Agda. A constructive proof is (roughly) equivalent to a normalization algorithm. The most common and extensible technique is to use some sort of reducibility predicate; the corresponding algorithm is called normalization by evaluation.

If you search for the keywords you would probably get enough information. But here I recommend Andreas Abel, Andras Kovacs (both code and paper). And if you would pardon me, my own repo, which aims more to explain existing work rather than doing novel work.

$\endgroup$
5
  • 1
    $\begingroup$ You link sources about normalization-by-evaluation, but it's not the same as strong normalization. We get from correct NbE that every term is convertible to a unique normal term. SN says that every sequence of reductions terminate. If we don't have eta rules, then SN+confluence implies unique normal forms, but the converse is not implied. With eta rules, SN proofs are often not available at all, which was an important motivation for moving to NbE from SN as a way to decide conversion. $\endgroup$ Mar 23 at 10:18
  • $\begingroup$ @AndrásKovács If the domain of semantics includes relevant proofs for (strong/weak) normalization, then NbE will correspond to a proof of (strong/weak) normalization. I think usually we prove weak normalization because it's way easier. But at least for STLC, strengthening it to SN is not a problem. $\endgroup$
    – Trebor
    Mar 23 at 10:40
  • $\begingroup$ Moving from WN to SN is not trivial already for STLC. Also, WN is not the same as NbE. The former usually mentions directed reduction, the latter undirected conversion. Undirected conversion can be identified with equality in algebraic or synthetic settings, and then everything automatically respects conversion. I have not seen analogous synthetic treatment of directed reductions. $\endgroup$ Mar 23 at 12:33
  • 2
    $\begingroup$ For a basic example of not getting SN from NbE easily, NbE for STLC+eta computes along beta-reduction and eta-expansion. But SN is false for beta-reduction and eta-expansion. $\endgroup$ Mar 23 at 12:36
  • $\begingroup$ Yes, I haven't figured out about eta yet. But it's a cool perspective to consider the directedness of conversion. $\endgroup$
    – Trebor
    Mar 24 at 5:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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