BRICS RS-94-27 T. Bra� uner: A Model of Intuitionistic Af�ne Logic from Stable Domain Theory

BRICS

Basic Research in Computer Science

A Model of Intuitionistic Af�ne Logic from Stable Domain Theory

(Revised and Expanded Version)

Torben Bra� uner

BRICS Report Series RS-94-27 ISSN 0909-0878 September 1994 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1994, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

A Model of Intuitionistic Affine Logic From Stable Domain Theory

(Revised and Expanded Version)

Torben Braüner^{∗}

BRICS^{†}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark

Abstract

Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model of Linear Logic. Now, the same phenomenon is present if we consider the category of pre dI domains and continuous stable maps, and the category of dI domains and linear stable maps; the functor that forgets the linearity has a left adjoint. This gives an alternative model of Intuitionistic Linear Logic. It turns out that this adjunction can be factored in two adjunctions yielding a model of Intuitionistic Affine Logic; the category of pre dI domains and affine stable functions. It is the goal of this paper to show that this category is actually a model of Intuitionistic Affine Logic, and to show that this category moreover has properties which make it possible to use it to model convergence/divergence behaviour and recursion.

∗Internet: tor@daimi.aau.dk †Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Contents

1 Introduction 3

2 Definition of the relevant categories 4

3 The category predI_{a} is a model of IAL 7 3.1 Definition of categorical models of ILL and IAL . . . . . . . . . . . . . . . 7 3.2 predI_{a} is a model of IAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 A strong monad on the category predI_{a} 12

5 Fixpoints in the category predI_{a} 13 5.1 Categorical fixpoints as usual . . . . . . . . . . . . . . . . . . . . . . . . . 13 5.2 Categorical fixpoints in models of ILL and IAL . . . . . . . . . . . . . . . 14 5.3 Fixpoints in predI_{a} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

A Appendix, categorical prerequisites 18 A.1 Monoidal categories etc. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 A.2 Monads etc. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 A.3 Comonads etc. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

1 Introduction

The category of dI domains and continuous stable functions is well known from the literature. It is for example described in [Win87] where it is shown equivalent to the category of stable event structures with stable maps, a category whose objects are a model for concurrency. A pre dI domain is a generalisation of a dI domain where we do not assume the existence of a bottom element. The category of pre dI domains and continuous stable functions will be denoted by predI_{s}. The monoidal closed category of dI domains and linear stable functions, dI_{l} is for example described in [Zha93] where it is shown equivalent to another model of concurrency, namely the category of stable event structures with linear maps. Now, the adjunction

predI_{s} [figure: ⊃; ⊤; !] dI_{l}

can be decomposed up to isomorphism into two adjunctions, and moreover, one can do it in two different ways:

\begin{matrix}predI_{s} & [figure: \overline{⊃}; ⊤; !] & predI_{a} \\ dI_{st} & ^{( )_{⊥}^{}}⊣_{∪} & [figure: \overline{⊃}; ⊤; !] & dI_{l} & ^{( )_{⊥}^{}}⊣_{∪} \end{matrix}

where predI_{a} is the category of pre dI domains and affine stable functions, and dI_{st} is the category of dI domains and strict stable functions. The functor ( )_{⊥} is the usual lift construction. In [Jac] similar situations are described, where an adjunction inducing another model of Intuitionistic Linear Logic (ILL) can be decomposed into adjunctions in two different ways, inducing models of Intuitionistic Affine Logic (IAL) and Intuitionistic Relevant Logic (IRL). Now, the question is whether that also is the case here.

The adjunction between predI_{s} and dI_{st} induces a comonad on dI_{st}, but how about the symmetric monoidal closed structure necessary to make it a model of IRL? The obvious internal-hom would be the strict stable function space ⊸, and the obvious symmetric monoidal structure would be smash product ⊗ with the Sierpinsky space I as unit. We would then get the correct isomorphism:

dI_{st}(A ⊗ B, C) ≅ dI_{st}(A, B ⊸ C)

The strict stable function space of two dI domains is a dI domain, but that is unfortunately not necessarily the case with the smash product. There is a counter example; the partial order

(I × I) ⊗ (I × I)

is not a dI domain. There does not seem to be any other obvious symmetric monoidal structure around, so we will not follow this track further.

The adjunction between predI_{s} and predI_{a} induce a comonad on predI_{a}, but in this case it turns out that we do have a symmetric monoidal closed structure around. The category predI_{a} is actually a model of full ILL, and since the unit of the tensor product is a terminal object, it is a model of IAL too. So the answer to the above mentioned question is a partial yes. Moreover, the adjunction between predI_{a} and dI_{l} induce a monad on predI_{a}. The monad is strong, so we can model convergence/divergence behaviour, cf. [Mog89]. One can define fixpoints in a sense suitable for models of ILL and IAL, and it turns out that we have such fixpoints in an appropriate subcategory of predI_{a} which enables us to model recursion too. It will be the goal of the present paper to describe the category predI_{a}.

The relevant categories will be defined formally in the next section. In the third section we will show that predI_{a} is a model of IAL. In the fourth section, predI_{a} will be shown to have a strong monad. The fifth section will deal with fixpoints in predI_{a}.

The work in the present paper is motivated by giving a sound and adequate denotational semantics to the term language for ILL, extended with recursion. Types are interpreted as pre dI domains, and terms as affine stable functions. The details of this work can be found in [Braa]. Moreover, fixpoints in a sense suitable for models of ILL and IAL are dealt with from a proof-theoretic point of view in [Brab].

2 Definition of the relevant categories

Definition 2.1 Let (D, ⊑) be a (possibly empty) poset, and assume that every non-empty finitely bounded X ⊆ D have join ⊔X and meet ⊓X. A subset X is finitely bounded iff every finite subset of X has an upper bound. Note that D does not necessarily have a bottom element.

An prime element of D is an element d s.t. d ⊑ ⊔X ⇒ ∃x ∈ X.d ⊑ x for any non-empty finitely bounded subset X. We will denote the set of prime elements of D by D_{p}.

D is called prime algebraic iff ∀d ∈ D.({d′ ∈ D_{p}|d′ ⊑ d} ≠ ∅ & d = ⊔{d′ ∈ D_{p}|d′ ⊑ d}).

A finite element of D is an element d s.t. d ⊑ ⊔X ⇒ ∃x ∈ X.d ⊑ x for any directed subset X. We will denote the set of finite elements of D by D_{o}.

D is called finitary iff ∀d ∈ D_{o}.|{d′ ∈ D|d′ ⊑ d}| < ∞

A pre dI domain is a finitary prime algebraic domain. A dI domain is a pre dI domain with a bottom element.

We will denote the set of minimal elements of D by D_{m}.

Note that each element in a pre dI domain has exactly one minimal element below it. This entails that a pre dI domain can be considered as a (not necessarily finite) sum of dI domains.

Definition 2.2 A monotone function f : D → E between pre dI domains is called stable iff f(⊓X) = ⊓f(X) for any non-empty finitely bounded subset X. A monotone function f : D → E between pre dI domains is called affine iff f(⊔X) = ⊔f(X) for any non-empty finitely bounded subset X. We will call an affine function f linear if both D and E are dI domains and f(⊥) =⊥.

Definition 2.3 Let predI_{s} be the category of pre dI domains and continuous stable functions, predI_{a} the category of pre dI domains and affine stable functions, and dI_{l} the category of dI domains and linear stable functions.

Proposition 2.4 Let f : D → E be a continuous function between two pre dI domains s.t. e ⊑ f(d) where d is arbitrary and e is finite. We can then find a finite minimal d′ ⊑ d with the property that e ⊑ f(d′). If f moreover is stable, then d′ is the least d′′ ⊑ d such that e ⊑ f(d′′).

Proof. Assume that f : D → E be a continuous function s.t. e ⊑ f(d) where d is arbitrary and e is finite. We then have

f(d) = f(⊔{d′ ∈ D_{p}|d′ ⊑ d})
= f(⊔{d′ ∈ D_{o}|d′ ⊑ d})
= ⊔{f(d′)|d′ ∈ D_{o} & d′ ⊑ d}

The assumption that D is prime algebraic gives us the first equation, the second comes from the fact that D_{p} ⊆ D_{o}, and the third comes from continuity of f, and the fact that ⊔{d′ ∈ D_{o}|d′ ⊑ d} is directed. But e is finite and {f(d′)|d′ ∈ D_{o} & d′ ⊑ d} is directed, so e ⊑ ⊔{f(d′)|d′ ∈ D_{o} & d′ ⊑ d} entails that there is at least one finite d′ ⊑ d such that e ⊑ f(d′). Now, we can pick a minimal finite d′ ⊑ d with that property because D is finitary and because any element below a finite element is finite. Assume moreover that f is stable and d′′ ⊑ d such that e ⊑ f(d′′), then e ⊑ f(d′) ⊓ f(d′′) = f(d′ ⊓ d′′). But d′ ⊓ d′′ ⊑ d′ and d′ is minimal, so d′ = d′ ⊓ d′′. Thus, d′ ⊑ d′′. □

This motivates the following definition:

Definition 2.5 Let f : D → E be a continuous stable function. We define

T race(f) = {(d, e) ∈ D_{o} × E_{p}|e ⊑ f(d) & ∀d′ ⊑ d.(e ⊑ f(d′) ⇒ d = d′)}

In what follows, X ↑ means that X has an upper bound. There is a close connection between functions and traces:

Theorem 2.6 Let {(d_{i}, e_{i})|i ∈ I} ⊆ D_{o} × E_{p} for some indexing set I s.t.

1. ∀d ∈ D.∃i ∈ I.d_{i} ⊑ d

2. ∀J ⊆_{fin} I.({d_{j}|j ∈ J}↑⇒ {e_{j}|j ∈ J}↑)

3. ∀i, j ∈ I.(d_{i}↑d_{j} & e_{i} = e_{j}) ⇒ d_{i} = d_{j}

4. ∀i ∈ I.∀e ∈ D_{p}.e ⊑ e_{i} ⇒ ∃j ∈ I.(e_{j} = e & d_{j} ⊑ d_{i})

Then the function f : D → E defined as

f(d) = ⊔{e|∃d′ ⊑ d.∃i ∈ I.(d′, e) = (d_{i}, e_{i})}

is a continuous stable function, and conversely, if f : D → E is a continuous stable function, then T race(f) has the above mentioned properties. Moreover, the operations are each others inverses.

Proof. If {(d_{i}, e_{i})|i ∈ I} has the mentioned properties, then it is straightforward to check that f is a continuous stable function. Conversely, let {(d_{i}, e_{i})|i ∈ I} = T race(f) for some continuous stable function f. If d ∈ D, then ∃e ∈ E_{p}.e ⊑ f(d) because E is prime algebraic. We can then find a finite minimal d′ ⊑ d s.t. e ⊑ f(d′), that is, (d′, e) ∈ T race(f), cf. Proposition 2.4. Thus, 1 is proved. 2 is obvious. Assume that d_{i}↑ d_{j} & e_{i} = e_{j}. Then f(d_{i} ⊓ d_{j}) = f(d_{i}) ⊓ f(d_{j}) and so e_{i}, e_{j} ⊑ f(d_{i} ⊓ d_{j}), which entails that d_{i} = d_{i} ⊓ d_{j} = d_{j}. This proves 3. Assume that e ⊑ e_{i} where e ∈ D_{p}. Then e ⊑ f(d_{i}), so we can find a finite minimal d′ ⊑ d_{i} s.t. e ⊑ f(d′), that is, (d′, e) ∈ T race(f), cf. Proposition 2.4. This proves 4. It is straightforward to check that the operations are each others inverses. □

From now on, we shall frequently identify a continuous stable function with its trace. There is a nice way of seeing whether a function is affine or not by looking at its trace:

Proposition 2.7 Let f : D → E be a continuous stable function. Then π_{0}(f) ⊆ D_{p} iff f is affine.

Proof. Assume that π_{0}(f) ⊆ D_{p}, and let X be non-empty finitely bounded. We obviously have ⊔f(X) ⊑ f(⊔X). Conversely, if e ∈ E_{p} such that e ⊑ f(⊔X), then there exists a d ∈ E_{o} such that (d, e) ∈ f and d ⊑ ⊔X, cf. Theorem 2.6. But d ∈ E_{p}, cf. the assumption that π_{0}(f) ⊆ D_{p}. This entails that there exists a x ∈ X such that d ⊑ x, and thus, e ⊑ f(x) ⊑ f(⊔X). We conclude that f(⊔X) ⊑ ⊔f(X). Conversely, assume that f is affine, and let (d, e) ∈ f. Then e ⊑ f(d). But f(d) = f(⊔{d′ ∈ D_{p}|d′ ⊑ d}) which is equal to ⊔{f(d′)|d′ ∈ D_{p} & d′ ⊑ d} because f is assumed to be affine. This entails that there exists a d′ ∈ D_{p} such that d′ ⊑ d and e ⊑ f(d′). We conclude that d = d′, because d is minimal, and thus d ∈ D_{p}. □

The following two results about composition of functions are very useful:

Theorem 2.8 Let f : C → D and g : D → E be continuous stable functions. Then

f; g = {(c, e)|∃(c_{1}, d_{1}), ..., (c_{n}, d_{n}) ∈ f.{c_{1}, ..., c_{n}}↑ & c = ⊔_{1≤i≤n}c_{i} & (⊔_{1≤i≤n}d_{i}, e) ∈ g}

Proof. First note that Theorem 2.6 entails that {d_{1}, ..., d_{n}}↑. Now, assume that (c, e) ∈ f; g. Then e ⊑ g(f(c)) entails that there exists a d ⊑ f(c) such that (d, e) ∈ g, cf. Proposition 2.4. Now, let {d_{1}, ..., d_{n}} = {d′ ∈ D_{p}|d′ ⊑ d}. Then we have for each i ∈ {1, ..., n} that d_{i} ⊑ f(c) entails that there exists a c_{i} ⊑ c such that (c_{i}, d_{i}) ∈ f, cf. Proposition 2.4. Thus, ⊔_{1≤i≤n}c_{i} ⊑ c and ⊔_{1≤i≤n}d_{i} = d, which entails that e ⊑ g(f(⊔_{1≤i≤n}c_{i})), cf. Theorem 2.6. We conclude that c = ⊔_{1≤i≤n}c_{i}, because c is minimal. Conversely, assume that (c_{1}, d_{1}), ..., (c_{n}, d_{n}) ∈ f such that {c_{1}, ..., c_{n}} ↑ and (⊔_{1≤i≤n}d_{i}, e) ∈ g. We have e ⊑ g(f(⊔_{1≤i≤n}c_{i})), cf. Theorem 2.6. Now, assume that we have a c ⊑ ⊔_{1≤i≤n}c_{i} such that e ⊑ g(f(c)). This entails that there exists a d ⊑ f(c) such that (d, e) ∈ g, cf. Proposition 2.4. But d ⊑ f(c) ⊑ f(⊔_{1≤i≤n}c_{i}) and ⊔_{1≤i≤n}d_{i} ⊑ f(⊔_{1≤i≤n}c_{i}), that is, d↑ ⊔_{1≤i≤n}d_{i}, which entails that d = ⊔_{1≤i≤n}d_{i}, cf. Theorem 2.6. Then we have for each i ∈ {1, ..., n} that d_{i} ⊑ f(c) entails that there exists a c′_{i} ⊑ c such that (c′_{i}, d_{i}) ∈ f, cf. Proposition 2.4. But c′_{i} ⊑ c ⊑ ⊔_{1≤i≤n}c_{i} and c_{i} ⊑ ⊔_{1≤i≤n}c_{i}, that is, c′_{i}↑ c_{i}, which entails that c′_{i} = c_{i}, cf. Theorem 2.6. So ⊔_{1≤i≤n}c′_{i} ⊑ c ⊑ ⊔_{1≤i≤n}c_{i} entails that c = ⊔_{1≤i≤n}c_{i}, and we conclude that (⊔_{1≤i≤n}c_{i}, e) ∈ f; g. □

Corollary 2.9 Let f : C → D and g : D → E be continuous stable functions. Assume moreover that g is affine. Then

f; g = {(c, e)|∃d ∈ D.(c, d) ∈ f & (d, e) ∈ g}

that is, the trace of the composition is equal to the traces composed as relations.

Proof. Assume that (c_{1}, d_{1}), ..., (c_{n}, d_{n}) ∈ f such that {c_{1}, ..., c_{n}}↑ and (⊔_{1≤i≤n}d_{i}, e) ∈ g. The function g is affine, so ⊔_{1≤i≤n}d_{i} ∈ D_{p}, cf. Proposition 2.7, which entails that there exists a q ∈ {1, ..., n} such that ⊔_{1≤i≤n}d_{i} = d_{q}. But then c_{i} ⊑ c_{q} for every i ∈ {1, ..., n}, cf. Theorem 2.6, and we conclude that ⊔_{1≤i≤n}c_{i} = c_{q}. □

3 The category predI_{a} is a model of IAL

3.1 Definition of categorical models of ILL and IAL

In [BBdPH92] proof-theoretic considerations are used to derive axioms for a category modelling multiplicative ILL. We take the resulting model as canonical:

Definition 3.1 A linear category is a symmetric monoidal closed category (C, I, ⊗, ⊸) equipped with

• A symmetric monoidal comonad (!, ε, δ, m, m_{I}).

• Monoidal natural transformations e :!(−) → I and d :!(−) →!(−)⊗!(−) s.t. 1. e_{A} and d_{A} are maps of coalgebras,

2. e_{A} and d_{A} give the free coalgebra (!A, δ) structure of a cocommutative comonoid,

3. maps between free coalgebras are maps between cocommutative comonoids.

Remark. The assumption that the comonad is symmetric monoidal means that ! is a symmetric monoidal functor and ε and δ are monoidal natural transformations. When assuming the natural transformations e and d to be monoidal, we are assuming the functors I and !(−)⊗!(−) to have the obvious monoidal structure induced by the monoidal structure on !. Hence, the assumption that the natural transformation e is monoidal amounts to commutativity of the following diagrams:

[figure: !A⊗!B; m_{A,B}; !(A ⊗ B); I ⊗ I; e_{A} ⊗ e_{B}; ≅; I; e_{A⊗B}; I; m_{I}; !I; I; I; e_{I}]

The assumption that the natural transformation d is monoidal amounts to commutativity of the following diagrams:

[figure: !A⊗!B; m_{A,B}; !(A ⊗ B); !A⊗!A⊗!B⊗!B; d_{A} ⊗ d_{B}; Id⊗ ≅ ⊗Id; !A⊗!B⊗!A⊗!B; m_{A,B} ⊗ m_{A,B}; !(A ⊗ B)⊗!(A ⊗ B); d_{A⊗B}]

I  m_{I}  ^{}!I
[figure: ≅]
I ⊗ I
[figure: m_{I} ⊗ m_{I}]
!I⊗!I^{d_{I} ^{}}

It can be shown that (I, m_{I}) and (!A⊗!A, (δ_{A}⊗δ_{A}); m_{!A,!A}) are coalgebras. The assumption that e_{A} is a map of coalgebras amounts to e_{A} being a map from (!A, δ_{A}) to (I, m_{I}), and the assumption that d_{A} is a map of coalgebras amounts to d_{A} being a map from (!A, δ_{A}) to (!A⊗!A, (δ_{A} ⊗ δ_{A}); m_{!A,!A}).

Definition 3.2 A model of ILL is a linear category with finite products (×, 1) and finite sums (+, 0). A model of IAL is a model of ILL where I ≅ 1.

It is easy to see that the arguments found in [BBdPH92] for a linear category can be extended to the full ILL, and to IAL. For example will the presence of a uniquely determined map A → I for any object A in a model of IAL enables us to interpret the weakening rule in an appropriate way.

3.2 predI_{a} is a model of IAL

Given X ⊆ D we define ⌜d⌝^{X} = {d′ ∈ X|d′ ⊑ d}. First of all, we need a symmetric monoidal structure on predI_{a}:

Definition 3.3 Let f : D → D′ and g : E → E′ be maps in predI_{a}. We define a bifunctor ⊗ : predI_{a} × predI_{a} → predI_{a} as follows:

D ⊗ E = ({t ⊆ D_{p} × E_{p}|(π_{1}(t))↑ & (π_{2}(t))↑ & t ≠ ∅ & t is down-closed }, ⊆)
f ⊗ g = {(⌜(d, e)⌝, ⌜(d′, e′)⌝)|(d, d′) ∈ f & (e, e′) ∈ g}

Proposition 3.4 The bifunctor ⊗ together with the pre dI domain I = ({⊥}, =) give symmetric monoidal structure to predI_{a}.

Note that

(D ⊗ E)_{o} = {t ∈ D ⊗ E||t| < ∞}
(D ⊗ E)_{p} = {⌜(d, e)⌝|d ∈ D_{p} & e ∈ E_{p}}
(D ⊗ E)_{m} = {{(d, e)}|d ∈ D_{m} & e ∈ E_{m}}

Hence, (D ⊗E)_{p} ≅ D_{p} ×E_{p} ordered coordinatewise. This is the key in showing that every functor (−) ⊗ D has a right adjoint D ⊸ (−).

Definition 3.5 Given two pre dI domains D and E, we define a new pre dI domain as follows:

D ⊸ E = (predI_{a}(D, E), ⊆)

Thus, we take all affine stable functions from D to E and order them by inclusion. It is straightforward to check that this is a pre dI domain. The following lemma gives us a handle on the prime elements:

Lemma 3.6 f ∈ (D ⊸ E)_{p} & f ≠ ∅ iff f ∈ D ⊸ E & ∃(d, e) ∈ f.f = f ∩ (⌜(d, e)⌝ ∪ D_{m} × E_{m})

The lemma induces the following definition:

Definition 3.7 The lemma says that if f ∈ (D ⊸ E)_{p} and f ∉ (D ⊸ E)_{m}, then there is a uniquely determined element (d, e) ∈ f such that f = f ∩ (⌜(d, e)⌝ ∪ D_{m} × E_{m}). We will denote this element by top(f).

Now, we want to extend the function that sends the object E into the object D ⊸ E to a functor, which is right adjoint to (−) ⊗ D. It is sufficient for every object E to give a map eval_{E,D} : (D ⊸ E) ⊗ D → E with the property that for every f : C ⊗ D → E, there exists a uniquely determined g : C → (D ⊸ E) which makes the following diagram commute:

(*) [figure: C ⊗ D; g ⊗ D; E; f; eval_{E,D}; (D ⊸ E) ⊗ D]

Thus, we define:

Definition 3.8 Given objects E and D, we define the map eval_{E,D} : (D ⊸ E) ⊗ D → E as follows:

eval_{E,D} =
{(⌜(f, d)⌝, e)|f ∈ ((D ⊸ E)_{p} \ (D ⊸ E)_{m}) & top(f) = (d, e)}∪
{(⌜(f, d)⌝, e)|f ∈ (D ⊸ E)_{m} & (d, e) ∈ f}

Theorem 3.9 For every map f : C ⊗ D → E, there exists a uniquely determined map g : C → (D ⊸ E) which makes (*) commute. The map g is given by

g = {(c, ∥ (d, e) ∥_{c}^{f})|(⌜(c, d)⌝, e) ∈ f}

where

∥ (d, e) ∥_{c}^{f}=
{(d′, e′)|∃c′ ⊑ c.d′ ⊑ d & e′ ⊑ e & (⌜(c′, d′)⌝, e′) ∈ f}∪
{(d′, e′)|∃c′ ⊑ c.({(c′, d′)}, e′) ∈ f}

Hence, we have specified a right adjoint D ⊸ (−) to every functor (−) ⊗ D such that eval_{(−),D} is counit.

Now, we want to have a comonad on predI_{a}. The forgetful functor U from predI_{a} to predI_{s} has a left adjoint !. This adjunction induces a comonad on predI_{a}, namely

(!U, ε :!U → Id,!ηU :!U →!U!U)

where Id is the identity functor on predI_{a}, η is the unit, and ε is the counit of the adjunction. We will first define an operation on pre dI domains as follows:

Definition 3.10 Given a pre dI domain D, we define a new pre dI domain !D as follows:

!D = ({t ⊆ D_{o}|t↑ & t ≠ ∅ & t is down-closed }, ⊆)

Note that

(!D)_{o} = {t ∈!D||t| < ∞}
(!D)_{p} = {⌜d⌝|d ∈ D_{o}}
(!D)_{m} = {{d}|d ∈ D_{m}}

Hence, (!D)_{p} ≅ D_{o} with the inherited ordering. This is the key in showing that the forgetful functor from predI_{a} to predI_{s} has a left adjoint. Now, ! is a function from objects in predI_{s} to objects in predI_{a}, and we want to extend this function to a functor which is left adjoint to the forgetful functor.

It is sufficient for every pre dI domain D to give a continuous stable function η_{D} : D →!D with the property that for every continuous stable function f : D → E there exists a uniquely determined affine stable function g :!D → E which makes the following diagram commute:

(**) [figure: D; η_{D}; !D; g; E; f]

Thus, we define:

Definition 3.11 Given an object D, we define the continuous stable function η_{D} : D →!D as follows:

η_{D} = {(d, ⌜d⌝)|d ∈ D_{o}}

Theorem 3.12 For every continuous stable function f : D → E, there exists a uniquely determined affine stable function g :!D → E which makes (**) commute. The function g is given by

g = {(⌜d⌝, e)|(d, e) ∈ f}

Hence, we have specified a left adjoint ! to the forgetful functor such that η is unit. We will rename the induced comonad on predI_{a} to

(!, ε :! → Id, δ :! →!!)

It will be useful to state the constructions in explicit terms:

Given a continuous stable function f : D → E, the affine stable function !f :!D →!E is defined as follows:

!f = {(⌜d⌝, ⌜e⌝)|d ∈ D_{o} & e ∈ E_{o} & e ⊑ f(d) & ∀d′ ⊑ d.(e ⊑ f(d′) ⇒ d = d′)}

The components ε_{D} :!D → D and δ_{D} :!D →!!D of the natural transformations ε and δ are defined as follows:

\begin{matrix}ε_{D} = \{(⌜d⌝, d)|d ∈ D_{p}\} \\ δ_{D} = \{(⌜d_{1} ⊔ ... ⊔ d_{n}⌝, ⌜(⌜\{d_{1}, ..., d_{n}\}⌝)⌝)|d_{1}, ..., d_{n} ∈ D_{p} & \{d_{1}, ..., d_{n}\}↑\} \end{matrix}

We moreover want that the comonad (!, ε, δ) is symmetric monoidal which means that ! is a symmetric monoidal functor and ε and δ are monoidal natural transformations. That ! is symmetric monoidal means that it comes equipped with a map m_{I} : I →!I and a natural transformation m :!(−)⊗!(+) →!(−⊗+), which matches the symmetric monoidal structure, that is, makes certain diagrams commute. See the appendix. This motivates the following definition:

Definition 3.13 We define a map m_{I} : I →!I, and a natural transformation m with components m_{D,E} :!D⊗!E →!(D ⊗ E) as follows:

\begin{matrix}m_{I} = \{(⊥, \{⊥\})\} \\ m_{D,E} = \{(⌜(⌜⊔(π_{1}(t))⌝, ⌜⊔(π_{2}(t))⌝)⌝, ⌜t⌝)|t ∈ (D ⊗ E)_{o}\} \end{matrix}

Theorem 3.14 The map m_{I} together with the natural transformation m gives symmetric monoidal structure to the functor ! s.t. ε and δ are monoidal natural transformations.

Finally, we want to have monoidal natural transformations e :!(−) → I and d :!(−) →!(−)⊗!(−), which motivates the following definition:

Definition 3.15 We define natural transformations e and d with components e_{D} :!D → I and d_{D} :!D →!D⊗!D as follows:

\begin{matrix}e_{D} = \{(\{d\}, ⊥)|d ∈ D_{m}\} \\ d_{D} = \{(⌜d ⊔ d′⌝, ⌜(⌜d⌝, ⌜d′⌝)⌝)|d, d′ ∈ D_{o} & d↑d′\} \end{matrix}

Proposition 3.16 The natural transformations e and d are monoidal.

The following three propositions say that the extra conditions on e_{D} and d_{D} are satisfied:

Proposition 3.17 The maps e_{D} and d_{D} are maps of coalgebras, that is, e_{D} : (!D, δ_{D}) → (I, m_{I}) and d_{D} : (!D, δ_{D}) → (!A⊗!A, (δ_{A} ⊗ δ_{A}); m_{!A,!A}).

Proposition 3.18 The maps e_{D} and d_{D} give the free coalgebra (!D, δ_{D}) the structure of a cocommutative comonoid, that is, each (!D, e_{D} :!D → I, d_{D} :!D →!D⊗!D) is a cocommutative comonoid.

Proposition 3.19 Maps between free coalgebras are maps between cocommutative comonoids, that is, if f : (!D, δ_{D}) → (!E, δ_{E}) then f : (!D, e_{D}, d_{D}) → (!E, e_{E}, d_{E}).

Now, it is easy to check that predI_{a} has finite products and finite sums in the usual way, hence it is a model of ILL. Moreover, the unit I of the tensor product ⊗ is obviously a terminal object, hence predI_{a} is a model of IAL.

4 A strong monad on the category predI_{a}

The forgetful functor U from dI_{l} to predI_{a} has a left adjoint (−)_{⊥}. This adjunction induces a monad on predI_{a}, namely

(U(−)_{⊥}, lift : Id → U(−)_{⊥}, Udown′(−)_{⊥} : U(−)_{⊥}U(−)_{⊥} → U(−)_{⊥})

where Id is the identity functor on predI_{a}, lift is the unit, and down′ is the counit of the adjunction. We will first define a function (the lift construction) from pre dI domains to dI domains as follows. The definition assumes an injective function ⌞−⌟_{D} on D, and an element ⊥_{D} different from all elements in the image of ⌞−⌟_{D}.

Definition 4.1 Given a pre dI domain D, we define a dI domain D_{⊥} with the underlying set {⌞d⌟|d ∈ D} ∪ {⊥}. The order on D_{⊥} is the order inherited from D extended s.t. ⊥ is a bottom element.

Note that (D_{⊥})_{p} = {⌞d⌟|d ∈ D_{p}} ∪ {⊥}. This is the key in showing that the forgetful functor from dI_{l} to predI_{a} has a left adjoint. Now, (−)_{⊥} is a function from objects in predI_{a} to objects in dI_{l}, and we want to extend this function to a functor which is left adjoint to the forgetful functor.

It is sufficient for every pre dI domain D to give an affine stable function lift_{D} : D → D_{⊥} with the property that for every affine stable function f : D → E where E is a dI domain, there exists a uniquely determined linear stable function g : D_{⊥} → E which makes the following diagram commute:

(***) [figure: D; lift_{D}; D_{⊥}; g; E; f]

Thus, we define:

Definition 4.2 Given an object D, we define the affine stable function lift_{D} : D → D_{⊥} as follows:

lift_{D} = {(d, ⌞d⌟)|d ∈ D_{p}} ∪ {(d, ⊥)|d ∈ D_{m}}

Theorem 4.3 For every affine stable function f : D → E, where E is a dI domain, there exists a uniquely determined linear stable function g : D_{⊥} → E which makes (***) commute. The function g is given by

g = {(⌞d⌟, e)|(d, e) ∈ f & e ≠⊥} ∪ {(⊥, ⊥)}

Hence, we have specified a left adjoint (−)_{⊥} to the forgetful functor such that lift is unit. We will rename the induced monad on predI_{a} to

((−)_{⊥}, lift : Id → (−)_{⊥}, down : (−)_{⊥⊥} → (−)_{⊥})

It will be useful to state the constructions in explicit terms:

Given an affine stable function f : D → E, the linear stable function f_{⊥} : D_{⊥} → E_{⊥} is defined as follows:

f_{⊥} = {(⌞d⌟, ⌞e⌟)|(d, e) ∈ f} ∪ {(⊥, ⊥)}

The component down_{D} : D_{⊥⊥} → D_{⊥}) of the natural transformations down is defined as follows:

down_{D} = {(⌞⌞d⌟⌟, ⌞d⌟)|d ∈ D_{p}} ∪ {(⊥, ⊥)}

Thus, we have a monad on predI_{a}. It turns out that the monad is strong w.r.t. the symmetric monoidal structure, that is, there is a “strength” natural transformation t : (−) ⊗ (+)_{⊥} → (− ⊗ +)_{⊥} such that certain diagrams commute. See the appendix.

Definition 4.4 We define a natural transformation t with components t_{D,E} : D ⊗ E_{⊥} → (D ⊗ E)_{⊥} as follows:

t_{D,E} =
{(⌜(d, ⌞e⌟)⌝, ⌞(⌜(d, e)⌝)⌟)|d ∈ D_{p} & e ∈ E_{p}}∪
{(⌜(d, ⊥)⌝, ⊥)|d ∈ D_{m}}

Theorem 4.5 The natural transformation t makes the monad ((−)_{⊥}, lift, down) strong w.r.t. the symmetric monoidal structure.

5 Fixpoints in the category predI_{a}

5.1 Categorical fixpoints as usual

The definitions and results concerning fixpoints and fixpoint operators in this subsection can also be found in [Poi92]. To start things off, we will state a definition of fixpoints in a category with finite products. In what follows, Δ_{A} : A → A × A is the diagonal map.

Definition 5.1 A category C with finite products has fixpoints iff for every map f : A × B → B there exists a specified fixpoint f† : A → B with the property that

f† = [A ^{Δ_{A}}^{}A × A ^{Id×f†}^{}A × B ^{f}^{}B]

Note how the diagonal map is used to copy parameters. We can deal with fixpoint operators if the category is closed w.r.t. the product structure:

Definition 5.2 A cartesian closed category C has fixpoint operators iff for every object B there is an arrow Y_{B} : [B ⇒ B] → B with the property that for every f : A × B → B the map curry(f); Y_{B} is a fixpoint of f.

Fixpoints and fixpoint operators are related cf. the following result:

Proposition 5.3 A cartesian closed category C has fixpoints iff it has fixpoint operators.

5.2 Categorical fixpoints in models of ILL and IAL

Proofs of the results in this subsection can be found in [Brab]. I will now consider fixpoints in a linear context. The categorical considerations in the following part of the paper applies to models of ILL, and thus to models of IAL. We can not use the previous definition of fixpoints because it assumes the presence of finite products.

Definition 5.4 Let (C, I, ⊗) be a monoidal category equipped with a comonad (!, ε, δ), and with a natural transformation d having components: d_{A} :!A →!A⊗!A. We say that C has linear fixpoints iff for every map f :!A⊗!B → B there exists a specified linear fixpoint f^{♯} :!A → B with the property that

f^{♯} = [!A ^{d_{A}}^{}!A⊗!A ^{Id⊗γ(f^{♯})}^{}!A⊗!B ^{f}^{}B]

where γ : C(!A, B) → C(!A,!B) is the coKleisli operator, that is,

γ(h) = [!A ^{δ_{A}}^{}!!A ^{!h}^{}!B]

It is simply an extension of the definition of fixpoints in a category with finite products to a linear context, where we have only a “diagonal map” d_{A} for objects of the shape !A. We can deal with linear fixpoint operators if our category is closed w.r.t. the monoidal structure:

Definition 5.5 Let (C, I, ⊗, ⊸) be a monoidal closed category equipped with a comonad (!, ε, δ), and with a natural transformation d having components d_{A} :!A →!A⊗!A. We say that C has linear fixpoint operators iff for every object B there is an arrow Y_{B}^{lin} :!(!B ⊸ B) → B with the property that for every f :!A⊗!B → B the map γ(curry(f)); Y_{B}^{lin} is a linear fixpoint of f.

Linear fixpoints and linear fixpoint operators are under appropriate circumstances related in a way analogous to the way fixpoints are related to fixpoint operators.

Proposition 5.6 A linear category has linear fixpoints iff it has linear fixpoint operators.

Now, the definition of linear fixpoints can be explained in terms of fixpoints in the category of free coalgebras. Given a category C equipped with a comonad (!, ε, δ), the coEilenberg-Moore category, C^{!} is the category of coalgebras, and the category of free coalgebras is the full subcategory of C^{!}, whose objects are free coalgebras, that is, coalgebras of the type (!A, δ). Recall that we have an adjunction U^{!} ⊣ F^{!} between C^{!} and C. The forgetful functor U^{!} : C^{!} → C simply forgets the coalgebra structure, while the free functor F^{!} : C → C^{!} takes any object A to the free coalgebra (!A, δ). The adjunction induces the following natural bijection between maps:

ϕ_{(C,h),A} : C^{!}((C, h), (!A, δ)) ≅ C(C, A)

where (C, h) is a coalgebra, and A is an object of C. The bijection is given by ϕ(f) = (f; ε_{A}) : C → A and ϕ^{−1}(g) = h; !g : (C, h) → (!A, δ).

In [Bie94] it is shown that C^{!} w.r.t. a symmetric monoidal category (C, I, ⊗) equipped with a symmetric monoidal comonad (!, ε, δ, m, m_{I}) has an induced symmetric monoidal structure; the unit I of the tensor product is given by (I, m_{I}), and given two coalgebras (A, k) and (B, h), their tensor product (A, k) ⊗ (B, h) is the coalgebra (A ⊗ B, (k ⊗ h); m_{A,B}). If moreover the category is a linear category (not necessarily with ⊸, that is, (−) ⊗ A does not necessarily have a right adjoint A ⊸ (−)), then the symmetric monoidal structure on C^{!} is a finite product structure, that is, I is a terminal object, and ⊗ is a binary product.

Theorem 5.7 Let C be a linear category (not necessarily with ⊸), then

h : (!A, δ) → (!B, δ) is fixpoint of f : (!A, δ) ⊗ (!B, δ) → (!B, δ) iff
ϕ(h) :!A → B is linear fixpoint of ϕ(f) :!A⊗!B → B

It is obvious that if the the category of free coalgebras is closed under finite products, that is, the terminal object (I, m_{I}) is isomorphic to a free coalgebra, and given two free coalgebras (!A, δ) and (!B, δ), their tensor product (A, k) ⊗ (B, h) is isomorphic to a free coalgebra, then it inherits the finite products from the ambient category. This leads to the following corollary:

Corollary 5.8 Let C be a linear category (not necessarily with ⊸) s.t. the category of free coalgebras is closed under finite products. Then the category of free coalgebras has fixpoints iff C has linear fixpoints.

If the category of free coalgebras w.r.t. a linear category is closed under finite products then it has finite products, as mentioned above. In [Bie94] it is shown that the category of free coalgebras moreover is cartesian closed. Given two free coalgebras (!A, δ) and (!B, δ), their exponential object (!A, δ) ⇒ (!B, δ) is given by the free coalgebra (!(!A ⊸ B), δ). Hence:

Theorem 5.9 Let C be a linear category s.t. the category of free coalgebras is closed under finite products. Then the category of free coalgebras has fixpoint operators iff C has linear fixpoint operators.

This result can also be derived more explicitly, namely as a straightforward consequence of the following theorem:

Theorem 5.10 Let C be a linear category s.t. the category of free coalgebras is closed under finite products in C^{!}. Then Y_{(!B,δ)} : (!B, δ) ⇒ (!B, δ) → (!B, δ) is a fixpoint operator in the category of free coalgebras iff ϕ(Y_{(!B,δ)}) :!(!B ⊸ B) → B is a linear fixpoint operator in C.

Now, under which circumstances is the category of free coalgebras closed under finite products? The following observation induces a sufficient condition:

Proposition 5.11 Let C be a category with a comonad (!, ε, δ). If C has terminal object 1 then (!1, δ) is a terminal object in C^{!}, and if C has binary product × then (!(A × B), δ) is a binary product of (!A, δ) and (!B, δ) in C^{!}.

This has the consequence that if C is a model of ILL as defined above, then the category of free coalgebras is closed under finite products. Note that the category of free coalgebras is equivalent to the coKleisli category; it is straightforward to check that the comparison functor from C_{!} to C^{!} is an equivalence of categories when considered as a functor from C_{!} to the category of free coalgebras.

5.3 Fixpoints in predI_{a}

The previous discussion on (linear) fixpoints supplied us with a characterisation of linear fixpoints; the category of free coalgebras induced by predI_{a} is cartesian closed, and predI_{a} has linear fixpoint operators if and only if the category of free coalgebras has fixpoints in the usual sense. But the category of free coalgebras is equivalent to predI_{a!}, and it is easy to see that predI_{a!} is isomorphic to predI_{s}. Now, according to [HP90], a cartesian closed category with fixpoints and finite sums is equivalent to the category with one object and one arrow. So predI_{s} cannot have fixpoints since it is cartesian closed and has finite sums. This entails that predI_{a} cannot have linear fixpoints. But if we cut our model down to the full subcategory of dI domains and affine stable functions, dI_{a} we still have a model of IAL, except that we do not have finite sums. Neither does the category of dI domains and continuous stable functions, dI_{s} have finite sums. This category is equivalent to the category of free coalgebras induced by the comonad on dI_{a}, so it is cartesian closed; the finite product structure is given in the usual way, and the exponential object [A ⇒ B] is the set of traces of continuous stable functions ordered by inclusion. Moreover, we have fixpoint operators in dI_{s}:

Theorem 5.12 Given a dI domain A, the continuous stable function Y_{A} : [A ⇒ A] → A defined as Y_{A}(f) = ⊔_{n∈ω}f^{n}(⊥) is a fixpoint operator.

This entails that we have linear fixpoint operators in dI_{a}.

Acknowledgments. I am grateful to my supervisor, Glynn Winskel, for his guidance and encouragement. My work has benefitted from conversations with members of the CLICS group in Cambridge. Paul Taylor’s macros are used in preparing this paper.

References

[BBdPH92] N. Benton, G. Bierman, V. de Paiva, and M. Hyland. Term assignment for intuitionistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, 1992.

[Bie94] Gavin Bierman. On Intuitionistic Linear Logic. PhD thesis, Computer Laboratory, University of Cambridge, 1994.

[Braa] T. Braüner. A general adequacy result for a linear functional language. Presented at MFPS ’94.

[Brab] T. Braüner. The girard translation extended with recursion. Accepted to CSL ’94, Warsaw, Poland.

[HP90] H. Huwig and A. Poigne. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73, 1990.

[Jac] B. Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic (to appear).

[Mac71] S. Mac Lane. Categories for the Working Matematician. Springer-Verlag, 1971.

[Mog89] E. Moggi. Computational lambda-calculus and monads. In 4th LICS Conference. IEEE, 1989.

[Poi92] A. Poigne. Basic category theory. In S. Abramsky et al, editor, Handbook of Logic in Computer Science. Oxford University Press, 1992.

[Win87] G. Winskel. Event structures. In Lecture Notes in Computer Science, volume 255. Springer-Verlag, 1987.

[Zha93] G.-Q. Zhang. Some monoidal closed categories of stable domains and event structures. Mathematical Structures in Computer Science, 3, 1993.

A Appendix, categorical prerequisites

I will now review some fundamental (and relevant) definitions and results in category theory. Most of them can be found (implicitly or explicitly) in [Mac71].

A.1 Monoidal categories etc.

Definition A.1 A monoidal category is a 6-tuple (C, I, ⊗, α, λ, ρ) where C is a category containing a neutral element I for a bifunctor ⊗ : C × C → C equipped with natural isomorphisms α, λ, ρ having components

α_{A,B,C} : A ⊗ (B ⊗ C) → (A ⊗ B) ⊗ C  λ_{A} : I ⊗ A → A  ρ_{A} : A ⊗ I → A

These are required to satisfy the socalled Kelly-Mac Lane equations, which are: the pentagon law (Id ⊗ α); α; (α ⊗ Id) = α; α, the triangle law α; (ρ ⊗ Id) = (Id ⊗ λ), and λ_{I} = ρ_{I}. Such a monoidal category is symmetric if there is an additional “symmetry” natural isomorphism γ with components

γ_{A,B} : A ⊗ B → B ⊗ A

satisfying γ; γ = Id, ρ = γ; λ , and α; γ; α = (Id ⊗ γ); α; (γ ⊗ Id).

A monoidal functor F from (C, I, ⊗, α, λ, ρ) to (C′, I′, ⊗′, α′, λ′, ρ′) is a functor F : C → C′ equipped with a map m_{I′} : I′ → F (I) and a natural transformation m : F (−) ⊗′ F (+) → F (−⊗+) which match the involved structure, that is, (Id⊗′m); m; F (α) = α′; (m⊗′Id); m, (m_{I′} ⊗′ Id); m; F (λ) = λ′, and (Id ⊗′ m_{I′}); m; F (ρ) = ρ′. It is a symmetric monoidal functor if additionally γ′; m = m; F (γ). F preserves the (symmetric) monoidal structure (or F is a morphism of (symmetric) monoidal categories) iff m_{I′} and m are isomorphisms.

A monoidal natural transformation between monoidal functors F, F′ : C → C′ is a natural transformation σ : F → F′ satisfying m; σ = (σ ⊗′ σ); m′ and m_{I′}; σ_{I} = m′_{I′}.

A (symmetric) monoidal closed category is a (symmetric) monoidal category where each functor (−) ⊗ A has a right adjoint; it will be denoted by A ⊸ (−).

Note that one obtains 2-categories of (symmetric) monoidal categories.

A.2 Monads etc.

Definition A.2 A monad ((−)_{⊥}, lift, down) on C is a functor (−)_{⊥} : C → C, and two natural transformations

lift : Id_{C} → (−)_{⊥} down : (−)_{⊥⊥} → (−)_{⊥}

s.t. the following diagrams commute:

[figure: (−)_{⊥⊥⊥}; down_{⊥}; (−)_{⊥⊥}; (−)_{⊥⊥}; down(−)_{⊥}; down; (−)_{⊥}; down; (−)_{⊥}; lift(−)_{⊥}; (−)_{⊥⊥}; lift_{⊥}; (−)_{⊥}; Id_{(−)_{⊥}}; Id_{(−)_{⊥}}; (−)_{⊥}; down]

Definition A.3 Let (C, I, ⊗, α, λ, ρ) be a monoidal category and ((−)_{⊥}, lift, down) a monad on C. The monad is called strong iff there is a “strength” natural transformation t : (−) ⊗ (+)_{⊥} → (− ⊗ +)_{⊥} s.t. the following diagrams commute:

[figure: A ⊗ (B ⊗ C_{⊥}); Id ⊗ t; A ⊗ (B ⊗ C)_{⊥}; t; (A ⊗ (B ⊗ C))_{⊥}; (A ⊗ B) ⊗ C_{⊥}; α; t; ((A ⊗ B) ⊗ C)_{⊥}; α_{⊥}; I ⊗ A_{⊥}; t; (I ⊗ A)_{⊥}; λ; A_{⊥}; λ_{⊥}]

[figure: A ⊗ B; Id ⊗ lift; A ⊗ B_{⊥}; lift; (A ⊗ B)_{⊥}; t; A ⊗ B_{⊥⊥}; t; (A ⊗ B_{⊥})_{⊥}; t_{⊥}; (A ⊗ B)_{⊥⊥}; A ⊗ B_{⊥}; Id ⊗ down; t; (A ⊗ B)_{⊥}; down]

A.3 Comonads etc.

Definition A.4 A comonad (!, ε, δ) on C is a functor ! : C → C, and two natural transformations

ε :! → Id_{C} δ :! →!!

s.t. the following diagrams commute:

[figure: !; δ; !!; !!; δ; δ!; !!!; !δ; !; Id_{!}; Id_{!}; !; ε!; !!; δ; !ε; !]

Definition A.5 Given a comonad (!, ε, δ) on C, one can define the coKleisli category, C_{!} as follows: the objects are the same as in C, the morphisms are given by C_{!}(A, B) = C(!A, B). If f : A → B is an arrow in C_{!}, then the corresponding arrow in C is denoted by f^{∗} :!A → B. Now, given f : A → B and g : B → C, arrows in C_{!}, their composition is defined to be (f; g)^{∗} = δ_{A}; !(f^{∗}); g^{∗} :!A → C. Given an object A, the unit is defined to be (Id_{A})^{∗} = ε_{A} :!A → A.

Recent Publications in the BRICS Report Series

RS-94-27 Torben Bra� uner. A Model of Intuitionistic Af�ne Logic from Stable Domain Theory (Revised and Expanded Version). September 1994. 19 pp. Full version of paper appearing in: ICALP ’94, LNCS 820, 1994.

RS-94-26 S�ren Riis. Count(q) versus the Pigeon-Hole Principle. August 1994. 3 pp.

RS-94-25 S�ren Riis. Bootstrapping the Primitive Recursive Functions by 47 Colors. August 1994. 5 pp.

RS-94-24 S�ren Riis. A Fractal which violates the Axiom of Determinacy. August 1994. 3 pp.

RS-94-23 S�ren Riis. Finitisation in Bounded Arithmetic. August 1994. 31 pp.

RS-94-22 Torben Bra� uner. A General Adequacy Result for a Linear Functional Language. August 1994. 39 pp. Presented at MFPS ’94.

RS-94-21 S�ren Riis. Count(q) does not imply Count(p). July 1994. 55 pp.

RS-94-20 Peter D. Mosses and Mart��n Musicante. An Action Semantics for ML Concurrency Primitives. July 1994. 21 pp. To appear in Proc. FME ’94 (Formal Methods Europe, Symposium on Industrial Bene�t of Formal Methods), LNCS, 1994.

RS-94-19 Jens Chr. Godskesen, Kim G. Larsen, and Arne Skou. Automatic Veri�cation of Real�Timed Systems Using Epsilon. June 1994. 8 pp. Appears in: Protocols, Speci�- cation, Testing and Veri�cation PSTV ’94.

RS-94-18 Sten Agerholm. LCF Examples in HOL. June 1994. 16 pp. To appear in: Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, 1994.

RS-94-17 Allan Cheng. Local Model Checking and Traces. June 1994. 30 pp.