Semantics of System F

Paul Taylor

June 1988

This is Appendix A to Proofs and Types by Jean-Yves Girard, translated and with appendices by Yves Lafont and myself, published by Cambridge University Press, 1988.

In this appendix we shall give a semantics for system F in terms of coherence spaces. In particular we shall interpret universal abstraction by means of a kind of “trace”, showing that the primary and secondary equations hold. We shall examine the way in which its terms are “uniform” over all types. Finally we shall attempt to calculate some universal types such as Emp = ΠX. X, Sgl = ΠX. X → X, Bool = ΠX. X → X → X and Int = ΠX. X → (X → X) → X.

1 Terms of universal type

1.1 Finite approximation

We have already said in section 11.2 that a term ΛX. t of universal type ΠX. T is intended to be a function which assigns to any type U a term t[U/X] of type T [U/X]. In particular, the interpretation of ΛX. λx. x is to be the function which assigns to any coherence space A (the trace of) the identity function, i.e.

Id^{A} = {({α}, α) : α ∈ |A|}

But we have a problem of size: there is a proper class of coherence spaces, so how can this be a legitimate function?

We can solve this problem in the same way as we did for functions, by requiring that every domain be expressible as a “limit” of finite domains. Then by continuity we can derive the value of a universal term at an arbitrary domain from its values at finite domains. Since there are only countably many finite domains up to isomorphism, the function is defined by a set — so long as we ensure that its values at isomorphic domains are equal (along the isomorphisms).

1.2 Saturated domains

There is a common but misleading alternative solution. We choose a “big” domain Ω which is saturated under all the relevant operations on types, and restrict our notion of domain A to “subdomains” of Ω. Thus for instance if A is such a subdomain then we require A → A to be one also; in particular Ω → Ω is one. Then the identity, being an element of Ω → Ω, which is identified with a subspace of Ω, is an element of Ω. Scott’s Pω model [Scott76] is a well-known example of this approach, and [Koymans] examined this in detail as a notion of model of the untyped lambda calculus^{1}.

However, besides the fact that not all domains are represented, this approach has several pitfalls.

1As an exercise, the reader is invited to construct a countable coherence space into which any other can be rigidly embedded (3.1).

• Whereas in set theory the notions of element and type are confused, here we have to distinguish between Ω as the “universe of elements” and some domain V whose elements may serve as names of types — a “universe of types”.

• It is not good enough to construct such a V with the property that every domain be named by a point of V: this is like the “by values” interpretation of recursive functions. We need that every variable domain be named by a term (with the same free variables) of type V. The obvious choice is the category of domains and embeddings, but this is not one of our domains. It is, however, possible to “cover” it with a domain, although the techniques required for this, which are set out in [Tay86], §5.6, are much more difficult than the construction of Ω.

• Isomorphic types may be represented by different elements of V, and there is nothing to force the values of universal terms at such elements to be equal. This means that the condition at the end of 1.1 for finite approximation is violated, there are far more points of universal types than corresponding terms in the syntax, and the interpretation of simple terms such as ΛX. λx. x is very uneconomical.

• It is possible to model system F, and more generally the Theory of Constructions, using the category of embeddings for V, as has been done in [CGW87] and [HylPit], but Jung has shown that this is not possible for all categories of domains in current use.

What really fails in the third remark is the “uniformity” of terms over all types.

1.3 Uniformity

It is as a result of “uniformity” that the model we present has its remarkably economical form. We shall have to treat this in detail relative to “subspaces”, but first consider the consequences of requiring a construction on a type to be uniform with respect to all isomorphisms of the type with itself, i.e. permutations. Taking common geometrical notions, the construction must be the centre of a sphere, the axis of a cone, and so on. A subgroup of a group which is (setwise) invariant under automorphisms is called characteristic. The more automorphisms there are, the more highly constrained a “uniform” construction has to be. Generally, something is uniform if it is “peculiar”

— described by some property which it alone satisfies. In our case we want it to be definable by a term of the syntax (cf. section 11.2), and in the last section of this appendix we shall examine to what extent this is true.

We obtain power from this condition by manufacturing automorphisms to order. One very crude construction suffices: we take the sum of a domain with itself (either lifted or amalgamated on some subdomain), which obviously has a “left-right” symmetry. (We shall say what we mean by a subdomain in the next section.) Given a subspace inclusion A ⊂ B, a “uniform” element of B +_{A} B cannot be in either the left or the right parts of the sum — it has to be in the common subspace A. This is the conundrum of the donkey which starves to death because it cannot choose between two equally inviting piles of hay, equidistant to its left and right.

There is a similar property (separability) for fields which underlies Galois Theory: given a subfield inclusion K ⊂ L, there is a bigger field L ⊂ M such that the automorphisms of M fixing K (pointwise) fix only K. For fields, M is the normal closure — a more complex construction than our B +_{A} B.

Uniformity with respect to automorphisms is a feature of any functorial theory, including Scott’s. However for such theories we only have a subuniformity with respect to subdomains: the value of a universal term at A need only be less than that at B (where A ⊂ B). It is the stability condition which puts the above separability property to use: A is the intersection of the two copies of B in B +_{A} B, and so by stability the value of the universal term at it must be equal to (the intersection of) the projection(s) of its value(s) at B. Hence the coherence space model is uniform.

We make this vague argument precise in A.4.1.

2 Rigid Embeddings

In order to make sense of the idea of “finite approximation” we have to formalise the notion of subdomain or approximation of domains.

The idea used in Scott’s domain theory is that of an embedding-projection pair, e : A ↣ B and p : B −▷ A, satisfying^{2} 1_{A} = pe and ep ≤ 1_{B}. The latter composite is idempotent and is called a coclosure on B.

We may use these functions to define when an element a of A is “less than” an element b of B (but not vice versa), namely if a ≤ pb in A, or equivalently ea ≤ b in B^{3}.

For coherence spaces we shall use the same idea, except that e now has to be stable (p is already) and the inequality ep ≤_{B} 1_{B} must hold in the Berry order. Now e is linear and identifies A with a down-closed subset of B; it also preserves and reflects atoms and the coherence relation. Consequently we may represent it by its restriction to the web, which is a graph embedding. This justifies the abuse of notation eα for the unique token β such that e{α} = {β}, and so enables us to regard e as a function between webs.

The traces of e and p are

\begin{matrix}Tr(e) = & \{⟨\{α\}, eα⟩ : α ∈ |A|\} \\ Tr(p) = & \{⟨\{eα\}, α⟩ : α ∈ |A|\} \end{matrix}

We shall often write e : A → B as e^{+} and p : B → A as e^{−} for a graph embedding e : |A| ↣ |B|.

For pedagogical purposes it is often easier to see a 1–1 function (such as a rigid embedding) as an isomorphism followed by an inclusion: the isomorphism changes the name of the datum to its value in the target and the inclusion is that of the set of represented values. In our case we may do this with either points a ∈ A or tokens α ∈ |A|.

Observe then that for inclusions the embedding is just the identity and the projection is the restriction:

e(a) = a p(b) = b ∩ |A|

2.1 Functoriality of arrow

The reason for using pairs of maps for approximations is that we need to make the functionspace functorial (positive) in its first argument: if A′ approximates A then we need A′ → B to approximate A → B and not vice versa.

Indeed if e : A′ ↣ A and f : B′ ↣ B then we have e → f : (A′ → B′) ↣ (A → B) by

\begin{aligned}(e → f)^{+}(t′)(a) & = f^{+}(t′(e^{−}a)) \\ (e → f)^{−}(t)(a′) & = f^{−}(t(e^{+}a′)) \end{aligned}

for a ∈ A, a′ ∈ A′, t : A → B and t′ : A′ → B′. (We leave the reader to check the inequalities.)

Recall that the tokens of A → B are of the form (a, β) where a is a clique (finite coherent subset) of |A| and β is a token of |B|. If e : |A′| ↣ |A| and f : |B′| ↣ |B| are rigid embeddings then the effect on the token (a′, β′) of A′ → B′ is simply the corresponding renaming throughout, i.e. (e^{+}a′, fβ′).

2There are reasons for weakening this to 1_{A} ≤ pe. We may consider that a domain is a better approximation than another if it can express more data, and this gives rise to an embedding. However we may also consider that a domain is inferior if its representation makes “a priori” distinctions between things which subsequently turn out to be the same, and such a comparison is of this more general form. On the other hand the limit-colimit coincidence and other important constructions such as Π and Σ types remain valid. However for rigid adjunctions 1_{A} = pe is forced because the identity is maximal in the Berry order.

3In fact ≤ is not a partial order but a category, because it depends on e. Applying this to a functor T , we obtain a category with objects the pairs (A, b) for b ∈ T (A) and morphisms given in this way by embeddings; this is called the total category or Grothendieck fibration of T and is written Σ ∘ X. T .

In particular the token ({α′}, α′) of Id^{A′} is mapped to ({eα′}, eα′), so the identity is uniform in the sense that

Id^{A′} = Id^{A} ∩ |A′ → A′|

where A′ ↣ A is a subspace.

Coherence spaces and rigid embeddings — or equivalently Graphs and embeddings — form a category Gem, and we have shown that → is a covariant functor of two arguments from Gem, Gem to Gem.

3 Interpretation of Types

We can use this to express any type T of F with n free type variables X_{1}, ..., X_{n} as a functor [[T]] : Gem^{n} → Gem as follows:

1. If T is a constant type then we assign to it a coherence space T and

[[T]](A_{1}, ..., A_{n}) = T

Any morphism is mapped to the identity on T .

2. If T is the variable X_{i} then the functor is the ith projection

[[X_{i}]](A_{1}, ..., A_{n}) = A_{i}

and similarly on morphisms.

3. If T is U → V, and U and V have been interpreted by the functors [[U]] and [[V]] then

[[U → V]](A_{1}, ..., A_{n}) = [[U]](A_{1}, ..., A_{n}) → [[V]](A_{1}, ..., A_{n})

Its value on morphisms is as given at the end of the previous section.

This definition respects substitution of types U_{1}, ..., U_{n} for the variables X_{1}, ..., X_{n}: [[T [U_{i}/X_{i}]]] = [[T]]([[U_{1}]], ..., [[U_{n}]]).

Because of functoriality, we immediately know that if A′ ≃ A then [[T]](A′) ≃ [[T]](A). It is convenient to assume for pedagogical reasons that if A′ ⊂ A is a subspace then the induced embedding [[T]](A′) ↣ [[T]](A) is also a subspace inclusion.

3.1 Tokens for universal types

The interpretation is continuous: if β ∈ |[[T]](A)| then there is a finite subspace A′ ↣ A such that β ∈ |[[T]](A′)|. (Categorically, we would say that the functor preserves filtered colimits.) This means that, as in section 1.1, we may restrict attention to finite coherence spaces. For an arbitrary coherence space A,

|[[T]](A)| = ⋃^{↑}{|[[T]](A′)| : A′ ↣ A finite}

But more than this, it is stable:

if A′, A′′ ⊂ A and β ∈ |[[T]](A′)|, |[[T]](A′′)| then β ∈ |[[T]](A′ ∩ A′′)|

i.e. the functor preserves pullbacks^{4}. For a stable function, if we know β ∈ f(a), then there is a least a′ ⊂ a such that β ∈ f(a′). We have a similar^{5} property here: if β ∈ |[[T]](A)| then there is a least subspace A′ ↣ A with β ∈ |[[T]](A′)|.

4As with continuity of →, this follows from a limit-colimit coincidence: for a pullback of rigid embeddings, the corresponding projections form a pushout, and if this occurs on the left of an → it is turned back into a pullback of embeddings. This does not, however, hold for equalisers.

The token β of [[T]](A) therefore intrinsically carries with it a particular finite subspace A′ ⊂ A, namely the least subspace on which it can be defined. It is not difficult to see that, in terms of the web, this is simply the set of tokens α which occur in the expression for β. Thus for instance the only token occurring in β = ({α}, α) is α, and the corresponding finite space is Sgl, whose web is a singleton, {•}.

We shall see later that the pairs ⟨A, β⟩, where β ∈ |[[T]](A)| and no proper A′ ↣ A has β ∈ |[[T]](A′)|, serve as (potential) tokens for [[ΠX. T]]. If A ≃ A′ then the token ⟨A′, β′⟩, where β′ is the image of β under the induced isomorphism [[T]](A) ≃ [[T]](A′), is equivalent to ⟨A, β⟩. These tokens involve pairs, finite (enumerated) sets and finite graphs, and so there are at most countably many of them altogether; consequently it will be possible to denote any type of F by a countable coherence space.

We may calculate |[[T]](A)| from these tokens as follows. For every embedding e : A′ ↣ A and every token β ∈ |[[T]](A′)|, we have a token [[T]](e)(β) ∈ |[[T]](A)|. However the fact that there may be several such embeddings (and hence several copies of the token, which must be coherent) gives rise to additional (uniformity) conditions on the tokens of |[[ΠX. T]]|. For instance we shall see that ⟨Sgl, •⟩ is not a token for [[ΠX. X]].

3.2 Linear notation for tokens

We can use the linear logic introduced in chapter 12 to choose a good notation for the tokens β and express the conditions on them. Recall that

A → B ≃ !A ⊸ B ≃ (!A ⊗ B^{⊥})^{⊥}

where

• The tokens of !A are the cliques (finite complete subgraphs) of |A|, and two cliques are coherent iff their union is a clique; we write cliques as enumerated sets.

• B^{⊥} is the linear negation of B, whose web is the complementary graph to that of B; it is convenient to write its tokens as \overline{β}. Then \overline{β} ⌢ ⌣ \overline{β′} iff β ⌣ ⌢ β′; this avoids saying “mod B” or “mod B^{⊥}”.

• |C ⊗ D| is the graph product of |C| and |D|; its tokens are pairs ⟨γ, δ⟩ and this is coherent with ⟨γ′, δ′⟩ iff γ ⌢ ⌣ γ′ and δ ⌢ ⌣ δ′.

The token of the identity, ΛX. λx^{X}. x, is therefore written

⟨Sgl, \overline{⟨\{•\}, \overline{•}⟩}⟩

In this notation it is easy to see how we can ascribe a meaning to the phrase “α occurs positively (or negatively) in β”. Informally, a particular occurrence is positive or negative according as it is over-lined evenly or oddly.

We can obtain a very useful criterion for whether a potential token can actually occur.

Lemma Let α ∈ |A| and β ∈ |[[T]](A)|. Define a coherence space A^{+} by adjoining an additional token α′ to |A| which bears the same coherence relation to the other tokens (besides α) as does α, and is coherent with α. There are two rigid embeddings A ↣ A^{+} (in which α is taken to respectively α and α′), so write β, β′ ∈ |A|^{+} for the images of β under these embeddings. Similarly we have A ↣ A^{−}, in which α′ ⌣ ⌢ α. Then

• if α does not occur in β then β = β′ in both [[T]](A^{+}) and [[T]](A^{−}).

5The argument by analogy is in some ways misleading, because even for a continuous functor T the fibration Σ ∘ X. T → Gem is stable.

• if α occurs positively but not negatively then β ⌢ ⌣ β′ in [[T]](A^{+}) and β ⌣ ⌢ β′ in [[T]](A^{−}).

• if it occurs negatively but not positively then the reverse holds.

Proof Induction on the type T.

We shall see that uniformity of the universal term ΛX. t forces e_{1}β and e_{2}β to be both present in (and hence coherent) or both absent from |[[t]](A)|, where ⟨A′, β⟩ is a token for T and e_{1}, e_{2} : A′ ↣ A are two embeddings. In fact ⟨A′, β⟩ is a token iff this holds. From this we have the simple

Corollary If ⟨A, β⟩ is a token of [[ΠX. T]] and α ∈ |A| then α occurs both positively and negatively in β.

The corollary is not a sufficient condition on ⟨A, β⟩ for it to be a token of [[ΠX. T]], but it is very a useful criterion to determine some simple universal types.

3.3 The three simplest types

Any token for X → X is of the form ⟨A, \overline{⟨a, \overline{α}⟩}⟩, in which only the token α appears positively, so a = {α}. Hence the only token for this type is the one given, and [[ΠX. X →X]] ≃ Sgl. This means that the only uniform functions of type X → X are the identity and the undefined function.

The case of T = X is even simpler. No token of A can appear negatively, and so there is no token at all: [[ΠX. X]] ≃ Emp has the empty web and only the totally undefined term, ∅. The reason for this is that if a term is defined uniformly for all types then it must be coherent with any term; since there are incoherent terms this must be trivial.

It is clear that no model of F of a domain-theoretic nature can exclude the undefined function, simply because ∅ is semantically definable. For higher types this leads to the same logical complexities as in section 8.2.2.

Unfortunately, even accepting partiality, coherence spaces do not behave as we might wish. The tokens for the interpretation of

Bool = ΠX. X → X → X

are of the form ⟨Sgl, \overline{⟨a, ⟨b, \overline{•}⟩⟩}⟩ such that a ∪ b = \{•\}. This admits not two but three (incoherent) solutions:

⟨Sgl, \overline{⟨\{•\}, ⟨∅, \overline{•}⟩⟩}⟩ ⟨Sgl, \overline{⟨\{•\}, ⟨\{•\}, \overline{•}⟩⟩}⟩ ⟨Sgl, \overline{⟨∅, ⟨\{•\}, \overline{•}⟩⟩}⟩

of which the first and last represent t and f.

The middle one is intersection. Although it is not definable in System F, it may be thought of as the program which reads two streams of tokens and outputs those common to both of them. It is a uniform linear function X ⊗ X ⊸ X, whereas t and f are linear X & X ⊸ X because they only use one of their arguments. Consequently we may eliminate intersection by considering the “linear booleans”

ΠX. X & X ⊸ X

Semantically, this bilinear function is just binary intersection, which is uniformly definable in our domains because they are boundedly complete (have joins of sets of points which are bounded above). One might imagine, therefore, that it would cease to be definable if we extended our class of domains to include Jung’s “L-domains”, in which for every point a ∈ A the set ↓ a =^{def} {a′ : a′ ≤ a} is a complete lattice. Unfortunately, like the Hydra the “intersection” function just becomes more complicated: we can define m(a, b) to be the join in ↓ a of the set {c : c ≤ a, c ≤ b}. So long as we only consider domains for which in the lattices ↓ a binary meet distributes over arbitrary joins, m : A ⊗ A ⊸ A is bilinear and uniform in the sense we have defined. By iterating it, we would obtain infinitely many additional points of ΠX. X→X→X — except that it’s worse than this, because the original size problems recur and we can no longer even form polymorphic types in the semantics!^{6}

4 Interpretation of terms

Having sketched the notation we shall now interpret terms and give the formal semantics of F using coherence spaces.

Recall that a type T with n free type variables X_{1}, ..., X_{n} is interpreted by a stable functor [[T]] : Gem^{n} → Gem. Let t be a term of type T with free variables x_{1}, ..., x_{m} of types U_{1}, ..., U_{m}, where the free variables of the U are included among the X. Then t likewise assigns to every ntuple A in Gem^{n} and every m-tuple b_{j} ∈ [[U_{j}]](A) a point c ∈ [[T]](A). Of course the function b ↦ c must be stable, and we may simplify matters by replacing t by λx. t and T by U_{1} → ... → U_{m} → T to make m = 0. We must consider what happens when we vary the A_{i}.

4.1 Variable coherence spaces

Let T : Gem → Gem be any stable functor and τ(A) ∈ T (A) a choice of points. Let e : A′ ↣ A be a rigid embedding; we want to make τ “monotone” with respect to it. We can use the idea from section 3.1 to do this: we want

τ(A′) ≤ T (e)^{−}(τ(A))

which becomes, when the embeddings are subspace inclusions,

τ(A′) ⊂ τ(A) ∩ |T (A′)|

We shall use the separability property to show that stability forces equality here. The following is due to Eugenio Moggi.

Lemma Let e : A′ ↣ A be a rigid embedding. Let A +_{A′} A be the coherence space whose web consists of two incoherent copies of |A| with the subgraphs |A′| identified. Then A has two canonical rigid embeddings into A +_{A′} A and their intersection is A′.

What does it mean for τ to be a stable function from Gem? We have not given the codomain^{7}, but we can still work out intersections using the definition of a ≤ b as a ≤ e^{−}b for e : A ↣ B. Write A_{1} and A_{2} for the two copies of A inside A +_{A′} A, whose intersection is A′.

Using the “projection” form of the inequality, ⟨A′′, β⟩ is in the intersection iff

A′′ ⊂ A_{1} ∩ A_{2}
β ∈ τ(A_{1}) ∩ |T (A′′)| = τ(A) ∩ |T (A′′)|
β ∈ τ(A_{2}) ∩ |T (A′′)| = τ(A) ∩ |T (A′′)|

The intersection of the values at A_{1} and A_{2} is therefore just

τ(A) ∩ |T (A′)|

By stability this must be the value at A′. This proves the

Proposition Let τ be an object of the variable coherence space T (X_{1}, ..., X_{n}), and e_{i} : A′_{i} ↣ A_{i} be rigid embeddings. Then^{8}

τ(A′) = τ(A) ∩ |T (A′)|

and indeed if τ satisfies this condition then it is stable.

6These two hitherto unpublished observations have been made by the author of this appendix since the original edition of this book.

7It is the total category Σ ∘ X. T (X) which we met in section 3.1.

8Note that this equality only holds for type variables and not for dependency over ordinary domains.

4.2 Coherence of tokens

In fact the lemma tells us slightly more. B = A +_{A′} A has an automorphism e exchanging the two copies of A. This must fix τ(B), so if β ∈ Tr(τ(B)) then also eβ is in this trace and consequently must be coherent with β. So,

Lemma Let β ∈ |T (A)| and e_{1}, e_{2} : A ↣ B be two embeddings. Then e_{1}β ⌢ ⌣ e_{2}β in B.

The converse holds:

Lemma Let β ∈ |T (A)| be such that (i) A is minimal for β and (ii) β has coherent images under any pair of embeddings of A into another domain. Then there is an object τ_{⟨A,β⟩} of type T whose value at T (B) is

{T (e)(β) : e : A ↣ B}

and moreover this is atomic, i.e. has no nontrivial subobject.

To test this condition we only need to consider graphs up to twice the size of |A|, and so it is a finite^{9} calculation to determine whether ⟨A, β⟩ satisfies it. For any given type these tokens are recursively enumerable. Because τ_{⟨A,β⟩} is atomic, we must have just one token for ΠX. T (X), so ⟨A, β⟩ and ⟨A′, β′⟩ are identified for any e : A ≃ A′ with eβ = β′.

We still have to say when these tokens are coherent.

Lemma Let β_{1} ∈ |T (A_{1})| and β_{2} ∈ |T (A_{2})| each satisfy these conditions. Then τ_{⟨A_{1},β_{1}⟩}(B) ⌢ ⌣ τ_{⟨A_{2},β_{2}⟩}(B) at every coherence space B iff for every pair of embeddings e_{1} : A_{1} ↣ C, e_{2} : A_{2} ↣ C, we have T (e_{1})(β) ⌢ ⌣ T (e_{2})(β).

Finally this enables us to calculate the universal abstraction of any variable coherence space.

Proposition Let T : Gem → Gem be a stable functor. Then its universal abstraction, ΠX. T (X), is the coherence space whose tokens are equivalence classes of pairs ⟨A, β⟩ such that

• β ∈ |T (A)|

• A is minimal for this, i.e. if A′ ⊂ A and β ∈ |T (A′)| then A′ = A (so A is finite).

• for any two rigid embeddings e_{1}, e_{2} : A ↣ B, we have

T (e_{1})(β) ⌢ ⌣ T (e_{2})(β)

in T (B).

• ⟨A, β⟩ is identified with ⟨A′, β′⟩ iff e : A ≃ A′ and T (e)(β) = β′ (so |A| may be taken to be a subset of IN).

• ⟨A, β⟩ is coherent with ⟨A′, β′⟩ iff for every pair of embeddings e : A ↣ B and e′ : A′ ↣ B we have T (e)(β) ⌢ ⌣ T (e′)(β′).

Proof ΠX. T (X) is a coherence space because if any ⟨A, β⟩ occurs in a point then so does the whole of τ_{⟨A,β⟩}, and any coherent union of these gives rise to a uniform element.

One ought to prove that if T : Gem×Gem → Gem is stable then so is ΠX. T : Gem → Gem, and also check that the positive and negative criterion remains valid.

9Though it would appear to be exponential in |A|^{2}.

4.3 Interpretation of F

Let us sum up by setting out in full the coherence space semantics of F. The type U in n free variables X is interpreted as a stable functor [[U]] : Gem^{n} → Gem as in §A.3, with the additional clause

4. If U = ΠX. T then the web of [[U]](A) is given as in the preceding proposition, where T (X) = [[T]](A, X). The embedding induced by e : A′ ↣ A is takes tokens of [[U]](A′) to the corresponding tokens with α′_{i} replaced by e_{i}α′_{i}.

The term t of type T with m free variables x of types U (the free type variables of T, U being X) is interpreted as an assignment to each A of a stable function

[[t]](A) : [[U_{1}]](A) & ... & [[U_{m}]](A) → [[T]](A)

such that for e : A′ ↣ A and b_{j} ∈ [[U_{j}]](A) the uniformity equation holds:

[[T]](e)^{−}([[t]](A)(b)) = [[t]](A′)([[U]](e)^{−}(b))

In detail,

1. The variable x_{j} is interpreted by the jth product projection.

[[x_{j}]](A)(b) = b_{j}

2. The interpretation of λ-abstraction λx. u is given in terms of that of u by the trace

[[λx. u]](A)(b) = \{\overline{⟨c, \overline{δ}⟩} : δ ∈ [[u]](A)(b, c), with c minimal\}

3. The application uv is interpreted using the formula (App) of section 8.5.2:

[[uv]](A)(b) = \{δ : ∃c ⊂ [[v]](A)(b). \overline{⟨c, \overline{δ}⟩} ∈ [[u]](A)(b)\}

4. The universal abstraction, ΛX. v, is also given by a “trace”:

[[ΛX. v]](A)(b) = {[⟨C, δ⟩] : δ ∈ [[v]](A, C)(b), with C minimal}

where [⟨C, δ⟩] denotes the equivalence class: ⟨C, δ⟩ is identified with ⟨C′, δ′⟩ whenever e : C ≃ C′ and [[v]](A, e)(b)(δ) = δ′.

5. The universal application, tU, is given by an application formula

[[tU]](A)(b) = {δ : ∃e : C ↣ [[U]](A). [⟨C, δ⟩] ∈ [[t]](A)(b)}

The conversion rules are satisfied because they amount to the bijection between objects of ΠX. T (X) and variable objects of T (we need to prove a substitution lemma similar to that in section 9.2).

5 Examples

5.1 Of course

We aim to calculate the coherence space denotations of the simple types we interpreted using system F in section 11.3, which were product, sum and existential types. These are all essentially derived^{10} from ΠX. (U → X) → X, so we shall consider this in detail and simply state the other results afterwards.

The positive and negative criterion remains valid even with constants like U, and so a token for this type is of the form

⟨Sgl, \overline{⟨\{\overline{⟨u_{i}, \overline{•}⟩} : i = 1, ..., k\}, \overline{•}⟩}⟩

where u_{i} range over finite cliques of U, i.e. tokens of !U. However although there is only one token, namely \overline{•}, available to tag the u_{i}s, it may occur repeatedly; the token is therefore given by a finite (pairwise incoherent) set of tokens of !U.

In other words, denotationally,

ΠX. (U → X) → X ≃ (!((!U)^{⊥}))^{⊥} = ?!U

which (by a slight abuse) we shall call ¬¬U.

The effect of the program

⟨Sgl, \overline{⟨\{\overline{⟨u_{1}, \overline{•}⟩}, \overline{⟨u_{2}, \overline{•}⟩}\}, \overline{•}⟩}⟩

at the type A and given the stable function f : U → A is to examine the trace Tr(f) and output those tokens α for which both ⟨u_{1}, \overline{α}⟩ and ⟨u_{2}, \overline{α}⟩ lie in it. This generalises the intersection we found in [[Bool]].

It is clearly an inevitable feature of domain models of system F that ∅ be added to U, since a program of type ¬¬U is under no obligation to terminate.

What seems slightly peculiar is that we may have u_{1} ≤ u_{2}, two finite points (or cliques) of U, which give rise to atomic tokens of type ¬¬U (on some functions one will output α and the other not, and on others the reverse). This is a consequence of the stable interpretation and the Berry order, which is much weaker than the pointwise order, since the test on the function is not just whether the datum u is sufficient for output α (as it would be with Scott’s domain theory), but also whether it is necessary we have already remarked on this in section 8.5.4.

We can now easily calculate the product, sum and existential types.

ΠX. (U → V → X) → X ≃ ¬¬(U & V) ≃ ?(!U ⊗!V)

where we see ⊗ as “linear conjunction”.

ΠX. (U → X) → (V → X) → X ≃ ¬¬(U + V) ≃ ?(!U ⊕!V)

Note that (apart from the “?”) this is the kind of sum we settled on in chapter 12.

ΠY. (ΠX. (V → Y)) → Y ≃ ¬¬(Σ ∘ X. V)

where for a variable type T : Gem → Gem, Σ ∘ X. T (X) is the total category which we met in section 3.1.

5.2 Natural Numbers

Finally let us apply our techniques to calculating the denotation of

Int = ΠX. X → (X → X) → X

Recall that besides the terms of F we have already met the undefined term ⊥ and the binary intersection ∧. We shall see that linear logic arises again when we try to classify the tokens for this type.

10[[Bool]] is also a special case if we admit the two-element discrete poset (not a coherence space) for the domain U, in a category with coproducts. The other three examples which we are about to consider are derived by means of the identities U →V →X ≃ (U×V)→X, (A→X)×(B→X) ≃ (A+B)→X and ΠX. (V(X)→Y) ≃ (Σ ∘ X. V(X))→Y.

In terms of the “linear” type constructors, we must consider

(!A ⊗!((!A ⊗ A^{⊥})^{⊥}) ⊗ A^{⊥})^{⊥}

whose tokens are of the form

\overline{⟨a, ⟨\{\overline{⟨b_{i}, \overline{γ_{i}}⟩} : i = 1, ..., k\}, \overline{δ}⟩⟩}

Using the “positive and negative” criterion we must have

|A| = {δ} ∪ ⋃_{i=1}^{k} b_{i} = a ∪ {γ_{1}, ..., γ_{k}}

The simplest case is k = 0, so a = \{δ\}. This gives the numeral \overline{0}, interpreted as the program which copies the starting value to the output, ignoring the transition function. The corresponding token for Int is just

⟨Sgl, \overline{⟨\{•\}, ⟨∅, \overline{•}⟩⟩}⟩

The intersection phenomenon manifests itself (in the simplest case) as the token

⟨Sgl, \overline{⟨\{α\}, ⟨\{\overline{⟨\{α\}, \overline{α}⟩}\}, \overline{α}⟩⟩}⟩

but the similar potential token

⟨α ⌢ ⌣ β, \overline{⟨\{α\}, ⟨\{\overline{⟨\{β\}, \overline{β}⟩}\}, \overline{α}⟩⟩}⟩

(although it passes the positive and negative criterion) is not actually a valid token of this type.

It is more enlightening to turn to the syntax and find the tokens of the numeral \overline{1}. Calculating [[ΛX. λx. λy. yx]] using section 4.3, we get tokens of the form

⟨A, \overline{⟨a, ⟨\{\overline{⟨a, \overline{γ}⟩}\}, \overline{γ}⟩⟩}⟩

where |A| consists of the clique a and the token γ.

• If a = ∅ we have the program which ignores the starting value stream and everything on the transition function stream apart from the “constant” part of its value, which is copied to the output.

• If a has m elements, the program reads that part of the transition function which reads its input exactly m times, and applies this to the starting value (which it reads m times). But,

• If γ ∈ a then the program outputs only that part of the result of the transition function which is contained in the input.

• If γ ∉ a then it only outputs that part which is not contained in the input. But,

• If γ ⌢ ⌣ α, where α ranges over r of the m tokens of the clique a, then γ is only output in those cases where the input and output are coherent in this way.

So even the numeral \overline{1} is a very complex beast: it amounts to a resolution of the transition function into a “polynomial”, the mth term of which reads its input exactly m times. It further resolves the terms according to the relationship between the input and output.

Clearly these complications multiply as we consider larger numerals. Along with ∅ and intersection, do they provide a complete classification of the tokens of Int? What does Int → Int look like?

5.3 Linear numerals

We can try to bring some order to this chaos by considering a linear version of the natural numbers analogous to the linear booleans.

LInt = ΠX. X ⊸ ((X ⊸ X) → X)

(we leave one classical implication behind!) The effect of this is to replace a by {α} and b_{i} by {β_{i}}, and then the positive and negative criterion gives

|A| = {α, γ_{1}, ..., γ_{k}} = {β_{1}, ..., β_{k}, δ}

which are not necessarily distinct. Besides the undirected graph structure given by coherence, the pairing \overline{⟨β_{i}, \overline{γ_{i}}⟩} induces a “transition relation” on A.

The linear numeral \overline{k} consists of the tokens of the form

α = γ_{1}, β_{1} = γ_{2}, ..., β_{k−1} = γ_{k}, β_{k} = δ

subject only to α_{i} ⌢ ⌣ α_{j} ⟺ α_{i+1} ⌢ ⌣ α_{j+1} — so there are still quite a lot of them! More generally, the transition relation preserves coherence, reflects incoherence, and contains a path from α to δ via any given token. The reader is invited to verify this characterisation and also determine when two such tokens are coherent.

6 Total domains

Domain-theoretic interpretations, as we have said, necessarily introduce partial elements such as ∅, and in the case of coherence spaces also the “intersection” operation. However we may use a method similar to the one we used for reducibility and realisability to attempt to get rid of these.

As with the two previous cases, we allow any subset R ⊂ A to be a totality candidate for the coherence space A. Then

1. If R is a totality candidate for A and S for B then we write R→S for the set of objects f of type A→B such that a ∈ R ⇒ fa ∈ S

2. If T [X, Y] is a type with free variables X and Y and S are totality candidates for coherence spaces B then f ∈ ΠX. T [S], i.e. f is total for the coherence space [[ΠX. T]](B) if for every space A and candidate R for [[T]](A, B) we have f(A) ∈ T [R, S].

As with reducibility and realisability, no parametricity remains for closed types.

This topic is discussed more extensively in [Gir85], from which we merely quote the following results:

Proposition If t is a closed term of closed type T, then [[t]] is total.

Proposition The total objects in the denotation of Bool and Int are exactly the truth values and the numerals.

References

[CGW87] Th. Coquand, C.A. Gunter and G. Winskel, Domain-theoretic models of polymorphism, University of Cambridge Computer Laboratory technical report 116 (1987).

[Gir85] J.Y. Girard, Normal Functors, power series and lambda-calculus, Annals of Pure and Applied Logic (1986).

[GrSc] J.W. Gray and A. Scedrov (eds.), Categories in computer science and logic, American Mathematical Society (Boulder, 1987).

[HylPit] J.M.E. Hyland and A.M. Pitts, The theory of constructions: categorical semantics and topos-theoretic models, in [GrSc].

[Koymans] C.P.J. Koymans, Models of the λ-calculus, Centruum voor Wiskunde en Informatica, 9 (1984).

[Scott76] D. Scott, Data types as lattices, SIAM Journal of Computing 5 (1976).

[Tay86] P. Taylor, Recursive domains, indexed category theory and polymorphism, Ph.D. thesis (University of Cambridge, 1986).