Termination of guarded recursion

I will now give a termination proof for the guarded recursion calculus I sketched in the last two posts. This post got delayed because I tried to oversimplify the proof, and that didn't work -- I actually had to go back and look at Nakano's original proof to figure out where I was going wrong. It turns out the proof is still quite simple, but there's one really devious subtlety in it.

First, we recall the types, syntax and values.

A ::= N | A → B | •A
e ::= z | s(e) | case(e, z → e₀, s(x) → e₁) | λx.e | e e 
   | •e | let •x = e in e | μx.e | x
v ::= z | s(e) | λx.e | •e

The typing rules are in an earlier post, and I give some big-step evaluation rules at the end of this post. Now, the question is, given · ⊢ e : A[n], can we show that e ↝ v?

To do this, we'll turn to our old friend, Mrs. step-indexed logical relation. This is a Kripke logical relation in which the Kripke worlds are given by the natural numbers and the accessibility relation is given by ≤. So, we define a family of predicates on closed values indexed by type, and by a Kripke world (i.e., a natural number n).

V(•A)ⁿ     = {•e | ∀j<n. e ∈ E(A)ʲ}
V(A ⇒ B)ⁿ  = {λx.e | ∀j≤n, v ∈ V(A)ʲ. [v/x]e ∈ E(B)ʲ}
V(N)ⁿ      = {z} ∪ { s(e) | ∀j<n. e ∈ E(N)ʲ}

E(A)ʲ      = {e | ∃v. e ↝ v and v ∈ V(A)ʲ}

This follows the usual pattern of logical relations, where we give a relation defining values mutually recursively with a relation defining well-behaved expressions (i.e., expressions are ok if they terminate and reduce to a value in the relation at that type).

Note that as we expect, j ≤ n implies V(A)ⁿ ⊆ V(A)ʲ. (The apparent antitonicity comes from the fact that if v is in the n-relation, it's also in the j relation.) One critical feature of this definition is that at n = 0, the condition on V(•A)⁰ always holds, because of the strict less-than in the definition.

The fun happens in the interpretation of contexts:

Ctxⁿ(· :: j)          = ()
Ctxⁿ(Γ,x:A[i] :: j)   = {(γ,[v/x]) | γ ∈ Ctxⁿ(Γ) and v ∈ Vⁿ(A)}     
                        when i ≤ j
Ctxⁿ(Γ,x:A[j+l] :: j) = {(γ,[e/x]) | γ ∈ Ctxⁿ(Γ) and •ˡe ∈ Vⁿ(•ˡA)} 
                        when l > 0

The context interpretation has a strange dual nature. At times less than or equal to j, it is a familiar context of values. But at future times, it is a context of expressions. This is because the evaluation rules substitute values for variables at the current time, and expressions for variables at future times. We abuse the bullet value relation in the third clause, to more closely follow Nakano's proof.

On the one hand, the fixed point operator is μx.e at any type A, and unfolding this fixed point has to substitute an expression (the mu-term itself) for the variable x. So the fixed point rule tells us that there is something necessarily lazy going on.

One the other hand, the focusing behavior of this connective is quite bizarre. It is not apparently positive or negative, since it distribute neither through all positives (eg, •(A + B) ≄ •A + •B) nor is it the case that it distributes through all negatives (eg, •(A → B) ≄ •A → •B). (See Noam Zeilberger, The Logical Basis of Evaluation Order and Pattern Matching.)

I take this to mean that •A should probably be decomposed further. I have no present idea of how to do it, though.

Anyway, this is enough to let you prove the fundamental property of logical relations:

Theorem (Fundamental Property). If Γ ⊢ e : A[j], then for all n and γ ∈ Ctxⁿ(Γ :: j), we have that γ(e) ∈ Eⁿ(A).
The proof of this is a straightforward induction on typing derivations, with one nested induction at the fixed point rule. I'll sketch that case of the proof here, assuming an empty context Γ just to reduce the notation:

Case:          · ⊢ μx.e : A[j]
By inversion: x:A[j+1] ⊢ e : A[j]
By induction, for all n,e'. if •e' ∈ Vⁿ(•A) then [e'/x]e ∈ Eⁿ(A)
By nested induction on n, we'll show that [μx.e/x]e ∈ Eⁿ(A)
Subcase n = 0:
   We know if •μx.e ∈ V⁰(•A) then [μx.e/x]e ∈ E⁰(A)
   We know •μx.e ∈ V⁰(•A) is true, since · ⊢ μx.e : A[j]
   Hence [μx.e/x]e ∈ E⁰(A)
   Hence μx.e ∈ E⁰(A)
Subcase n = x+1: 
   We know if •μx.e ∈ Vˣ⁺¹(•A) then [μx.e/x]e ∈ Eˣ⁺¹(A)
   By induction, we know [μx.e/x]e ∈ Eˣ(A)
   Hence μx.e ∈ Eˣ(A)
   Hence •μx.e ∈ Vˣ⁺¹(A)
   So [μx.e/x]e ∈ Eˣ⁺¹(A)
   Hence μx.e ∈ Eˣ⁺¹(A)

Once we have the fundamental property of logical relations, the normalization theorem follows immediately.

Corollary (Termination). If · ⊢ e : A[n], then ∃v. e ↝ v.

Evaluation rules:

                                 e₁ ↝ (λx.e)  e₂ ↝ v  [v/x]e ↝ v'
    ——————                       ————————————————————————————————
    v ↝ v                                 e₁ e₂ ↝ v'  



    e ↝ z    e₀ ↝ v                 e ↝ s(e)    [e/x]e₁ ↝ v       
——————————————————————————————   —————————————————————————————————
case(e, z → e₀, s(x) → e₁) ↝ v   case(s(e), z → e₀, s(x) → e₁) ↝ v



e₁ ↝ •e   [e/x]e' ↝ v            [μx.e/x]e ↝ v 
—————————————————————            ——————————————
let •x = e₁ in e₂ ↝ v               μx.e ↝ v