CS263–Spring 2008
Topic 1: The Lambda Calculus
Section 3.1: Semantics I

Dana S. Scott
Hillman University Professor (Emeritus)
School of Computer Science
Carnegie Mellon University
====
Visiting Professor EECS
Visiting Scientist
Logic & Methodology Program
University of California, Berkeley

Last edited 3 February 2008

A Calculus of Operators

Pairs and sequences

Those combinators (in case we need them)

Here is the total suite of definitions we have been using (plus a couple of extra).  
Marked in yellow are the Mathematica definitions for manipulating combinations.  
The others are assignments for introducing short-hand names for specific combinators.

crules={J[x_]->x,S[x_][y_][z_]->x[z][y[z]],K[x_][y_]->x};

ToC[vars_,comb_]:=Fold[rm,comb,Reverse[vars]];

rm[v_,v_]:=J;
rm[f_[v_],v_]/;FreeQ[f,v]:=f;
rm[h_,v_]/;FreeQ[h,v]:=K[h];
rm[f_[g_],v_]:=S[rm[f,v]][rm[g,v]];

Y=ToC[{f},ToC[{x},f[x[x]]][ToC[{x},f[x[x]]]]];

zero=K[J];
succ=S[S[K[S]][K]];
plus=S[K[S]][S[K[S[K[S]]]][S[K[K]]]];
times=S[K[S]][K];
power=S[K[S[J]]][K];

one=succ[zero];
two=succ[one];
three=succ[two];
four=succ[three];

sum=ToC[{n,m},n[succ][m]];
prod=ToC[{n,m},n[sum[m]][zero]];
exp=ToC[{n,m},m[prod[n]][one]];

cnum[0]:= zero;
cnum[n_]:= succ[cnum[n-1]];

pair=ToC[{x,y,z},z[x][y]];

left=ToC[{x,y},x];
right=ToC[{x,y},y];

shift=ToC[{p},pair[succ[p[left]]][p[left]]]//.crules;
pred=ToC[{n},n[shift][pair[zero][zero]][right]]//.crules;

shift1=ToC[{p},pair[p[right]][right]]//.crules;
zeroQ=ToC[{n},n[shift1][pair[left][right]][left]]//.crules;

equalQ=ToC[{n,m},pair[zeroQ[m[pred][n]]][right][zeroQ[n[pred][m]]]];

godel[J]:=0;
godel[S]:=1;
godel[K]:=2;
godel[a_[b_]]:=2+(2^(godel[a])) (2 godel[b]+1);

combo[0]:=J;
combo[1]:=S;
combo[2]:=K;
combo[n_]:=Block[{p=IntegerExponent[n-2,2]},Block[{q=(1/2) (((n-2)/(2^p))-1)},combo[p][combo[q]]]];

Sequences of integers

For a period in these lectures we need to discuss the (non-negative) integers in a mathematical way.

Let ℕ stand for the set of integers, and consider this one-one correspondence:

ℕ≅1+ℕ× ℕ

In words, we can say that, save for one integer, every integer can be regarded as a pair of integers.  We have used this before, and we gave this definition of a pair:

(n,m)==(2^n) (2 m+1)

The one integer left out is, of course, 0.

Let (SuperStar[ℕ]) stand for the set of finite sequences of integers, and consider this one-one correspondence:

ℕ≅(SuperStar[ℕ])

This relationship can be justified via the following recursive definition:

⟨⟩==0
⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1]),(Subscript[x, n])⟩==(⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩,(Subscript[x, n]))

Theorem. Under this definition every integer can be uniquely regarded as a sequence number.

Proof. Inasmuch as pair numbers uniquely determine their components, so sequence numbers uniquely determine all their components.

To argue that every integer is a sequence number, argue by Strong Induction.

Assume about an integer k that all smaller integers are sequence numbers.  If k==0, then it is — by definition — the number of the empty sequence.

If k>0, then we know (in view of integer factorization) that uniquely k==(2^p) (2 q+1)==(p,q).

Because p<k, then, by the inductive assumption, p==⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩ for suitable uniquely determined integers.  Let (Subscript[x, n])==q, and then k==⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1]),(Subscript[x, n])⟩.  Q.E.D.

Operations on sequences

From time to time, we will need to concatenate sequences and to check their lengths.  Try these definitions:

x⌢⟨⟩==x
x⌢(y,z)==(x⌢y,z)

|⟨⟩|==0
|(y,z)|==|y|+1

Question.  Why are these definitions justified?

Question. And can you prove these next equations?

⟨⟩⌢x==x
x⌢(y⌢z)==(x⌢y)⌢z

⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩⌢⟨(Subscript[y, 0]),(Subscript[y, 1]),…,(Subscript[y, m-1])⟩==⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1]),(Subscript[y, 0]),(Subscript[y, 1]),…,(Subscript[y, m-1])⟩
⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩==⟨(Subscript[x, 0])⟩⌢⟨(Subscript[x, 1])⟩⌢…⌢⟨(Subscript[x, n-1])⟩

|x⌢y|==|x|+|y|
|⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩|==n

We also need to form the set of terms of a sequence:

§⟨(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])⟩=={(Subscript[x, 0]),(Subscript[x, 1]),…,(Subscript[x, n-1])}

Here are some facts:

§⟨⟩==∅
§ (y,z)==§ y⋃{z}
§ (x⌢y)==§ x⋃§ y

Warning.  Remember in standard mathematics sets and sequences are different.

Operations on sets

Some key types of sets

We have been letting ℕ stand for the set of integers, but what we need in addition are some key families of sets of integers.  First we have the so-called powerset consisting of all sets of integers.

ℙ==𝒫 ℕ=={X|X⊆ℕ}

For the theory of computability, a subfamily of ℙ, the recursively enumerable sets, is important,
as is the family of recursive sets.

ℝ𝔼=={X|X⊆ℕ & X is recursively enumerable}
ℝ𝕖𝕔=={X|X⊆ℕ & X is recursive}

As a simplifying convention we are going to identify singleton sets of integers with the corresponding integer:  n=={n} for n∈ℕ.  In Set Theory is not generally done, but on one set which is not otherwise correlated with sets this is harmless.

With this convention about singleton sets, we have so far this range of types.

ℕ⊆ℝ𝕖𝕔⊆ℝ𝔼⊆ℙ

One more important family is the family of finite sets:

𝔽=={X|X⊆ℕ & X is finite}

And we have:

ℕ⊆𝔽⊆ℝ𝕖𝕔⊆ℝ𝔼⊆ℙ

Note.  There is of course a vast range of families between ℝ𝔼 and ℙ, but we do not stop now to notate any of them.

Continuous operators

There are many useful operations mapping sets of integers to sets of integers.  Here are several we will use:

X⋂Y=={n|n∈X& n∈Y}
X⋃Y=={n|n∈X∨m∈Y}
X+Y=={m+n|n∈X& m∈Y}
X×Y=={(n,m)|n∈X& m∈Y}
(SuperStar[X])=={x|§ x⊆X}
X⌢Y=={x ⌢ y|x∈X& y∈Y}

These particular operations also have some special properties.  First, as operators, they are monotone.  For set operators Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])), monotonicity is defined as:

Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1]))⊆Φ((Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1])) whenever (Subscript[X, i])⊆(Subscript[Y, i]) for all i<n.

In words you can say: The more you put in, the more you get out.  It is to be hoped that it is clear that all the specific operators defined above do have this monotonicity property.

Note. The prime example of a non-monotone set operator is the operation of set-theoretical complement:

X∖Y == {n | n∈X & n∉Y}

However, our monotone operators above also have an additional property, roughly described as: If you only want a little more out, you only have to put a little more in.

That is not a very precise statement!  We have to interpret "little" as "finite" to make a better characterization.  We give the definition for operators on two sets of integers.  It is easy to generalize this to more arguments.

A monotone operator Φ(X,Y) is said to be continuous if, and only if, 
for all X,Y∈ℙ whenever F⊆Φ(X,Y) and F∈𝔽, then 
there are D, E∈𝔽 with D⊆X and E⊆Y 
such that F⊆Φ(D,E), for all X,Y∈ℙ.

Note. There are many reasons to call this property "continuous", but it is sufficient to say now that it is analogous to the ϵ-δ-definitions of continuity from The Calculus.

And, it is to be hoped that it is clear that all the specific operators defined above do have this continuity property.

In the case of operators on one variable, continuity and monotonicity can be captured together in one equation:

Theorem.  An operator Φ:ℙ→ℙ mapping sets of integers to sets of integers is both monotone and continuous if, and only if, for all X∈ℙ we have
                                     Φ(X)==⋃{Φ(D)|D∈𝔽 & D⊆X}.

Note. We can generalize this result to operators with many arguments easily.

Note. And to save writing, we will now assume "continuous" implies "monotone".

λ Abstraction

Observation.  A continuous operator Φ:ℙ→ℙ is completely determined by the information n∈Φ(D) for D∈𝔽.  (Why?)

Let's consider as well continuous operators of many arguments.  To each such operator Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1])), where one argument has been singled out, we now associate this new operator:

λ X. Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]))=={0}⋃{(x,n)|n∈Φ(§ x,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]))}

On the right-hand side, x ranges over all sequence numbers (i.e., all integers), and then § x ranges over all finite sets of integers.

Note. The right-hand side of the definition does not depend on the set variable X anymore.  In other words the λ X on the left-hand side is a new variable-binding construct.

The result is an operator that only depends on the remaining variables (Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]).  We call the result the λ-abstract.

Note. The need for the {0} will be explained later.  For the time being, it does no harm.

Theorem.  If Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1])) is a continuous operator of all its variables X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]), then  λX. Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1])) is a continuous operator of the remaining variables (Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]).

In order to show that not only does the λ-abstraction construct preserve enough information to determine the original continuous operator, but it also makes it easy to define what we mean by a computable operator.  To this end, consider the following binary set operator called application:

U[X]=={n|∃(x,n)∈U. § x⊆X}

Theorem.  Not only is U[X] continuous, but we have
                          λX. Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1]))[X]==Φ(X,(Subscript[Y, 0]),(Subscript[Y, 1]),…,(Subscript[Y, n-1])) 
 for every continuous operator Φ.

The detailed proof is left for a project (though the truth of the assertion should be apparent).

Consider a continuous operator Φ(X,Y,Z) of three set variables as an example.  The iterated λ-abstract U==λ X. λ Y. λ Z. Φ(X,Y,Z) is just a (slightly) complicated set of integers.  (Why?)  But, it contains all the necessary information to redefine the given operator Φ, because U[X][Y][Z]==Φ(X,Y,Z).  (Why?)  Hence,

Corollary.  ℙ is a model for the crules of combinators using this defined set operator  U[X]  as the application operation.

Corollary.  Under the crules, no combinator can reduce both to K and K[J].

Question.  Are the other models?