CS263–Spring 2008
Topic 1: The Lambda Calculus
Section 4.1: Semantics III

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

Set-theoretic Properties of the Models

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

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]))∈ℝ𝔼

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?

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?)

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]))}∈ℝ𝔼

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?)

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 ℙ using the same U[X]?  Exercise?

Connections with inclusion properties

In general, under our definitions, U==λ X. U[X] is not always true.

For example take U==ℕ×{0}.  Then we have λ X. U[X]=={0}⋃ℕ×{0}.

Question.  Is it true that U⊆λ X. U[X]?  Exercise?

Another connection with inclusions a a kind of monotonicity of λ-abstraction:

Theorem.  For continuous operators we have:
   (Subscript[λX, 0]). (Subscript[λX, 1]). (Subscript[…λX, n-1]). Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) ⊆ (Subscript[λX, 0]). (Subscript[λX, 1]). (Subscript[…λX, n-1]). Ψ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1]))
                                            if, and only if
   for all (Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])∈ℙ. Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) ⊆ Ψ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1]))   
                                            if, and only if
   for all (Subscript[E, 0]),(Subscript[E, 1]),…,(Subscript[E, n-1])∈𝔽. Φ((Subscript[E, 0]),(Subscript[E, 1]),…,(Subscript[E, n-1])) ⊆ Ψ((Subscript[E, 0]),(Subscript[E, 1]),…,(Subscript[E, n-1]))

Related to this monotonicity, we have useful results concerning unions and intersections.

Theorem.  For U,V,X∈ℙ and for continuous operators Φ and Ψ we have: 
     U[X]⋃V[X]==(U⋃V)[X]  and  λ X. (Φ (X)⋃Ψ (X))==λ X. Φ (X)⋃λ X. Ψ (X) .

Note.  This theorem can be generalized to operators of more variables and to infinite unions.

Theorem.  For for continuous operators Φ and Ψ we have: 
                            λ X. (Φ (X)⋂Ψ(X))==λ X. Φ (X)⋂λ X. Ψ (X) .

Note.  This theorem can be generalized to operators of more variables.

Question.  Why can we not generalize the intersection result to infinite intersections?

Another theorem connected with monotonicity gives an alternative definition of continuity.

Theorem.  An operator Φ:ℙ→ℙ is continuous if, and only if, for all expanding infinite sequences of sets (Subscript[X, 0])⊆(Subscript[X, 1])⊆…⊆(Subscript[X, i])⊆…∈ ℙ we have
                                                 Φ((⋃_(i==0)^∞)(Subscript[X, i]))=(⋃_(i==0)^∞)Φ((Subscript[X, i])).

The least fixed point

A the very basis of the idea of recursion is the principle that recursive definitions can be achieved by iteration.  In the case of of continuous operators, this can be made very explicit in a form much promoted by S.C. Kleene in his work on the theory of recursive functions

Theorem.  Any continuous operator Φ:ℙ→ℙ has a least fixed point given by
                                                 P==(⋃_(i==0)^∞)(Φ^i)(∅)

Proof.  The notation (Φ^i)(X) means Φ iterated i-times starting with X.

Now, if we set X==∅, then in the beginning ∅⊆Φ(∅).  Because Φ is monotone, it then easily follows that in all the later stages of iteration (Φ^i)(∅)⊆(Φ^(i+1))(∅).  (Why?)

Note, too, that if we knew that Φ had a fixed point Q, then because ∅⊆Q, we could conclude that (Φ^i)(∅)⊆Q holds for all i.  (Why?)  So this means that for the P of the theorem, we would have P⊆Q.

Therefore, if P can be shown to be a fixed point, it must be the least.

Well, take the P of the theorem and calculate the action of Φ on it using what we know about continuity.  We find:

Φ(P)==Φ((⋃_(i==0)^∞)(Φ^i)(∅))==(⋃_(i==0)^∞)(Φ^(i+1))(∅)==(⋃_(i==1)^∞)(Φ^i)(∅)==(⋃_(i==0)^∞)(Φ^i)(∅)==P.  (Why?)

This shows that P is a fixed point.  Q.E.D.

Question.  Can this last argument be used to show that the following theorem holds?

Theorem.  The least fixed point of a computable operator Φ:ℙ→ℙ is ℝ𝔼.

Proof.  We give an argument by combinators.  First, we are assuming that

F==λ X. Φ (X)∈ℝ𝔼.

Let D==λX. F[X[X]].  This is in ℝ𝔼.  Then, so is P==D[D].  (Why?)

From our knowledge of the formal use of reductions rules we know that P==F[P] holds.

But, by definition, F[P]==Φ (P).  So P is a fixed point of Φ in ℝ𝔼.

Ah, ha!  But is our combinator-created fixed point the least one?  Some proof is needed.

Let Q any fixed point of Φ in ℙ (not just in ℝ𝔼).  We have to show P⊆Q.

Because the operator X[X] is continuous, we can write: P==(⋃_(x∈(SuperStar[D])))§ x[§ x].  (Why?)

So we need to prove that for all x, if x∈(SuperStar[D]), then § x[§ x]⊆Q.

And we do that by Strong Induction.

So, assume that x∈(SuperStar[D]) and for integers less than x, the implication holds.

Assume y∈§ x[§ x].  We have to prove y∈Q.

By definition of application, we know that there is a pair (z,y)∈§ x with § z⊆§ x.

Inasmuch as the pair is a term of the sequence with number x, we know that z<x.

Now because § x⊆D, we have § z⊆D and so z∈(SuperStar[D]).  Hence, § z[§ z]⊆Q by the inductive assumption.

Also, because § x⊆D, we have (z,y)∈D. Hence, y∈F[§ z[§ z]] by the definition of D.

By monotonicity, F[§ z[§ z]]⊆F[Q]==Q.  Hence, y∈Q.  Q.E.D.

Note.  This proof is adapted from an old proof of the late David Park (Warwick University, UK) for a different model.

A note on defining fixed points

Note.  This proof is added for those students who might be interested.  It goes beyond what we need to know about definitions of computable objects, however.

In a more general set-theoretical setting, every monotone operator on a powerset has fixed points.

Knaster–Tarski Theorem (1928).  If the operator Φ∶𝒫 𝔸->𝒫 𝔸 is monotone, then the sets
	(Subscript[LFP, Φ])==⋂{X⊆𝔸|Φ(X)⊆X} and
	(Subscript[GFP, Φ])==⋃{X⊆𝔸|X⊆Φ(X)}
are, respectively, the least and greatest fixed point of Φ.

Proof.  Remark first that the definition of (Subscript[LPF, Φ]) is a proper intersection over a non-empty class, because we have Φ(𝔸)⊆𝔸.  Hence, (Subscript[LPF, Φ])∈𝒫 𝔸.  Of course, (Subscript[GPF, Φ])∈𝒫 𝔸.

Note too, that all fixed points P of Φ belong to the classes in the two definitions, thus
	(Subscript[LFP, Φ])⊆P⊆(Subscript[GFP, Φ]).
However, this does not prove that the two sets are fixed points.

Suppose that Φ(X)⊆X⊆𝔸 is any one of those sets in the first definition.  Then we have:
	(Subscript[LFP, Φ])⊆X.

By monotonicity we find:
	Φ((Subscript[LFP, Φ]))⊆Φ(X)⊆X.

Because Φ((Subscript[LFP, Φ])) is included in all the sets in the intersection, we conclude:
	Φ((Subscript[LFP, Φ]))⊆(Subscript[LFP, Φ]).

Again, by monotonicity we have:
	Φ(Φ((Subscript[LFP, Φ])))⊆Φ((Subscript[LFP, Φ])).

In other words, Φ((Subscript[LFP, Φ])) is one of the sets in the intersection, and so:
	(Subscript[LFP, Φ])⊆Φ((Subscript[LFP, Φ])).

Thus, we have proved:
	(Subscript[LFP, Φ])==Φ ((Subscript[LFP, Φ])).

And, by what we noted at the beginning, it must be the least fixed point.

The argument for (Subscript[GFP, Φ]) is analogous.  Q.E.D.

Note.  The proof for (Subscript[GFP, Φ]) can also be given by defining the operator:
	Ψ(X)==𝔸∖Φ(𝔸∖X),
and noting that Ψ is also monotone, and so (Subscript[GFP, Φ])==𝔸∖(Subscript[LFP, Ψ]).

Note. Here are two original references:
B. Knaster (1928). "Un théorème sur les fonctions d'ensembles". Ann. Soc. Polon. Math., vol. 6, pp. 133–134.
A. Tarski (1955). "A lattice-theoretical fixpoint theorem and its applications". Pacific Jour. Math., vol. 5. pp. 285–309.