Syntax in big-step normalisation paper
I recently studied "Big Step Normalisation for Type Theory" and rewrote the implementation for learning purpose. Meanwhile I filled up all the unsolved holes that were in the original implementation.
You can check it up here.
The syntax described in the paper is interesting. It was kept small for simplicity. The most interesting detail in this syntax is that function elimination is symmetric to function introduction.
app (λ u) = uλ (app u) = u
That is, 'apply' has no argument. How do you pass an argument then? The 'app' opens up a context that you can fill with a substitution.
(app f) [ id , x ]Substitutions are themselves terms in this language. We have several constructors for substitutions:
id - identity substitutiong ∘ f - compositionε - epsilonp , x - extensionfst p - elimination
Identity is an unit for composition and composition is associative.
id ∘ f = fg ∘ id = gf ∘ g ∘ h = (f ∘ (g ∘ h)) = ((f ∘ g) ∘ h)
Substitutions with no codomain to fill, can be replaced by empty substitution.
(p : Tms X → ∙) → (p = ε)Elimination has two obvious rules:
fst (p , u) = p(fst p , snd p) = p
Composition can pass through extension, perhaps in an obvious manner:
(p , u) ∘ v = (p ∘ v, u [ v ])Terms of this language include the following:
snd p - second elimination for substitutionu [ p ] - substitutionλ u - lambdaapp u - application
The rules are again, simple for most part.
snd (p , u) = uapp (λ u) = ulam (λ u) = u
The substitution can climb up into the lambda:
(λ u) [ p ] = λ (u [ p ∘ fst id , snd id ])Syntax comes with a separate space for types. Types accept substitution and behave in way you'd expect.
A [ p ] - substitution for typeU - universe or base typeEl u - element from term spacePi A B - product type
Types have their own rules for substitutions that are similar to term space. The first two rules are available for term space as well, but they can be derived there.
A [ id ] = AA [ p ∘ v ] = A [ p ] [ v ]
Universe or base type eats any substitution it gets.
U [ p ] = UElements transfer the substitution into term space.
El u [ p ] = El (u [ p ])Pi types distribute the substitution, matching it up with how it goes with lambdas.
Pi A B [ p ] = Pi (A [ p ]) (B [ p ∘ fst id , snd id ])As presented in the paper, the universe -type has no terms. It'd work in the following way if it had.
U^ - term for universePi^ u v - term for pi
There would be obvious rules for sliding substitutions across them:
U^ [ p ] = U^Pi^ u v [ p ] = Pi^ (u [ p ]) (v [ p ∘ fst id , snd id ])
But most importantly there would be interaction with the type space:
El U^ = UEl (Pi^ u v) = Pi (El u) (El v)
That's it.
To illustrate how it works, lets work through lambda application.
(app (λ f)) [ id , x ]──────────────────────f [ id , x]
The application is simply eliminated.
How about, can we pass substitution through application?
app f [ p ]───────────────────────app (lam (app f [ p ]))
Since we don't have explicit rule for 'app' then the only obvious way is to do it through eta or beta expansion rules.
To make it work, we have to use something that slides through lambda.
app f [ p ∘ fst id , snd id ]─────────────────────────────────────────app (lam (app f [ p ∘ fst id , snd id ]))─────────────────────────────────────────app (lam (app f) [ p ])─────────────────────────────────────────app (f [ p ])
The another interesting thing we can try is to take an application. Can we pass a substitution through it?
(app f) [ id , x ] [ p ]───────────────────────────────────────────────────────(app f) [ (id , x) ∘ p ]───────────────────────────────────────────────────────(app f) [ (id ∘ p , x [ p ]) ]───────────────────────────────────────────────────────(app f) [ p , x [ p ] ]───────────────────────────────────────────────────────(app f) [ id ∘ (p , x [ p ]) ]───────────────────────────────────────────────────────(app f) [ (fst id , snd id) ∘ (p , x [ p ]) ]───────────────────────────────────────────────────────(app f) [ (fst id ∘ (p , x [ p ]) , snd id [ (p , x [ p ]) ] ) ]───────────────────────────────────────────────────────(app f) [ (fst id ∘ (p , x [ p ]) , snd id [ (p , x [ p ]) ] ) ]
At this point it goes complicated, so lets separate the first and second part.
fst id ∘ (p , x [ p ])───────────────────────────────────────────────────────fst (fst id ∘ (p , x [ p ]) , snd id [ p , x [ p ] ])───────────────────────────────────────────────────────fst (fst id ∘ (p , x [ p ]) , snd id [ p , x [ p ] ])───────────────────────────────────────────────────────fst ((fst id , snd id) ∘ (p , x [ p ]))───────────────────────────────────────────────────────fst (id ∘ (p , x [ p ]))───────────────────────────────────────────────────────fst (p , x [ p ])───────────────────────────────────────────────────────p
And the second part.
snd id [ (p , x [ p ]) ]───────────────────────────────────────────────────────snd (fst id ∘ (p , x [ p ]) , snd id [ (p , x [ p ]) ])───────────────────────────────────────────────────────snd ((fst id , snd id) ∘ (p , x [ p ]))───────────────────────────────────────────────────────snd (id ∘ (p , x [ p ]))───────────────────────────────────────────────────────snd (p , x [ p ])───────────────────────────────────────────────────────x [ p ]
Somewhere we took a wrong turn and ended up with value we already had, but it's entertaining and we discovered other rules.
Actually we need to change them in a different way.
p───────────────────────────────────────────────────────p ∘ id───────────────────────────────────────────────────────p ∘ fst (id , x [ p ])───────────────────────────────────────────────────────p ∘ fst (id ∘ (id , x [ p ]))───────────────────────────────────────────────────────p ∘ fst ((fst id , snd id) ∘ (id , x [ p ]))───────────────────────────────────────────────────────p ∘ fst (fst id ∘ (id , x [ p ]) , snd id [ id , x [ p ] ])───────────────────────────────────────────────────────p ∘ fst id ∘ (id , x [ p ])
The second one needs to come like this:
x [ p ]───────────────────────────────────────────────────────snd (id , x [ p ])───────────────────────────────────────────────────────snd (id ∘ (id , x [ p ]))───────────────────────────────────────────────────────snd ((fst id , snd id) ∘ (id , x [ p ]))───────────────────────────────────────────────────────snd ((fst id ∘ (id , x [ p ]), snd id [id , x [ p ]])───────────────────────────────────────────────────────snd id [ id , x [ p ] ]
Now it's possible to "slide" the substitution past the argument's substitution.
(app f) [ p ∘ fst id ∘ (id , x [ p ]) , snd id [ (id , x [ p ]) ] ) ]───────────────────────────────────────────────────────(app f) [ (p ∘ fst id , snd id) ∘ (id , x [ p ]) ]───────────────────────────────────────────────────────(app f) [ (p ∘ fst id , snd id) ] [ (id , x [ p ]) ]───────────────────────────────────────────────────────(app f) [ (p ∘ fst id , snd id) ] [ (id , x [ p ]) ]───────────────────────────────────────────────────────app (f [ p ]) [ (id , x [ p ]) ]
See! We slid it past and discovered rules for how substitions work. Here's two most interesting ones I noticed.
fst id ∘ p──────────fst psnd id [ p ]────────────snd p
One interesting thing left not mentioned is, how do the scope works? How do you obtain traditional variables? Easy:
snd id - de bruijn index 0snd (fst id) - de bruijn index 1snd (fst (fst id)) - de bruijn index 2... - ...
Finally, lets go through the typing rules as they're interesting. First we cover substitutions.
Identity substitutions alter no context, and composition is like expected. These resemble functions.
──────────id : X » Xf : Y » Z g : X » Y───────────────────────f ∘ g : X » Z
Epsilon rule is for empty contexts. It's allowable when there are no variables to complete in an expression.
─────────ε : X » ∙
Context extension is the first typing rule that has something interesting going on with it. Mainly, we are expected to substitute the context into the type.
p : X » Y u : X ⊢ A [ p ]────────────────────────────(p , u) : X » Y , A
There's a very obvious rule for the first eliminator.
p : X » Y , A─────────────fst p : X » Y
Next lets cover the terms. The second eliminator is roughly what you'd expect.
p : X » Y , A───────────────────────snd p : X ⊢ A [ fst p ]
Substitution always follows the same form. Also the function introduction/elimination are very interesting because they're symmetric rules.
u : Y ⊢ A p : X » Y───────────────────────u [ p ] : X ⊢ A [ p ]u : X , A ⊢ B────────────────λ u : X ⊢ Pi A Bu : X ⊢ Pi A B─────────────────app u : X , A ⊢ B
Here are the type formation rules. Blank universe works as a base type, along with elements.
────────U : X 〒u : X ⊢ U───────────El u : X 〒
Pi passes the domain's type to the context of the codomain's type. Also substitution is like what you'd expect.
A : X 〒 B : X , A 〒────────────────────────Pi A B : X 〒A : Y 〒 p : X » Y─────────────────────A [ p ] : X 〒
For completeness, context typing rules:
──────∙ : ★X : ★ A : X 〒─────────────────────X , A : ★
Lets check types for something before we stop. For instance those de bruijn indices.
id : X , A » X , A─────────────────────────────snd id : X , A ⊢ A [ fst id ]id : X , A , B » X , A , B─────────────────────────────────────fst id : X , A , B » X , A─────────────────────────────────────────────snd (fst id) : X , A , B ⊢ A [ fst (fst id) ]
Context extension is interesting enough rule on its own.
Lets consider what would happen if we were to give it
El (snd id) as a type.
p : X » Y u : X ⊢ A [ p ]────────────────────────────(p , u) : X » Y , Ap : X , U » Y u : X , U ⊢ El (snd id) [ p ]──────────────────────────────────────────────(p , u) : X , U » Y , El (snd id)p : X , U » Y u : X , U ⊢ El (snd [ p ])──────────────────────────────────────────────(p , u) : X , U » Y , El (snd id)
Now, what were to happen if we passed 'q' into that context?
q : Z ⊢ U────────────────────(id , q) : Z » Z , Uq : Z ⊢ U p : X , U » Y u : X , U ⊢ El (snd [ p ])─────────────────────────────────────────────────────────(p , u) ∘ (id , q) : Z » Y , El (snd id)q : Z ⊢ U────────────────────────────────────────────────────────────────────────p ∘ (id , q) : Z » Y u [ id , q ] : Z ⊢ El (snd [ p ]) [ id , q ]────────────────────────────────────────────────────────────────────────(p ∘ (id , q), u [id , q]) : Z » Y , El (snd id)q : Z ⊢ U────────────────────────────────────────────────────────────(p , q) : Z » Y u [ id , q ] : Z ⊢ El (snd [ p , q ])────────────────────────────────────────────────────────────(p , q , u [id , q]) : Z » Y , El (snd id)q : Z ⊢ U──────────────────────────────────────────────(p , q) : Z » Y u [ id , q ] : Z ⊢ El q───────────────────────────────────────────────(p , q , u [id , q]) : Z » Y , El (snd id)
Notice that the type of the context doesn't change. Now if we were going to take the variable out from the context, it would change.
(p , q , u [id , q]) : Z » Y , El (snd id)───────────────────────────────────────────────────────────────────────snd (p , q , u [id , q]) : Z ⊢ El (snd id) [ fst (p , q , u [id , q]) ]─────────────────────────────────────────────────────────────snd (u [id , q]) : Z ⊢ El (snd id) [ (p , q) ]───────────────────────────────────────snd (u [id , q]) : Z ⊢ El (snd (p , q))───────────────────────────snd (u [id , q]) : Z ⊢ El q
That's it for now.
Conclusion
This syntax is compact and it can be implemented in Agda as an intrinsically typed structure. It is implemented as a type which's elements are reduction groups of terms. That is, if two terms are equal, they have the same element. Every reduction group has an unique normal form, that is proven by the existence of a terminating normaliser.
The intrinsic typing adds complexity but also verifies that everything is correct. It took me a month to implement a normaliser for this simple syntax. It's a huge project, 5000 lines of Agda. The syntax is the core of that project.