Quantitative Domains, Groupoids and Linear Logic

Paul Taylor

1989

Abstract

We introduce the notion of a candidate for “multiple valued universal constructions” and define stable functors (which generalise functors with left adjoints) in terms of factorisation through candidates. There are many mathematical examples, including the Zariski spectrum of a ring (as shown by Diers [81]) and the Galois group of a polynomial, but we are mainly interested in Berry’s [78] minimum data property. In fact we begin with a completely nonmathematical example.

The aim is to find domain models in which terms of the typed or polymorphic λ-calculus are interpreted as stable functors. We study Girard’s quantitative domains [85], in which information is represented by a collection of tokens from a universe of tokens for a particular type, and there is no restriction on the ability of different tokens to co-exist or on the number of occurrences of a particular token. This idea may be used to code parallelism (with no suppression of duplicated output) or accounted resources.

Unfortunately Girard did not fully describe the function-spaces, which should be equipped with the “Berry order”; this turns out to mean that function-tokens must have “internal symmetries”. It is our purpose to describe the smallest cartesian closed category with these function-spaces which contains Set (the simplest non-trivial quantitative domain, with one token which may appear arbitrarily often) as an object.

The natural way of presenting this is as a new interpretation of Linear Logic given by group (and more generally groupoid) actions. These stand in the same relation to quantitative domains as coherence spaces do to qualitative domains, and there is a kind of coherence between group(oid) elements. By a similar analysis of stable functors we obtain an of course operation. Finally, our (generalised) quantitative domains themselves form a domain of this kind with rigid comparisons as morphisms, and hence we have a type of types.

Presented at Category Theory and Computer Science 3 (Manchester); published in the proceedings, edited by David Pitt, Springer-Verlag Lecture Notes in Computer Science 389 (1989) 155–181.

1 Stable Functors

1.1 The Minimum Data Property

Imagine marking examination scripts in history, the question set being

What were the causes of the Second World War?

Of course it is not our business to pass judgement on this question ourselves, but merely to imagine the process whereby the examiner awards marks for what the student has written. In programming terms, she executes a function from scripts to numbers which is defined by her mark-sheet.

This is what a typical student wrote:

The Germans invaded Poland. The Japanese invaded Manchuria. The Italian sbombed Pearl Harbor.

Marie-Antoinnette said “let them eat cake.”

He obviously gets marks for the first two assertions but not the last two: the third because it is false (or a confusion) and the last because it is irrelevant (noise).

Perhaps the examiner had the following mark-sheet:

Japanese invaded Manchuria.  10 marks
Japanese bombed PearlHarbor.  5 marks
Germans invaded Poland.  5 marks
Germans invaded Czechoslovakia. 10 marks
Italians invaded Abyssinia.  10 marks

and so she gave this student 15 marks.

Suppose our student had just written

Germans invaded Poland.

and so got 5 marks. Obviously writing less than this (i.e. omitting any of these three words) would have got him none at all, and adding comments about Marie-Antoinette, King Canute or his history teacher would only have wasted time. So these three words are the least part of the script which would gain these marks. The same is true of each of the other four lines of the marksheet. Observe that (i) although the Polish marks and those for Pearl Harbor are interchangeable for the purpose of awarding the final grade, they accumulate rather than become identified, and (ii) it’s no good trying to match half of one pattern (Pearl Harbor) with half of another (the Italians).

Now let us formalise this a bit^{1}. The marking process is a function S which takes a script X and returns a number of marks SX. Suppose that the script X includes the assertion that the Germans invaded Poland; then five marks Y = 5 are distinguishably included in the total SX, by a function w : Y → SX. (If it also included the assertion about Pearl Harbor there would be a different function w′ : Y → SX.) Let X_{∘} be the one-line script containing just this assertion, then again u : Y → SX_{∘}, and since this is a sub-script, f : X_{∘} → X. We don’t write X_{∘} ⊂ X because parts of the pattern X_{∘} might be counted twice, for instance if

X_{∘} = Germans invaded Poland. Germans invaded Czechoslovakia.

and X = The Germans invaded Poland and Czechoslovakia.

then the function is not mono on “Germans invaded”.

The minimal sub-script X_{∘} has a certain “universal property”. Suppose g : X′ → X is another sub-script which also wins these same marks, so that v : Y → SX′ and Sg ∘ v = Sf ∘ u, then X′ contained the one-line script X_{∘}, i.e. h : X_{∘} → X′ such that^{2} v = Sh ∘ u and g ∘ h = f. (h is not mono, for the same reason as f).

Let us write this definition in its general form.

Definition 1.1 Let S : X → Y be a functor. Then the map u : Y → SX_{∘} in Y is said to be a candidate for [a universal map from the object Y to the functor] S if for any triple of maps v : Y → SX′ in Y and f : X_{∘} → X and g : X′ → X in X, such that the square

1The reader with little mathematical background should concentrate on section 2 and ignore the remainder of the paper.

2This is left handed composition, contrary to my personal habits, so that later A ⊢ B will be a left action of A and a right action of B, not vice versa.

[figure: Y; u; SX_{∘}; SX′; v; Sg; SX; Sf]

commutes, there is a unique h : X_{∘} → X′ such that both triangles

[figure: Y; u; SX_{∘}; Sh; SX′; v; and; X_{∘}; h; X′; g; X; f]

commute. Note that X_{∘}, as well as u, Y and SX_{∘}, is part of the data defining the candidate. The word candidate is used to signify that this is one of many (for given Y), and derives from the special case of coproduct candidates (this term appears in [Lamarche 88]).

There are numerous mathematical^{3} examples of this idea, and we only give a few representatives; the first is typical of the special case of functors with left adjoint.

Example 1.2 Let S be the forgetful functor from X = Gp to Y = Set and Y ∈ Y. Then u : Y → SX_{∘} is a candidate iff X_{∘} is the free group on Y and u is the inclusion of generators. In this case, there is only one candidate (up to unique isomorphism) for S for given Y. □

Example 1.3 Let X = IntDom, the category of integral domains and monomorphisms, and Y = CRng, the category of commutative rings and homomorphisms. Then u : Y → SX_{∘} is a (quotient) candidate iff X_{∘} is the quotient of Y by a prime ideal; any particular ring Y may have many quotient candidates. In this case (as in the previous one) f = g ∘ h is a corollary of Sh ∘ u = v. □

Example 1.4 Let p be a polynomial with integer coefficients. Let X = Fld[p] be the category of fields in which p splits into linear factors and S be its inclusion in Y = Fld, the category of all fields (and homomorphisms). Then u : Y → SX_{∘} is a candidate iff X_{∘} is the splitting field for p over Y. In this case there is only one candidate for given Y, but it has many automorphisms; indeed they form the Galois group of p over Y. □

Example 1.5 Consider a program S consisting of several parallel processes which merge their output indiscriminantly without suppression of duplication; for instance “parallel or” would output t twice on input ⟨t, t⟩. Suppose that on input X (a bag of tokens from A) its output includes an instance Y = {j} of a token^{4} j ∈ B. This has come from a particular process, which itself has pursued a sequential execution path, involving certain “hurdles” which amount to reading and matching a pattern X_{∘} in X; moreover if X had contained only this pattern, Y would still have been output. The candidate is the function u : Y → SX_{∘} which identifies this instance of the token j in the output, but there may have been many other ways in which this or other parallel processes could have generated j, but identified by different u’s.

3All prerequisites from mainstream pure mathematics will be found in, for example, [Cohn 77] or [Lang 65].

4The reason for the convention j ∈ B will become clear in section 2.3.

1.2 Factorisation

Stable functors generalise functors with left adjoints, and can be characterised as functors which acquire adjoints whenever they are restricted to slices (down-sets or principal lower sets). The following definition is, however, the most useful.

Definition 1.6 A functor S : X → Y is stable if every map w : Y → SX factors as Sf ∘ u with u : Y → SX_{∘} a candidate and f : X_{∘} → X. By definition of candidacy, it is immediate that this factorisation is unique up to unique isomorphism.

Example 1.7 (Vickers) Let X be the category of complete Boolean algebras and frame monomorphisms and Y be the category of frames and homomorphisms, with S : X → Y the forgetful functor. Then S is stable.

Definition 1.8 A wide pullback is a diagram d : I → X (or its limit, according to context) such that I has a terminal vertex (and has a set rather than a proper class of vertices and edges). Thus ordinary (binary) pullbacks are wide pullbacks, and any cofiltered limit diagram is equivalent to a wide pullback, but equalisers, binary products and terminal objects are not.

Exercise 1.9 Show that stable functors preserve wide pullbacks and monos. □

Suppose we are given a functor S : X → Y; how might we prove that it is stable? We may consider all possible factorisations w = Sf′ ∘ u′; these form a category whose morphisms are as illustrated:

SX′  X′
[figure: u′; f′]
Y  X
[figure: u′′; f′′]
[figure: SX′′; Sh; X′′; h]

Clearly the factorisation is through a candidate iff the corresponding object of this category is initial. We know that stable functors must preserve wide pullbacks, and the idea of the converse is to take the wide pullback of all possible factorisations. The problem is that we are only allowed to do this with a set of them, and so we need the following:

Definition 1.10 S : X → Y satisfies the solution set condition if for every w : Y → SX the (possibly large) category of factorisations has a small full cofinal subcategory. This means that for any given factorisation Sf′′ ∘ u′′ there is a factorisation Sf′ ∘ u′ in the subcategory and a morphism h with Sh ∘ u′ = u′′ and f′′ ∘ h = f′, and that between any two factorisations in the subcategory there is only a set of morphisms h.

There are important examples where this condition fails, but in the cases which are of interest to us in this paper it will hold automatically (essentially because we shall be using toposes).

Theorem 1.11 Let S : X → Y be any functor, where the category X has wide pullbacks. Then the following are equivalent:

(α) S is stable, i.e. the factorisation property holds;

(β) S has a left adjoint on each slice;

(γ) S preserves wide pullbacks and satisfies the solution set condition. □

We’re going to be interested in stable functors in this paper, but we want to assume something else of them (and will modify the terminology accordingly).

Definition 1.12 A functor is continuous if it preserves filtered colimits.

Definition 1.13 An object X ∈ X is finitely presentable if the functor Hom_{X} (X, −) : X → Set is continuous. This means that if we have f : X → colim^{↑} Y^{(r)} then for some (non-unique) r_{∘} and g : X → Y^{(r_{∘})} we have f = ν^{(r_{∘})} ∘ g, where ν^{(r_{∘})} : Y^{(r_{∘})} → colim^{↑} Y^{(r)} belongs to the colimiting cocone. The corresponding property for lattices is called compactness.

The following exercise serves as a good test of the reader’s understanding of the important concepts of candidates, continuity and finite presentability, although it doesn’t use stability.

Exercise 1.14 Suppose u : Y → SX_{∘} is a candidate, where S is continuous, and Y is finitely presentable. Then X_{∘} is also finitely presentable. □

1.3 Bags and Power Series

Now we shall turn our attention to the domains of specific interest to us.

Definition 1.15 Let A be a set. A bag of elements of A is an assignment of an abstract set X_{i} (its multiplicity) to each element i ∈ A. Abstractly, a bag is represented by a multiplicity function X_{−} : A → Set or by a display x : X = (⋃_{i∈A} X_{i}) → A. Hence a finite bag may be written as an unordered list (with repetition) whose terms are from A.

Definition 1.16 Set^{A} denotes the category of bags of elements of A. There are three ways of seeing its morphisms: (α) as an A-indexed family of functions f_{i} : X_{i} → Y_{i}; (β) as a natural transformation f : X_{−} → Y_{−} between functors A ⇉ Set, or (γ) as functions f : X → Y such that y ∘ f = x.

Exercise 1.17 Show that a bag is finitely presentable (Definition 1.2.9) iff it is finite, i.e. all elements of A have finite multiplicity and all but finitely many of them have zero multiplicity. The notation n⃗ will be used for a finite bag, where n_{i} is the multiplicity of i ∈ A. □

Girard’s quantitative domains were the categories of the form Set^{A}; we shall begin by investigating stable functors between these, but will find that more complicated categories are needed for functor-spaces.

Lemma 1.18 Let n⃗ be a finite bag. The representable functor

(−)n⃗ : Set^{A} → Set by X ↦ Set^{A}(n⃗, X) = ∏_{i}(X_{i})^{n_{i}}

(which acts on morphisms by composition) is stable and continuous. Proof Continuity is immediate from the Exercise, and actually there is a left adjoint. I claim that u : Y → (X_{∘})n⃗ is a candidate iff its exponential transpose^{5} e : Y ×n⃗ → X_{∘} is an isomorphism. For in

Y \overline{\begin{matrix}u = ⌜e⌝ \\  \end{matrix}}(n⃗)n⃗

[figure: h ∘ −]

[figure: (X′)n⃗; v = ⌜h ∘ e⌝; g ∘ −; (X)n⃗; f ∘ −]

5Actually Y × n⃗ is a copower, i.e. Y -fold coproduct, not a product.

it is clear that h exists and is uniquely determined by v iff e is invertible. The factorisation of w : Y → Xn⃗ is (f ∘ −) ∘ u where u = ⌜id⌝ and f is the exponential transpose of w. □

Girard’s power-series expansion amounts to a sum of representable functors (“monomials”), so we have to show that we can compute sums pointwise. For coherence spaces this is not possible (directly resulting in the non-representability of parallel or) and so we have to make crucial use of the idea that quantitative domains admit arbitrary sums without suppression of duplication. Categorically, this amounts to the following two properties:

Proposition 1.19 Sums in Set^{A} are disjoint and universal.

[figure: 0; X^{(r′)}; X^{(r′′)}; ν^{(r′′)}; ∑_{r} X^{(r)}; ν^{(r′)}; Y^{(r_{∘})}; X^{(r_{∘})}; Y; f; ∑_{r} X^{(r)}; ν^{(r_{∘})}]

Disjoint means that when we form the intersection of different inclusions (r′ ≠ r′′) we get the initial object 0. Universal means that when we form the pullback of the coproduct diagram against an arbitrary map f, we get another coproduct diagram: Y ≅ ∑_{r} Y^{(r)}. In the special case of the empty coproduct (the initial object) this is equivalent to strictness, i.e. any map Y → 0 is an isomorphism. □

We defer to section 1.5 the proof that we may compute sums pointwise, and merely state that any bag (cn⃗) of finite bags gives rise to a stable functor:

SX = ∑_{n⃗} cn⃗ × Xn⃗

Now we shall prove the converse: every stable functor Set^{A} → Set is (isomorphic to one) of this form. The following lemma will be the source of the complication (creeds) which we shall meet later.

Lemma 1.20 Let S : Set^{A} → Set be a continuous stable functor and u : 1 → Sn⃗ be a candidate. Suppose that h : n⃗ → n⃗ in Set^{A} is such that Sh ∘ u = u. Then h = id. Proof The notation n⃗ is justified because we know that it is finite. Let X = A be the bag in which each element of A occurs just once (so X_{i} = 1); there is a unique map f : n⃗ → X in Set^{A}, i.e. X is the terminal object. Then Sf ∘ u = Sf ∘ u, so there is a unique h : n⃗ → n⃗ in Set^{A} with Sh ∘ u = u and f ∘ h = f; clearly both the given h and also the identity will do, so by uniqueness h = id. □

Theorem 1.21 Every stable functor Set^{A} → Set is a power-series. Proof For each [isomorphism class of] finite bag n⃗, let cn⃗ be the set of equivalence classes of candidates u : 1 → Sn⃗, where we identify u with Sh ∘ u for automorphisms h : n⃗ ≅ n⃗. If w ∈ SX, then this is a map w : 1 → SX, which factorises as Sf ∘ u, and isomorphic factorisations belong to the same equivalence class; hence w corresponds to a unique element of cn⃗ together with a function f ∈ Xn⃗. □

Girard proved this result on the additional assumption that stable functors are to preserve equalisers; but by Lemma 1.3.6 this assumption is actually a consequence of having a terminal object. However Lamarche has shown (privately) that evaluation does not preserve equalisers, and so this stronger notion of stability does not lead to a cartesian closed category. We shall in fact see that for higher types there is no terminal object, and so this lemma breaks down.

Exercise 1.22 Let S : X → Y be a stable functor between categories with equalisers. Show that S preserves equalisers iff Lemma 1.3.6 holds, i.e. for every candidate u : Y → SX and automorphism h : X ≅ X, we have Sh ∘ u = u ⇒ h = id.

In this case, commutativity of the second triangle in Definition 1.1.1 is automatic, and we are reduced to Diers’ original definition of diagonal universality (candidacy); cf. Example 1.1.3.

The power-series expansion was really as far as Girard developed this topic. We shall proceed by insisting on the notion of stable functor, but one may alternatively take the point of view that the power-series is itself the essential feature. This is the subject of work in progress by Lamarche [89] on polynomial algebras, which is also the idea behind [Joyal 87].

1.4 Cartesian Transformations

Morphisms between bags (in the category Set^{A}) are “colour-preserving” (1.3.2γ) functions X → Y, i.e. the set X_{i} of elements of kind i is taken to the set Y_{i}. Although the copies of i are regarded as being alike, we nevertheless consider as different functions which affect them differently; in particular the “switch” function on the bag {•, •} is not the same as the identity.

With this in mind we look for the morphisms of the stable function-space, which we call

[X → Y]

If S, T : Set^{A} ⇉ Set^{B} are two stable functors, for each A-bag X there are B-bags SX and T X, and a morphism ϕ : S → T (in particular) gives functions ϕX : SX → T X. In the special case where A = B = 1 and S = T = (−)^{2}, the identity and switch functions (−)^{2} → (−)^{2} are regarded as being different.

Recall that stable functors preserve (wide) pullbacks. Since we’re aiming to describe a cartesian closed category, we need in particular that the evaluation functor ev : [X → Y]×X → Y be stable. There is a particular pullback square which it must preserve, for any given morphisms ϕ : S → T in [X → Y] and f : X′ → X in X, namely

⟨S, X′⟩ \overline{\begin{matrix}⟨ϕ, id⟩ \\  \end{matrix}}⟨T, X′⟩

[figure: ⟨S, X⟩; ⟨id, f⟩; ⟨ϕ, id⟩; ⟨T, X⟩; ⟨id, f⟩]

[figure: SX′; ϕX′; T X′; SX; Sf; ϕX; T X; T f]

giving the square on the right. This leads to the

Definition 1.23 A cartesian transformation ϕ : S → T is an assignment of a function ϕX : SX → T X in Y to each X ∈ X making the right-hand square above a pullback for each f : X′ → X. If the square merely commutes for each f, we say ϕ is natural.

Our main concern is to investigate the relationship between cartesian transformations and functions between bags of finite bags. This relationship is a close one, but it is not as direct as Girard would have us believe, as the following example shows:

Example 1.24 The squaring functor (−)^{2} : Set → Set is stable, being represented by the singleton bag {⌜2⌝}. The identity and switch functions (−)^{2} → (−)^{2} are distinct cartesian transformations from this functor to itself, whereas a singleton bag has only one endofunction (the identity). □

This shows that the token n⃗ which stands for the representable functor has “internal structure” which we must take into account. This becomes relevant when we consider higher-order functions. For instance, in a large public examination, many examiners must be employed to mark the scripts, and so there must be an “examiner of examiners” (moderator) to ensure fairness. The moderator would observe the behaviour of the examiners on typical scripts (say on the minimal ones we discussed). Instead of searching for particular words in scripts, the moderator would test for the inclination of the examiner to award marks for particular phrases. This has two important consequences.

First, the stable order is capable of detecting lazy behaviour, i.e. when the process outputs without reading its input. For instance there may be “free marks” awarded to all candidates irrespective of performance; one marker may award these marks automatically, even to students who failed to return scripts, whilst another may require to see a (blank) sheet of paper before giving the marks. The moderator, of course, will detect this behaviour. Phrasing this more computationally, the stable order can detect that a process has read its input, whilst the pointwise order can only detect that it has not.

Second, although this is not something we can see in the examples given, there are “internal symmetries” of tokens at higher order. A first order function may be searching for two occurrences of a (zero-order) token x in its input; its output will then be the square of the number of occurrences (this is a representable functor). Multiples of this functor are also stable, but the functor “\frac{1}{2}X^{2}” (which returns the set^{6} of unordered pairs, or two-element bags) is not (by Lemma 1.3.6). However if we test this functor, we can look for occurrences of the pattern “match x^{(1)}, x^{(2)}”, which is isomorphic to the pattern “match x^{(2)}, x^{(1)}”, and we are permitted to count these two patterns (which necessarily occur together) as one if we wish. This illustrates that higher-order patternmatching is inherently more complicated, and may help the reader to grasp the behaviour of creeds in section 3.

Returning to candidates and cartesian transformations the correspondence is summed up abstractly by the following result:

Lemma 1.25 Let S, T : X → Y be functors and ϕ : S → T a cartesian transformation. Then u′ : Y → SX in Y is a candidate for S iff u = ϕX ∘ u′ : Y → T X is a candidate for T. Conversely, if S is stable and postcomposition with the natural transformation ϕ preserves candidates then ϕ is cartesian. Proof The following diagram was discovered independently by Lamarche (with Y atomic); we shall use it three times.

Y  \overline{u′} SX

[figure: v; t; Sh; Sf]

SX′′  \overline{Sg} SX′

T X \begin{aligned}ϕX \\ &  \end{aligned}

[figure: T h; T f]

[figure: T X′′; ϕX′′; T g; T X′; ϕX′]

We are given f, g and either t or v.

[⇒] Given v, let t mediate the pullback and define h by candidacy of u′; then it mediates for u. Conversely h determines t = Sh ∘ u′.

[⇐] Given t, put v = ϕX′′ ∘t and define h by candidacy of u, so that f = g ∘h. Then t and Sh∘u′ both mediate for the pullback. But any h which makes the diagram commute mediates for u.

6“ \frac{1}{2} ” does not mean numerical division here, but quotient by the natural action of the group of order 2.

[converse] Use stability of S to factorise one of the sides of an arbitrary commutative square as Sf ∘ u′. Define h by candidacy of u and put t = Sh ∘ u′; conversely t determines h by candidacy of u′.

In all three parts we have to use naturality of ϕ, i.e. the commutation of the square faces of the prism. □

Cartesian transformations therefore correspond to functions between sets of candidates. In the examination example, the candidates correspond to items in the mark-sheet, i.e. pairings of a minimal answer with the number of marks it gains. A cartesian transformation ϕ : S → T from one examiner S to another T is determined by a function which assigns to each line of the first mark-sheet a line of the second. In particular T gives marks for at least as many things as S does, whatever the nature of ϕ; however some of the marks which S gave might become collapsed. Thus S might end up giving fewer marks than T, unless ϕ is mono.

However although T may be more willing to award marks than S, she never awards the same marks for less information. (This is the effect of cartesianness.)

Exercise 1.26 Show that every cartesian transformation into a representable functor S → (−)n⃗ is an isomorphism, so that representables are atomic. Moreover the automorphisms of (−)n⃗ are given by composition with an automorphism of n⃗ [Hint: Yoneda]. □

Remark 1.27 Lamarche has studied the similar situation with M, the category of sets and monomorphisms, instead of Set. In this case, the representable functors, M(n⃗, −), are still atomic, but they are not the same as the powering functors (−)n⃗ = Set^{A}(n⃗, −). Indeed as functors M → M, X × X ≅ M(1, X) + M(2, X), where the first inclusion is the diagonal Δ : X = M(1, X) → X × X, which is not cartesian as a transformation between functors Set → Set. The second component consists of the (ordered) unequal pairs.

1.5 Power Series Revised

We shall now reformulate Girard’s result to give a precise characterisation of the stable functionspace [Set^{A} → Set]. First we show that we can form sums of stable functors.

Proposition 1.28 Suppose (X and) Y have disjoint universal coproducts, and let S^{(r)} : X → Y be stable functors. Then the pointwise coproduct S : X ↦ ∑_{r} S^{(r)}X is a stable functor, the inclusion ν^{(r_{∘})} : S^{(r_{∘})} → ∑_{r} S^{(r)} is cartesian and this is the coproduct in [X → Y]. Proof We use the diagram to show (a) that ν^{(r)} is cartesian, (b) how to factorise maps using (c) “sums” of candidates, and (d) that ∑_{r} S^{(r)} is the coproduct in [X → Y].

Y^{(r_{∘})}  \overline{u^{(r_{∘})}} S^{(r_{∘})}X^{(r_{∘})}

[figure]

Y = ∑_{r} Y^{(r)}  \overline{u} S^{(r_{∘})}f^{(r_{∘})}  ∑_{r} S^{(r)}( ∑_{s} X^{(s)})

[figure: S^{(r_{∘})}X′; v^{(r_{∘})}; S^{(r_{∘})}g; S^{(r_{∘})}X]

[figure: ν^{(r_{∘})}X′; ν^{(r_{∘})}X]

[figure: ∑_{r} S^{(r)}X′; v; ∑_{r} S^{(r)}g; ∑_{r} S^{(r)}X; ∑_{r} S^{(r)}[f^{(s)}]]

[figure: T X′; τX′; T g; T X; τX]

(a) Suppose ν^{(r_{∘})}X ∘ t = ∑_{r} S^{(r)}g ∘ v. Define Y^{(r)} by making the left face a pullback. Then we have Y^{(r)} → S^{(r)}X and Y^{(r)} → Y →^{t} S^{(r_{∘})}X, so this factors through the intersection, which (for r ≠ r_{∘}) is 0 by disjointness. Then Y^{(r)} ≅ 0 by strictness and Y ≅ Y^{(r_{∘})} by universality, so v^{(r_{∘})} is (essentially) the required mediator. Uniqueness is easy.

(b) Given w : Y → ∑_{r} S^{(r)}X, factorise its pullback (ν^{(r)}X)^{∗}w = S^{(r)}f^{(r)} ∘ u^{(r)} : Y^{(r)} → S^{(r)}X with u^{(r)} : Y^{(r)} → S^{(r)}X^{(r)} a candidate for S^{(r)} and f^{(r)} : X^{(r)} → X. Define v^{(r)} using cartesianness and u out of the coproduct (by universality).

(c) Using candidacy of u^{(r)} we have diagonal fill-ins h^{(r)} : S^{(r)}X^{(r)} → S^{(r)}X′ at the back, and the required fill-in is their sum h = ∑_{r} h^{(r)} at the front.

(d) Given a cocone S^{(r)} → T over the diagram, there is a unique natural mediator τ: we have to show it’s cartesian. If w : Y → ∑_{r} S^{(r)}X and Y → T X′ make the diagram commute, we find v^{(r)} by cartesianness of the cocone and v = ∑_{r} v^{(r)} as their sum, using universality of sums again. □

To explain this result in the terms of the original example, suppose S′ is the behaviour of the history examiner and S′′ that of the geography examiner. The function w : Y → S′X + S′′X means that certain specific marks were awarded in the two examinations, Y′ ⊂ Y of them in history and Y′′ ⊂ Y in geography. Only the part X′ → X of the script was actually considered worthwhile history (and this got the Y′ marks), and similarly X′′ → X in geography, so altogether X′ + X′′ → X was what earned the student the Y marks.

Exercise 1.29 Suppose X has binary coproducts and that S : X → Y and T : X → Z are stable. Show that ⟨S, T ⟩ : X → Y × Z is stable. In what sense are binary coproducts necessary? □

We can now characterise cartesian transformations between stable functors Set^{A} → Set precisely, but to describe this we have to modify the power-series representation. First we reformulate Lemma 1.3.6.

Lemma 1.30 Let S : Set^{A} → Set be a stable functor. For each finite bag n⃗, let σn⃗ be the set of candidates u : 1 → Sn⃗. This carries a locally faithful action of the group Aut(n⃗) on the left, by

h · u = Sh ∘ u

whilst the representable Xn⃗ carries an action on the right:

f · h = f ∘ h

Proof We shall discuss group actions at length in section 2. An action is locally faithful if ∀h, u.(h · u = u ⇒ h = 1): this property was shown in Lemma 1.3.6. □

Definition 1.31 Suppose the group Aut(n⃗) acts on the left of σn⃗ and the right of Xn⃗. Then we can form their tensor product, Xn⃗ ⊗_{Aut(n⃗)} σn⃗, which consists of set of pairs ⟨f, u⟩ with f ∈ Xn⃗ and u ∈ σn⃗ subject to the equivalence relation that ⟨f ∘ h^{−1}, Sh ∘ u⟩ = ⟨f, u⟩.

Theorem 1.32 Let S : Set^{A} → Set be a stable functor and σn⃗ be the set of candidates u : 1 → Sn⃗. Then

SX ≅ ∑_{n⃗} Xn⃗ ⊗_{Aut(n⃗)} σn⃗

Let T : Set^{A} → Set be another stable functor corresponding to (τn⃗). Then cartesian transformations ϕ : S → T correspond bijectively to families of functions

ϕn⃗ : σn⃗ → τn⃗

which respect the action of Aut(n⃗). Hence the stable function-space [Set^{A} → Set] is equivalent to the category of locally faithful actions of the groupoid whose components are Aut(n⃗). Proof

[≅] The proof of the isomorphism runs the same as Theorem 1.3.7, except that we have taken the quotient by the equivalence relation at a later stage. Notice we have also swapped the order of the product.

[⇒] By Lemma 1.4.3, every cartesian transformation ϕ restricts to a function on candidates which we may write as ϕn⃗ (in fact this is the restriction of the component ϕn⃗ of ϕ to the subset σn⃗ ⊂ Sn⃗). Moreover naturality of ϕ with respect to automorphisms h : n⃗ ≅ n⃗ implies that the action is respected.

[⇐] For ⟨f, u⟩ ∈ SX, so that u : 1 → Sn⃗ is a candidate and f : n⃗ → X, put ϕX⟨f, u⟩ = ⟨f, ϕn⃗(u)⟩. This is independent of the choice from the equivalence class because ϕn⃗ respects the action of Aut(n⃗). We have to show that ϕ is natural: let g : X → X_{1}; then Sg⟨f, u⟩ = ⟨g ∘ f, u⟩, so

ϕX_{1}(Sg⟨f, u⟩) = ⟨g ∘ f, ϕn⃗(u)⟩ = T g⟨f, ϕn⃗(u)⟩ = T g(ϕX⟨f, u⟩)

as required. Cartesianness then follows from the converse of Lemma 1.4.3. □

Corollary 1.33 [Set^{A} → Set] does not have a terminal object (unless A = 0). □ Clearly we must study actions of groups and groupoids in detail, replacing Girard’s set

Int(A) = Int(Set^{A})_{f}

with the groupoid whose components are Aut(n⃗) for n⃗ ∈ Int(A). Moreover these actions must, it would appear, be locally faithful. However, as this was the result of Lemma 1.3.6, which depended on the existence of a terminal object, this is invalidated (for higher types) by the Corollary, and so we have to introduce a more flexible concept (creeds).

2 Groups and Linear Logic

2.1 Group Actions and the Multiplicative Fragment

This section describes the groupoid interpretation of linear logic in an informal way. We leave the reader to work out the interpretation of the linear λ-calculus [Lafont]; this is more or less obvious, but inadequate as it involves equations between terms which are objects of categories. We shall concentrate on group theory and use the characterisation of stable functors as our correctness criterion.

Let us say a word here about cardinality. In everything we do the groups are finite, but the groupoids will be countable (but recursively enumerable): infinitely many distinct finite groups may occur, each infinitely often, and different occurrences of the same group may carry different creeds. It doesn’t really harm matters to assume that the actions are also countable, but on the other hand it doesn’t help either.

One of the virtues of category theory is that it describes not only collections of mathematical objects (and their morphisms), but also in many cases the objects themselves. In particular, a group, which is of course a set with an associative binary operation (∘), an identity and inverses^{7}, is (the morphism-set of) a category with one object in which every morphism is invertible. For purposes of calculation, the classical definition is more appropriate, but for theoretical use the abstract version simplifies matters, as we shall see. In fact we shall find it convenient to use both definitions interchangeably.

Definition 2.1 Let A be a group and X a set. A right action A on X is a function · : X ×A → X such that

x · id = x  and  x · (a ∘ b) = (x · a) · b

for all x ∈ X and a, b ∈ A. Suppose Y also carries an action of A; then a function f : X → Y respects the action of A, or is equivariant, if

f(x · a) = (fx) · a

for all x ∈ X and a ∈ A (where · on the left is the action on X and on the right is that on Y). Similarly left action.

Lemma 2.2 Right actions of A are isomorphic to left actions of A^{op} (the group with the same elements as A — written â for clarity — but the opposite composition: âb̂ = b̂a). Proof Exercise. [Hint: â · x = x · a] □

The value of the categorical definition lies in the following:

Proposition 2.3 The category of right A-actions and equivariant functions is isomorphic to the functor-category Set^{A^{op}}, whose objects are functors A^{op} → Set (presheaves on A) and whose morphisms are natural transformations. Similarly the category of left A-actions is isomorphic to Set^{A}. Proof The “single object” is taken by the functor to the set X; what’s interesting is what happens to the morphisms: they are taken to the corresponding automorphisms of the set. That naturality and equivariance are the same is an elementary (but important) exercise. □

We shall introduce a few more classical ideas about permutation actions later, but our main point is to show how we can use groups to interpret the multiplicative fragment of linear logic, i.e. that involving only ⊗, ⅋ and ^{⊥}, together with the identity (axiom) and the cut rule. In fact in this interpretation, ⊗ =⅋. The interpretation will be in some ways similar to Girard’s coherence space interpretation; in particular neither of them has any obvious direct connection with logic (“linear logic is not necessarily logic”).

7The inverses are a bit misleading as part of the exposition, and produce red herrings like A ≅ A^{op} by a ↦ â^{−1}.

In fact the strictly linear parts (i.e. this section) can be done with general categories, but when we return to stable functors in the next section, we shall need invertibility (but see Proposition 3.5.4).

The notation

A_{(1)}, A_{(2)}, ..., A_{(k)} ⊢ B_{(1)}, B_{(2)}, ..., B_{(l)}

informally means that we can deduce at least one of the conclusions B_{(j)} using some of the hypotheses A_{(i)}. Better, it means that we have a particular proof, not specified in the notation. In these non-logical interpretations, there is usually at least one “proof” for any hypotheses and conclusions, so it is really a specific “proof-object” (whatever that is) that we’re interested in.

In classical logic, the A_{(i)}’s may be permuted (the technical word is exchanged) and if two hypotheses are actually (different occurrences of) the same formula we may identify them (contraction). This means that the string A_{(1)}, A_{(2)}, ..., A_{(k)} is a (finite) set. The same holds for the B_{(j)}’s, and in fact there is a further possibility (structural rule), namely to add further hypotheses to the set (weakening).

The point of linear logic is to forbid contraction and weakening, so that we have a proof which uses the hypotheses exactly once each. The set {A_{(1)}, A_{(2)}, ..., A_{(k)}} now becomes a bag since we may now have duplicates but may still exchange. The effect of this is that there are now two different conjunctions (⊗ and &) and two different disjunctions (⅋ and ⊕). The power of intuitionistic logic is regained by the “of course” operator ! A, which manufactures as many copies of the hypothesis A as we need. The reader is referred to any of the recent work of Girard or Lafont for further descriptions of the system.

When we say that linear logic is not necessarily logic we mean that what we call “proofs” may bear no resemblance to ordinary deduction. This is the case with the group-action interpretation.

Definition 2.4 A proof of

A_{(1)}, A_{(2)}, ..., A_{(k)} ⊢ B_{(1)}, B_{(2)}, ..., B_{(l)}

is a set P together with an action of each A_{(i)} on the left, and each B_{(j)} on the right, i.e.

a_{(i)} · p  and  p · b_{(j)}

for each p ∈ P, a_{(i)} ∈ A_{(i)} and b_{(j)} ∈ B_{(j)}, which commute, i.e.

a_{(i)} · (a_{(i′)} · p) = a_{(i)} · (a_{(i′)} · p)
(a_{(i)} · p) · b_{(j)} = a_{(i)} · (p · b_{(j)})
(p · b_{(j)}) · b_{(j′)} = (p · b_{(j)}) · b_{(j′)}

for i ≠ i′ and j ≠ j′.

When k = l = 1, a proof of A ⊢ B is a functor P : A × B^{op} → Set, which also called a profunctor from A to B. This numerical restriction is unimportant because of the

Exercise 2.5 A simultaneous action of A_{(1)}, ..., A_{(k)} on the left and B_{(1)}, ..., B_{(l)} on the right of X is the same as an action of A_{(1)}^{op} × ... × A_{(k)}^{op} × B_{(1)} × ... × B_{(l)} on the right. □

What justifies the use of the word “proof” for these very un-proof-like objects is the fact that the sequent rules for the (linear) logical connectives are sound, although with (single) groups we shall only be able to interpret ⊗, ⅋ and ^{⊥}.

Proposition 2.6 For groups C and D, let C ⊗ D = C⅋D = C × D, the cartesian product. Also, let C^{⊥} = C^{op}, the opposite group. Then the rules

\frac{A⃗, C, D ⊢ B⃗}{A⃗, C ⊗ D ⊢ B⃗} L⊗  R⅋\frac{A⃗ ⊢ C, D, B⃗}{A⃗ ⊢ C⅋D, B⃗}

and

\frac{A⃗ ⊢ C, B⃗}{A⃗, C^{⊥} ⊢ B⃗} L^{⊥}  R^{⊥} \frac{A⃗, C ⊢ B⃗}{A⃗ ⊢ ^{⊥}C, B⃗}

are interpreted as isomorphisms. The rules

\frac{A⃗, C ⊢ B⃗  A⃗′, D ⊢ B⃗′}{A⃗, A⃗′, C⅋D ⊢ B⃗, B⃗′} L⅋  R⊗\frac{A⃗ ⊢ C, B⃗  A⃗′ ⊢ D, B⃗′}{A⃗, A⃗′ ⊢ C ⊗ D, B⃗, B⃗′}

are interpreted by a product. Proof We have dealt with the first four rules in the Exercise. For the last two, if P and Q are the actions corresponding to the proofs above the line, P × Q corresponds to that below; the action is

a_{(i)}·⟨p, q⟩ = ⟨a_{(i)}·p, q⟩, a_{(i′)}·⟨p, q⟩ = ⟨p, a_{(i′)}·q⟩, ⟨p, q⟩·b_{(j)} = ⟨p·b_{(j)}, q⟩, ⟨p, q⟩·b_{(j′)} = ⟨p, q·b_{(j′)}⟩

and

⟨c, d⟩ · ⟨p, q⟩ = ⟨c · p, d · q⟩  or  ⟨p, q⟩ · ⟨c, d⟩ = ⟨p · c, q · d⟩

for L⅋ and R⊗ respectively. □

2.2 Identity and Cut

So far we have given definitions and constructions but no concrete examples of actions. The most important example was found by Cayley, and we shall use it to interpret the identity (axiom) A ⊢ A: we take P = A, i.e. just the set of elements of the group, where a·p = a∘p and p·a = p∘a. (This same idea occurs in category theory as the Yoneda lemma.) We take this opportunity to introduce some more general notation; we shall also often drop the ∘ when composing group elements.

Definition 2.7 Let A be a group and H any subgroup, written H ≤ A. For x ∈ A, xH = {xh : h ∈ H} is a left coset and Hx = {hx : h ∈ H} is a right coset. Write A_{/H} for the set of left cosets and _{H\}A for the set of right cosets.

Definition 2.8 Let X carry a right action of A and x ∈ X. Then the orbit of x is the set

x · A = {x · a : a ∈ A}

and if this is the whole of X we call the action transitive. The stabiliser of x is the subgroup

Stab_{A}(x) = {a ∈ A : x · a = x}

The action of A on X is called faithful if

∀a ∈ A.(∀x ∈ X.x · a = x) ⇒ a = id

but the condition we had in Lemma 1.5.4 was

∀a ∈ A.(∃x ∈ X.x · a = x) ⇒ a = id i.e. ∀a ∈ A.∀x ∈ X.(x · a = x ⇒ a = id)

which we call locally faithful^{8}. Alternatively, the action is locally faithful at x iff Stab_{A}(x) = {id}; of course if Stab_{A}(x) = A then x is a fixed point.

Proposition 2.9 Let A be a group. Then

(a) For any subgroup H, _{H\}A carries a transitive right action given by Hx · a = H(xa) and A_{/H} carries a transitive left action given by a · xH = (ax)H.

(b) Every action of A on a set X is uniquely expressible as the disjoint union of actions on cosets.

8The term semi-regular is used in group theory: Cayley’s action is the regular one: cf. simple and semi-simple in ring theory. I am grateful to Steve Linton for his remarks on standard terminology.

Proof Checking that [a] is well-defined is an easy standard exercise. For [b] we decompose X as a disjoint union of orbits, on each of which the action is transitive. With H = Stab_{A}(x), the right action of A on _{H\}A is isomorphic to that on x · A by Ha ↔ x · a. □

This gives us a concrete representation of actions.

Exercise 2.10 Show that Stab_{A}(x · a) = a^{−1} Stab_{A}(x) a; this is called a conjugate subgroup.

Notation 2.11 Write Conj(A) for the set of conjugacy classes of subgroups of a group A. For an action of A on X and [H] ∈ Conj(A), write X^{[H]} for the number (set) of orbits whose stabiliser belongs to the conjugacy class [H], so that

X ≅ ∑_{[H]∈Conj(A)} X^{[H]} × _{H\}A

We also need two-sided cosets:^{9} if H ≤ A^{op} × B we write A_{/H\}B for the set of objects aHb ≡ H⟨â, b⟩ with a ∈ A and b ∈ B. This has left action of A and right action of B by

a′ · aHb = a′aHb  and  aHb · b′ = aHbb′

and so is an (atomic) proof of A ⊢ B. As a special case of this, write

Δ = {⟨â^{−1}, a⟩ : a ∈ A} ≤ A^{op} × A

for the diagonal subgroup; then A_{/Δ\}A is (isomorphic to) the set A with its obvious (regular) two-sided action.

Proposition 2.12

(a) For a group A,

A_{/Δ\}A  is a proof of  A ⊢ A

(b) The rule

\frac{A⃗ ⊢ C, B⃗  A⃗′, C ⊢ B⃗′}{A⃗, A⃗′ ⊢ B⃗, B⃗′} Cut

is interpreted by

P, Q ↦ P ⊗_{C} Q

where P ⊗_{C} Q is the set of pairs ⟨p, q⟩ with p ∈ P and q ∈ Q subject to the equivalence relation ⟨p · c, q⟩ = ⟨p, c · q⟩ (Definition 1.5.4), and the action of A⃗ etc. is as in Proposition 2.1.5.

Proof It is an exercise to show that the actions respect the equivalence relation. □

Observe that this rule is the same as R⊗ (and L⅋) but with C ⊗ C^{⊥} (respectively C^{⊥}⅋C) deleted. In simpler terms, this amounts to the rule

\frac{C ⊢ C}{⊢}

which, semantically, turns an action of C on both sides of P into a set without any action, using the condensation

p ↦ [p] = {c^{−1} · p · c : c ∈ C}

which forms the quotient by an equivalence relation. With linear (now in the traditional sense of Linear Algebra) instead of permutation representations of groups, we may express [p] as an “average”

[p] = \frac{1}{|C|} ∑_{c∈C} c^{−1} · p · c

9In computational group theory, a double coset is of the form HaK.

(cf. Maschke’s theorem; [Lang] Theorem 18.1.1). This is essentially what Girard does in his “ℂ^{∗}-algebra” interpretation of linear logic [89].

Exercise 2.13 Show that every equivariant function f : _{H\}A → _{J\}A is onto, and is of the form Hx ↦ Jfx where H ⊂ f^{−1}Jf. Suppose that K : ℚ is a normal field extension with Galois group A; show that the category of intermediate fields and homomorphisms (not necessarily commuting with the inclusion in K) is dual to this category of transitive actions.

2.3 Groupoids and the Additive Fragment

The multiplicative fragment of Linear Logic is very inexpressive: we need to extend it with the additive connectives, & and ⊕. In our interpretation, they become identified, and in fact are interpreted as a disjoint sum of groups.

But what is a disjoint sum of groups? Just what it says, and certainly not their coproduct in Gp. It is at this point that we see the value of the abstract (categorical) definition of a group.

Definition 2.14 A groupoid is a category in which every morphism is invertible.

Lemma 2.15 Every groupoid is equivalent to a unique bag of groups. Proof A bag of groups is a skeletal groupoid, i.e. one in which if two objects are isomorphic (quâ objects of the category, not just that their automorphism groups are isomorphic in Gp) then they are equal. Given any groupoid, we choose (arbitrarily) one object in each component and form the full subcategory; this is a skeletal groupoid. Any object is isomorphic to a unique chosen object, but not uniquely so, hence we have also to choose a particular isomorphism. By pre-composing morphisms with this chosen isomorphism and post-composing with its inverse, we can define a functor from the whole groupoid to its skeleton, and this provides an equivalence. The bag of groups is easily seen to be unique up to isomorphism, although (the pair of functors defining) the equivalence is certainly not unique. □

As we said, both the abstract and the concrete definitions are useful, even for connected groupoids. A good example is the Fundamental Group of a (path-connected) topological space, which consists of the loops at a given basepoint under concatenation. The abstract version of this is the groupoid of paths between any two points, which enables us to extend the definition to the non-connected case. The functoriality of this construction is more easily seen abstractly, whereas for calculations in algebraic topology the additional copies of the same group serve no useful purpose. The same will apply in our case.

We shall in future use A to denote a groupoid and write A_{i} for a typical component, which we shall consider to be a group (skeletal). Note that the i ∈ I correspond to components and not objects of the groupoid. We shall also drop the usual shorthand X ∈ C for an object of a category, instead using a ∈ A to mean that a is a morphism of A; this generalises a ∈ A_{i} for an element of a group. This is consistent with seeing a skeletal groupoid as its set of morphisms with partial composition.

Just as a groupoid is a bag of groups, A_{i}, so a groupoid action is a bag of sets, X^{i} (one for each group). The elements a ∈ A_{i} act on the x ∈ X^{i} in the corresponding set, and local faithfulness is defined in the obvious way. (Contrast this with Definition 2.1.4, in which all the A_{(i)} acted on the same set X.) Moreover an equivariant function f : X → Y is a bag of functions f^{i} : X^{i} → Y^{i} each respecting the action of the A_{i}. The abstract definition proves its worth in the following result, which unifies 1.3.2 and 2.1.3.

Lemma 2.16 Let A be a groupoid. The category of right A-actions is isomorphic to the category Set^{A^{op}} of functors from A^{op} to Set (or presheaves on A) and natural transformations between them. Similarly left actions form the category Set^{A}. □

If we add groups to a bag, it can still act on the same family of sets, on the understanding that the missing sets are empty. Thus if X carries an action of C then X + 0 carries an action of C + D. This is “vectorial addition” in the sense that the set X^{i} is “oriented” by the group A_{i}. In particular we shall write _{H\}A_{i} for the “unit vector”, i.e. action of the groupoid A on the family of sets which are empty in all components except i, where it is the set of right cosets of H ≤ A_{i}.

Lemma 2.17 _{H\}A_{i} is atomic: it has no proper subobject as an object of Set^{A^{op}}. Every object of this category may be expressed uniquely as a coproduct of atoms. Proof Clearly

X ≅ ∑_{i∈I} ∑_{[H]∈} ; Conj(A_{i}) X^{i,[H]} × _{H\}A_{i}

whilst it is an exercise to show that if f : X → Y is an equivariant function between two such decompositions, each component of X is mapped onto some unique component of Y. □

Of course we shall now interpret C&D = C ⊕D = C +D as the disjoint union of groupoids, but certain other things have to be generalised about the earlier interpretation. We have to replace the product of groups and of sets by the product of groupoids and families of sets; this means that we form the product of the indexing sets, I × J, and for each ⟨i, j⟩ form the product of the groups, A_{i} × B_{j}, or sets, X^{i} × Y^{j}. Observe that the sum and product of skeletal groupoids are again skeletal.

Proposition 2.18 The rules

\frac{A⃗, C ⊢ B⃗}{A⃗, C&D ⊢ B⃗} L1&  L2&\frac{A⃗, D ⊢ B⃗}{A⃗, C&D ⊢ B⃗}

and

\frac{A⃗ ⊢ B⃗, C}{A⃗ ⊢ B⃗, C ⊕ D} R1⊕  R2⊕\frac{A⃗ ⊢ B⃗, D}{A⃗ ⊢ B⃗, C ⊕ D}

are interpreted by X ↦ X + 0 or X ↦ 0 + X, whilst the rules

\frac{A⃗, C ⊢ B⃗  A⃗, D ⊢ B⃗}{A⃗, C ⊕ D ⊢ B⃗} L⊕  and  R&\frac{A⃗ ⊢ C, B⃗  A⃗ ⊢ D, B⃗}{A⃗ ⊢ C&D, B⃗}

are interpreted by X, Y ↦ X + Y. □

The interpretation of Cut is also more complicated: if X is a proof of ⊢ C and Y of C ⊢ then we have to reinterpret

X ⊗_{C} Y = ∑_{i} X^{i} ⊗_{C_{i}} Y_{i}

which is already reminiscent of Theorem 1.5.5. The categorically-minded will observe that this is a colimit or coend over a diagram whose type is a groupoid (namely C).

Before we return to our discussion of stable functors, let us first complete the interpretation of the linear connectives by giving the units.

Exercise 2.19 Show that with 1 = ⊥ interpreted as the one-element group and 0 = ⊤ as the empty groupoid, the rules

\begin{matrix}L⊥\overline{⊥ ⊢} = \overline{⊢ 1}R1 & L1\frac{A⃗ ⊢ B⃗}{A⃗, 1 ⊢ B⃗} = \frac{A⃗ ⊢ B⃗}{A⃗ ⊢ ⊥, B⃗} R⊥ \\ L0\overline{A⃗, 0 ⊢ B⃗} = \overline{A⃗ ⊢ ⊤, B⃗} R⊤ & (no rule L⊤ = R0) \end{matrix}

are sound. [Hint: use a singleton singleton for the first two, and an empty bag for the third.] □

3 Quantitative Domains

3.1 Linear Functors

We have already defined a proof of ⊢ A to be an object of Set^{A^{op}}, so more generally what is the relationship between proofs (actions)

A_{(1)}, ..., A_{(k)} ⊢ B_{(1)}, ..., B_{(l)}

and stable functors

Set^{A_{(1)}^{op}×...×A_{(k)}^{op}} → Set^{B_{(1)}^{op}×...×B_{(l)}^{op}}

(without loss of generality, k = l = 1)? Suppose that P is a proof of A ⊢ B, i.e. an action of A on the left and B on the right, and let X ∈ Set^{A^{op}}, i.e. an action of A on the right. We may form the tensor product

SX = X ⊗_{A} P  i.e.  (SX)^{j} = ∑_{i} X^{i} ⊗_{A_{i}} P_{i}^{j}

and hence define a functor S : Set^{A^{op}} → Set^{B^{op}}.

Now S is not stable, but S^{op} : (Set^{A^{op}})^{op} → (Set^{B^{op}})^{op} is!

Lemma 3.1 S has a right adjoint and preserves cofiltered limits. Proof The right adjoint is given by

Y ↦ Y/_{A}P ≡ {x : P →_{B} Y } with x · a : p ↦ x · (a · p)

Preservation of cofiltered limits uses the fact that the intersection of a descending sequence of non-empty finite sets is non-empty, which depends on our use of finite groups. □

Exercise 3.2 Show that if S : Set^{A^{op}} → Set^{B^{op}} has a right adjoint then S ≅ − ⊗_{A} P for some P : A ⊢ B. □

The problem is that S does not preserve pullbacks (we already have the counterexample \frac{1}{2}X^{2}), but it does preserve a wider class of squares:

Definition 3.3 A square in Set^{A^{op}} is called sur-cartesian if it commutes and the mediator to the pullback is an epimorphism.

Exercise 3.4 By considering the decomposition in Lemma 2.3.4, show that a commutative square is sur-cartesian iff the underlying square of atoms is a pullback. Hence show that S preserves sur-cartesian squares. □

Since not every two-sided action (profunctor) gives rise to a stable functor, we have to modify the theory. We have (at least) three options:

(a) Replace stability with this weaker notion of preserving sur-cartesian squares. Joyal [87] has studied this, proving similar results to ours (in particular uniqueness in the definition of candidacy is dropped) but unfortunately not quite in sufficient generality to give a cartesian closed category. However he does also develop a theory with vector spaces instead of sets, to which we have only alluded.

(b) Restrict the morphisms to monos, forcing sur-cartesian=cartesian to restore stability: Lamarche has shown (privately) that domains of the form M(A) and stable functors form a cartesian closed category, where M(A) is the category of locally faithful A-actions and monomorphisms.

(c) Restrict the objects to those for which the functor does preserve pullbacks: this is what we choose to do.

The interested reader should be able to adapt our results to cases (a) and (b), which are somewhat simpler. Joyal’s ideas probably lead to other models of Linear Logic worthy of study.

Definition 3.5 A functor is linear if its restriction to slices has adjoints on both sides; we write S : X ⊸ Y.

The term is justified semantically by the representation S ≅ − ⊗_{A} P, which says that a linear functor performs “matrix multiplication” on atoms. The syntactic justification lies in the prooftheoretic principle of using each hypothesis exactly once. We cannot say that S has a (global) right adjoint, because Y/_{A}P may not lie in the chosen full subcategory.

What help is this in classifying stable functors? As Girard put it, it is that every stable functor can be made linear if only we change the domain. Indeed, comparing

SX = X ⊗_{A} P = ∑_{i} X^{i} ⊗_{A_{i}} P_{i}^{j}  with  SX ≅ ∑_{n⃗} Xn⃗ ⊗_{Aut(n⃗)} σn⃗

we see that we can write

SX ≅ ! X ⊗_{! A} σ

if we make the following

Definition 3.6

(a) ! A is the groupoid of finite A-actions (n⃗) and isomorphisms; as a bag of groups its components are Aut(n⃗).

(b) ! X is the right ! A-action with (! X)n⃗ = Xn⃗ (i.e. Hom(n⃗, X), cf. Lemma 1.5.3).

In the language of category theory [Mac Lane, Chapter VI], ! − is a comonoid in the monoidal category with linear functors as morphisms, and the category with stable functors is the coKleisli category [Lafont]. The fact that

[X → Y] ≃ [! X ⊸ Y]

is a non-trivial achievement, because we have reduced a complex binary operator → to a simple binary operator [− ⊸ −] (the linear function-space) and a complex unary operator ! .

Observe that evaluation is linear in the functor. This means that although a process may have to read its input many times to match the parts of a pattern, the pattern (a token of the function) need itself only be read once. Girard noticed that many λ-definable operations are actually linear.

3.2 Creeds

We have already seen that for a set (or groupoid) A, the groupoid of all finite objects of Set^{A^{op}} is involved in ! A, but this is further complicated by local faithfulness. In order to state and prove the theorem correctly, we must therefore make a definition of quantitative domains which is sufficiently complex to account for these phenomena.

Definition 3.7 A creed on a group A is a subset Γ ⊂ A which is closed under inverses, powers and conjugation (not multiplication: that would make it a normal subgroup, which is too strong). A creed on a groupoid is a creed on each component group. An action of A on X is locally faithful to Γ if ∀x ∈ X. Stab_{A}(x) ⊂ Γ, or equivalently ∀x ∈ X, a ∈ A.(a · x = x ⇒ a ∈ Γ).

Exercises 3.8

(a) Let A be a groupoid equivalent to the bag of groups (A_{i}) (cf. Lemma 2.3.2), and let Γ_{i} ⊂ A_{i} be a family of subsets. Using the chosen isomorphisms this can be extended to a family of subsets of the automorphisms of the other objects. Show that this extension is independent of the choice of isomorphisms iff each Γ_{i} is closed under conjugation by elements of A_{i}. [Hint: cf. Exercise 2.2.4.] (b) Show that every subset of a group contains a largest creed, to which it is equivalent as a

way of defining local faithfulness. [Hint: Stab_{A}(x) might be a cyclic subgroup.] □

Definition 3.9 A quantitative type is a groupoid A equipped with a creed Γ, i.e. a creed Γ_{i} on each component group A_{i}. The corresponding quantitative domain, QD(A, Γ), is the category of locally Γ-faithful right A-actions and equivariant functions. Note that QD(A, Γ) does not have a terminal object unless Γ = A, so Lemma 1.3.6 fails, but everything else carries over.

Lemma 3.10 X = QD(A, Γ) ⊂ Set^{A^{op}} is closed under

(i) backwards-arrows (isotomic): if Y ∈ X and f : X → Y in Set^{A^{op}} then X ∈ X,

(ii) morphisms (full): if X, Y ∈ X and f : X → Y in Set^{A^{op}} then f ∈ X,

(iii) isomorphisms (replete): special case of (i) with f : Y ≅ X,

(iv) coproducts: if X, Y ∈ X and Z = X + Y in Set^{A^{op}} then Z ∈ X,

(v) filtered colimits: if X = colim^{↑} X^{(r)} in Set^{A^{op}} with X^{(r)} ∈ X then X ∈ X.

(vi) representable objects: _{1\}A_{i} ∈ X (in fact _{H\}A_{i} ∈ X iff H ⊂ Γ).

Conversely, if X ⊂ Set^{A^{op}} is a subcategory with these closure conditions then there is a unique creed Γ with QD(A, Γ) = X. Proof [i] If f : X → Y then the stabilisers of points of X are no bigger than those in Y.

[ii] Definition. [iv] Lemma 2.3.4. [v] Exercise. [vi] The representable objects are locally faithful actions because their stabilisers are {1} ⊂ Γ. [⇐] Let Γ_{i} = ⋃{H ≤ A_{i} : _{H\}A_{i} ∈ X }. □

Corollary 3.11 QD(A, Γ) ⊂ Set^{A^{op}} is also closed under binary products with, and exponentiation by, arbitrary objects of Set^{A^{op}}. Also equalisers, but not coequalisers. □

We have chosen a definition in terms of a unary predicate on group(oid) elements, viz. membership of a creed. One could alternatively define a (reflexive, symmetric) binary predicate

a ⌢ ⌣ b ⟺ ∃i.a, b ∈ A_{i} ∧ ab^{−1} ∈ Γ_{i}

making an analogy with coherence spaces [GLT, chapter 8]. We recover the creed by Γ = {a ∈ A : id ⌢ ⌣ a}. A pairwise coherent subset of a groupoid which is also closed under the (partial) Mal’cev operation

μ(a, b, c) = ab^{−1}c

is the same thing as a right coset of a subgroup H ⊂ Γ_{i}, and this is a token of a locally Γ-faithful A-action. An object of a quantitative domain is a set of coherent Mal’cev-closed sets. In contrast, an object of a qualitative domain is just a coherent set. The reason is that in qualitative domains we are controlling sums, whilst in quantitative domains we need to control quotients.

We have to generalise the power-series expansion and the interpretation of linear logic. We shall abuse notation by writing

(A, Γ)&(B, Δ)  as  (A&B, Γ&Δ)

and similarly for the other connectives. This is an abuse, because ! A (in particular) depends on Γ as well as A, because its objects are locally Γ-faithful finite right actions. Obviously ! Γ depends on A.

Exercise 3.12 Every stable functor S : QD(A, Γ) → QD(B, Δ) has a power-series expansion similar to Theorem 1.4.9, except for the local faithfulness condition, and so extends to a functor (not necessarily stable) Set^{A^{op}} → Set^{B^{op}}. □

The units are given by

QD(⊥) = Set = QD(1) QD(⊤) = 1 = QD(0)

whilst the additives are both given as before by disjoint unions:

(A, Γ)&(B, Δ) = (A, Γ) ⊕ (B, Δ) = (A + B, Γ + Δ)

where A + B is the disjoint union and Γ + Δ is similarly the family in which Γ_{i} corresponds to A_{i} and Δ_{j} to B_{j}.

Exercise 3.13 Show that

[ QD(A, Γ) ⊸ QD(B_{1}, Δ_{1}) × QD(B_{2}, Δ_{2})] ≃ [ QD(A, Γ) ⊸ QD(B_{1}&B_{2}, Δ_{1}&Δ_{2})]

and

[ QD(A_{1}, Γ_{1}) × QD(A_{2}, Γ_{2}) ⊸ QD(B, Δ)] ≃ [ QD(A_{1} ⊕ A_{2}, Γ_{1} ⊕ Γ_{2}) ⊸ QD(B, Δ)]

where [X ⊸ Y] is the linear function-space: we have yet to define the linear connective (A, Γ) ⊸ (B, Δ). Show also that Proposition 2.3.5 remains valid. □

Recall that in coherence spaces, ⊕ and ⊗ have simple descriptions as sums and products of graphs, whereas & and ⅋ are defined via linear negation. In our case, linear negation commutes with ⊕, so &= ⊕, but (unlike for groups) it does not commute with ⊗. We define

(A, Γ) ⊗ (B, Δ) = (A × B, Γ × Δ)

in the obvious way, and it is easy to check this gives a creed.

Exercise 3.14 Describe QD ((A, Γ) ⊗ (B, Δ)) and show that it is a topological product.

3.3 Creeds and Negation

Now it was Lemma 1.3.6 which was the source of our difficulties, so let us look carefully at how the problem arose. Because of the existence of the terminal object, it was possible to satisfy

∃X, f : n⃗ → X . f ∘ h = f

for arbitrary h ∈ Aut(n⃗). In general, if h satisfies this property, we call it an annihilable automorphism. (In the study of linear functors, we shall just have h = a ∈ A_{i} ≅ _{1\}Aut(A_{i}) .)

Lemma 3.15 a ∈ A_{i} is annihilable iff a ∈ Γ_{i}. Proof [⇐] Put X = _{⟨a⟩\}A_{i} where ⟨a⟩ ≤ A_{i} is the cyclic subgroup generated by a. [⇒] Any annihilating f factors through this. □

It is then clear that we must let ! Γn⃗ ⊂ Aut(n⃗) be the set of annihilable automorphisms. We shall see shortly that !(A, Γ) ⊸ (B, Δ) gives the function-space. However the basic difficulty actually lies in the linear negation, which we want to satisfy

[QD(A, Γ) ⊸ Set] ≃ QD(A^{⊥}, Γ^{⊥})

since Set = QD(⊥) and A ⊸ ⊥ = A^{⊥}.

Lemma 3.16 A^{⊥} = A^{op} and Γ^{⊥} = {â : ∀k.a^{k} ∈ Γ ⇒ a^{k} = 1}. Proof The question is when SX = X ⊗_{A} P is stable, for a left action of A on P; without loss of generality this is atomic, so P = A_{i}_{/H} where H ≤ A_{i}. An element of X ⊗_{A} P is then a pair ⟨x, aH⟩ where x ∈ X_{i} and aH ∈ A_{i}_{/H} ; but this is identified with ⟨x ∘ a, H⟩, so we may write it as xaH. The (potential) candidate is H = idH ∈ _{1\}A_{i} ⊗_{A_{i}} A_{i}_{/H} and the factorisation is xH = Sx ∘ H.

The problem is uniqueness of the diagonal a in the definition of the candidacy of H.

[figure: 1; H; _{1\}A_{i} ⊗_{A_{i}} A_{i}_{/H}; Sa; _{1\}A_{i} ⊗_{A_{i}} A_{i}_{/H}; H; Sx; _{H\}A_{i} ⊗_{A_{i}} X_{i}; Sx; 1; H; _{1\}A_{i} ⊗_{A_{i}} A_{i}_{/H}; Sh; X′ ⊗_{A_{i}} A_{i}_{/H}; x′H; Sf; X_{i} ⊗_{A_{i}} A_{i}_{/H}; Sx]

If a = id is to be the unique diagonal in the diagram on the left for all x, we must have

\frac{a ∈ H ∃x ∈ X.x ∘ a = x}{a = id}

Conversely, if the right-hand square commutes then xH = fx′H and so there is some a_{1} ∈ H with x = fx′a_{1}; in fact h_{1} = x′a_{1} is a typical diagonal. If a_{2} = a_{1}a also satisfies this then the rule makes a_{1} = a_{2}. So we have shown that the rule is necessary and sufficient.

By lemma 3.3.1, the rule says that

H ⊂ {a ∈ A_{i} : a ∈ Γ_{i} ⇒ a = id}

However H, being a subgroup, is closed under powers, so we can strengthen this to the given definition of Γ^{⊥}_{i}. On the other hand, cyclic subgroups show that this is the most we can do. It is also easy to show that Γ^{⊥} is closed under inverses and conjugation. □

We do not in general have (A, Γ)^{⊥}^{⊥} = (A, Γ) (Exercise 3.6.4). The other two binary connectives, ⅋ and ⊸, are related by

(A, Γ)^{⊥} ⊗ (B, Δ)^{⊥} = ((A, Γ)⅋(B, Δ))^{⊥}  and  (A, Γ) ⊸ (B, Δ) = (A, Γ)^{⊥}⅋(B, Δ)

where

(Γ⅋Δ)_{ij} = {⟨a, b⟩ : ∀k.(a^{k} ∈ Γ_{i} ∧ b^{k} ∈ Δ_{j}) ∨ (id ≠ a^{k} ∈ Γ_{i}) ∨ (id ≠ b^{k} ∈ Δ_{j})}

and

(Γ ⊸ Δ)_{ij} = {⟨â, b⟩ : ∀k.(a^{k} ∈ Γ_{i} ⇒ b^{k} ∈ Δ_{j}) ∧ (a^{k} ∈ Γ_{i} ∧ b^{k} = id ⇒ a^{k} = id)}

so

((C, Θ) ⊗ (A, Γ)) ⊸ (B, Δ) = (C, Θ) ⊸ ((A, Γ) ⊸ (B, Δ))

Lemma 3.17 With this definition we have

[ QD(A, Γ) ⊸ QD(B, Δ)] ≃ QD ((A, Γ) ⊸ (B, Δ))

Proof Put SX = X ⊗ P with P = A_{i}_{/K\}B_{j} for some subgroup K ≤ A_{i}^{op} × B_{j}. We have to show that the action of B on SX is locally faithful to Δ and the diagonals for the potential candidate K ∈ _{1\}A_{i} ⊗ A_{i}_{/K\}B_{j} are unique. A typical element of SX is xKb where x ∈ X_{i} and b ∈ B_{j}, but since b is an isomorphism we may assume b = id. Local faithfulness to Δ amounts to the rule

\frac{⟨â, b⟩ ∈ K ∃x ∈ X.x ∘ a = x}{b ∈ Δ_{j}}

and candidacy, as before, to the rule

\frac{⟨â, id⟩ ∈ K ∃x ∈ X.x ∘ a = x}{a = id}

Again ∃x ∈ X.x ∘ a = x ⟺ a ∈ Γ_{i} and the rules may be strengthened to ⟨â, b⟩^{k}. These two rules correspond exactly to the two parts of the expression for ((A, Γ) ⊸ (B, Δ)). □

Finally, we leave the identity

[ QD(A, Γ) → QD(B, Δ)] ≃ QD (!(A, Γ) ⊸ (B, Δ))

as an exercise: the argument is exactly analogous to Lemmas 3.3.2&3. We have already shown that evaluation is not just stable but linear, so we have completed the proof of the

Theorem 3.18 Quantitative types model linear logic, and quantitative domains and stable functors form a cartesian closed category. □

Exercise 3.19 State and prove the adjunctions between ⊗ and ⊸ and between & and →.

3.4 Rigid Adjunctions and the Type of Types

Following standard practice with domain models of polymorphism, we shall use the following to interpret dependent types:

Definition 3.20 Φ : X → Y is a rigid comparison if it has a right adjoint Θ : Y → X and the unit η : id_{X} → ΘΦ and counit ϵ : ΦΘ → id_{Y} are cartesian.

Theorem 3.21 Rigid comparisons are comonadic. Proof Suppose α : Y → ΦΘY is a coalgebra, so ϵY ∘ α = id — we don’t even need the other equation ΦΘα ∘ α = νY ∘ α because it will follow automatically! Form the pullback

X  \overline{β} ΘY

[figure: ΘY; β′; ηΘY; ΘΦΘY; Θα; ΘϵY; ΘY]

and since ΘϵY ∘ Θα = id = ΘϵY ∘ ηΘY we have β = β′. We shall show that its adjoint transpose, β̃ = ϵY ∘Φβ : ΦX → Y, is a coalgebra isomorphism. Since Φ preserves pullbacks and ϵ is cartesian, the left-hand diagram below is a pullback:

[figure: ΦX; Φβ; ΦΘY; ϵY; Y]

[figure: ΦΘY; Φβ; ΦηΘY; ΦΘΦΘY; ΦΘα; ϵΦΘY; ΦΘY; α]

ΦX  \overline{β̃} Y

[figure: Φβ]

[figure: ΦΘΦX; ΦηX; ΦΘβ̃; ΦΘY; α]

The lower composite is an identity, so β̃ is an isomorphism of objects. However the right-hand diagram now commutes, so in fact it is a coalgebra isomorphism. In categorical jargon we have now shown that the Eilenberg-Moore comparison functor (which is always full and faithful) is essentially surjective. □

Definition 3.22 A local isomorphism θ : (A, Γ) → (B, Δ) between quantitative types is a full and faithful functor θ : A → B which preserves and reflects creeds. In terms of bags of groups, θ = (f, θ_{i}) where f : I → J is an arbitrary function and θ_{i} : A_{i} ≅ B_{f(i)} are group isomorphisms such that θ_{i}(Γ_{i}) = Δ_{f(i)}. An automorphism θ : B ≅ B is called inner if there is some family b_{j} ∈ B_{j} such that θ_{j} : B ↦ b_{j}^{−1}b b_{j}.

Proposition 3.23 Each local isomorphism θ : A → B gives rise to a rigid comparison Φ : QD(A, Γ) → QD(B, Δ) by

Φ(X)^{j} = ∑_{f(i)=j} X^{i}
Θ(Y)^{i} = Y^{f(i)}
Ψ(X)^{j} = ∏_{f(i)=j} X^{i}

where the actions are translated via θ_{i} and Φ ⊣ Θ ⊣ Ψ. Conversely, every rigid comparison arises uniquely up to isomorphism in this way, where θ = ϵB. Moreover cartesian transformations between rigid comparisons correspond to postcomposition with inner automorphisms and so are invertible. Proof By B ∈ QD(B, Δ) we mean the right action on itself, i.e. B^{j} = _{1\}B_{j} . Since any equivariant function into B^{j} is invertible (Exercise 1.4.4), ϵB : Â ≡ ΦΘB → B must be of the form of a local isomorphism, where Â ≅ ∑_{i} B^{f(j)} is naturally a groupoid and Γ̂ is induced in the obvious way. We have to show that QD(A, Γ), which we already know to be equivalent to the category of coalgebras, is equivalent to QD(Â, Γ̂). But if α : Y → ΦΘY is a coalgebra, the elements y ∈ Y^{j} already carry an action of B_{j}, whilst the function α (where ϵ_{Y} ∘ α = id) corresponds to a choice of i ∈ f^{−1}(j). The remaining details are left to the reader. □

Notice that the 2-structure is induced in some way by 1-automorphisms. This is in contrast to the continuous analogue, cf. [Hyland-Pitts], where it corresponds to homomorphisms of models of theories and is therefore essential. If we ignore it, it not difficult to see that the category of quantitative domains and rigid comparisons (or quantitative types and local isomorphisms) is equivalent to a quantitative domain of the form QD(V, 1). The wastage committed by this, though less, still seems comparable to our original complaint against Girard (Example 1.4.2), but we shall indicate later what the effect actually is (Remark 3.5.3).

Definition 3.24 V denotes the groupoid of finite groups with creeds (G, Δ) and group isomorphisms θ : G ≅ G′ which preserve and reflect creeds, i.e. θ(Δ) = Δ′. As a bag of groups, V has one component for each isomorphism class of finite groups with creeds, and the component group is the group of creed-preserving automorphisms.

Corollary 3.25 (V, 1) is a quantitative type of types. □

For T ∈ QD(V, 1) we shall write [[T]] for the corresponding quantitative type, i.e. groupoid with creed. Since the action of V on T is locally faithful, the components of T are of the form 1\Aut(G, Δ) and correspond to components (G, Δ) of [[T]].

It is now easy to code the quantifier-free types of the Girard & Reynolds’ System F and of Coquand & Huet’s Theory of Constructions (for details of the method, see [Hyland-Pitts]). Indeed we have

Exercise 3.26 Show that the following are linear functors:

\begin{matrix}⊕, & : (V, 1) ⊕ (V, 1) ⊸ (V, 1) & ⊗, ⅋, ⊸ : (V, 1) ⊗ (V, 1) ⊸ (V, 1) \\ ^{⊥} : (V, 1) ⊸ (V, 1) & ! : ! (V, 1) ⊸ (V, 1) \end{matrix}

□

3.5 Dependent Sums and Products

Before attempting to compute dependent (sums and) products of quantitative domains we need a more explicit description of dependent types. Fix a domain of variation X = QD(A, Γ) and write Q for a functor which to each object X ∈ X assigns a quantitative domain Q(X) and to each morphism f : X′ → X of X a rigid comparison Q(f)_{!} : Q(X′) → Q(X) with Q(f)_{!} ⊣ Q(f)^{∗} ⊣ Q(f)_{∗} . Using the “type of types”, Q corresponds to a stable functor QD(A, Γ) → QD(V, 1) and hence to a proof Q : ! (A, Γ) ⊢ (V, 1) such that

Q(X) ≃ QD ([[! X ⊗_{! A} Q]])

Such a proof is a sum of atoms, and so we shall concentrate on the case where it is the atom Q = Aut(m⃗)_{/K\}Aut(G, Δ) . More generally, we shall abuse notation by using K to index components of Q.

Exercise 3.27 Let K ≤ A^{op} × B. Show that the action of B on A_{/K\}B is locally faithful iff K → A^{op} × B → A^{op} is mono; we write K_{∘} ≤ A for the image, so K_{∘} ≅ K^{op}. This means that K defines a partial homomorphism κ : A^{op} ⇀ B with support K_{∘}. Then if B has a right action on an object G, there is an induced left action of A on G × A_{/K} . □

Lemma 3.28 [[! X ⊗_{! A} Q]] is the (non-skeletal) groupoid with

(i) objects x⃗Kθ for x⃗ : m⃗ → X and θ ∈ Aut(G, Δ),

(ii) morphisms ⟨ϕ, g⟩ : x⃗Kθ → x′Kθ′ where x⃗Kθϕ = x′Kθ′ and

(iii) composition ⟨ϕ, g⟩⟨ϕ′, g′⟩ = ⟨ϕϕ′, ϕ′(g)g′⟩.

If f : X′ → X in QD(A, Γ),

(iv) the local isomorphism [[! f ⊗ Q]] is given by precomposition with f, i.e. x⃗Kθ ↦ fx⃗Kθ and ⟨ϕ, g⟩ ↦ ⟨ϕ, g⟩.

Equivalently, the component groups are G with creed Δ and are indexed by a choice of representatives for the classes x⃗K_{∘} but [[! f ⊗ Q]] involves a renormalisation of this choice, which gives an element of K and hence an automorphism of G. □

Remark 3.29 This action of K_{∘} ≤ Aut(m⃗) on G gives rise to a (split) group extension G : K which is the set of pairs ⟨k, g⟩ with ⟨k, g⟩⟨k′, g′⟩ = ⟨kk′, ϕ′(g)g′⟩ where ⟨k̂, ϕ⟩, ⟨k̂′, ϕ′⟩ ∈ K. Observe that K_{∘} is a subgroup of G: K (this is the meaning of “split”), but in the more general case where we take account of the 2-structure of the category of domains by admitting pseudofunctors and general (non-split) fibrations, we obtain general group extensions where G is a kernel and K_{∘} is only a quotient. Alternatively the data may be coded as an arbitrary (creed-preserving) groupoid homomorphism.

If we attempt to perform the Grothendieck construction to interpret dependent sums, we find that we never get a quantitative domain (except in the constant case: the binary product).

Proposition 3.30 Let C be the category obtained by adding to the groupoid A the group G: K for each atom of Q and the hom-set Hom(A_{i}, G : K) = m^{i}, where m^{i} is the i-component of m⃗ and carries the obvious left action of G: K (via Aut(m⃗)) and right action of A_{i}. Then the total category ΣX : X .Q(X) is embedded as a subcategory of Set^{C^{op}} with the same closure properties as in Lemma 3.2.4. Proof Corresponding to ⟨X, Y ⟩ is a presheaf on C which extends that (viz. X) on A. The value at G: K is Σx⃗ : Xm⃗.Y^{x⃗K} with ⟨x⃗, y⟩ · ⟨k, g⟩ = ⟨x⃗ · k, y · g⟩, and for r ∈ m^{i} in the other hom-set, r : ⟨x⃗, y⟩ ↦ x^{r}. Verification is left to the reader. □

We chose not to develop this paper with general presheaf categories because the action of noninvertible C-maps on candidates is not defined. Nevertheless we only need to consider candidates u : Y → SX where Y is a generator. Corresponding to the two kinds of generator for the total category are two essential kinds of candidate for sections of the display map, but the first is useless because we always have the unique candidate ⟨id,?⟩ : ⟨_{1\}A_{i} , 0⟩ → ⟨_{1\}A_{i} , S(_{1\}A_{i})⟩. The other kind is of the form

u : ⟨m⃗, _{1\}G_{[K]} ⟩ → ⟨n⃗, S(n⃗)⟩

where n⃗ is finite by Exercise 1.2.9.

Notation 3.31 μ⃗ : m⃗ → n⃗ denotes the underlying map of u in X. For x⃗ : m⃗ → X, we write

xμ⃗ = {f : n⃗ → X : f ∘ μ⃗ ∈ x⃗K_{∘}}

In particular for x⃗ = μ⃗, Aut(μ⃗) = μμ⃗ = {f : f ∘ μ⃗ ∈ μ⃗K_{∘}} ⊂ Aut(n⃗); this carries the creed Γμ⃗ = Γn⃗ ∩ Aut(μ⃗).

Lemma 3.32 The set σ[K] ; μ⃗ of candidates of the above form carries an action of Aut(μ⃗) on the left which is locally faithful to Γμ⃗, and an action of G on the right which is locally faithful to Δ. Likewise xμ⃗ carries a right action of Aut(μ⃗). □

Proposition 3.33 Every object S of the dependent product ΠX : QD(A, Γ).Q(X) is of the form

(SX)^{x⃗K} ≅ ∑_{μ⃗} xμ⃗ ⊗_{Aut(μ⃗)} σ[K] ; μ⃗

where K ranges over the copies of subgroups corresponding to atoms of Q and x⃗ : m⃗ → X. Conversely every such power series is an object of the product. Proof As in Lemma 1.3.7 and Theorem 1.5.4, an element of (SX)^{x⃗K} is a (vertical) map ⟨X, _{1\}G_{x⃗K} ⟩ → ⟨X, SX⟩. By the ophorizontal-vertical factorisation, this corresponds to a map ⟨m⃗, _{1\}G_{K} ⟩ → ⟨X, SX⟩ over x′ : m⃗ → X (for any x′ ∈ x⃗K). Using stability of X ↦ ⟨X, SX⟩, we factorise this into a candidate u : ⟨m⃗, _{1\}G_{K} ⟩ → ⟨n⃗, S(n⃗)⟩ and ⟨f, Sf⟩ for f : n⃗ → X. Considering alternative factorisations yields the given tensor product. The converse is an exercise. □

Theorem 3.34 Quantitative domains admit dependent products and hence model System F and the Theory of Constructions. Proof The components of the quantitative type are of the form

( Aut(μ⃗),! Γμ⃗) ⊸ (G, Δ)

and there is such a component for each component K of Q and each μ⃗ : m⃗ → n⃗. □

3.6 Some Calculations

We have not described ! Γ explicitly, but the following sketch should serve as a guide to the serious group theory addict.

Exercises 3.35

(a) Write n⃗ = ∑_{i,[H]} _{H\}A_{i} × n_{i,[H]}, where H ranges over the conjugacy classes of subgroups of A_{i} contained in Γ_{i}.

(b) Show that

Aut(n⃗) = ∏_{i,[H]} (A_{i}/ ⋂[H]) ≀ Symm (n_{i,[H]})

where P ≀ Q denotes the wreath product, which is the split extension of B^{N} by the implicit action of Q on the set N.

(c) Hence h ∈ Aut(n⃗) can be written as h = h_{∘} ∘ π, where π is a permutation of isomorphic atoms and h_{∘} acts on individual atoms.

(d) Hence h can be written as a product of commuting terms each of the form h_{∘} ∘ π in which π = (12...k) is a cycle (possibly k = 1) of atoms with the same i and [H].

(e) Suppose n⃗ = _{H\}A_{i} × k and h = ⟨h_{1}, h_{2}, ..., h_{k}⟩ ∘ (12...k). Then there is an object X = K\A_{i} ∈ QD(A, Γ) and a map f : n⃗ → X with f ∘ h = f iff the subgroup of A_{i} generated by H and the product h_{1}h_{2}...h_{k} (is contained in K which) is contained in Γ_{i}.

(f) Hence (! Γ)n⃗ ⊂ Aut(n⃗) consists of those h = h_{∘}∘π such that for every cycle of π, the subgroup of A_{i} generated by H and the product of the h_{x} in the cycle is contained in Γ_{i}. □

From this we may recover our preliminary results.

Example 3.36 ! 1^{⊥} is the groupoid consisting of the finite permutation groups Symm (n) once each, with the creed {1} ⊂ Symm (n). (cf. Lemmas 1.3.6 and 1.5.4) □

Example 3.37 ! ! 1^{⊥}^{⊥} is the groupoid with components

∏_{n} Symm (n) ≀ Symm (m_{n}) for (m_{n}) finite

with the creed ∏_{n} Symm (n)^{m_{n}}. (cf. Corollary 1.5.6) □

Example 3.38 Let A = 2 ≀ 2 (the dihedral group of order eight) and Γ = 2^{2}; this is for instance one of the components of ! ! 1^{⊥}^{⊥}. Let n⃗ = { A_{/1} }, so Aut(n⃗) = A. Then {1} ∪ A \ (! Γ)n⃗ has five elements, but is not closed under powers. The creed ! Γ^{⊥} has three elements and is not closed under multiplication. Finally, Γ^{⊥}^{⊥} has six elements. □

Exercise 3.39 Show that Aut(A, Γ) ≤ Aut(A^{⊥}, Γ^{⊥}), but the inclusion may be strict.

Since the formula 3.6.1b involves quotients and not subgroups, the groups generated from Set using ! and ^{⊥} involve only the symmetric groups with binary and wreath product (because the alternating groups are simple). This means that our original claim to have found the smallest cartesian closed category including Set as an object is false. However from 3.5.5, we construct Aut(μ⃗) using subgroups, so it seems reasonable to suppose that the following is true (but only group junkies should attempt to prove it).

Conjecture 3.40 Every quantitative type is a subtype (in the sense implicit in Definition 3.4.3) of the interpretation of some type of System F or the Theory of Constructions.

Conclusions

Finally we might ask about polymorphic types such as Πα.α. This is very disappointing, because it involves the group G: Aut(G, Δ) for each isomorphism class of finite groups and creeds. Moggi’s “uniformity property” (which holds for the coherence space model) also fails. It seems that Stable Domain Theory has not lived up to its early promise of giving “minimal” models of polymorphism, but we should not therefore consider it to have been a dead end: we have profited by the discovery of Linear Logic, which has shown that (and how) Intuitionistic Logic and Cartesian Closed Categories are not as simple as we once thought.

I would like to express my appreciation for the deep interest shown in this work by Steven Vickers and François Lamarche. John Horton Conway was the source of my amateur fascination for Finite Group Theory.

4 Bibliography

M. Barr and R. Diaconescu

[80] Atomic toposes, Journal of Pure and Applied Algebra 17 (1980) 1–24 M. Barr and C. Wells

[85] Toposes, triples and theories, Springer Gr. d. math. W. 278 G. Berry

[78] Stable models of typed lambda calculi, Automata, Languages and Programming (Udine, July

1978), Springer Lecture Notes in Computer Science 62, 62–90 P.M. Cohn

[77] Algebra, Wiley, 2 vols (frequently reprinted)

Y. Diers

[81] Some spectra relative to functors, JPAA 22 (1981) 57–74 J.Y. Girard

[85] Normal functors, power series and lambda calculus, Ann. P.&A. Logic, 1986

[86] The system F of variable types, fifteen years later, Theoretical Computer Science 45 (1986) 159–192

[87] Linear Logic, TCS 50 (1987) 1–102

[88] Towards a geometry of interaction, in [Gray & Scedrov]

[89] Geometry of interaction I: interpretation of system F, ASL meeting (Padova, August 1988),

to appear J.Y. Girard and Y. Lafont

[87] Linear logic and lazy computation, TAPSOFT ’87 (Pisa), Springer LNCS 250 (1987) II 52–

66 J.Y. Girard, translated and with appendices by Y. Lafont and P. Taylor

[89] Proofs and Types, CUP Cambridge Tracts in Theoretical Computer Science 7 J.W. Gray and A. Scedrov, editors

[89] Categories in computer science and logic (Boulder, June 1987), American Mathematical

Society Contemporary Mathematics, to appear J.M.E. Hyland and A.M. Pitts

[87] The theory of constructions: categorical semantics and topos-theoretic models, in [Gray &

Scedrov] A. Joyal

[87] Foncteurs analytiques et espèces de structures, Combinatoire énumérative (Montréal, 1986),

Springer L.N. Mathematics 1234 (1987) 126–159 Y. Lafont

[88] The linear abstract machine, TCS 59 (1988) 157–180

F. Lamarche

[87] A simple model of the theory of constructions, in [Gray & Scedrov]

[88] Modelling polymorphism with categories, Ph.D. thesis, McGill University.

[89] Domains and infinitary algebras, seminar S. Lang

[65] Algebra, Addison-Wesley (frequently reprinted)

R.A.G. Seely

[87] Linear logic, *-autonomous categories and co-free alebras, in [Gray & Scedrov] P. Taylor

[85] Internal completeness of categories of domains, Category Theory and Computer Programming (Guildford, September 1985), Springer LNCS 240 (1986) 449–465

[88] An algebraic approach to stable domains, submitted to JPAA

[89] The trace factorisation and cartesian closure for stable categories, manuscript 70pp.