Proving metatheorems:Simply typed LF
|Proving metatheorems with Twelf|| Next:|
In the previous section, we discussed representing object-language syntax in LF. As we saw, to prove that an LF representation is correct, you need to be able to reason by induction on the canonical forms of LF. To do so, you will need a basic understanding of the LF type theory. This understanding will pay off later on, as we will also use induction on canonical forms to prove metatheorems about encoded languages.
In this section, we present simply-typed LF in more detail.
The syntax of simply-typed LF is as follows:
The types consist of base types (), which are declared in the signature (e.g., nat), and function types (). The terms of LF consist of variables (), constants () declared in the signature, application (), and lambda-abstractions (), which in Twelf's concrete syntax are written [x] M. This much should be familiar to you if you've seen the simply-typed lambda-calculus before. What may be unfamiliar to you is that the grammar is stratified into and . We discuss the reason for this stratification now.
The above syntax describes what we call canonical forms (as long as they are well-typed, more on this below). 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. In the previous section, we represented 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. This would contradict the third part of the adequacy argument in the previous section, but restricting LF to canonical forms avoids these counterexamples.
It is not worth presenting the typing rules for canonical forms here (see, e.g., ). The only detail we need to note here is that 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.
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.
Substitution of one canonical form into another does not necessarily produce a canonical result. For example:
Even though both terms are canonical forms, the result is beta-reducible.
However, it is possible to define a notion of hereditary substitution, which directly computes the canonical result of an ordinary substitution. When ordinary substitution would return a non-canonical form, hereditary substitution continues to reduce by substituting the argument into the body of the function. In the above example, the hereditary substitution
Whenever we use the notation for LF, we mean hereditary substitution.
Induction on canonical forms
The above syntax constitutes an inductive definition of the canonical forms of LF. Consequently, we can reason by induction on canonical forms using structural induction over this syntax. When a type adequately represents some informal object-language syntax, induction on the canonical forms of the type corresponds to the structural induction principle for the informal syntax. For example, the induction principle for the type nat defined in the previous section corresponds to the standard induction principle for the natural numbers. As we discussed in the previous section, induction on canonical forms is used to prove adequacy. Additionally, as we discuss below, induction on canonical forms is used to prove metatheorems about deductive systems.
Why a lambda calculus?
At this point, you may be wondering what we gain by using a lambda-calculus to represent other deductive systems—to represent the natural numbers, all we needed was constants and application; we never even used a term of the form . At a high level, the answer is that using a meta-language with variable binding permits clean representations of object languages with variable binding. However, we defer a real answer to this question until we talk about representing the syntax and judgements of a language with binding.
Robert Harper, Daniel R. Licata - Mechanizing Metatheory in a Logical Framework
|Proving metatheorems with Twelf|| Next:|