O'Reilly logo

Lambda Calculus with Types by Richard Statman, Wil Dekkers, Henk Barendregt

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

1

The Simply Typed Lambda Calculus

1.1 The systems image

Untyped lambda calculus

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

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.

image

Figure 1.1 Untyped lambda terms

This makes ∨ = {x, x, x, …}.

1.1.2 Notation

  (i) x, y, z, …, x0, y0, z0, …, x1, y1, z1, … denote arbitrary variables.

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

(iii) MN1Nk ≡ (..(MN1) … Nk),

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required