1

The Simply Typed Lambda Calculus

1.1 The systems

Recall the untyped lambda calculus denoted by ** λ**, see e.g. B[1984]

**1.1.1 Definition** The set of untyped *λ*-terms Λ is defined by the so-called ‘*simplified syntax*’ in Fig. 1.1. This basically means that parentheses are left implicit.

This makes ∨ = {*x*, *x*^{′}, *x*^{″}, …}.

**1.1.2 Notation**

(i) *x, y, z, …, x*_{0}, *y*_{0}, *z*_{0}*, …, x*_{1}, *y*_{1}, *z*_{1}, … denote arbitrary variables.

(ii) *M, N, L*, … denote arbitrary lambda terms.

(iii) *MN*_{1} … *N _{k}* ≡ (..(

Start Free Trial

No credit card required