CS263–Spring 2008
Topic 2: Type Theory
Section 7.1: Type Semantics IV

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 10 March 2008

Modelling (ληγ)-calculus

𝔻-continuity

All we really need to know about (Subscript[D, ∞]) can be stated as follows :

𝟙⊆D==D∘D==λ U. U∘D

And note we have dropped the ∞-subscript to simplify writing.  We also introduced a PER  and a special set associated to this D:

U 𝒟 V⟺U∘D==V∘D
𝔻=={U∈ℙ|U==U∘D}=={U∘D|U∈ℙ}

Concerning these notions we also proved earlier:

Theorem.  ℐ𝒹(𝔻)≅𝒟≅(𝒟->𝒫)≅(𝒟×𝒟)≅(𝒟->𝒟)

Before turning to showing how these properties lead us to a new model of λ-calculus, we need to consider how continuous functions behave on 𝔻.

Suppose Φ((Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])) is a continuous operator of n-variables.

Φ is said to be 𝔻-continuous provided that
Φ((Subscript[U, 0]),(Subscript[U, 1]),…,(Subscript[U, n-1]))∈𝔻 whenever (Subscript[U, 0]),(Subscript[U, 1]),…,(Subscript[U, n-1])∈𝔻.

A very broad class of operators is 𝔻-continuous:

Theorem.  The operator λ X. Φ((Subscript[U, 0])[X],(Subscript[U, 1])[X],…,(Subscript[U, n-1])[X]) is always 𝔻-continuous.

Proof. It will be sufficient to consider just two variables and to show:
			λ X. Φ(U[X],V[X])∈𝔻 whenever U,V∈𝔻.

Assume we have U,V∈𝔻. We then calculate:
		(λ X. Φ(U[X],V[X]))∘D
		==λ X. Φ(U[D[X]],V[D[X]])
		==λ X. Φ(U∘D[X],V∘D[X])
		==λ X. Φ(U[X],V[X])∈𝔻.

Q.E.D.

We can conclude at once from this result that many operators have the desired continuity property.

Pairing, application and abstraction

Theorem.  The following operators are 𝔻-continuous:
		((U,V))==λ X. ⌊U[X],V[X]⌋,
		𝟙𝕤𝕥(W)==λ X. 1st[W[X]], and
		𝟚𝕟𝕕(W)==λ X. 2nd[W[X]].

Note.  Everything here has been written as operators rather than as combinators in ℙ.

Recall that ℙ×ℙ==ℙ.  Properties of the underlying pairing can now be lifted from ℙ to 𝔻.  The proofs should be obvious.  (Why?)

Theorem.  For U,V,W∈𝔻 we have:
		𝟙𝕤𝕥(((U,V)))==U,
		𝟚𝕟𝕕(((U,V)))==V, and
		((𝟙𝕤𝕥(W),𝟚𝕟𝕕(W)))==W.

Note.  Any continuous operator Φ((Subscript[U, 0]),(Subscript[U, 1]),…,(Subscript[U, n-1])) can be made into a 𝔻-continuous one by changing it to Φ((Subscript[U, 0]),(Subscript[U, 1]),…,(Subscript[U, n-1]))∘D.  This cheap trick does not necessarily mean that the new operator has interesting properties, however.  We need to use the device in the next two definitions, nevertheless.
Take note of a special property of the elements of 𝔻.

Theorem.  If U∈𝔻, then U==λ X. U[X].

Proof. Under the assumption we find:
		 λ X. U[X]
==λX.(U∘D)[X]
==λ X. U[D[X]]
==U∘D==U
Q.E.D.

We can now give the two basic definitions of the new λ-calculus.  And read the strange symbol £ as "fancy λ" to distinguish it from the ordinary λ we have used for ℙ.  We have do this work since it is not the case that 𝔻 is closed under the ordinary application operator F[U].  (Why?)

F[[U]]==(λ V. F[((U,V))])∘D
£ U. Φ(U,(Subscript[V, 0]),(Subscript[V, 1]),…)==(λ W. Φ(𝟙𝕤𝕥(W), (Subscript[V, 0]),(Subscript[V, 1]),…)[𝟚𝕟𝕕(W)])∘D

Note.  The D in the above equations can be brought inside.  For example, the first equation could have been written as: F[[U]]==λ V. F[((U,D[V]))].
Note, too, it does not matter which variable we use in defining £ U.  (Why?)

The conversion rules

Our first main task is to verify that 𝔻 models β-conversion under these definitions.

Note.  In the next theorem we write Φ(U) instead of Φ(U,(Subscript[V, 0]),(Subscript[V, 1]),…) just to save space and to save writing in the  formulae.  The longer form is what is intended, however.

Theorem.  Assuming that Φ(U) is 𝔻-continuous and W∈𝔻, we have
			(£ U. Φ(U))[[W]]==Φ(W).

Proof. We have to compute using the definitions:

(£ U. Φ(U))[[W]]
== (λ V. (£ U. Φ(U))[((W,V))])∘D
==(λ V. ((λ Z. Φ(𝟙𝕤𝕥(Z))[𝟚𝕟𝕕(Z)])∘D )[((W,V))])∘D
==(λ V. ((λ Z. Φ(𝟙𝕤𝕥(D[Z]))[𝟚𝕟𝕕(D[Z])]) )[((W,D[V]))])
==λ V. Φ(𝟙𝕤𝕥(D[((W,D[V]))]))[𝟚𝕟𝕕(D[((W,D[V]))])]
==λ V. Φ(𝟙𝕤𝕥(((W,D[V]))))[𝟚𝕟𝕕(((W,D[V])))]
==λ V. Φ(W)[D[V]]
==(λ V. Φ(W)[V])∘D
==Φ(W)∘D
==Φ(W)
Q.E.D.

Our next main task is to verify that 𝔻 models η-conversion under our definitions.

Theorem.  Assuming that F∈𝔻, we have £ U. F[[U]]==F.

Proof. We have to compute using the definitions:

£ U. F[[U]]
==(λ W. F[[𝟙𝕤𝕥(W)]][𝟚𝕟𝕕(W)])∘D 
==(λ W.((λ V. F[((𝟙𝕤𝕥(W),V))])∘D)[𝟚𝕟𝕕(W)])∘D
==(λ W.(λ V. F[((𝟙𝕤𝕥(W),D[V]))])[𝟚𝕟𝕕(W)])∘D
==(λ W. F[((𝟙𝕤𝕥(W),D[𝟚𝕟𝕕(W)]))])∘D
==λ W. F[((𝟙𝕤𝕥(D[W]),D[𝟚𝕟𝕕(D[W])]))]
==λ W. F[((𝟙𝕤𝕥(D[W]),𝟚𝕟𝕕(D[W])))]
==λ W. F[D[W]]
==F∘D
==F

Q.E.D.

Our next main task is to verify that 𝔻 models γ-conversion under our definitions.

Theorem.  Assuming that U,V,W∈𝔻, we have ((U,V))[[W]]==((U[[W]],V[[W]])).

Proof. We have to compute using the definitions:

((U,V))[[W]]
==(λ Z. ((U,V))[((W,Z))])∘D
==(λ Z. ⌊U[((W,Z))],V[((W,Z))]⌋)∘D
==λ Z. ⌊U[((W,D[Z]))],V[((W,D[Z]))]⌋
==λ Z. ⌊U[[W]][D[Z]],V[[W]][D[Z]]⌋
==(λ Z. ⌊U[[W]][Z],V[[W]][Z]⌋)∘D
==((U[[W]],V[[W]]))∘D
==((U[[W]],V[[W]]))

Q.E.D.

As a direct consequence of this theorem we can prove another tidy equation.

Theorem.  Assuming that Φ(U) and Ψ(U) are 𝔻-continuous, we have:
		£ U. ((Φ(U),Ψ(U)))==((£ U. Φ(U),£ U. Ψ(U))).

Proof. We have these equations:
		((£ U. Φ(U),£ U. Ψ(U)))
==£ V. ((£ U. Φ(U),£ U. Ψ(U)))[[V]]
==£ V. (((£ U. Φ(U))[[V]],(£ U. Ψ(U))[[V]]))
==£ V. ((Φ(V),Ψ(V)))
==£ U. ((Φ(U),Ψ(U)))

Q.E.D.

Here is another useful theorem following a definition.

U • V==£ Z. U[[V[[Z]]]]

Theorem.  Assuming that U,V,W∈𝔻, we have ((U,V)) • W==((U • W,V • W)).

Proof. We have these equations:
		((U,V)) • W
==£ Z. ((U,V)) [[W[[Z]]]]
==£ Z. ((U [[W[[Z]]]],V [[W[[Z]]]]))
==((£ Z. U [[W[[Z]]]],£ Z. V [[W[[Z]]]]))
==((U • W,V • W))

Q.E.D.

Bibliographical Notes.  The (λβγ)-calculus was introduced and discussed in the book Lambda-Calculus, Combinators, and Functional Programming by G.E. Revesz, x + 188 pp., Cambridge University Press, 1988, ISBN 0-521-34589-8.  The book discusses LISP and other list-processing ideas, including the language FP of John Backus described most fully in his article Can programming be liberated from the von Neumann style? A functional style and its algebra of programs, pp. 63–130 in 1966 to 1985: ACM Turing Award Lectures, The First Twenty Years, xviii + 483 pp., ACM Press and Addison-Wesley Publishing Co., 1987, ISBN 0-201-07794-9.  The model presented here is a simplified form of that worked out as a M.Sc. Thesis by Glenn Durfee in a Carnegie-Mellon Techincal Report, A model for a list-oriented extension of the lambda calculus, 29 pp., CMU-CS-97-151, May 1997.

Lattice-theoretic properties

The model 𝔻 has many properties under inclusion (⊆) similar to those of ℙ.  We note without proof, for example, that K[∅] is the smallest element of 𝔻, while K[ℕ]==ℕ is the largest.  (Why?)

Theorem.  Assuming that U,V∈𝔻, then U⋃V∈𝔻.

Proof. We have these equations:
		U⋃V
==(U∘D)⋃(V∘D)
==(λ X. U[D[X]])⋃(λ X. V[D[X]])
==λ X. (U[D[X]]⋃V[D[X]])
==λ X. (U⋃V)[D[X]]
==(U⋃V)∘D

Q.E.D.

Note.  This theorem can easily be generalized to infinite unions.  Hence, 𝔻-continuous operators have their least fixed points in 𝔻.  The author has not checked whether the so-called paradoxical combinator defined in terms of £-abstraction and [[]]-application gives the expected least fixed point.  It seems reasonable to conjecture that it does.

Theorem.  Assuming that U,V∈𝔻, then U⋂V∈𝔻.

Proof. We have these equations:
		U⋂V
==λ X. U[X]⋂λ X. V[X] 
==λ X. (U[X]⋂V[X])
==λ X. (U[D[X]]⋂V[D[X]])
==(λ X. (U[X]⋂V[X]))∘D
But that is enough to give the conclusion.  (Why?)  Q.E.D.

Theorem.  Assuming that Φ(U) and Ψ(U) are 𝔻-continuous, we have:
		£ U. Φ(U)⊆£ U. Ψ(U)⟺∀U∈𝔻. Φ(U)⊆Ψ(U).

Proof. We have these equivalences:
		∀U∈𝔻. Φ(U)⊆Ψ(U)
⟺∀U∈𝔻. ∀X∈ℙ. Φ(U)[X]⊆Ψ(U)[X]
⟺∀U∈𝔻. ∀X∈ℙ. Φ(U)[D[X]]⊆Ψ(U)[D[X]]
⟺∀U∈𝔻. ∀V∈𝔻. Φ(U)[V]⊆Ψ(U)[V]
⟺∀W∈𝔻.  Φ(𝟙𝕤𝕥(W))[𝟚𝕟𝕕(W)]⊆Ψ(𝟙𝕤𝕥(W))[𝟚𝕟𝕕(W)]
⟺∀W.  Φ(𝟙𝕤𝕥(D[W]))[𝟚𝕟𝕕(D[W])]⊆Ψ(𝟙𝕤𝕥(D[W]))[𝟚𝕟𝕕(D[W])]
⟺λW.  Φ(𝟙𝕤𝕥(D[W]))[𝟚𝕟𝕕(D[W])]⊆λW.Ψ(𝟙𝕤𝕥(D[W]))[𝟚𝕟𝕕(D[W])]
⟺(λW.  Φ(𝟙𝕤𝕥(W))[𝟚𝕟𝕕(W)])∘D⊆(λW.Ψ(𝟙𝕤𝕥(W))[𝟚𝕟𝕕(W)])∘D
⟺£ U. Φ(U)⊆£ U. Ψ(U)

Q.E.D.