Highlights on Kovács' NbE STLC thesis

I read Kovács thesis this weekend.

András Kovács: A Machine-Checked Correctness Proof of Normalization by Evaluation for Simply Typed Lambda Calculus (2017)

The thesis presents an efficient and verified implementation of beta-eta-normalization for simply typed lambda calculus, written in Agda.

I ended up reading this thesis because I was interested about an example of how to prove that a normalization algorithm is correct.

Embeddings & Substitutions forming a category

The thesis uses De-Bruijn indices. Interesting thing to me is that it's presenting substitution in a way that it forms a category.

Substitutions are presented in a form where every variable is substituted in at once. They get identity substitutions, and they can be composed.

Paper also describes embeddings as contexts that are obtained by retrieving embedding context and dropping entries from it.

Both order-preserved-embeddings and the substitutions are treated as categories.

Convertibility of terms

Conversion is defined with a structure that behaves a bit like the LT/GT relation in Idris.

For example, the conversion inside the lambda is denoted as:

lam : (t ~ t') → (lam t ~ lam t')

The structure defining convertibility also declares reflectivity, commutation and composition.

Completeness, Soundness, Stability

The thesis proves completeness, soundness and stability for STLC normalization.

  1. Complete: The input to the term is convertible to the output.
  2. Sound: Convertible terms normalize to same normal form.
  3. Stable: Normalization has no action on normal terms.

Stability is not as crucial as completeness and soundness, but it tells whether the normalization matches up with the definition of normal forms.

The soundness, as it's defined as (t ~ t') → (nf t ≡ nf t'), might be convenient for STLC only. Once you add coproducts into the language, normal forms of two convertible terms may vary.

For example: 

λf.λx. case f of { False -> x; True -> x }
λf.λx. x

Both are normal forms, but they seem like convertible to the same term? I should check the convertibility on this one, but nevertheless can still shuffle around case statements in expressions without changing their meaning.

Presheaf models

The thesis mentions that variables and terms of a given type are presheaves on order preserving embeddings.

Presheaves on C are C^op → Set -functors.

I don't entirely understand what this means.

Link to the Agda formalization

https://github.com/AndrasKovacs/stlc-nbe

Other remarks

I remember unification algorithm can be represented as an algorithm that finds a coequalizer in a category where morphisms are substitutions for certain sort of terms.

The Kripke Models -section in the thesis is interesting on its own. I may have to especially resume on that later.

Similar posts