CS263–Spring 2008
Topic 2: Type Theory
Section 5.1: Type Semantics I

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

A set-theoretic interpretation of types

Restricting abstraction

When we introduced λ-abstraction in the models, it was pointed out that if Φ is a continuous operator, then λ X. Φ(X) is the largest set U∈ℙ such that U[X]==Φ(X) for all X∈ℙ.  If we had known there was at least one set representing Φ this way, then we could have used this as the definition, bytaking a union.  Then we could have proved:  λX. Φ(X)[Y]==Φ(Y) .

But an explicit formula was given that not only gave one such U but also was the largest.

Note. To emphasize the above remark, suppose that U[X]⊆Φ(X) for all X∈ℙ.  Then we showed that U⊆λ X. U[X]⊆λ X.Φ(X).   So λ X.Φ(X) is indeed the largest representative.

In turning next to a discussion of types, it will helpful to represent functions on subsets of ℙ — but with values in ℙ.  An important example is ℕ⊆ℙ (and remember we take n=={n} for n∈ℕ).  But, we will also consider smaller sets 𝕄⊆ℕ⊆ℙ.

By definition we take λ n∈𝕄. (Subscript[X, n]) to be the largest set U⊆ℕ such that
U[n]⊆(Subscript[X, n]) holds for all n∈𝕄.

Phrased this way, there certainly are such U because U==∅ is a trivial choice.  But, why is there a largest?

The answer is to take the union of all the U satisfying the displayed condition above.  One of the Projects was to prove that under our definition of U[X] we have
		                          ⋃{U[Y]|U∈𝕌}==(⋃𝕌)[Y]
for any family of sets 𝕌⊆ℙ and any Y∈ℙ.  That justifies the definition.  (Why?)

Theorem.  For any given system of sets (Subscript[X, n]) for n∈𝕄, we have (λ n∈𝕄. (Subscript[X, n]))[m]==(Subscript[X, m]) for all m∈𝕄.

Proof. Take, with an m given, as one of the sets in the union: U=={(⟨m⟩,k)|k∈(Subscript[X, m])}.  Clearly, U[m]==(Subscript[X, m]),while, for n≠m, we have U[m]==∅. Q.E.D.

Note.  When n∈ℕ∖𝕄, because the λ-abstract is taken as maximal, we will have: 
			(λ n∈𝕄. (Subscript[X, n]))[m]==ℕ, the largest set in ℙ.

A special case we need to use often is 𝕄=={0,1,…,n-1}.  We introduce an abbreviation:

⟨⟨(Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])⟩⟩==λ i<n . (Subscript[X, i])

In other words, though we had n-tuples of elements of ℕ before, we also have to have n-tuples of elements of ℙ.  They work out a little differently, however.  In ℕ, we find ⟨i,j⟩≠⟨i,j,k⟩; but in ℙ, 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]),ℕ,ℕ,…⟩⟩.
Moreover, ⟨⟨(Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])⟩⟩[i]==(Subscript[X, i]), if i<n; but ⟨⟨(Subscript[X, 0]),(Subscript[X, 1]),…,(Subscript[X, n-1])⟩⟩[i]==ℕ, if i≥n.

Warning.  There are many different ways of introducing ordered pairs into ℙ.

In order to make a later task easier, we give one more definition of pairs.

⌊X,Y⌋==2 X⋃2 Y+1 for X, Y∈ℙ
1st==λ Z.{n|2 n∈Z}
2 nd==λ Z.{n|2 n+1∈Z}

The idea here in defining ⌊X,Y⌋ is to put a copy of X on the even integers and a copy of Y on the odd integers.   Clearly we are working with continuous and computable operators here and the key formulae about pairing are easy to prove:

Theorem.  For all X, Y, Z∈ℙ we have:
	1st[⌊X,Y⌋]==X;
	2 nd[⌊X,Y⌋]==Y; and
	⌊1st [Z],2 nd[ Z]⌋==Z.

We defined at least two notions of cartesian product for sets in ℙ.  Now we use this pairing just defined for taking the products of subclasses of ℙ.

𝕌×𝕍=={⌊X,Y⌋|X∈𝕌& Y∈𝕍} for 𝕌,𝕍⊆ℙ

Note.  Under this definition it follows that ℙ×ℙ==ℙ.  (Why?)

Types as equivalences

The semantics for types we will be using is based on a kind of equivalence relations.

A partial equivalence relation or PER is a binary relation
ℛ⊆ℙ×ℙ
which is symmetric and transitive; that is, the implications
X ℛ Y=>Y ℛ X and X ℛ Y& Y ℛ Z=>X ℛ Z
hold for all X, Y, Z∈ℙ.
And, in the above, we use this familiar shorthand:
X ℛ Y⇔ ⌊X, Y⌋∈ℛ

It is important to keep in mind that we are not assuming that reflexivity X ℛ X holds for all X∈ℙ.  Thus, the subset of ℙ given by {X|X ℛ X} is being used a "preliminary" subtype of ℙ.  However, keep in mind that the whole type is the relation ℛ.

For X∈ℙ and ℛ a PER, we write X∶ℛ to mean X ℛ X.
And we read X∶ℛ as X is of type ℛ.

When X ℛ Y we have, however, to think of X and Y as equivalent representatives of objects of type ℛ.  In other words, the same object may have many representations.

Warning.  Mathematicians often insist on having uniquely determined objects by introducing equivalence classes and quotient sets.  One notation for this is as follows:

For X∶ℛ, define X/ℛ=={Y∈ℙ|X ℛ Y}. Then
ℙ/ℛ=={X/ℛ|X∶ℛ}.

This is sometimes convenient, but we will not make much use of the idea here.

Of course, every subclass of ℚ⊆ℙ can be thought of as a type by defining:

X ℐ𝒹(ℚ) Y⇔X==Y∈ℚ

But, as we will find from examples, these may not be the most interesting types.

We note that ℐ𝒹(∅)==∅.  But a slightly more interesting PER will often use is this one:

^==ℐ𝒹({∅})

The difference between ℐ𝒹(∅) and ℐ𝒹({∅}) is that ℐ𝒹(∅) being empty, there is no way to map into it.  On the other hand ∅∶ℐ𝒹({∅}), and so many operations map into this type — e.g., K[∅] ought to be a good candidate.

Type mappings

There is a very great variety of types — even among the PERs.  To be able to explore them, we define a number of ways of constructing new types from old.

The prime reason we want to single out a specific kinds of type in this way is to have a guaranteed structure on our data.

Warning.  From now on we will often say type instead of PER.

When, given two types 𝒜 and ℬ, we write U∶𝒜->ℬ to mean that U represents an operator mapping objects of type 𝒜 to objects of type ℬ, we want to be sure that whenever X∶𝒜 we will know that U(X)∶ℬ and that U[X] is not just some random element of ℙ.  More, actually, is required of operators, because types allow equivalent representations of objects.

By definition, U∶𝒜->ℬ means that
whenever X 𝒜 Y holds, then U[X] ℬ U[Y] holds.
We can read U∶𝒜->ℬ as saying: 
U is a mapping from 𝒜 to ℬ, or
U maps 𝒜 to ℬ

Already, there are some very easy theorems to prove:

Theorem.  For any type 𝒜, it is true that λ X. X∶𝒜->𝒜.

Theorem.  For types 𝒜 and ℬ, if B∶ℬ, then K[B]==λ X. B∶𝒜->ℬ.

Theorem.   For types 𝒜 , ℬ, and 𝒞, if U∶𝒜->ℬ and V∶ℬ->𝒞, then 
		λ X. V[U[X]]∶𝒜->𝒞.

We need to use the composition of mappings so often we will write:
(V∘U)==λ X. V[U[X]].

Note.  The notation (V∘U) is preferred, because it is more readable than using a combinator!

Also clear is that a type with just one element picks out just one element of a type under a mapping.  A typical one-element type is the type ^==ℐ𝒹({∅}).

Theorem.  For any B∈ℙ and any type ℬ, we have B∶ℬ if, and only if, there is a mapping U∶^->ℬ such that U[∅]==B.

We remark that the empty type ℐ𝒹(∅)==∅ has an extreme property.

Theorem.  For any U∈ℙ and any type ℬ, we have U∶ℐ𝒹(∅)->ℬ.

Now, we have been writing U∶𝒜->ℬ as if this were a type statement.  Is it possible that 𝒜->ℬ can be considered as being a type in itself made up from 𝒜 and ℬ?  The answer is YES!

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.

This means, roughly speaking,  that U and V — as operators — do equivalent things in ℬ to equivalent things in 𝒜.

Note.  Under this definition that U∶𝒜->ℬ does mean the same as U (𝒜->ℬ) U.

We should, however, verify the following statement.

Theorem.  Under the definition, (𝒜->ℬ) is a PER, provided 𝒜 and ℬ are.

The proof is easy.

Warning.  By the way, (ℐ𝒹(∅)->ℬ)==ℙ.  (Why?)

We should also relate restricted abstraction to the unrestricted version.

Theorem.  For types 𝒜 and ℬ, if λ X. U[X]∶𝒜->ℬ, then 
                                      λ X∶𝒜. U[X](𝒜->ℬ)λ X. U[X].

Proof.  Suppose S 𝒜 T.  Then U[S] ℬ U[T].

We have S∶𝒜.  (Why?)  Therefore, (λ X∶𝒜. U[X])[S]==U[S].

Of course, (λ X. U[X])[T]==U[T].

Hence, (λ X∶𝒜. U[X])[S](𝒜->ℬ)(λ X. U[X])[T}.  Q.E.D.

We should also generalize an earlier theorem.

Theorem.  If types 𝒜, ℬ, and 𝒞 are such there are mappings where
 (Subscript[U, 0])(𝒜->ℬ)(Subscript[U, 1]) and (Subscript[V, 0])(ℬ->𝒞)(Subscript[V, 1]) , then we have (Subscript[V, 0])∘(Subscript[U, 0])(𝒜->𝒞)(Subscript[V, 1])∘(Subscript[U, 1]).

Type constructs

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