CS263–Spring 2008
Topic 2: Type Theory
Section 6.1: Type 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 23 February 2008

A set-theoretic interpretation of types (Review)

Type constructs

Given types 𝒜 and ℬ, the type (𝒜->ℬ) is the PER defined as follows:
U (𝒜->ℬ) V if, and only if, whenever X 𝒜 Y holds, then U[X] ℬ V[Y] holds.

The definition of (𝒜->ℬ) is one way of making new types out of old, and there are a multitude of other ways of doing so.  In this section we present five important ones.

The first is by intersection.

U (𝒜⋂ℬ) V if, and only if, both U 𝒜 V and U ℬ V.

Theorem.  If 𝒜 and ℬ are PERs, then so is 𝒜⋂ℬ.

In fact, the intersection of any family of PERs is again a PER, as is easily proved.

It is not the case that the union of PERs is necessarily a PER.  The example of the two Pers {{0},{1}}×{{0},{1}} and {{1},{2}}×{{1},{2}} show this.  (Why?)  What is needed is to add something to a union.

U (𝒜⊎ℬ) V if, and only if, ∃ Z∈ℙ, n∈ℕ. such that Z[0]==U and Z[n]==V and 
∀i<n. either  Z[i] 𝒜 Z[i+1] or Z[i] ℬ Z[i+1].

Theorem.  If 𝒜 and ℬ are PERs, then so is 𝒜⊎ℬ.

We could say that 𝒜⊎ℬ is the PER that is generated by the union 𝒜⋃ℬ.  It is also the least PER containing the union.  (Why?)

There are situations when the union of PERs is again a PER, however.  We formulate two.

Theorem.  If two PERs 𝒜 and ℬ are such that 𝒜⋂ℬ==∅, then 𝒜⋃ℬ is again a PER.

Theorem.  If a sequence of PERs is such that (Subscript[𝒜, 0])⊆(Subscript[𝒜, 1])⊆…⊆(Subscript[𝒜, i])⊆… , then the union  (⋃_(i==0)^∞)(Subscript[𝒜, i]) is again a PER.

The next definition expands the idea of a cartesian product from sets to PERs.

U (𝒜×ℬ) V if, and only if, both 1st[U] 𝒜 1st[V] and 2nd[U] ℬ 2nd[V].

We need to remember here that under our interpretation of ordered pairs of sets in ℙ, every set is at the same time a pair: U==⌊1st [U],2 nd[ U]⌋.  So we could have written this definition equivalently as follows:

⌊(Subscript[U, 0]),(Subscript[U, 1])⌋ (𝒜×ℬ) ⌊(Subscript[V, 0]),(Subscript[V, 1])⌋, and only if, both (Subscript[U, 0]) 𝒜 (Subscript[V, 0]) and (Subscript[U, 1]) ℬ (Subscript[V, 1]).

Theorem.  If 𝒜 and ℬ are PERs, then so is 𝒜×ℬ.

Warning.  Do not confuse 𝒜×ℬ  and 𝒜⋂ℬ.  (Why?)

The idea of making a disjoint sum (sometimes called coproduct) is to make disjoint copies of 𝒜 and of ℬ and then take a union.

U (𝒜+ℬ) V if, and only if, either 1st[U]==1st[V]==0 and 2nd[U] 𝒜 2nd[V] or
 1st[U]==1st[V]==1 and 2nd[U] ℬ 2nd[V]

Again, there is another way of writing this definition:

⌊(Subscript[U, 0]),(Subscript[U, 1])⌋ (𝒜+ℬ) ⌊(Subscript[V, 0]),(Subscript[V, 1])⌋ if, and only if, either (Subscript[U, 0])==(Subscript[V, 0])==0 and (Subscript[U, 1]) 𝒜 (Subscript[V, 1]) or
 (Subscript[U, 0])==(Subscript[V, 0])==1 and (Subscript[U, 1]) ℬ (Subscript[V, 1])

Theorem.  If 𝒜 and ℬ are PERs, then so is 𝒜+ℬ.

We can also relate the sum to the product via a union:

Theorem.  𝒜+ℬ==(ℐ𝒹({0}}×𝒜)⋃(ℐ𝒹({1}}×ℬ)

Note also these equations :

Corollary.   ℐ𝒹({0}}×𝒜==𝒜+∅ and ℐ𝒹({1}}×ℬ==∅+ℬ.

The last construct to be defined now is called lifting.

(Subscript[𝒜, ^])==(𝒜+∅)⋃^

The need for this construct will be clear later in discussing partial functions.

There are many, many relationships between types that can be explained in terms of mappings.  That will be the subject of the next lecture.

Relating types

Isomorphism

Many types represent the same structure.  For example, types such as ℐ𝒹({n}) and ℐ𝒹({m}) are both types of a single, isolated element, and it makes little difference whether we call it n==0 or m==1001or some other integer.  The two types give us the same kind of structure and are isomorphic.  Similarly, ℐ𝒹({0,1}) and ℐ𝒹({13,666}) are isomorphic.

Here is the formal definition:

Two types 𝒜 and ℬ are said to be isomorphic provided that
there are U and V with U∶𝒜->ℬ and V∶ℬ->𝒜 such that
V∘U(𝒜->𝒜)λ X. X and U∘V(ℬ->ℬ)λ X. X.
We notate this relationship as 𝒜≅ℬ.

Note.  A stronger condition is being recursively isomorphic.  This adds the extra condition that both U and V are  in ℝ𝔼.  We shall find many examples where this stronger relationship holds because so many basic operators are computable.

The conditions on U and V for giving an isomorphism could also have been stated as:
                            ∀ X∶𝒜 . V[U[X]] 𝒜 X and ∀ Y∶ℬ . U [V [Y]] ℬ Y.
(Why?)

Theorem.  Isomorphism (and, likewise, recursive isomorphism) is an equivalence relation among types.

Proof.  (1) Inasmuch as λ X. X (𝒜->𝒜) λ X. X, then 𝒜≅𝒜 follows.

(2) If we have 𝒜≅ℬ using U and V as in the definition, then we have ℬ≅𝒜 using V and U.

(3) Suppose 𝒜≅ℬ using U and V,  and ℬ≅𝒞 using S and T.  Then we can show that 𝒜≅𝒞 by using S∘U and V∘T.  (Why?)  Q.E.D.

Note.  In formulating these conditions, some authors prefer the more algebraic notation using these abbreviations: 𝟙==λ X.X and (Subscript[𝟙, 𝒜])==λ X∶𝒜. X.

Theorem.  For A∈ℙ and 𝔸⊆ℙ, we have ^≅ℐ𝒹({A})≅𝔸×𝔸≅(𝔸×𝔸)->(𝔸×𝔸).

We also note that isomorphisms compose under some of our type constructs:

Theorem.  For PERs (Subscript[𝒜, 0])≅(Subscript[𝒜, 1]) and (Subscript[ℬ, 0])≅(Subscript[ℬ, 1]), we have
			(Subscript[𝒜, 0])->(Subscript[ℬ, 0])≅(Subscript[𝒜, 1])->(Subscript[ℬ, 1]),
			(Subscript[𝒜, 0])× (Subscript[ℬ, 0])≅(Subscript[𝒜, 1]) ×(Subscript[ℬ, 1]),
			(Subscript[𝒜, 0])+(Subscript[ℬ, 0])≅(Subscript[𝒜, 1])+(Subscript[ℬ, 1]), and
			       (Subscript[(Subscript[𝒜, 0]), ^])≅(Subscript[(Subscript[𝒜, 1]), ^]).

Question.  What about ⋂ and ⊎?

Order-theoretic properties

Note.  On pp. 116–118 of "An Introduction to Lambda Calculi for Computer Scientists" by Chris Hankin, a number of properties of intersection types are mentioned.  We shall now verify the corresponding properties using our definitions.

Clearly ⊆ is a partial ordering, and we have no need of discussing the obvious properties of that relation in connection with  ⋂ .  There are also similar properties for ⊎.

Keep in mind that we also have two extreme types ∅ and ℙ==ℙ×ℙ, so that for all types 𝒜 we have ∅⊆𝒜⊆ℙ.  And ℙ is a very silly type making all things equivalent.  Hence, we can say both that ℙ==ℙ->ℙ and ℙ≅ℐ𝒹({0}).  (Why?)  Those are the uninteresting order-theoretic properties.  Here are more interesting ones:

Theorem.   For types 𝒜 , ℬ, and 𝒞 we have 
                                 (𝒜->𝒞)⋂(ℬ->𝒞)⊆((𝒜⋂ℬ)->𝒞), and                          
                                 (𝒜->(ℬ⋂𝒞))==(𝒜->ℬ)⋂(𝒜->𝒞).

The proofs are very easy from the definitions.

Warning.  The reason that the first relationship is not an equality is that we might have (𝒜⋂ℬ)==∅ thereby making ((𝒜⋂ℬ)->𝒞) too large!

In the cases of the other constructs, we find some monotonicity.  But one case is special.

Theorem.   If we have types 𝒜⊆ℬ, and 𝒞⊆𝒟, then we have 
                                           (𝒜+𝒞)⊆(ℬ+𝒟),                                                                      
                                           (𝒜×𝒞)⊆(ℬ×𝒟), 
                                                  (Subscript[𝒜, ^])⊆(Subscript[ℬ, ^]), and
                                          (ℬ->𝒞)⊆(𝒜->𝒟).

Warning.  In the case of the mapping-space construct there is a reversal of order.  (Why?)