strong normalization of STLC

Stream: lean4

[Elif Uskuplu]

Hi, I'm working on STLC with de Bruijn indices in Lean4 link. I would like to formalize strong normalization for terms. I don't know how hard it is, but I have difficulties with the definition.

According to notes I looked, the predicate of strongly normalized SN on terms should be

inductive SN : Term → Prop
  | sn : (∀ t', beta_red t t' → SN t') → SN t

where beta_red is the one-step reduction. Those notes were using "Reducibility candidates" method to prove that every typable term is strongly normalized. This is how they formulate the strong normalization of STLC.

It's said that SN is always backwards closed with respect to application. Namely, if SN (t @ s) then SN t ∧ SN s. It's said that the proof goes by induction on SN (t @ s), but it does not seem easy to me. I think the idea is that if we have a reduction sequence starting with t, then we can obtain a corresponded reduction sequence starting with t @ s. Since the letter halts in finitely many steps, so is the former. But, how we relate SN predicate with the property of having finite reduction sequences??

I'm also not sure whether this is the right approach to prove the strong normalization of STLC. Is there any idea to formulate it other than using SN predicate??

[Mario Carneiro]

IIRC @Jeremy Avigad has a really nice presentation of this proof in his book "Mathematical Logic and Computation". Jeremy do you have anything else I could point to here?

[Mario Carneiro]

Oh, apparently this was @Sarah Mameche 's bachelor thesis (lean 3): https://www.ps.uni-saarland.de/~mameche/images/thesis.pdf

[Elif Uskuplu]

Mario Carneiro said:

IIRC Jeremy Avigad has a really nice presentation of this proof in his book "Mathematical Logic and Computation". Jeremy do you have anything else I could point to here?

Thanks for the suggestion, I have this book. It says:

A term t is strongly normalizing or strongly normalizable if there is no infinite sequence of one-step reductions beginning with t, that is, every sequence of one-step reductions starting from t is finite.

I'm just not sure about how this is related with the following?

inductive SN : Term → Prop
  | sn : (∀ t', beta_red t t' → SN t') → SN t

[Mario Carneiro]

AFAIK that is indeed the right definition

[Mario Carneiro]

SN is not actually the same thing as "strongly normalizing", or rather establishing the equivalence between those two is most of the proof

[Mario Carneiro]

SN has some nice properties that facilitate the proof

[Mario Carneiro]

doing induction directly on the literal definition of "strongly normalizing" doesn't work

[Mario Carneiro]

I think in Jeremy's book SN is called "strongly computable"

[Elif Uskuplu]

Mario Carneiro said:

I think in Jeremy's book SN is called "strongly computable"

I think this is "Reducibility Relation" in the note you shared.

[Mario Carneiro]

actually I think I'm mixing things up, the SN inductive you defined is pretty clearly equivalent to "every reduction sequence terminates"

[Elif Uskuplu]

And that's why "every typable term is strongly normalized" (using SN) is the same as "The relation →1 is strongly normalizing (i.e. for each t, every sequence of one-step reductions starting from t is finite)." in Jeremy's book, right?

[Mario Carneiro]

Is the relation ->1 is the same as beta_red?

[Elif Uskuplu]

beta_red is the one-step reduction. Since I'm using locally nameless representation (de Bruijn indices), the definition is different than ->1, but I think they are intuitively same.

[Elif Uskuplu]

I think I made progress: I've shown that

lemma SN_finlist (t : Trm) :
  SN t →
 (∀ (f : Nat → Trm), ((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) → ∃ k, (normal (f k))) :

This means if we have SN t, then for every sequence of beta reductions starting with t, there is a normal term in the sequence, namely, the sequence is eventually constant.

I want to prove the other way, but I think I should define the proposition

 (∀ (f : Nat → Trm), ((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) → ∃ k, (normal (f k)))

inductively so that I can prove the other direction using induction on the definition we built.
I hope I could explain :) How can I define it using inductive environment?

[Mario Carneiro]

Shouldn't it say that there is no such sequence? Can a normal term have a beta_red?

[Mario Carneiro]

The converse you can prove by contradiction using the axiom of choice: Suppose t is not SN, then it has a beta_red which is also not SN, and so on, this defines an infinite sequence

[Elif Uskuplu]

Mario Carneiro said:

Shouldn't it say that there is no such sequence? Can a normal term have a beta_red?

Sorry, I forgot to say. If a term t is normal it means whenever beta_red t u holds, we have t = u. So in the definition I gave before, the sequence will be the constant t sequence after finite step. I think it gives the idea that every reduction sequence starting with t terminates, right?

[Mario Carneiro]

@Elif Uskuplu In that case you will have to modify the argument to only consider beta_red values not equal to the original, or else you could end up spuriously spinning on a non-normal term even though proper reductions exist

[Elif Uskuplu]

Mario Carneiro said:

Elif Uskuplu In that case you will have to modify the argument to only consider beta_red values not equal to the original, or else you could end up spuriously spinning on a non-normal term even though proper reductions exist

Sorry, I couldn't get it. If we have a reduction sequence t_n, namely beta_red t_n t_{n+1} for all n, and t_k is normal for some k, don't we have that the sequence is the constant t_k sequence after k steps? So we have only a finite sequence t_0, t_1, ..., t_k. Am I missing something?

[Mario Carneiro]

yes, but what if you have a reduction sequence t_n with beta_red t_n t_{n+1} for all n, but it's not normal for any k? (i.e. the negation of your statement) This doesn't tell you anything: it could be that you just chose to repeat some non-normal term t forever without progressing

[Mario Carneiro]

Put another way, I don't see why the statement SN_finlist would be true if beta_red is reflexive, because any term, even one which is SN but not normal, would have a trivial sequence which is just constantly t and fails the conclusion

[Mario Carneiro]

If beta_red is irreflexive, then the conclusion of the theorem is not strong enough, it should just be ∀ (f : Nat → Trm), ((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) → False

[Elif Uskuplu]

beta_red is not reflexive, yes.

[Elif Uskuplu]

I think I see your point. If SN tis not true, we can find an infinite sequence of reduction via AC, but this might not give the negation of my statement . That's why it needs modification, right?

[Mario Carneiro]

You can still prove the negation of your statement, because you can find an infinite sequence of non-equal reduction

[Elif Uskuplu]

Right, I see. But, as you suggest, the right statement should be∀ (f : Nat → Trm), ((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) → False to have the right definition in Jeremy's book?

[Mario Carneiro]

If you have a normal term, I assume that it has no beta_red at all?

[Elif Uskuplu]

I didn't define it in that way, but you're right, I should define like this. If normal means no beta_red, my statement is ok?

[Mario Carneiro]

Jeremy's book supports this definition:

Definition 13.2.1. 1. A term t is reducible if there is some t′ such that $t \to_1 t^′$, and irreducible otherwise. A term that is irreducible is also said to be normal, or in normal form.

[Mario Carneiro]

if normal means no beta_red then the statement is equivalent but unnecessarily complicated because you can immediately prove that a sequence with such k is impossible by just taking one more step

[Elif Uskuplu]

I agree, it's better to take ... → False.

[Elif Uskuplu]

Thanks for the discussion, what about the application? I mean I want to prove that if SN (t @ s) then SN t and SN s via induction on SN. But it does not seem easy to me. Do you think other characterization of SN works well?

[Mario Carneiro]

Ah, that's what "strongly computable" is for

[Mario Carneiro]

it is importantly defined by recursion on types:

For each type α, we define the set of strongly computable terms of type $α$:
* If $t$ is a term of a basic type, then $t$ is strongly computable if and only if it is strongly normalizing.
* If $t$ is a term of type $α → β$, then $t$ is strongly computable if and only if for every strongly computable $s$ of type $α$, $t s$ is strongly computable.
* If $t$ is a term of type $α × β$, then $t$ is strongly computable if and only if both $(t)_0$ and $(t)_1$ are strongly computable.

[Mario Carneiro]

in some sense this explains why STLC has strong normalization while LC doesn't - at some point you need to make use of the typing structure in the proof

[Elif Uskuplu]

I see, probably the problem is that I'm referring different notes and the definition varies. Strong computable is like reducibility candidate in the note you shared first. We need to prove CR1,CR2,CR3 lemmas in that note (these are like Lemma 13.2.7. in Jeremy's book). And the proof of lemmas uses the fact SN (t @ s) then SN t and SN s. That's why I'm not sure if strongly computable notion is suitable for my case. In the end, I think the first thing I should do is referring only one textbook or note :smile: to avoid confusion.

[Elif Uskuplu]

@Mario Carneiro Thank you for taking the time.

[Mario Carneiro]

IIRC Jeremy's proof is very efficient, I think the reducibility candidate proof is closer to the original version of the proof

[Mario Carneiro]

but yes, doing both proofs at the same time is likely to be confusing :)

[Elif Uskuplu]

Well, it's almost done, but I still need to characterize the height notion for a strongly normalizing term. I mean I don't know how can I formalize the expression for some n, every sequence of one-step reductions starting from t has length at most n ?

[Mario Carneiro]

I'm not sure this is true, or at least it doesn't follow from strong normalization alone

[Mario Carneiro]

for example, if we consider decreasing sequences of ordinals starting from $\omega$, it is true that every sequence terminates, but it is not true that there exists an n such that every sequence of reductions has length at most n

[Elif Uskuplu]

This is from the book:

Lemma 13.2.4. A term t is strongly normalizing if and only if for some n every sequence of one-step reductions starting from t has length at most n.

Proof : The backward direction is immediate. To prove the forward direction, suppose t is strongly normalizing. Build a tree with t at the root; as children of node labeled s, add a node for each term s' such that s →1 s' . Clearly this tree is finitely branching. Strong normalization implies that there is no infinite branch through the tree. By Proposition 1.4.4 (Kőnig’s lemma), the tree is finite.

In the proof below, whenever t is strongly normalizing, let h(t) denote the least n such that every sequence of one-step reductions from t has length at most n. Note that if t is strongly normalizing and t →1 s, then s is strongly normalizing as well and h(s) < h(t).
...

[Mario Carneiro]

Oh I see, if you have finite branching then yes it follows

[Mario Carneiro]

the rank of each term is the max of all of its possible reductions plus 1

[Mario Carneiro]

and this is well founded by strong normalization

[Elif Uskuplu]

I understand this conceptually, but I couldn't figure it out how can I write this expression as a Lean code. :smile:

[Elif Uskuplu]

I mean the RHS of Lemma 13.2.4

[Mario Carneiro]

do you know how to state it?

[Mario Carneiro]

e.g. "sequence of one step reductions"

[Mario Carneiro]

I think you already wrote a variation on that for infinite sequences

[Mario Carneiro]

you can prove it by induction on SN

[Elif Uskuplu]

Yes, (f : Nat → Trm), ((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) gives a sequence of one step reductions starting from t, right?

[Mario Carneiro]

yes but that is infinite length

[Mario Carneiro]

you need one of length n

[Elif Uskuplu]

So I should change Nat with set of n numbers?

[Mario Carneiro]

or you could say \all i < n, beta_red (f i) (f (succ i))

[Elif Uskuplu]

I see, that makes sense. Thanks.

[Elif Uskuplu]

deleted

[Elif Uskuplu]

Sorry for the possible repetition, but it's like I'm entering a vicious circle :)

I have two definitions of being strongly normalizable: First is

def strongly_normalizable (t : Trm) : Prop :=
  ∀ (f : Nat → Trm), (((f 0 = t) ∧ (∀ n, (beta_red (f n) (f (succ n))))) → False)

The other is inductive version, I think it's better than working with finite sequences:

inductive SN : Trm → Prop
  | sn : (∀ t', (beta_red t t') → SN t') → SN t

The first one is good for to show that if app t u is strongly normalizable, then so are t and s. I need this fact in the base case of CR3 (lemma 13.2.7 c).

The second one is good for finishing the last step in the arrow case of CR3.

Thus, I would prefer to use both interchangeably, but the equivalence between them seems hard to me. I mean it seems we need AC, but in the formalization, I'm not sure how can I use it. Or I'm not sure if the idea is right. So my remaining difficulty is only to show the equivalence between these definitions (if exists).

[Mario Carneiro]

What is the issue? I thought I already explained that one above, so if this is giving you trouble you should show more of your work and what part is causing problems

[Mario Carneiro]

I suspect that any proof using strongly_normalizable can be reframed to use SN instead though, and then you won't need the equivalence

[Elif Uskuplu]

Let me also write here, both I learned the way to handle the equivalence between strongly_normalizable and SN via a suitable choice, and I learned to solve the issue that cause such a need for equivalence. For the discussion, see. So, as @Mario Carneiro pointed, no need the equivalence. Thanks again.