Simply-typed lambda calculus

The simply-typed lambda calculus (or STLC) is a common example of a simple typed programming language. This article discusses its encoding in STELF.

If you’re trying to learn STELF from this example, you may wish to read the discussion starting in “Representing the syntax of the STLC” from the Introduction to Proving Metatheorems in STELF. 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 by Harper and Licata. The STELF in this article closely tracks Figure 7 and Figure 13 from that paper, and 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.

$$\tau ::= \mathsf{unit} \mid \tau_1 \rightarrow \tau_2$$

%sort tp %.
%term arrow %pi tp %-> tp %-> tp %.
%term unit tp %.
%worlds () (tp) %.

The terms are the variable $x$, the empty pair (which has type $\mathsf{unit}$), lambda abstraction (with a type annotation), and application.

$$e ::= x \mid \langle\rangle \mid \lambda x{:}\tau.e \mid e_1\,e_2$$

%sort tm %.
%term empty tm %.
%term app %pi tm %-> tm %-> tm %.
%term lam %pi tp %-> (%pi tm %-> tm) %-> tm %.
%block tmvar {x tm}%.
%worlds (tmvar) (tm) %.

Encoding of judgments

Static semantics

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

$${ \over \gamma \vdash \langle\rangle : \mathsf{unit} }\mathit{of\textit{-}empty} \qquad { x : \tau \in \gamma \over \gamma \vdash x : \tau }\mathit{of\textit{-}var}$$ $${ \gamma, x :\tau_2 \vdash e : \tau \over \gamma \vdash \lambda x{:}\tau_2.e : (\tau_2 \rightarrow \tau) }\mathit{of\textit{-}lam} \qquad { \gamma \vdash e_1 : (\tau_2 \rightarrow \tau) \qquad \gamma \vdash e_2 : \tau_2 \over \gamma \vdash e_1\,e_2 : \tau }\mathit{of\textit{-}app}$$

This judgement is represented by the following LF signature:

%sort of {_ tm} {_ tp} %.
%term of-empty of empty unit %.
%term of-lam
  %pi (of (lam T2 ([x] E x)) (arrow T2 T))
  %<- ({x tm} %pi (of x T2) %-> (of (E x) T)) %.
%term of-app %pi (of (app E1 E2) T) %<- (of E1 (arrow T2 T)) %<- (of E2 T2) %.
%block tmof [T tp] {x tm} {d of x T}%.
%worlds (tmof) (of _ _) %.

Assumptions $x : \tau$ in the typing context $\gamma$ are represented as a pair of objects x:tm and d: of x T in the LF context $\Gamma$ (where T is the LF representation of some type $\tau$). 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, because the necessary judgment is directly assumed by the of-lam rule. This method avoids the need for a substitution lemma: 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 $e\,\mathtt{value}$ identifies the values:

$${ \over \langle\rangle\,\mathtt{value} }\mathit{value\textit{-}empty} \qquad { \over \gamma x{:}\tau.e\,\mathtt{value} }\mathit{value\textit{-}lam}$$

Next, we define the operational semantics with a judgement $e \mapsto e'$:

$${ e_1 \mapsto e_1' \over e_1\,e_2 \mapsto e_1'\,e_2 }\mathit{step\textit{-}app_1} \qquad { e_1\,\mathtt{value} \qquad e_2 \mapsto e_2' \over e_1\,e_2 \mapsto e_1\,e_2' }\mathit{step\textit{-}app_2}$$ $${ e_2\,\mathtt{value} \over (\lambda x{:}\tau.e)\,e_2 \mapsto e[e_2/x] }\mathit{step\textit{-}app\textit{-}beta}$$

These judgments are represented by the following STELF signature:

%sort value {_ tm} %.
%term value-empty value empty %.
%term value-lam value (lam T ([x] E x)) %.
%sort step {_ tm} {_ tm} %.
%term step-app-1 %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step-app-2 %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step-app-beta %pi (step (app (lam T2 ([x] E x)) E2) (E E2)) %<- (value E2) %.
%worlds () (value _) (step _ _) %.

Metatheorems

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

• Proving metatheorems about the STLC for a proof of type preservation
• Output factoring for a proof of progress
• Uniqueness lemmas for a proof of determinacy of the operational semantics
• Proving totality assertions in non-empty contexts for a height judgement
• Proving metatheorems in non-empty contexts for a proof that the height of a term can only be increased by substitution.