CS263–Spring 2008
Topic 1: The Lambda Calculus
Section 3.2: Semantics II

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 9 February 2008

Computable Operators

Defining computability

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 and operators (in case we need them)

Let ℕ stand for the set of integers.

ℕ≅1+ℕ× ℕ

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

Let (SuperStar[ℕ]) stand for the set of finite sequences of integers.

ℕ≅(SuperStar[ℕ])

⟨⟩==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.

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

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

⟨⟩⌢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

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

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

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

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

Convention.   n=={n} for n∈ℕ.

ℕ⊆ℝ𝕖𝕔⊆ℝ𝔼⊆ℙ

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

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

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}
⟨X⟩=={⟨x⟩|x∈X}
⟨X,Y⟩=={⟨x,y⟩|x∈X& y∈Y}
(SuperStar[X])=={s|§ s⊆X}
X⌢Y=={s ⌢ t|s∈X& t∈Y}

Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) is monotone if, and only if, for all values of the variables,
 Φ((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.

Note. This operator is non-monotone:
X∖Y == {n | n∈X & n∉Y}

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∈ℙ.

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}.

Theorem.  Continuous operators (of any number of arguments) are closed under composition.

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

We call the following result the λ-abstract:
λ 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]))}

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]).

We call the following binary set operator 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 Φ.

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].

Using recursive enumerability

The recursively enumerable sets represent what is computable among sets of integers — at least in theory. We now use them to define what we mean by a computable operator.

A continuous operator Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) is said to be computable if, and only if, 
 (Subscript[λX, 0]). (Subscript[λX, 1]). (Subscript[…λX, n-1]). Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1]))∈ℝ𝔼

Some examples are needed, which have to be worked out from the definition of the λ-abstraction process.

Theorem.  Writing J==λ X. X and K==λ X. λ Y. X and K[J]==λ Y. λ X. X , we find:
	J=={0}⋃{(x,n)|n∈§ x},
	K=={0}⋃{(x,0)|x∈ℕ}⋃{((x,(y,n))|n∈§ x}, and
	K[J]=={0}⋃{(y,0)|y∈ℕ}⋃{((y,(x,n))|n∈§ x}.

Note. The above sets are all  recursive.

Question.  What about S==λ X. λ Y. λ Z. X[Z][Y[Z]] ?  Exercise?

Here is another important one, which brings in application:

Theorem.  Writing Ap==λ U. λ X. U[X], we find:
	Ap=={0}⋃{(u,0)|u∈ℕ}⋃{((u,(x,n))|∃((Subscript[x, 1]),n)∈§ u . § (Subscript[x, 1]) ⊆ § x}.

Note. It is another recursive set.  (Why?)

The stuff seen above with all those 0s is not so important.  The definition comes down to something simpler:

Theorem.  A continuous operator Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) is computable 
                                               if, and only if, 
         {((Subscript[x, 0]),((Subscript[x, 1]),…,((Subscript[x, n-1]),m)…))|m ∈ Φ(§ (Subscript[x, 0]),§ (Subscript[x, 1]),…,§ (Subscript[x, n-1]))}∈ℝ𝔼

This means that you have a recursively enumerable way of generating how output from the operator depends on (finite) inputs.

Note.  In the recursive-function literature, the computable, continuous operators are called "enumeration operators".  Unfortunately that literature does not relate so directly to Computer Science.

ℝ𝔼 as a model for combinators

From the definition of U[X] we can see that in case U∈ℝ𝔼, then if X∈ℝ𝔼, so is U[X].  This observation is important enough to call a theorem, which has several corollaries:

Theorem.  Not only is U[X] a computable operator (of two arguments), but the family ℝ𝔼 is closed under application.

Corollary.  Computable operators (of any number of arguments) are closed under composition.  (Why?)

Now, since the sets corresponding to J, K, and S are indeed in  ℝ𝔼, we see at once we have another model for the combinators.

Corollary.  ℝ𝔼 is a model for the crules of combinators using the operator  U[X]  as the application operation.

Note.  The models ℙ and ℝ𝔼 both have the property that the crules are satisfied as equations, not just reduction rules:
	J[X]==X
K[X][Y]==X
S[X][Y][Z]==X[Z][Y[Z]]

Question.  Are there other models for the crules between 
ℝ𝔼  and ℙ also using the same U[X] ?  Exercise?