CS263–Spring 2008
Topic 2: Type Theory
Section 6.2: Type 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 5 March 2008

Isomorphisms and higher types

A function-space question

As we recall ℙ==ℙ×ℙ and 𝒫==ℐ𝒹(ℙ) are non-isomorphic types.  (Why?)  The next question concerns (𝒫->𝒫).

Theorem.  There is a ℚ⊆ℙ such that 𝒬==ℐ𝒹 (ℚ)≅(𝒫->𝒫).

Proof.  It is true that every U∶(𝒫->𝒫).  (Why?)  But that does not mean that (𝒫->𝒫) is a trivial PER.  In fact, U (𝒫->𝒫) V means that U[X]==V[X] for all X∈ℙ.  (Why?)  But this, in turn, means that λ X. U[X]==λ X. V[X].  (Why?)  And, moreover, U (𝒫->𝒫) λ X. U[X] holds.  (Why?)

OK.  Let ℚ=={λ X. U[X]|U∈ℙ}.  Then the desired isomorphism will follow.  Q.E.D.

Theorem.  The two types 𝒫 and 𝒬 are not isomorphic.

Proof.  Suppose they were isomorphic.  We want to derive a contradiction.

Isomorphism means we have operators P∶𝒫->𝒬 and Q∶𝒬->𝒫 such that Q∘P==(Subscript[𝟙, 𝒫]) and P∘Q==(Subscript[𝟙, 𝒬]).  (Why?).  Because these operators are monotone, it would follow that for all X, Y∈ℙ, we would have 
                                         X⊆Y if, and only if, P[X]⊆P[Y].
By the same token, it would follow that for all U, V∈ℚ, we would have 
                                         U⊆V if, and only if, Q[U]⊆Q[V].
(Why?)   Note that this implies P[∅]=λ X. ∅.  (Why?)

Now in ℙ the set {0} has a very special property: for all X∈ℙ, if X⊆{0}, then either X==∅ or X=={0}.  (Why?)  It then follows that for all U∈ℚ, if U⊆P[{0}], then either U==P[∅] or U==P[{0}].  (Why?)  This means that P[{0}] has only two subsets in ℚ.  Note also that P[{0}]≠P[∅].  (Why?)  Therefore, P[{0}][ℕ]≠∅.  (Why?)  Hence, P[{0}][E]≠∅ for some finite E∈ℙ.  (Why?)  Let S==P[{0}][E].

Consider the operator W==λ X.{n∈S|E⊆X}.  Then W∈ℚ, W⊆P[{0}] and W≠P[∅].  (Why?)  Now let e∈ℕ∖E.

Consider the operator V==λ X.{n∈S|E⋃{e}⊆X}.  Then V∈ℚ, V⊆P[{0}] and V≠P[∅].  (Why?)  But V≠W.  (Why?)

Thus, we have a contradiction! (Why?)  Q.E.D.

Question.  What about 𝒬 and (𝒫->𝒬) and (𝒬->𝒫)?

Higher-type spaces

We are going to consider whether the types
    𝒫, (𝒫->𝒫), ((𝒫->𝒫)->𝒫), (((𝒫->𝒫)->𝒫)->𝒫), ((((𝒫->𝒫)->𝒫)->𝒫)->𝒫), …
naturally have some kind of "limit".  To do this, we define operators which can be used to define these types in a convenient way.

(Subscript[D, 0])==λ U. U
(Subscript[D, n+1])==λ U λ X. U[(Subscript[D, n])[X]]==λ U. (U∘(Subscript[D, n]))

U(Subscript[𝒟, n])V⟺(Subscript[D, n])[U]==(Subscript[D, n])[V]

Whatever the operator (Subscript[D, n]) is, it is clear that (Subscript[𝒟, n]) is a (total) equivalence relation.  (Why?)

Note.  We can unwind the definition of (Subscript[D, 4]) in order to understand better what these operators do.  Some changes of variables will help us follow the uses of the definitions.
	  (Subscript[D, 4])[(Subscript[U, 4])]== λ (Subscript[U, 3]). (Subscript[U, 4])[(Subscript[D, 3])[(Subscript[U, 3])]]
	==λ (Subscript[U, 3]). (Subscript[U, 4])[λ (Subscript[U, 2]). (Subscript[U, 3])[(Subscript[D, 2])[(Subscript[U, 2])]]]
	==λ (Subscript[U, 3]). (Subscript[U, 4])[λ (Subscript[U, 2]). (Subscript[U, 3])[λ (Subscript[U, 1]). (Subscript[U, 2])[(Subscript[D, 1])[(Subscript[U, 1])]]]]
	==λ (Subscript[U, 3]). (Subscript[U, 4])[λ (Subscript[U, 2]). (Subscript[U, 3])[λ (Subscript[U, 1]). (Subscript[U, 2])[λ (Subscript[U, 0]). (Subscript[U, 1])[(Subscript[D, 0])[(Subscript[U, 0])]]]]]
	==λ (Subscript[U, 3]). (Subscript[U, 4])[λ (Subscript[U, 2]). (Subscript[U, 3])[λ (Subscript[U, 1]). (Subscript[U, 2])[λ (Subscript[U, 0]). (Subscript[U, 1])[(Subscript[U, 0])]]]]
Now, if we knew in general that the equation U==λ X. U[X] held, then the above expression would collapse to (Subscript[U, 4]).  But, this is not true in ℙ.  All we can conclude is (Subscript[U, 4])⊆(Subscript[D, 4])[(Subscript[U, 4])].

Theorem. The D-operators form a tower:  (Subscript[D, 0])⊆(Subscript[D, 1])⊆(Subscript[D, 2])⊆…⊆(Subscript[D, n])⊆(Subscript[D, n+1])⊆… .

Proof.  As the first inclusion means that λ U. U⊆λ U λ X. U[X], we know this is true.  So, we then proceed by induction.  Assume that (Subscript[D, n])⊆(Subscript[D, n+1]), and try to prove that (Subscript[D, n+1])⊆(Subscript[D, n+2]).

By definition (Subscript[D, n+2])==λ U. (U∘(Subscript[D, n+1])).  By the inductive assumption and monotonicity, we see that (Subscript[D, n+2])⊇λ U. (U∘(Subscript[D, n]))==(Subscript[D, n+1]).  Q.E.D.

Theorem.  For all n∈ℕ, we have (Subscript[D, n])∘(Subscript[D, n])==(Subscript[D, n]).

Proof.  Use induction.  (Subscript[D, 0])∘(Subscript[D, 0])==(Subscript[D, 0]) is obvious.  So, assume (Subscript[D, n])∘(Subscript[D, n])==(Subscript[D, n]), and try to prove (Subscript[D, n+1])∘(Subscript[D, n+1])==(Subscript[D, n+1]).

We use the definitions:           (Subscript[D, n+1])∘(Subscript[D, n+1])==λ U. (Subscript[D, n+1])[(Subscript[D, n+1])[U]]
		==λ U. (Subscript[D, n+1])[U∘(Subscript[D, n])]
		==λ U . (U∘(Subscript[D, n]))∘(Subscript[D, n])
		==λ U . U∘((Subscript[D, n])∘(Subscript[D, n]))
		==λ U . U∘(Subscript[D, n])
		==(Subscript[D, n+1])
Q.E.D.

Theorem.  For all n∈ℕ, we have (Subscript[D, n])∘(Subscript[D, n+1])==(Subscript[D, n+1])==(Subscript[D, n+1])∘(Subscript[D, n]).

Proof. Because (Subscript[D, 0])⊆(Subscript[D, n]), we can argue by monotonicity:
		(Subscript[D, n+1])==(Subscript[D, 0])∘(Subscript[D, n+1])⊆(Subscript[D, n])∘(Subscript[D, n+1])⊆(Subscript[D, n+1])∘(Subscript[D, n+1])==(Subscript[D, n+1]).
Hence, the first equation follows.  The second equation is proved similarly.  Q.E.D.

Corollary.  For all n,m∈ℕ if m≥n, we have (Subscript[D, n])∘(Subscript[D, m])==(Subscript[D, m])==(Subscript[D, m])∘(Subscript[D, n]).

Proof. This is an easy induction.  Q.E.D.

Corollary.  For all n∈ℕ, we have (Subscript[𝒟, n])⊆(Subscript[𝒟, n+1]).

Proof. Assume U (Subscript[𝒟, n]) V holds.  This means that (Subscript[D, n])[U]==(Subscript[D, n])[V].  But then:
			(Subscript[D, n+1])[(Subscript[D, n])[U]]==(Subscript[D, n+1])[(Subscript[D, n])[V]].	
Then, by our theorem, we see that
			(Subscript[D, n+1])[U]==(Subscript[D, n+1])[V].
In other words, U (Subscript[𝒟, n+1]) V holds.  Q.E.D.

We now can derive at once some limiting properties using the equations for the (Subscript[D, n])-operators and continuity.  The proofs can safely be left to the reader.

(Subscript[D, ∞])==(⋃_(n==0)^∞)(Subscript[D, n])
U(Subscript[𝒟, ∞])V⟺(Subscript[D, ∞])[U]==(Subscript[D, ∞])[V]

Theorem.  (Subscript[D, ∞])∘(Subscript[D, ∞])==(Subscript[D, ∞])==λ U. U∘(Subscript[D, ∞])

Theorem.  For all n∈ℕ, we have (Subscript[D, n])∘(Subscript[D, ∞])==(Subscript[D, ∞])∘(Subscript[D, n])==(Subscript[D, ∞]).

Corollary.  For all n∈ℕ, we have (Subscript[𝒟, n])⊆(Subscript[𝒟, ∞]).

With these 𝒟-equivalence relations, the larger the relation the fewer the distinctions.  This "decrease" in structure can be made clearer by picking out canonical representatives of each equivalence class.

(Subscript[𝔻, n])=={(Subscript[D, n])[U]|U∈ℙ}  including n==∞.

Theorem.  For all n∈ℕ⋃{∞}, we have ℐ𝒹 ((Subscript[𝔻, n]))≅(Subscript[𝒟, n]).

Proof. Take any one of these D-operators.  The corresponding 𝒟-relation is defined as: U 𝒟 V⟺D[U]==D[V].  Because D==D∘D, we see U 𝒟 D[U], for all U.  We also see that ℐ𝒹(𝔻)⊆𝒟.   The desired isomorophisms are thus D∶𝒟->ℐ𝒹(𝔻) and λ U. U∶ℐ𝒹(𝔻)->𝒟.  Q.E.D.

Warning.  While (Subscript[𝒟, n]) is a total equivalence relation, (Subscript[𝔻, n]) is just a PER.  (Why?)

Theorem.  For all n∈ℕ, we have (Subscript[𝔻, n+1])⊆(Subscript[𝔻, n]) and (Subscript[𝔻, ∞])==(⋂_(n==0)^∞)(Subscript[𝔻, n]).

Proof. The first inclusion follows from the  equation (Subscript[D, n])∘(Subscript[D, n+1])==(Subscript[D, n+1]).  That (Subscript[𝔻, ∞])⊆(Subscript[𝔻, n]), follows from the equation (Subscript[D, n])∘(Subscript[D, ∞])==(Subscript[D, ∞]).  Suppose U∈(⋂_(n==0)^∞)(Subscript[𝔻, n]).  Because (Subscript[D, ∞])==(⋃_(n==0)^∞)(Subscript[D, n]), we find that (Subscript[D, ∞])[U]==U∈(Subscript[𝔻, ∞]).  Q.E.D.

We can now establish a key connection between mapping spaces.

Theorem.  ((Subscript[𝒟, ∞])->𝒫)⊆(Subscript[𝒟, ∞])

Proof. Suppose that U ((Subscript[𝒟, ∞])->𝒫) V.  This means that, for all X and Y, if (Subscript[D, ∞])[X]==(Subscript[D, ∞])[Y], then U[X]==V[Y].  We need to show that (Subscript[D, ∞])[U]==(Subscript[D, ∞])[V].  But, the equation (Subscript[D, ∞])[(Subscript[D, ∞])[X]]==(Subscript[D, ∞])[(Subscript[D, ∞])[X]] is obviously true.  Hence, for all X, we have U[(Subscript[D, ∞])[X]]==V[(Subscript[D, ∞])[X]].  This implies λ X. U[(Subscript[D, ∞])[X]]==λ X.V[(Subscript[D, ∞])[X]].  But we know that (Subscript[D, ∞])[U]== λ X. U[(Subscript[D, ∞])[X]] and (Subscript[D, ∞])[V]== λ X. V[(Subscript[D, ∞])[X]].  Q.E.D.

Note.  It would be nice if we could prove now that (Subscript[𝒟, ∞])⊆((Subscript[𝒟, ∞])->𝒫), and, hence, (Subscript[𝒟, ∞])==((Subscript[𝒟, ∞])->𝒫).  But this is not true.  We can, however, estabilsh an isomorphism.  The problem here is that as a PER (Subscript[𝒟, ∞]) is a total equivalence relation, but ((Subscript[𝒟, ∞])->𝒫) is not.  What we can prove first is this:

Theorem.  U ((Subscript[𝒟, ∞])->𝒫) U if, and only if, λ X. U[X]==(Subscript[D, ∞])[U] .

Proof.   We have the following equivalences:

U ((Subscript[𝒟, ∞])->𝒫) U
		⟺ ∀X,Y [ (Subscript[D, ∞])[X]==(Subscript[D, ∞])[Y] ⟹ U[X]==U[Y] ]
		⟺ ∀X . U[X]== U[(Subscript[D, ∞])[X]]         (Why?)
		⟺ λ X. U[X]==λ X. U[(Subscript[D, ∞])[X]]==(Subscript[D, ∞])[U]
Q.E.D.

Note.  The right-hand side of the theorem is not true when U==λ X. X, as we showed in the last section.

Theorem.  (Subscript[𝒟, ∞])≅((Subscript[𝒟, ∞])->𝒫)

Proof.  Remember 𝟙==λ X. X.  Owing to the inclusion we did prove, it is clear that 𝟙∶((Subscript[𝒟, ∞])->𝒫)->(Subscript[𝒟, ∞]).  (Why?)

For a mapping in the other direction, we will show (Subscript[D, ∞])∶(Subscript[𝒟, ∞])->((Subscript[𝒟, ∞])->𝒫).

We note next these equations:
		(Subscript[D, ∞])[(Subscript[D, ∞])[U]]
	==(Subscript[D, ∞])[U]
	==λ X. U[(Subscript[D, ∞])[X]]
	==λ X. (Subscript[D, ∞])[U][X] .
And, by our previous theorem, (Subscript[D, ∞])[U]((Subscript[𝒟, ∞])->𝒫) (Subscript[D, ∞])[U] then holds for all U.

So, suppose U (Subscript[𝒟, ∞]) V is true.  This means that (Subscript[D, ∞])[U]==(Subscript[D, ∞])[V].  By what we just proved, (Subscript[D, ∞])[U]((Subscript[𝒟, ∞])->𝒫) (Subscript[D, ∞])[V] must hold, and so (Subscript[D, ∞]) has the right mapping property.

To show we have an isomorphism, we need to establish two facts:
	∀U∶(Subscript[𝒟, ∞]).  (Subscript[D, ∞])[U](Subscript[𝒟, ∞])U  and  ∀U∶((Subscript[𝒟, ∞])->𝒫).  (Subscript[D, ∞])[U]((Subscript[𝒟, ∞])->𝒫)U.

Inasmuch as (Subscript[D, ∞])[(Subscript[D, ∞])[U]]==(Subscript[D, ∞])[U], the first fact is clear.

To prove the second, assume that U ((Subscript[𝒟, ∞])->𝒫) U.  Next, assume (Subscript[D, ∞])[X]==(Subscript[D, ∞])[Y].  We have these equalities:
		(Subscript[D, ∞])[U][X]
	== U[(Subscript[D, ∞])[X]]
	== U[(Subscript[D, ∞])[Y]]
	== (Subscript[D, ∞])[U][Y]
	== U[Y] .
Thus,  (Subscript[D, ∞])[U]((Subscript[𝒟, ∞])->𝒫)U holds.  Q.E.D.

Theorem.  ((Subscript[𝒟, ∞])×(Subscript[𝒟, ∞]))≅(Subscript[𝒟, ∞])

Proof. We recall that ℙ×ℙ==ℙ and so 𝒫×𝒫==𝒫.  We then argue:

((Subscript[𝒟, ∞])×(Subscript[𝒟, ∞]))≅((Subscript[𝒟, ∞])->𝒫)×((Subscript[𝒟, ∞])->𝒫)
			≅((Subscript[𝒟, ∞])->(𝒫×𝒫))
			==((Subscript[𝒟, ∞])->𝒫)
			≅(Subscript[𝒟, ∞]) .	Q.E.D.

Theorem.  ((Subscript[𝒟, ∞])->(Subscript[𝒟, ∞]))≅(Subscript[𝒟, ∞])

Proof. We can now argue:
 	    ((Subscript[𝒟, ∞])->(Subscript[𝒟, ∞]))≅((Subscript[𝒟, ∞])->((Subscript[𝒟, ∞])->𝒫))
			≅(((Subscript[𝒟, ∞])×(Subscript[𝒟, ∞]))->𝒫)
			≅((Subscript[𝒟, ∞])->𝒫)
			≅(Subscript[𝒟, ∞]) .	Q.E.D.

Note.  The existence of isomorphisms ((Subscript[𝒟, ∞])->(Subscript[𝒟, ∞]))≅(Subscript[𝒟, ∞])≅((Subscript[𝒟, ∞])×(Subscript[𝒟, ∞])) can be used to show that (Subscript[𝒟, ∞]) is a model of the λη-calculus.  This will be spelled out in a later lecture.