Canonical form
- This page describes the canonical forms of the LF type theory. You might also be looking for the canonical forms lemma used to prove the progress theorem about a programming language.
Canonical forms are terms in a type theory that are both β-normal and η-long.
The LF type theory is defined so that all well-typed terms are canonical forms. This is useful because the LF methodology for representing object languages consists of creating an isomorphic representation of the object language as the canonical forms of particular LF types. Defining the type theory with only canonical forms uses an algorithm called hereditary substitution.
Syntax of LF
In Twelf's concrete syntax, the type 
is written {x:A1} A2, the kind 
is written {x:A} K, and the term 
is written [x] M. The type families include both dependent function types and applications 
of type families to terms. The kind level classifies type families. Type families of kind 
classify terms. Type families that are not yet fully instantiated have kinds 
. In both types and kinds, we use -> as an abbreviation when the argument is not free in the result.
Motivation for canonical forms
The above syntax describes what we call canonical forms. Note what is not a canonical form: there is no syntactic way to apply a lambda-abstraction to an argument. Based on your past experience with programming languages, it may seem strange to define LF so that only canonical forms exist—we are not allowed to write down any programs that have any computation left to do. However, this restriction makes sense if you think about our methodology for representing object languages in LF. For example, we represent natural numbers with the following LF signature:
nat : type. z : nat. s : nat -> nat.
For this representation to be adequate, the only LF terms of type nat must be z, s z, s (s z), and so on. It is easy to see that non-canonical LF terms interfere with this encoding. For example, the LF term 
would have type nat, but it is not the representation of any informal natural number.
Canonical LF
If you have encountered beta-reduction and eta-expansion before in your study of programming languages, it may help your intuition to know that the canonical forms of LF coincide with the beta-normal, eta-long terms of the lambda calculus. What we were saying above is that the syntax of canonical forms forces them to be beta-normal, and that the typing rules for canonical forms ensure that they are eta-long. In logic, canonical forms correspond to normal and neutral natural deduction proofs and cut-free sequent calculus proofs.
We do not present the typing rules for canonical forms here (see, e.g., Mechanizing Metatheory[1]). However, we note two details:
Terms 
are only canonical at base type 
, not at function type. For example, the constant s is not a canonical form of type nat -> nat. However, the term 
, which is equivalent, is a canonical form.
In a dependently typed language, the application typing rules must substitute the argument into the body of the dependent function type:
In LF, this substitution is in fact a hereditary substitution, ensuring that the terms embedded in the result of the substitution are in canonical form. The typing rule for family applications 
has a similar substitution into the result kind.
See also
- See the introductions to Twelf to learn how object languages are represented as the canonical forms of LF.
References
- ↑
Robert Harper, Daniel R. Licata - Mechanizing Metatheory in a Logical Framework
This page is incomplete. We should expand it.
