Simple Typed Lambda Calculus

$$\newcommand{\unit}{\textsf{unit}} \newcommand{\t}{\tau} \newcommand\proves\vdash $$

1. Syntax and Semantics

Recall that the syntax of pure $\lambda$-calculus formally defined as follows

$$e:= x\mid \lambda x. e\mid e_1\ e_2 $$

Definition. Basic on this, we can define simple typed lambda calculus (STLC). The biggest difference is that we now have two inductively defined expressions: terms and types.

$$\begin{aligned} &\text{Types}& &\tau:=\unit \mid \tau_1\to\tau_2\\ &\text{Terms}& &e:=()\mid x\mid \lambda x:\t\ e\mid e_1\ e_2 \end{aligned} $$

where

• $():\unit$
• $\lambda x:\tau. e$ is a function that takes one input of type $\tau$ and evaluates $e$.

By convention, the function arrow is right-associative, so $\t_1\to\t_2\to\t_3$ is the same as $\t_1\to(\t_2\to\t_3)$. This convention matches left-associative function application.

The operational semantics of this language is unchanged from CBV-calculus, counting $()$ as a value which has no reduction rule. That is, we have the following definitions.

Definition. Values in STLC

$$v:=()\mid \lambda {x:\t}. e\\ $$

Definition. Evaluation Contexts of STLC

$$E:=[\cdot]\mid E\ e\mid v\ E $$

Definition. Reduction Rules of STLC

$$\infer{e\to e'}{E[e]\to E[e']}\quad \infer{}{(\lambda{x:\t}.e)v\to e[x\mapsto v]} $$

One other small change is that the presence of $()$ means there are now closed -terms can get stuck. For example

$$() (\lam{x:\unit}x) $$

is a perfectly good closed $\lambda$-term that is also stuck. We would like to eliminate these, and the type system will allow us to do so.

2. Typing Rules