Computer Science 591i
Environment Models, Combinatory Models.

How far can we squash the -calculus down?

In an environment model we identify certain terms of

(D) which are syntactically distinct. For example

is necessarily mapped to the same value as

(+ p a) in any environment model. Moreover, further identification is possible. For example (+ a b) will be mapped to the same value as (+ b a) in any environment model which implements addition defined by the standard rules. How far can this identification process go? Can we project the lambda-calculus down to an environment model consisting of a single element, or to a finite number of elements? The following two lemmas demonstrate that the values of projection functions must be distinct in any non-trivial environment model.

From now on we'll write (d₁ d₂) for (d₁)(d₂).

Lemma EM4

In any environment model if, for some environment

₁

then for any d₁ . . .d_n in D, (p d₁ . . .d_n) = d

Lemma EM5

In any environment model if, for some environment

₁

then for any d₁ . . .d_n in D, (p d₁ . . .d_n) = d_i

Proof

By induction on i.

Base Case: i=1

₁

= (f)

where

₂

₁

= [ ( x₂ . . . . x_n . x₁) [x₁:=d] ()

by the substitution lemma

= [ ( x₂ . . . . x_n . d)] ()

₁

₂

₁

by lemma EM4

Inductive Step

Suppose that if for some i

₁

then for any d₁ . . .d_n in D, (p d₁ . . .d_n) = d_i

Consider

₁

_i+1

where

₂

_i+1

₁

= [ ( x₂ . . . . x_n . x_i+1) [x₁:=d] ()

by the substitution lemma

= [ ( x₂ . . . . x_n . x_i+1)] [x₁:=d] ()

= [ ( x₂ . . . . x_n . x_i+1)] ()

Now consider

₁

₂

= ([ ( x₂ . . . . x_n . x_i+1)] () d₂ . . .d_n)

= d_i+1

by the inductive hypothesis. Hence result.

Lemma EM6

The equation

₁

where 1 i < j n is not valid in any environment model , for which D has more than one element.

Proof

Since D has more than one element, we can choose d₁ . . . d_i . . . d_j . . . d_n where d_i d_j and apply lemma EM5.

Combinatory Models

At this point, let's return to our consideration of combinators. We have already shown that any term E of (C) has a corresponding combinatory lambda term E' which is alpha-beta equivalent to it. We also showed that any applicative algebra which was the image of (C) under a valuation necessarily contained the combinators S,K,I.

Now in considering environment models, we have already adopted the convention that we write (d₁ d₂) for (d₁)(d₂). This immediately raises the idea, could we get an environment model from a combinatory algebra by defining

₁

₂

₁

₂

Unfortunately the axioms for a combinatory algebra aren't quite strong enough for this to work, because we also need the function, which is a left-inverse of . Let's consider the function which maps d to ((d)). Indeed, let's suppose it is a function which corresponds to an element
e D. Then we have

₀

₁

= ((((d₀))) d₁)

= ( (d₀) d₁) = (d₀ d₁)

since

is the left inverse of

Computer Science 591i Environment Models, Combinatory Models.

How far can we squash the -calculus down?

Lemma EM4

Lemma EM5

Proof

Base Case: i=1

Inductive Step

Lemma EM6

Proof

Combinatory Models

Computer Science 591i
Environment Models, Combinatory Models.