Simply-typed lambda calculus

From The Twelf Project
Jump to: navigation, search

The simply-typed lambda calculus is a common example of a simple typed programming language. This article discusses its encoding in Twelf.

If you're trying to learn Twelf from this example, you may wish to read the discussion starting in Representing the syntax of the STLC in the tutorial Proving metatheorems with Twelf. That introductory guide discusses this representation of the STLC and why it works in more detail. This page summarizes the judgements of the STLC and the corresponding LF code for reference, but does not explain them in detail.

What is illustrated by this example?

There are simpler examples of LF representations (see, e.g., the natural numbers). However, the STLC is a good first example of a representation that uses higher-order abstract syntax and higher-order judgments. These two representation techniques drastically simplify the process of representing and proving theorems about many programming languages and logics. The idea is that the binding structure of LF is used to represent the binding structure of the object language. At the level of syntax, this gives alpha-equivalence and capture-avoiding substitution "for free" from the representation. At the level of judgements, this gives the properties of a hypothetical judgement, such as weakening and substitution, for free.

This encoding of the STLC is adapted from Mechanizing Metatheory in a Logical Framework[1]. Section 3 of that paper exhaustively discusses the adequacy of this encoding.

Encoding of syntax

The types of the simply typed lambda calculus are simply the unit type and the arrow or function type.

tp : type.
arrow : tp -> tp -> tp.
unit : tp.

The terms are the variable , the empty pair (which has type unit), lambda abstraction (with a type annotation), and application.

tm : type.
empty : tm.
app : tm -> tm -> tm.
lam : tp -> (tm -> tm) -> tm.

Encoding of judgments

Static semantics

The typing rules for the simply typed lambda calculus use a typing context to record the type annotations that have been encountered at lambda-bindings.

                             

This judgement is represented by the following LF signature:

of : tm -> tp -> type.
of-empty : of empty unit.
of-lam : of (lam T2 ([x] E x)) (arrow T2 T)
          <- ({x: tm} of x T2 -> of (E x) T).
of-app : of (app E1 E2) T
          <- of E1 (arrow T2 T)
          <- of E2 T2.

Assumptions in the typing context are represented as a pair of objects x:tm and d:of x T in the LF context (T is the LF representation of the type ). This can be seen in the encoding of the judgment of_lam. There is no need to write out the equivalent of the of-var rule, becuase the necessary judgment is directly assumed by the of-lam rule. This method avoids the need for a substitution lemma, and the article on that subject discusses the matter further.

Dynamic semantics

We define the dynamic semantics of the STLC by a call-by-value, left-to-right structural operational semantics on closed terms.

The judgement identifies the values:

            

Next, we define the operational semantics with a judgement :

            

These judgments are represented by the following Twelf signature:

value : tm -> type.
value-empty : value empty.
value-lam : value (lam T ([x] E x)).

step : tm -> tm -> type.
step-app-1 : step (app E1 E2) (app E1' E2)
              <- step E1 E1'.
step-app-2 : step (app E1 E2) (app E1 E2') 
              <- value E1
              <- step E2 E2'.
step-app-beta : step (app (lam T2 ([x] E x)) E2) (E E2)
                 <- value E2.

You can see or download the full Twelf source, which is almost exactly that of Figure 7 and Figure 13 of Mechanizing Metatheory [1]. You can also see Twelf's output, which is closer to the LF code in Figure 7 and Figure 10 of that paper, because it makes the implicit parameters explicit. Note that in Twelf's concrete syntax, curly brackets ({}) are used for pi-bindings instead of the symbol.

Metatheorems

Several metatheorems about this formulation of the simply typed lambda-calculus are proved on this wiki. See, for example:

References

  1. 1.0 1.1 Robert Harper, Daniel R. Licata - Mechanizing Metatheory in a Logical Framework
    Journal of Functional Programming ,2007
    Bibtex
    Author : Robert Harper, Daniel R. Licata
    Title : Mechanizing Metatheory in a Logical Framework
    In : Journal of Functional Programming -
    Address :
    Date : 2007