BRICS RS-94-22 T. Bra� uner: A General Adequacy Result for a Linear Functional Language

BRICS

Basic Research in Computer Science

A General Adequacy Result for a Linear Functional Language

Torben Bra� uner

BRICS Report Series RS-94-22 ISSN 0909-0878 August 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 General Adequacy Result for a Linear Functional Language

Torben Braüner^{∗}

BRICS^{†}

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

Abstract

A main concern of the paper will be a Curry-Howard interpretation of Intuitionistic Linear Logic. It will be extended with recursion, and the resulting functional programming language will be given operational as well as categorical semantics. The two semantics will be related by soundness and adequacy results. The main features of the categorical semantics are that convergence/divergence behaviour is modelled by a strong monad, and that recursion is modelled by ”linear fixpoints” induced by CPO structure on the hom-sets. The ”linear fixpoints” correspond to ordinary fixpoints in the category of free coalgebras w.r.t. the comonad used to interpret the “of course” modality. Concrete categories from (stable) domain theory satisfying the axioms of the categorical model are given, and thus adequacy follows in these instances from the general result.

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

Contents

1 Introduction 4

2 A linear functional language, LTS_{+Rec} 5 2.1 The Curry-Howard isomorphism . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Definition of LTS_{+Rec} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Properties of LTS_{+Rec} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 The choice of rule for ! introduction . . . . . . . . . . . . . . . . . . . . . . 6 2.5 The choice of rule for recursion . . . . . . . . . . . . . . . . . . . . . . . . 7

3 Operational semantics of LTS_{+Rec} 8 3.1 Definition of the operational semantics . . . . . . . . . . . . . . . . . . . . 8 3.2 Properties of the operational semantics . . . . . . . . . . . . . . . . . . . . 8

4 General considerations about the categorical semantics 9 4.1 The connection to denotational semantics . . . . . . . . . . . . . . . . . . . 9 4.2 Initial assumptions about the interpretation . . . . . . . . . . . . . . . . . 10 4.3 Modelling convergence/divergence behaviour . . . . . . . . . . . . . . . . . 10 4.4 Two examples, the (⊗ − I) and (⊗ − E) rules . . . . . . . . . . . . . . . . 11

5 Categorical semantics of LTS_{+Rec} 13 5.1 Introduction to the category O . . . . . . . . . . . . . . . . . . . . . . . . 13 5.2 Definition of the categorical semantics . . . . . . . . . . . . . . . . . . . . 13 5.3 Properties of the categorical semantics . . . . . . . . . . . . . . . . . . . . 16

6 Fixpoints in a linear context 18 6.1 Fixpoints as usual . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.2 Linear fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.3 Generalisation of linear fixpoints . . . . . . . . . . . . . . . . . . . . . . . . 22

7 Concrete models 23 7.1 The category predI_{a} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 7.2 The category O . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

A Appendix, ILL in Natural Deduction style 27

B Appendix, ILL in Gentzen style 28

C Appendix, LTS_{+Rec} with categorical semantics 30

D Appendix, operational semantics for LTS_{+Rec} 33

E Appendix, proof of the Soundness Theorem 34

F Appendix, proof of the Approximation Lemma 35

G Appendix, categorical prerequisites 38 G.1 Monoidal categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 G.2 Monads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 G.3 Comonads . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

1 Introduction

Linear logic was discovered by J.-Y. Girard in 1987 and published in a now famous paper [Gir87]. In the abstract of this paper, it is stated that “a completely new approach to the whole area between constructive logics and computer science is initiated”. Since then, a lot of work has been done to corroborate this claim. The present paper will deal with a computational interpretation of Intuitionistic Linear Logic (ILL).

In [Abr90] the first Curry-Howard interpretation of ILL is given. The resulting system is essentially a refinement of the usual λ-calculus where the copying and discarding of values is written explicitly in the terms. One of the rules of this system has a deficiency that force ! to be isomorphic to !! in any reasonable categorical interpretation. It was in 1992 repaired by the authors of [BBdPH92] (and by the author of this paper) by changing the system in an appropriate way, and by discovering a Natural Deduction style presentation equivalent to the hitherto known Gentzen style presentation of ILL. This work settled the question about how to interpret ILL via the Curry-Howard isomorphism. The Natural Deduction style proof-rules will in the present paper be considered as type assignment rules for a programming language cf. Curry-Howard. Moreover, the system will extended with recursion (every decent programming language has recursion!), and given operational as well as categorical semantics such that the two semantics are related by soundness and adequacy results. Our categorical model is able to model convergence/divergence behaviour, and moreover, it deals with fixpoints in a linear context. We have devoted a section to show some results on fixpoints in a linear contexts and their relations to ordinary fixpoints.

Now, Girard worked with coherence spaces and stable maps and observed that the stable function space A ⇒ B can be decomposed into more basic operations, namely !A ⊸ B, where ! is an operation on coherence spaces, and ⊸ is the operation corresponding to formation of linear stable function space. To be more precise: 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, and the corresponding coherence space interpretation has since been considered canonical. Now, it turns out that the same phenomenon is present if we consider the category of pre dI domains and stable functions, predI_{s}, and the category of predI domains and affine stable functions, predI_{a}. The functor from predI_{a} to predI_{s} that forgets the affine nature has a left adjoint !. This induces a comonad on the symmetric monoidal closed category predI_{a} in the same way as we have a comonad on the symmetric monoidal closed category of coherence spaces and linear stable maps. Moreover, the forgetful functor from the category of dI domains and linear stable functions, dI_{l}, to predI_{a} has a left adjoint which induces a monad on predI_{a}, namely what in similar contexts is called a lift monad. Thus, we have a model of ILL with additional structure which enables us to model convergence/divergence behaviour. This model satisfy all the axioms of our categorical model, and we therefore have a sound and adequate denotational semantics where types are interpreted as pre dI domains, and terms as affine stable functions.

2 A linear functional language, LTS_{+Rec}

2.1 The Curry-Howard isomorphism

The classical Curry-Howard isomorphism relates the λ-calculus to Intuitionistic Logic. It says that types can be viewed as formulas and typable terms as proofs and vice versa. The point is that proof-rules for Intuitionistic Logic can be “decorated” with terms such that the term induced by a proof encodes the proof. An appropriate term language for this purpose is the λ-calculus. It turns out that we then get the rules for assigning types to terms, [GLT89]. The present paper deals with an analogous correspondence between ILL and the Linear Term System (LTS). Historically, LTS was discovered as a term language to decorate proof-rules for ILL, but it can be considered as a programming language independently of its historical roots. The proof-rules will then appear as typing rules. We then get the Curry-Howard isomorphism as follows: given a proof of A_{1}, ..., A_{n} ⊢ A in ILL, that is, a proof of the formula A, one can inductively construct a derivation of a sequent x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ t : A in LTS, that is, a term t of type A. Conversely, if one has a derivable sequent x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ t : A in LTS, there is an easy way to get a proof of A_{1}, ..., A_{n} ⊢ A in ILL: erase all variables and terms in the derivation of the type assignment. The two processes are each others inverses modulo renaming of variables. Proof-rules for ILL in Natural Deduction style are given in Appendix A and LTS is introduced formally below.

2.2 Definition of LTS_{+Rec}

Types are given by the grammar s ::= I | s ⊗ s | s ⊸ s | s&s | s ⊕ s | !s, and terms by the grammar

t ::= x |
∗ | let t be ∗ in t |
t ⊗ t | let t be x ⊗ y in t |
λx.t | tt |
(t, t) | fst(t) | snd(t) |
inl(t) | inr(t) | case t of inl(x) => t | inr(y) => t |
let t, ..., t be x_{1}, ..., x_{n} in !t | derelict(t) |
discard t in t | copy t as x, y in t |
let t, ..., t be x_{1}, ..., x_{n} in recz.t

where t, ..., t means a sequence of n occurrences of t. In what follows, A, B, C, D will range over types, and u, v, w, f will range over terms. Some terms can be assigned a type in a way analogous to the typed λ-calculus. The type assignments will have the form of sequents x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A where x_{1}, ..., x_{n} are pairwise distinct variables and {x_{1}, ..., x_{n}} is the set of free variables of the term u. We will frequently write Γ instead of x_{1} : A_{1}, ..., x_{n} : A_{n} or A_{1}, ..., A_{n}, and !Γ instead of x_{1} :!A_{1}, ..., x_{n} :!A_{n} or !A_{1}, ...,!A_{n}. The type assignments are derived according to the rules in Appendix C (which also contains the rules for assignment of categorical semantics). The notation will be abused when necessary in the following way: the expression “Γ ⊢ u : A” can mean either the sequent itself or a certain derivation of the sequent. The name of a rule, for example (Id), can mean either the rule itself or a certain instance of the rule. The actual interpretation is to be decided by the context. The terms together with the typing rules for the fragment corresponding to ILL will be called LTS, and the extension with recursion will be called LTS_{+Rec}. Note that if we remove the terms from the typing rules for LTS, we get the proof-rules for ILL given in Appendix A. From now on, we will consider only typable terms.

Note that the definition of sequents implicitly restricts use of the rules. It is for example not possible to use the (⊗ − I) rule if Γ and Δ have common variables.

2.3 Properties of LTS_{+Rec}

The derivation of a type assignment is essentially unique (which actually is the essence of the Curry-Howard isomorphism):

Proposition 2.1 If the sequent Γ ⊢ u : A is derived by a given derivation, then the rule corresponding to the first rule instance above the sequent Γ ⊢ u : A which is different from an instance of (Exchange), is uniquely determined by the term u.

Proof. Induction in the derivation of Γ ⊢ u : A. □

Lemma 2.2 (Substitution Property) If Γ ⊢ u : A and Δ, x : A, Λ ⊢ v : B both are derivable s.t. the variables in Γ and Δ, Λ are pairwise distinct, then Δ, Γ, Λ ⊢ v[u/x] : B is derivable too.

Proof. Induction in the derivation of Δ, x : A, Λ ⊢ v : B. □

The expression v[u/x] denotes the term v where u has been substituted for every free occurence of x, and where bound variables of v have been renamed to avoid capture of free variables in u.

2.4 The choice of rule for ! introduction

Seen from a historical point if view, the term corresponding to the rule for introduction of ! has caused problems. In [Abr90], the first Curry-Howard interpretation of ILL was published. Here the rules are given in Gentzen style, named after the discoverer of a similar system of proof-rules for classical logic. The Natural Deduction formulation was not discovered at this time. In Gentzen style, we only have introduction rules. A connective can be introduced on both sides of the sequent, in opposition to Natural Deduction style, where we can either eliminate a connective, or introduce it on the right hand side. A Gentzen style formulation of ILL can be found in Appendix B. The (! − I) rule of the Natural Deduction formulation corresponds to the (!−R) rule of the Gentzen formulation. In the above mentioned article the (! − R) rule is decorated with the following terms:

x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ u : A
(! − R)
x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢!u :!A

The Gentzen style system enjoys the substitution property simply because it is a rule of the system, namely the (Cut) rule. The problem, as pointed out in [Wad91], is as follows: The (Cut) rule together with (! − R) (decorated with terms as above) forces a collapse in the categorical model corresponding to the system. The ! modality is interpreted as a functor, and the two rules together would force ! to be isomorphic to !!. The problem is basically that a given sequent can have several derivations, and they all ought to give rise to the same categorical interpretation. The presence of (Cut) gives us two different interpretations of the same sequent (unless ! ≅!! in a canonical way).

In 1992 a new way to decorate the (! − R) rule with terms, together with a Natural Deduction formulation of ILL, was discovered by the authors of [BBdPH92] (and by the author of this paper). The new decoration of (! − R) is as follows:

x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ u : A
(! − R)
z_{1} :!A_{1}, ..., z_{n} :!A_{n} ⊢ let z_{1}, ..., z_{n} be x_{1}, ..., x_{n} in !u :!A

The new rule can coexist with (Cut) without collapsing the model, and the derivations that with the old term decoration concluded with identical sequents, now concludes with different sequents (because the induced terms are different). We get a system equivalent to LTS if we take the Gentzen style formulation of ILL and decorate it with terms as originally done in [Abr90] except that we pick the correct decoration of the (! − R) rule, cf. the discussion above. The Natural Deduction style formulation of ILL is given in Appendix A. The (! − I) rule of the Natural Deduction formulation, corresponding to the above mentioned (! − R) rule of the Gentzen formulation, is as follows:

Γ_{1} ⊢ w_{1} :!A_{1} , ..., Γ_{n} ⊢ w_{n} :!A_{n} x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ u : A
(! − I)
Γ_{1}, ..., Γ_{n} ⊢ let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in !u :!A

2.5 The choice of rule for recursion

We want to extend LTS with a rule for parameterised recursion. Values corresponding to the parameters are copied in any reasonable semantics, so the corresponding types should be of ! type because we are in a linear context. Hence, a natural first choice would be:

x_{1} :!A_{1}, ..., x_{n} :!A_{n}, z : B ⊢ u : B
(Recursion)
x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ recz.u : B

An argument against this solution is that the function which assigns a fixpoint f† ∈ B to a function f : B → B in our canonical model dI_{a} is not affine, that is, it can not be internalised as a map (a fixpoint operator) in the category. Thus, since we want give a denotational semantics to the rule in the category dI_{a} (via a categorical semantics), we should look for another definition of recursion. The next suggestion is:

x_{1} :!A_{1}, ..., x_{n} :!A_{n}, z :!B ⊢ u : B
(Recursion)
x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ recz.u : B

This rule is actually the one used in [Mac92]. We can now give a denotational semantics with our canonical model dI_{a}, but LTS extended with this rule does not enjoy the Substitution Property. Now, we are trying to extend LTS, where the underlying proof-rules for ILL are in Natural Deduction style, with a rule for recursion. LTS would loose the Substitution Property in a similar way if we replaced the (! − I) rule with the first of the above mentioned (! − R) rules induced by the Gentzen formulation of ILL. We know how to deal with this problem, so we solve the problem with the rule for recursion in a similar way:

Γ_{1} ⊢ w_{1} :!A_{1} , ..., Γ_{n} ⊢ w_{n} :!A_{n} x_{1} :!A_{1}, ..., x_{n} :!A_{n}, z :!B ⊢ u : B

(Recursion)

Γ_{1}, ..., Γ_{n} ⊢ let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in recz.u : B

LTS extended with this rule, (that is, LTS_{+Rec}) enjoys the Substitution Property, and it allows definition of operational as well as denotational semantics in natural ways.

3 Operational semantics of LTS_{+Rec}

3.1 Definition of the operational semantics

We will now give an operational semantics for LTS in Natural Semantics style. We will consider free variables as placeholders for canonical terms, which corresponds to a call-by-value parameter passing strategy where we only substitute canonical terms for variables.

Definition 3.1 A canonical term is a closed typable terms of one of the following shapes:

∗ d ⊗ e λx.u (u, v) inl(c) inr(d) let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u

where c, d, e, c_{1}, ..., c_{n} are canonical terms.

Let T be the set of closed typable terms, and C the set of canonical terms. The evaluation rules in Appendix E induces a relation, the evaluation relation: ⟶ ⊂ T ×C. Note how the choice of call-by-value parameter passing strategy is reflected in the evaluation rule for application: we evaluate a parameter to a canonical term before plugging it in.

Definition 3.2 Given a term u, we will write u ↓ iff there exists a term c s.t. u ⟶ c. We will say that u converges.

3.2 Properties of the operational semantics

If one considers the Gentzen style formulation of LTS, then cut-elimination gives rise to certain reductions on terms in the same way as cut-elimination in ordinary Intuitionistic Logic gives rise to reductions on terms in the λ-calculus. It turns out that the reductions induced by our operational semantics without recursion all are reductions induced by cut-elimination. It should be noted that our operational semantics only evaluates closed terms, and not every redex corresponding to cut-elimination is reduced. For example, every closed term λx.u is canonical, whatever is “inside” the abstraction. The operational semantics enjoys the following properties:

Proposition 3.3 (Subject Reduction) If ⊢ u : A and u ⟶ c, then ⊢ c : A.

Proof. Induction in the derivation of u ⟶ c, where we use the Substitution Property. □

Proposition 3.4 (Determinacy) If u ⟶ c and u ⟶ d, then c = d.

Proof. Induction in the derivation of u ⟶ c. □

Proposition 3.5 (Convergence) If the term u is without recursion, then u ↓.

Proof. A modified version of the proof in [Abr90]. □

4 General considerations about the categorical semantics

4.1 The connection to denotational semantics

In what follows, [[A]] will mean the interpretation of A and [[u]] the interpretation of u. When appropriate, we will abuse notation and omit the brackets. We have stated a reference where the categorical notions used can not be found in [Lan71].

In denotational semantics, a type A is normally interpreted as a set [[A]] with a certain structure. A term u of type A with free variables x_{1}, ..., x_{n} of type A_{1}, ..., A_{n} is then interpreted as a function [[u]] from [[A_{1}]] × ... × [[A_{n}]] to [[A]]. In particular, if u is closed, then the interpretation is a point in [[A]]. For example in [Win93], computer programs are interpreted as continuous functions between appropriate domains. One wants the denotational semantics to have certain properties w.r.t. the operational semantics. Firstly, it has to be sound, that is, evaluation has to preserve the denotation. Secondly, the denotational and operational semantics has to agree w.r.t. relevant observations. This is called adequacy. For example in [Win93], a term may diverge because of recursion, so one wants this to be reflected in the denotational semantics: a term ought to converge if and only if it is interpreted as a non-bottom element in the relevant domain.

I will not give an explicit concrete denotational semantics of LTS_{+Rec} here, but instead give a categorical semantics, defined with the above mentioned goals in mind. It then follows that any concrete category satisfying the axioms of the categorical model induce a sound and adequate denotational semantics. The categorical semantics adheres to the following fundamental ideas of the categorical treatment of proof theory:

• Formulas are interpreted as objects

• Proofs are interpreted as maps

• Proof-rules correspond to natural transformations between appropriate hom-functors.

In [BBdPH92] a categorical semantics is given to a Gentzen style formulation of LTS without additives, but it is not equivalent to the relevant parts of our categorical semantics. Neither is their reductions on terms the same as the reductions on terms induced by the relevant part of our operational semantics. It is important to notice how the differences in choice of rules for reductions on terms is reflected in differences in the choices of categorical semantics. For example, if we for a moment restrict our attention to LTS without additives, then the reductions induced by our operational semantics is a strict subset of the reductions induced by cut-elimination, as remarked earlier. Therefore the equations imposed on our model to get soundness w.r.t. our Natural Semantics style operational semantics are weaker than the equations imposed on their model to get soundness w.r.t. the reductions on terms induced by cut-elimination. If we compare the full system consisting of LTS_{+Rec} equipped with the operational semantics given in the previous section to the system given in [BBdPH92], there is an important difference: the first system has diverging terms, the second system does not. We therefore need additional categorical machinery to model convergence/divergence behaviour as we are interested in an adequacy result.

4.2 Initial assumptions about the interpretation

Types will be interpreted as objects, and we want to interpret sequents as arrows between appropriate objects. So we need an operation on objects to “put together” the interpretations of hypotheses into one object. To this end, we will assume that we are dealing with a monoidal category (C, I, ⊗). Good reasons for this choice can be found in [BBdPH92]. The interpretation of a sequent will be defined by induction in its derivation, so we have to be sure that the definition is independent of the derivation. The derivation of a sequent is unique up to applications of the (Exchange) rule, which suggests that our category should be symmetric monoidal.

4.3 Modelling convergence/divergence behaviour

Following [Mog89] , we assume that we have a monad (T, η, μ) on C to model convergence/divergence behaviour. This induces the usual kleisli operator kleisli as follows:

\begin{matrix}kleisli_{A,B} : hom(A, T B) ⟶ hom(T A, T B) \\ kleisli_{A,B}(f) = [T A ^{T f}^{}T T B ^{μ_{B}}^{}T B] \end{matrix}

The idea is to distinguish between A, the object of values of type A, and T A, the object of computations of type A. Intuitively, η is the inclusion of values into computations, and kleisli(f) is the extension of a function f from values to computations, to a function from computations to computations, which first evaluates a computation, and then applies f to the resulting value. In this context, canonical terms are to be thought of as values and arbitrary closed terms as computations. A sequent x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A will then be interpreted as a map [[u]] : [[A_{1}]] ⊗ ... ⊗ [[A_{n}]] → T [[A]] because we consider free variables as placeholders for canonical terms. Now, a program (a closed term) ⊢ u : A will be interpreted as a point [[u]] : I → T [[A]] (a point is a map with domain I). According to the intuition, it should be considered as a value iff it has η as factor. In a concrete case where the objects are CPOs of some kind, this corresponds to [[u]] being non-bottom. This motivates the following definition:

Definition 4.1 For any point f : I → T B, we will write f ⇓ iff there exists a map h : I → B s.t. f = h; η_{B}. We will say that f converges semantically.

As in the case with [Mog89] we will use a strength natural transformation

t : (−) ⊗ T (+) → T (− ⊗ +)

to transform a pair consisting of a value and a computation into the computation of a pair of values. The intuition is that t evaluates the second component, and returns the pair of relevant values if the computation converges. Four diagrams have to commute, but the most important one is the following:

A ⊗ B \overline{Id ⊗ η_{}}A ⊗ T B
[figure: η]
T (A ⊗ B)^{^{}t}

It says that if we transform a value-computation pair, where the computation is a value, into the computation of a pair of values, then we get a value.

We also need to be able to transform a pair of computations into a computation of a pair of values. Following [Mog89], a natural transformation

ψ : T (−) ⊗ T (+) → T (− ⊗ +)

is induced by the strength t as follows:

ψ_{A,B} = (≅; t_{T B,A}; T (≅); T (t_{A,B}); μ_{A⊗B})

Where ≅ is the “symmetric” natural isomorphism. The intuition is that ψ first evaluates the first component, if the first computation converges, it evaluates the second component, and if the second computation also converge then it returns the pair of relevant values. It makes the following diagram commute:

A ⊗ B \overline{η ⊗ η_{}}T A ⊗ T B
[figure: η]
T (A ⊗ B)^{^{}ψ}

It says that if both computations are values, then the resulting computation is a value too.

4.4 Two examples, the (⊗ − I) and (⊗ − E) rules

According to previous assumptions, we are dealing with a symmetric monoidal category (C, I, ⊗) with a monad (T, η, μ) and a strength t on it. This is enough machinery to give an example of an interpretation of a rule. We will interpret the logical connective ⊗ as the tensor product given by the monoidal structure, that is, [[A ⊗ B]] = [[A]] ⊗ [[B]].

Warning: In what follows, the symbol ⊗ can be interpreted in three different ways: as a functor, as a logical connective, and as part of the syntax for terms.

Now, the rule for introduction of ⊗ looks like this:

Γ ⊢ u : A Δ ⊢ v : B
(⊗ − I)
Γ, Δ ⊢ u ⊗ v : A ⊗ B

and should give rise to an operation on arrows:

{[[Γ]] ^{[[u]]}^{}T [[A]] [[Δ]] ^{[[v]]}^{}T [[B]] \atop [[Γ]] ⊗ [[Δ]] ^{[[u⊗v]]}^{}T [[A ⊗ B]]}

Hence, we define:

[[u ⊗ v]] = [[[Γ]] ⊗ [[Δ]] ^{[[u]]⊗[[v]]}^{}T [[A]] ⊗ T [[B]] ^{ψ}^{}T ([[A]] ⊗ [[B]])]

It is easy to see that this corresponds to the appropriate rule of the operational semantics:

{u ⟶ c v ⟶ d \atop u ⊗ v ⟶ c ⊗ d}

If we want to evaluate the two computations, u and v, then we evaluate both terms, and if they both converge, the result is the two results paired together. This strategy is used in the categorical as well as in the operational semantics. Now, the rule for elimination of ⊗:

Λ ⊢ w : A ⊗ B Γ, x : A, y : B ⊢ u : C
Γ, Λ ⊢ let w be x ⊗ y in u : C

induces the following operation on arrows:

{[[Λ]] ^{[[w]]}^{}T [[A ⊗ B]] [[Γ]] ⊗ [[A]] ⊗ [[B]] ^{[[u]]}^{}T [[C]] \atop [[Γ]] ⊗ [[Λ]] ^{Id⊗[[w]]}^{}[[Γ]] ⊗ T ([[A]] ⊗ [[B]]) ^{t}^{}T ([[Γ]] ⊗ [[A]] ⊗ [[B]]) ^{kleisli([[u]])}^{}T [[C]]}

Again, it is easy to see that this corresponds to the appropriate rule of the operational semantics:

{w ⟶ d ⊗ e u[d/x, e/y] ⟶ c \atop let w be x ⊗ y in u ⟶ c}

We first evaluate w, and if it converges, it gives a pair of values. We then run u with these values as the input. Again, we see that the same strategy is used in the categorical as well as in the operational semantics. Recall that kleisli([[u]]) is the extension of [[u]] which first evaluates the computation given as input, and then applies [[u]] to the resulting value. Note that we need the natural transformation t to be able to “move” a tuple of parameters (that is: values) “inside” a computation.

5 Categorical semantics of LTS_{+Rec}

5.1 Introduction to the category O

Before stating the definition of a categorical model for LTS_{+Rec}, we need to know O, the category of CPOs and continuous functions. A CPO is a partial order where every increasing chain {f_{n}}_{n∈ω} has a join ⨆_{n∈ω} f_{n}. Note that we do not assume the existence of a bottom element. A continuous function between CPOs is a monotone function that preserves joins of increasing chains. The category O is cartesian closed; the finite products (1, ×) are induced by the usual structure on partial orders, and the exponential object ⇒ is the set of continuous functions equipped with the pointwise order. We also have finite sums (0, +) induced by the usual structure on partial orders. The usual lift construction on partial orders induces a strong monad ((−)_{⊥}, lift, down, u) on (O, ×, 1), see Appendix G. Note that a cartesian category also is a monoidal category.

Definition 5.1 If f is a function between partial orders, we will say that it reflects the order iff f(x) ≤ f(y) implies x ≤ y whenever x and y are elements in the domain of f.

5.2 Definition of the categorical semantics

In this part we will state the necessary machinery to interpret LTS_{+Rec}. To give a categorical semantics to the rule for recursion, we will assume that some of our constructions are O-enriched. An O-category is a category where each hom-set has CPO structure such that composition is continuous. An O-functor between O-categories is a functor between the underlying categories which is continuous on each hom-set. Other notions from category theory can be defined similarly in an O-enriched setting, but we shall not need it here. See [Poi92] for an introduction to enriched category theory.

Proposition 5.2 An O-category C induce the functor hom(I, −) : C → O. If C moreover is equipped with a monoidal structure (I, ⊗) where ⊗ is an O-functor, then a monoidal structure on the functor hom(I, −) is induced by the map n_{1} : 1 → hom(I, I) and the natural transformation n : hom(I, −) × hom(I, +) ⟶ hom(I, − ⊗ +) defined as n_{1}(∗) = Id_{I} and n_{A,B}(f, g) = (≅; (f ⊗ g)) respectively.

Remark: When assuming the functor ⊗ : C×C → C to be an O-functor, we are implicitly assuming C × C to have the obvious O-enrichment induced by the O-enrichment of C.

Remark: The functor hom(I, −) should be thought of as a functor that forgets all structure on an object except the CPO structure on its points. It is easy to see that hom(I, −) is monotone on hom-sets when the maps in O are ordered pointwise; this corresponds to the ordering of maps in C being included in the pointwise ordering w.r.t. the partial order on points. Note that hom(I, −) does not necessarily reflect the order on hom-sets. This is for example not the case with the predI_{a} model where the ordering on hom-sets is the so-called stable order. If hom(I, −) does reflect the order, then the ordering of maps in C is the pointwise ordering.

Definition 5.3 A categorical model for LTS_{+Rec} is an O-category C equipped with:

1. a symmetric monoidal closed structure (I, ⊗, ⊸) where ⊗ is an O-functor s.t. each n_{A,B} induced by the monoidal structure reflects the order

2. a symmetric monoidal comonad (!, ε, δ, m_{I}, m) where ! is an O-functor

3. monoidal natural transformations e :!(−) → I and d :!(−) →!(−)⊗!(−)

4. binary product × and sum + which both are preserved by hom(I, −)

5. a strong monad (T, η, μ, t) and an isomorphism σ : hom(I, −)_{⊥} → hom(I, T (−)) making (hom(I, −), σ) a functor of strong monads

6. a bottom element ⊥_{A,B} in every hom(A, T B) s.t. h; ⊥_{A,B}=⊥_{I,B}for every h : I → A

Remark: The assumption that the comonad is symmetric monoidal means that ! is a symmetric monoidal functor and ε and δ are monoidal natural transformations, see Appendix G. When assuming the natural transformations e and d to be monoidal, we are implicitly assuming the functors I and !(−)⊗!(−) to have the obvious monoidal structure induced by the monoidal structure on !.

Remark: Since hom(I, −) should be thought of as a functor that forgets all structure on an object except the CPO structure on its points, then a property saying that hom(I, −) respect some structure present on both C and O should be thought of as a property saying that the structure on C behaves as the corresponding structure on O when only CPO structure on points is considered. The way in which the structure on C behaves as the structure on O is determined by the property of hom(I, −). The requirement that hom(I, −) preserves products says that the points hom(I, A × B) of the product of two objects is isomorphic to the product hom(I, A) × hom(I, B) of the points hom(I, A) and hom(I, B) of the two objects. Similarly for sum. Condition 6 can also be stated in terms of a preservation property of the hom(I, −) functor; it is equivalent to commutativity of the following diagram:

hom(I, A)
[figure] hom(I, ⊥_{A,B})

[figure: hom(I, B)_{⊥}; ⊥; σ_{B}; hom(I, T B)]

where ⊥: hom(I, A) ⟶ hom(I, B)_{⊥} is the bottom element of hom_{O}(hom(I, A), hom(I, B)_{⊥}) that sends every element in hom(I, A) to the bottom element of hom(I, B)_{⊥}. The requirement of an isomorphism σ making (hom(I, −), σ) a functor of strong monads from the strong monad (T, η, μ, t) on (C, I, ⊗) to the strong monad ((−)_{⊥}, lift, down, u) on (O, ×, 1) say that the strong monad T behaves like the strong monad (−)_{⊥}.

Definition 5.4 We can now define a generalised cokleisli operator γ:

\begin{matrix}γ : hom(!A_{1} ⊗ ...⊗!A_{n}, B) ⟶ hom(!A_{1} ⊗ ...⊗!A_{n},!B) \\ γ(f) = [!A_{1} ⊗ ...⊗!A_{n} ^{δ_{A_{1}}⊗...⊗δ_{An}}^{}!!A_{1} ⊗ ...⊗!!A_{n} ^{m_{A_{1},...,An}}^{}!(!A_{1} ⊗ ...⊗!A_{n}) ^{!f}^{}!B] \end{matrix}

Note that in case n = 0 then γ(f) = m_{I}; !f. In case n = 1 this definition is consistent with the usual cokleisli operator. It should be mentioned that the definition of γ is due to [BBdPH92]. Note that the definition of γ is unrelated to the product structure. In [See89], another generalised cokleisli operator is used which is related to the product structure. Proposition 5.5 If f :!A_{1} ⊗ ...⊗!A_{n} → B, then γ(f); ε_{B} = f. Proof. Straightforward calculation. □ Proposition 5.6 If f_{i} : I → A_{i} for i ∈ {1, ..., n}, and h :!A_{1} ⊗ ...⊗!A_{n} → B, then

\begin{matrix}[I ≅ I ⊗ ... ⊗ I ^{γ(f_{1})⊗...⊗γ(f_{n})}^{}!A_{1} ⊗ ...⊗!A_{n} ^{γ(h)}^{}!B] = \\ γ([I ≅ I ⊗ ... ⊗ I ^{γ(f_{1})⊗...⊗γ(f_{n})}^{}!A_{1} ⊗ ...⊗!A_{n} ^{h}^{}B]) \end{matrix}

Proof. Induction in n. □ Proposition 5.7 If f : I → A, then the following diagram commutes:

[figure: I; γ(f); !A; I ⊗ I; ≅; γ(f) ⊗ γ(f); !A⊗!A; d_{A}]

Proof. Straightforward calculation, where we use monoidality of d. □ Proposition 5.8 (A + B) ⊗ C is naturally isomorphic to (A ⊗ C) + (B ⊗ C). Proof. The functor (−) ⊗ C has a right adjoint, wherefore it preserve sums. The isomorphism can be shown to be natural in A, B and C. □ Definition 5.9 Given f :!A_{1} ⊗ ...⊗!A_{n}⊗!T B → T B, define f^{♯} :!A_{1} ⊗ ...⊗!A_{n} → T B as

f^{♯} = ⨆_{n∈ω} Φ_{f}^{n}(⊥)

where the continuous function Φ_{f} : hom(!A_{1} ⊗ ...⊗!A_{n}, T B) ⟶ hom(!A_{1} ⊗ ...⊗!A_{n}, T B) is defined as follows:

\begin{matrix}Φ_{f}(h) = \\ [!A_{1} ⊗ ...⊗!A_{n} ^{D}^{}!A_{1} ⊗ ...⊗!A_{n}⊗!A_{1} ⊗ ...⊗!A_{n} ^{Id⊗γ(h)}^{}!A_{1} ⊗ ...⊗!A_{n}⊗!T B ^{f}^{}T B] \end{matrix}

where D is a generalisation of the natural transformation d, that is:

\begin{matrix}D_{A_{1},...,A_{n}} = \\ [!A_{1} ⊗ ...⊗!A_{n} ^{d_{A_{1}}⊗...⊗d_{An}}^{}!A_{1}⊗!A_{1} ⊗ ...⊗!A_{n}⊗!A_{n} ^{≅}^{}!A_{1} ⊗ ...⊗!A_{n}⊗!A_{1} ⊗ ...⊗!A_{n}] \end{matrix}

The operator (−)^{♯} will be used to interpret the rule for recursion. Note that {Φ_{f}^{n}(⊥)}_{n∈ω} is an increasing chain in hom(!A_{1} ⊗...⊗!A_{n}, T B). It follows from the usual fixpoint theorem for CPOs that f^{♯} is well defined and equal to a uniquely determined least solution to the equation x = Φ_{f}(x). A solution to this equation is actually what in a later section of this paper will be called a linear fixpoint of the map f.

Definition 5.10 The interpretation of formulas are defined by induction as follows:

• [[1]] = I

• [[A ⊗ B]] = [[A]] ⊗ [[B]]

• [[A ⊸ B]] = [[A]] ⊸ T [[B]]

• [[A&B]] = T [[A]] × T [[B]]

• [[A ⊕ B]] = [[A]] + [[B]]

• [[!A]] =!T [[A]]

Note how the interpretation of ⊸ reflects the call-by-value parameter passing of the operational semantics. A term of type A ⊸ B expects a value of type A and computes a value of type B. Therefore the interpretation of the type is [[A]] ⊸ T [[B]].

Definition 5.11 Given a derivation of the sequent

x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A

we inductively define a map

[[A_{1}]] ⊗ ... ⊗ [[A_{n}]] ^{[[u]]} T [[A]]

cf. the operations on arrows (corresponding to the typing rules) given in Appendix C.

As shown earlier, the proof is unique up to applications of the (Exchange) rule. Given a derivable sequent, the interpretation is therefore uniquely determined.

5.3 Properties of the categorical semantics

I will now sum up what we can obtain with the machinery defined. We will consider naturality of the operation on arrows corresponding to recursion as naturality in the interpretation of Γ_{1}, ..., Γ_{n}.

Proposition 5.12 The typing rules induce operations on arrows which are natural in the interpretation of the unchanged components of the sequents.

Proof. Check each rule. □

This result gives us an extension of the Substitution Property essentially saying that substitution corresponds to composition. This is necessary to deal with substitutions in the operational semantics:

Lemma 5.13 (Substitution Lemma) If Γ ⊢ u : A and Δ, x : A, Λ ⊢ v : B both are derivable s.t. the variables in Γ and Δ, Λ are pairwise distinct, and there exists a map h : [[Γ]] → [[A]] with the property that [[u]] = h; η, then Δ, Γ, Λ ⊢ v[u/x] : B is derivable too with the interpretation

[[[Δ]] ⊗ [[Γ]] ⊗ [[Λ]] ^{Id⊗h⊗Id}^{}[[Δ]] ⊗ [[A]] ⊗ [[Λ]] ^{[[v]]}^{}T [[B]]]

Proof. The theorem is proved by induction in the derivation of Δ, x : A, Λ ⊢ v : B. All cases except (Id) are covered by the naturality property given by the previous theorem. The (Id) case is trivial. □

Lemma 5.14 Given a canonical term ⊢ c : A, then [[c]] ⇓.

Proof. Induction in the derivation of ⊢ c : A. □

Lemma 5.15 Given a canonical term ⊢ let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u, then

[[let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u]] = γ(h); η

for some h : I → T A.

Proof. Induction in the derivation of ⊢ let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u :!A. □

Theorem 5.16 (Soundness Theorem) Given a closed term u s.t. u ⟶ c, then [[u]] = [[c]].

Proof. See Appendix E.

To prove the “if” part of the Adequacy Theorem, we will use the fact that a fixpoint is calculated in a certain way, namely as the join of a certain increasing chain in a hom-set. We can then use the technique of Logical Relations to prove a result, which has the “if” part of the Adequacy Theorem as a special case. Logical Relations relate the categorical interpretation of a term to its operational behaviour.

Definition 5.17 (Logical Relations) Let T_{A} be the set of closed typable terms of type A, and C_{A} the set of canonical terms of type A. We define the relations

≲_{A}^{∘}⊆ hom(I, [[A]]) × C_{A} ≲_{A}⊆ hom(I, T [[A]]) × T_{A}

by induction in the type. The relation ≲_{A}^{∘} is defined in terms of relations corresponding to smaller types as follows:

• Id_{I} ≲_{1}^{∘} ∗

• f ≲_{A⊗B}^{∘} d ⊗ e iff ∃g ∈ hom(I, [[A]]).∃h ∈ hom(I, [[B]]). f = [I ≅ I ⊗ I ^{g⊗h}^{}[[A]] ⊗ [[B]]] & g ≲_{A}^{∘} d & h ≲_{B}^{∘} e

• f ≲_{A⊸B}^{∘} λx.u iff ∀g ∈ hom(I, [[A]]).∀c ∈ C_{A}. g ≲_{A}^{∘} c ⇒ [I ≅ I ⊗ I ^{f⊗g}^{}([[A]] ⊸ T [[B]]) ⊗ [[A]] ^{eval}^{}T [[B]]] ≲_{B} u[c/x] • f ≲_{A&B}^{∘} (u, v) iff

∃g ∈ hom(I, T [[A]]).∃h ∈ hom(I, T [[B]]). f =< g, h > & g ≲_{A} u & h ≲_{B} v

• f ≲_{A⊕B}^{∘} inl(c) iff ∃g ∈ hom(I, [[A]]). f = g; inj_{1} & g ≲_{A}^{∘} c

• f ≲_{A⊕B}^{∘} inr(d) iff ∃h ∈ hom(I, [[B]]). f = h; inj_{2} & h ≲_{B}^{∘} d

• f ≲_{!A}^{∘} let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u iff ∃g ∈ hom(I, T [[A]]). f = γ(g) & g ≲_{A} u[c_{1}/x_{1}, ..., c_{n}/x_{n}]

The relation ≲_{A} is defined in terms of ≲_{A}^{∘} as follows:

• f ≲_{A} u iff ∀g ∈ hom(I, [[A]]). f = g; η ⇒ ∃c ∈ C_{A}. u ⟶ c & g ≲_{A}^{∘} c

We are now in a position to prove that the predicate (−) ≲_{A} u is inclusive for any term ⊢ u : A. This amounts to the following lemma:

Lemma 5.18 (Inclusiveness Lemma) Let a term ⊢ u : A be given. If {f_{n}}_{n∈ω} is an increasing chain in hom(I, T A) s.t. f_{n} ≲_{A} u for every n, then ⨆_{n∈ω} f_{n} ≲_{A} u.

Proof. Induction in the type. □

Lemma 5.19 (Approximation Lemma) Let x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : C be given. Let J be a finite set s.t. for all j ∈ J we are given ⊢ v_{j} : B_{j} and f_{j} ∈ hom(I, [[B_{j}]]) with the property that f_{j}; η ≲_{B_{j}} v_{j}. Moreover, assume that for each j we have a variable z_{j}, s.t. for all i, k ∈ J we have i ≠ k ⇒ z_{i} ≠ z_{k}, s.t. {x_{1}, ..., x_{n}} ⊆ {z_{j}| j ∈ J}, and s.t. for all r ∈ {1, ..., n} and j ∈ J we have x_{r} = z_{j} ⇒ A_{r} = B_{j}. We then have:

[I ≅ I ⊗ ... ⊗ I ^{f_{j_{1}}⊗...⊗f_{jn}}^{}[[A_{1}]] ⊗ ... ⊗ [[A_{n}]] ^{[[u]]}^{}T [[C]]] ≲_{C} u[..., v_{j}/z_{j}, ...]

where for all r in {1, ..., n} we have chosen j_{r} s.t. x_{r} = z_{j_{r}}.

Proof. See Appendix F.

Theorem 5.20 (Adequacy Theorem) Given a closed term u, then u ↓ iff [[u]] ⇓.

Proof. The interpretation of a canonical term converges semantically, which together with Soundness gives the “only if” part. The “if” part is a special case of the Approximation Lemma. □

6 Fixpoints in a linear context

In the categorical semantics of LTS_{+Rec} we used the operator (−)^{♯} to interpret the rule for recursion. The map f^{♯} was defined to be a certain solution to the equation x = Φ_{f}(x). The previous section showed that this was an appropriate interpretation of the rule for recursion in the sense that we get soundnes and adequacy results. Solutions to the equation x = Φ_{f}(x) are what we in this section will call linear fixpoints, which we will characterise in terms of ordinary fixpoints.

6.1 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 6.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 6.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 according to the following result:

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

Proof. Define Y_{B} = eval†, and conversely, given f : A × B → B, define f† = curry(f); Y_{B}. □

6.2 Linear fixpoints

I will now consider fixpoints in a linear context. The paper [Bra] deals with this topic from a proof theoretic point of view. We can not use the previous definition of fixpoints because it assumes the presence of finite products.

Definition 6.4 Let (C, I, ⊗) be a monoidal category equipped with a comonad (!, ε, δ), and with a natural transformation d :!(−) →!(−)⊗!(−). 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]

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 6.5 Let (C, I, ⊗, ⊸) be a monoidal closed category equipped with a comonad (!, ε, δ), and with a natural transformation d :!(−) →!(−)⊗!(−). 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. In what follows, we need the notion of a categorical model of multiplicative ILL as defined in [BBdPH92]:

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

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

• Monoidal natural transformations e :!(−) → I and d :!(−) →!(−)⊗!(−) such that 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 !. 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}).

If we impose this extra structure on our category we get the following result:

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

Proof. Define Y_{B}^{lin} = ((ε_{!B⊸B} ⊗ Id); eval)^{♯}, and conversely, given f :!A⊗!B → B, define f^{♯} = γ(curry(f)); Y_{B}^{lin}. □

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 an object A to the free coalgebra (!A, δ). The adjunction induces the following natural bijection between maps:

ϕ_{(C,h),A} : hom_{C^{!}}((C, h), (!A, δ)) ≅ hom_{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 [Bie93] it is shown that C^{!} w.r.t. a symmetric monoidal category (C, I, ⊗) equipped with a symmetric monoidal comonad (!, ε, δ, m_{I}, m) has an induced symmetric monoidal structure: the unit 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, m_{I}) is a terminal object, and □ is a binary product.

Theorem 6.8 Let C be a linear category (not necessarily with ⊸), then h : (!A, δ) → (!B, δ) is a fixpoint of f : (!A, δ)□(!B, δ) → (!B, δ) iff ϕ(h) :!A → B is a linear fixpoint of ϕ(f) :!A⊗!B → B.

Proof. Calculation. □

It is obvious that if the the category of free coalgebras is closed under finite products in C^{!}, 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 result:

Corollary 6.9 If C is a linear category (not necessarily with ⊸) s.t. the category of free coalgebras is closed under finite products in C^{!}, then the category of free coalgebras has fixpoints iff C has linear fixpoints.

Proof. A straightforward consequence of the theorem. □

If the category of free coalgebras w.r.t. a linear category is closed under finite products in C^{!} then it has finite products, as mentioned above. In [Bie93] 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), δ). This leads to the following result:

Theorem 6.10 If C is a linear category s.t. the category of free coalgebras is closed under finite products in C^{!}, then the category of free coalgebras has fixpoint operators iff C has linear fixpoint operators.

Proof. Follows from the previous results. □

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

Theorem 6.11 If C is 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.

Proof. Calculation. □

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

Proposition 6.12 Let C be a category equipped 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^{!} .

Proof. The free functor F^{!} : C → C^{!} is right adjoint to U^{!} : C^{!} → C. Right adjoints preserve finite products, so if C has terminal object 1 then 1 is sent into a terminal object (!1, δ) in C^{!}, and if C has binary product ×, then a product diagram A ← A × B → B in C is sent into a product diagram (!A, δ) ← (!(A × B), δ) → (!B, δ) in C^{!}. □

This has the consequence that if C is a linear category with finite products, then the category of free coalgebras is closed under finite products.

Moreover, since both (I, m_{I}) and (!1, δ) are terminal objects in C^{!}, I is isomorphic to !1, and analogously, since both (!A⊗!B, (δ⊗δ); m_{!A,!B}) and (!(A×B), δ) are products of (!A, δ) and (!B, δ) in C^{!}, !A⊗!B is isomorphic to !(A × B) such that the isomorphism is natural in A and B. Thus we can define a model of ILL as described in [See89]. Calculations show that the way the isomorphisms are defined and the universal property of (I, m_{I}) and (!A⊗!B, (δ ⊗ δ); m_{!A,!B}) forces ! to take the cocommutative comonoid structure w.r.t. the finite products to the cocommutative comonoid structure w.r.t. the symmetric monoidal structure, that is:

e_{A} = [!A ^{!<>_{A}}^{}!1 ≅ I] d_{A} = [!A ^{!Δ_{A}}^{}!(A × A) ≅!A⊗!A]

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.

6.3 Generalisation of linear fixpoints

The definition of linear fixpoints can be generalised to an arbitrary number of parameters such that it “fits” the definition of recursion in a linear context:

Definition 6.13 (Generalisation) Let (C, I, ⊗) be a symmetric monoidal category equipped with a symmetric monoidal comonad (!, ε, δ, m_{I}, m) and a natural transformation d :!(−) →!(−)⊗!(−). We say that C has linear fixpoints iff for every map f :!A_{1} ⊗ ...⊗!A_{n}⊗!B → B there exists a specified linear fixpoint f^{♯} :!A_{1} ⊗ ...⊗!A_{n} → B with the property that:

f^{♯} = [!A_{1} ⊗ ...⊗!A_{n} ^{D}^{}!A_{1} ⊗ ...⊗!A_{n}⊗!A_{1} ⊗ ...⊗!A_{n} ^{Id⊗γ(f^{♯})}^{}!A_{1} ⊗ ...⊗!A_{n}⊗!B ^{f}^{}B]

In linear categories, this generalisation is equivalent to the original definition of linear fixpoints. Note that in case n = 1 we get the original definition. Similarly, the definition of linear fixpoint operators can be generalised as follows:

Definition 6.14 (Generalisation) Let (C, I, ⊗, ⊸) be a symmetric monoidal closed category equipped with a symmetric monoidal comonad (!, ε, δ, m_{I}, m) and a natural transformation d :!(−) →!(−)⊗!(−). 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_{1} ⊗ ...⊗!A_{n}⊗!B → B the map γ(curry(f)); Y_{B}^{lin} is a linear fixpoint of f.

In linear categories, this generalisation is equivalent to the original definition of linear fixpoint operators. Note that in case n = 1 we get the original definition.

7 Concrete models

It should be mentioned that the category of coherence spaces and linear stable functions is not a model of LTS_{+Rec} as defined above. This is also the case with the category of coherence spaces and affine stable functions, where an affine function is defined as below. The problem is that a model of LTS_{+Rec} assumes the existence of an isomorphism hom(I, A)_{⊥} ≅ hom(I, T A), which amounts to the points of T A being isomorphic (as CPO’s) to the usual lift construction applied to the points of A. But the lift construction applied to a coherence space is not necessarily a coherence space, thus, we can not use the mentioned categories as models of LTS_{+Rec}.

7.1 The category predI_{a}

In what follows, we will present a concrete category which is a model of LTS_{+Rec}. It is the category of pre dI domains and affine stable functions, predI_{a}. The details can be found in the paper [Bra94], so we will only give a sketch of the constructions here. Pre dI domains are defined as follows:

Let (D, ⊑) be a (possible empty) poset, and assume that all non-empty finitely bounded subsets X have joins ⊔X and meets ⊓X. A subset X is finitely bounded if and only if every finite subset of X has an upper bound. Note that D does not necessarily have a bottom element.

An affine 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 affine elements of D by D_{a}. D is called prime algebraic iff

∀d ∈ D.({d′ ∈ D_{a}|d′ ⊑ d} ≠ ∅ & d = ⊔{d′ ∈ D_{a}|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.

A monotone function f is called stable iff f(⊓X) = ⊓{f(x)| x ∈ X} for any non-empty finitely bounded subset X. A monotone function f is called affine iff f(⊔X) = ⊔{f(x)| x ∈ X} for any non-empty finitely bounded subset X. An affine function f between dI domains is called linear iff f(⊥) =⊥.

The trace T r(f) of an affine stable function f : D → E is a subset of D_{a} × E_{a} defined analogously to the trace of a linear stable function between ordinary dI domains.

In what follows, X ↑ means that X has an upper bound. First of all, we need a symmetric monoidal closed structure on predI_{a}. Let D and E be pre dI domains. The tensor product of D and E is defined as follows:

D ⊗ E = ({t ⊆ D_{a} × E_{a}|(π_{1}(t)) ↑ & (π_{2}(t)) ↑ & t ≠ ∅ & t is down-closed }, ⊆)

The unit I is defined to be I = ({⊥}, =). Moreover, we define the internal-hom of D and E as follows:

D ⊸ E = ({T r(f)| f : D → E in predI_{a}}, ⊆)

Now, we want to have a symmetric monoidal comonad on predI_{a}. We will just state how the functor ! is defined on objects. Given a pre dI domain D, we define !D as follows:

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

The CPO structure on homsets is the stable order, that is, it is the order induced by the inclusion order on traces, and it is easy to check that the appropriate constructions enrich w.r.t. this structure. We also have to define monoidal natural transformations e and d. Given X ⊆ D we define ⌜d⌝^{X} = {d′ ∈ X|d′ ⊑ d}, and let D_{m} denote the set of minimal elements of D. The traces of the components are defined as follows:

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

Binary products and sums are defined as usual for CPOs, and the functor part of the strong monad on predI_{a} is the usual lift functor.

Note that predI_{a} is actually a model of Intuitionistic Affine Logic since I is a terminal object.

In the categorical semantics we used the operator (−)^{♯} to interpret the rule for recursion. Given a map f is defined to be a certain solution to the equation x = Φ_{f}(x). The solutions to x = Φ_{f}(x) are exactly the linear fixpoints of f, cf. the definitions given in previous sections. Linear fixpoints is the same as fixpoints in the category of free coalgebras under the assumption that we are dealing with a linear category. predI_{a} is actually a linear category, and the category of free coalgebras is equivalent to coK(predI_{a}), which is isomorphic to predI_{s}, the category of pre dI domains and continuous stable functions. This category has finite sums, but according to [HP90], a cartesian closed category with fixpoints and finite sums is equivalent to the category with one object and one arrow. Thus, predI_{s} cannot have fixpoints of arbitrary maps which entails that predI_{a} cannot have linear fixpoints of arbitrary maps. But we do only need linear fixpoints of maps with codomain in the image T, and we do have linear fixpoints of such maps, cf. the categorical results given above since predI_{a} is a model of LTS_{+Rec}.

Now, if we for a moment make the simplifying assumption that we only apply (−)^{♯} to maps without parameters, it is easy to see that linear fixpoints in predI_{a} are the same as fixpoints in dI_{s}, the category of dI domains and continuous stable functions. Notice that f :!T B → T B as well as f^{♯} : I → T B are maps in the subcategory dI_{a}. This category can also be shown to be a linear category with structure inherited from predI_{a}. Moreover, it has finite products, so the category of free coalgebras is closed under finite products. Again we have that the category of free coalgebras is equivalent to coK(dI_{a}), which is isomorphic to dI_{s}, the category of dI domains and continuous stable functions. Hence, to calculate a linear fixpoint with the operator (−)^{♯} in predI_{a}, is the same as calculating a fixpoint in dI_{s}.

7.2 The category O

The category O is itself a model of LTS_{+Rec}. We take as the required symmetric monoidal closed structure the cartesian closed structure, and as symmetric monoidal comonad we take the identity functor equipped with appropriate identity maps as components of the required natural transformations. The ordering on arrows is the pointwise ordering, and it is easy to check that the appropriate constructions enrich w.r.t. this structure. We also have to define monoidal natural transformations e and d with components e_{A} : A → 1 and d_{A} : A → A × A. As e_{A} we take the canonical map to the terminal object, and as d_{A} we take the diagonal map. Binary products and sums are defined as usual for CPOs. As strong monad we take the one induced by the lift construction on partial orders. It is obvious that hom(I, −) has the wanted properties.

Note that O is actually a model of Intuitionistic Logic since it is cartesian closed.

Acknowledgments. I am grateful to my supervisor, Glynn Winskel, for his guidance and encouragement. Thanks to Gavin Bierman and Valeria de Paiva for comments on a draft of this paper. The diagrams and proof-rules are produced using Paul Taylor’s macros.

References

[Abr90] S. Abramsky. Computational interpretations of linear logic. Technical Report 90/20, Department of Computing, Imperial College, 1990.

[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.

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

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

[Bra94] T. Braüner. A model of intuitionistic affine logic from stable domain theory. In ICALP ’94, LNCS 820, 1994.

[Gir87] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50, 1987.

[GLT89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

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

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

[Mac92] I. Mackie. Lilac : A Functional Programming Language Based on Linear Logic. M.Sc. dissertation, Imperial College, 1992.

[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.

[See89] R. A. G. Seely. Linear logic, ∗-autonomous categories, and cofree coalgebras. In Contemporary Mathematics, Categories in Computer Science and Logic, volume 92. American Mathematical Society, 89.

[Wad91] Philip Wadler. There’s no substitute for linear logic. Manuscript, 1991.

[Win93] G. Winskel. The Formal Semantics of Programming Languages. The MIT Press, 1993.

A Appendix, ILL in Natural Deduction style

Axiom

\begin{aligned}& (Id) \\ A ⊢ A \end{aligned}

Structural rule

Γ, A, B, Δ ⊢ C

(Exchange)

Γ, B, A, Δ ⊢ C

Logical rules, the I, ⊗, ⊸ fragment

\begin{aligned}& (1 − I) \\ ⊢ 1 \end{aligned}  Λ ⊢ 1 Γ ⊢ A ; (1 − E) ; Γ, Λ ⊢ A
Γ ⊢ A Δ ⊢ B ; (⊗ − I) ; Γ, Δ ⊢ A ⊗ B  Λ ⊢ A ⊗ B Γ, A, B ⊢ C ; (⊗ − E) ; Γ, Λ ⊢ C
Γ, A ⊢ B ; (⊸ −I) ; Γ ⊢ A ⊸ B  Λ ⊢ A ⊸ B Δ ⊢ A ; (⊸ −E) ; Λ, Δ ⊢ B

Logical rules, the &, ⊕ fragment

Γ ⊢ A Γ ⊢ B ; (& − I) ; Γ ⊢ A&B  Λ ⊢ A&B ; (& − E_{1}) ; Λ ⊢ A  Λ ⊢ A&B ; (& − E_{2}) ; Λ ⊢ B
Γ ⊢ A ; (⊕ − I_{1}) ; Γ ⊢ A ⊕ B Γ ⊢ B ; (⊕ − I_{2}) ; Γ ⊢ A ⊕ B Λ ⊢ A ⊕ B Γ, A ⊢ C Γ, B ⊢ C ; (⊕ − E) ; Γ, Λ ⊢ C

Logical rules, the ! fragment

Γ_{1} ⊢!A_{1} , ..., Γ_{n} ⊢!A_{n} !A_{1}, ...,!A_{n} ⊢ A ; (! − I) ; Γ_{1}, ..., Γ_{n} ⊢!A  Λ ⊢!A ; (Dereliction) ; Λ ⊢ A
Λ ⊢!A Γ,!A,!A ⊢ B ; (Contraction) ; Γ, Λ ⊢ B  Λ ⊢!A Γ ⊢ B ; (W eakening) ; Γ, Λ ⊢ B

B Appendix, ILL in Gentzen style

Axiom

\begin{aligned}& (Id) \\ A ⊢ A \end{aligned}

Structural rule

Γ, A, B, Δ ⊢ C

(Exchange)

Γ, B, A, Δ ⊢ C

Cut rule

Λ ⊢ A Δ, A ⊢ C

(Cut)
Δ, Λ ⊢ C

Logical rules, the I, ⊗, ⊸ fragment

\begin{aligned}& (1 − R) \\ ⊢ 1 \end{aligned}  Γ ⊢ C ; (1 − L) ; Γ, 1 ⊢ C
Γ ⊢ A Δ ⊢ B ; (⊗ − R) ; Γ, Δ ⊢ A ⊗ B  Γ, A, B ⊢ C ; (⊗ − L) ; Γ, A ⊗ B ⊢ C
Γ, A ⊢ B ; (⊸ −R) ; Γ ⊢ A ⊸ B  Λ ⊢ A Δ, B ⊢ C ; (⊸ −L) ; Δ, Λ, A ⊸ B ⊢ C

Logical rules, the &, ⊕ fragment

Γ ⊢ A Γ ⊢ B ; (& − R) ; Γ ⊢ A&B  Λ, A ⊢ C ; (& − L_{1}) ; Λ, A&B ⊢ C  Λ, B ⊢ C ; (& − L_{2}) ; Λ, A&B ⊢ C
Γ ⊢ A ; (⊕ − R_{1}) ; Γ ⊢ A ⊕ B  Γ ⊢ B ; (⊕ − R_{2}) ; Γ ⊢ A ⊕ B  Γ, A ⊢ C Γ, B ⊢ C ; (⊕ − L) ; Γ, A ⊕ B ⊢ C

Logical rules, the ! fragment

!A_{1}, ...,!A_{n} ⊢ A ; (! − R) ; !A_{1}, ...,!A_{n} ⊢!A  Γ, A ⊢ C ; (Dereliction) ; Γ,!A ⊢ C

Γ,!A,!A ⊢ C ; (Contraction) ; Γ,!A ⊢ C  Γ ⊢ C ; (W eakening) ; Γ,!A ⊢ C

C Appendix, LTS_{+Rec} with categorical semantics

Axiom

(Id)

x : A ⊢ x : A  A ^{η}^{}T A

Structural rule

(Exchange)

{Γ, x : A, y : B, Δ ⊢ u : C \atop Γ, y : B, x : A, Δ ⊢ u : C} Γ ⊗ A ⊗ B ⊗ Δ ^{u}^{}T C

Γ ⊗ B ⊗ A ⊗ Δ ^{Γ⊗≅⊗Δ}^{}Γ ⊗ A ⊗ B ⊗ Δ ^{u}^{}T C

Logical rules, the I, ⊗, ⊸ fragment

(1 − I)

⊢ ∗ : 1  I ^{η}^{}T I

(1 − E)

Λ ⊢ w : 1 Γ ⊢ u : A
Γ, Λ ⊢ let w be ∗ in u : A

{Λ ^{w}^{}T I Γ ^{u}^{}T A \atop Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ T I ^{t}^{}T (Γ ⊗ I) ^{kleisli(≅;u)}^{}T A}

(⊗ − I)

{Γ ⊢ u : A Δ ⊢ v : B \atop Γ, Δ ⊢ u ⊗ v : A ⊗ B}  {Γ ^{u}^{}T A Δ ^{v}^{}T B \atop Γ ⊗ Δ ^{u⊗v}^{}T A ⊗ T B ^{ψ}^{}T (A ⊗ B)}

(⊗ − E)

Λ ⊢ w : A ⊗ B Γ, x : A, y : B ⊢ u : C

Γ, Λ ⊢ let w be x ⊗ y in u : C

{Λ ^{w}^{}T (A ⊗ B) Γ ⊗ A ⊗ B ^{u}^{}T C \atop Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ T (A ⊗ B) ^{t}^{}T (Γ ⊗ A ⊗ B) ^{kleisli(u)}^{}T C}

(⊸ −I)

{Γ, x : A ⊢ u : B \atop Γ ⊢ λx.u : A ⊸ B}  {Γ ⊗ A ^{u}^{}T B \atop Γ ^{curry(u)}^{}A ⊸ T B ^{η}^{}T (A ⊸ T B)}

(⊸ −E)

{Λ ⊢ f : A ⊸ B Δ ⊢ u : A \atop Λ, Δ ⊢ fu : B}

{Λ ^{f}^{}T (A ⊸ T B) Δ ^{u}^{}T A \atop Λ ⊗ Δ ^{f⊗u}^{}T (A ⊸ T B) ⊗ T A ^{ψ}^{}T ((A ⊸ T B) ⊗ A) ^{kleisli(eval)}^{}T B}

Logical rules, the &, ⊕ fragment

(& − I)

{Γ ⊢ u : A Γ ⊢ v : B \atop Γ ⊢ (u, v) : A&B}  {Γ ^{u}^{}T A Γ ^{v}^{}T B \atop Γ ^{<u,v>}^{}T A × T B ^{η}^{}T (T A × T B)}

(& − E_{1})

{Λ ⊢ w : A&B \atop Λ ⊢ fst(w) : A}  {Λ ^{w}^{}T (T A × T B) \atop Λ ^{w}^{}T (T A × T B) ^{kleisli(π_{1})}^{}T A}

(& − E_{2}) Analogous. (⊕ − I_{1})

{Γ ⊢ w : A \atop Γ ⊢ inl(w) : A ⊕ B}  {Γ ^{w}^{}T A \atop Γ ^{w}^{}T A ^{T (inj_{1})}^{}T (A + B)}

(⊕ − I_{2}) Analogous. (⊕ − E)

Λ ⊢ w : A ⊕ B Γ, x : A ⊢ u : C Γ, y : B ⊢ v : C

Γ, Λ ⊢ case w of inl(x) => u | inr(y) => v : C
Λ ^{w}^{}T (A + B) Γ ⊗ A ^{u}^{}T C Γ ⊗ B ^{v}^{}T C

Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ T (A + B) ^{t}^{}T (Γ ⊗ (A + B)) ^{kleisli(≅;<u;v>)}^{}T C

Logical rules, the ! fragment

(! − I)

Γ_{1} ⊢ w_{1} :!A_{1} , ..., Γ_{n} ⊢ w_{n} :!A_{n} x_{1} :!A_{1}, ..., x_{n} :!A_{n} ⊢ u : A Γ_{1}, ..., Γ_{n} ⊢ let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in !u :!A

{Γ_{1} ^{w_{1}}^{}T!T A_{1} , ..., Γ_{n} ^{w_{n}}^{}T!T A_{n} !T A_{1} ⊗ ...⊗!T A_{n} ^{u}^{}T A \atop Γ_{1} ⊗ ... ⊗ Γ_{n} ^{w_{1}⊗...⊗w_{n}}^{}T!T A_{1} ⊗ ... ⊗ T!T A_{n} ^{ψ}^{}T (!T A_{1} ⊗ ...⊗!T A_{n}) ^{T (γ(u))}^{}T!T A}

(Dereliction)

Λ ⊢ u :!A

Λ ⊢ derelict(u) : A

{Λ ^{u}^{}T!T A \atop Λ ^{u}^{}T!T A ^{kleisli(ϵ)}^{}T A}

(W eakening)

Λ ⊢ w :!A Γ ⊢ u : B Γ, Λ ⊢ discard w in u : B

Λ ^{w}^{}T!T A Γ ^{u}^{}T B

Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ T!T A ^{t}^{}T (Γ⊗!T A) ^{kleisli((Γ⊗e);≅;u)}^{}T B

(Contraction)

Λ ⊢ w :!A Γ, x :!A, y :!A ⊢ u : B
Γ, Λ ⊢ copy w as x, y in u : B
Λ ^{w}^{}T!T A Γ⊗!T A⊗!T A ^{u}^{}T B

Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ T!T A ^{t}^{}T (Γ⊗!T A) ^{kleisli((Γ⊗d);u)}^{}T B

Other rules

(Recursion)

Γ_{1} ⊢ w_{1} :!A_{1} , ..., Γ_{n} ⊢ w_{n} :!A_{n} x_{1} :!A_{1}, ..., x_{n} :!A_{n}, z :!B ⊢ u : B Γ_{1}, ..., Γ_{n} ⊢ let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in recz.u : B

{Γ_{1} ^{w_{1}}^{}T!T A_{1} , ..., Γ_{n} ^{w_{n}}^{}T!T A_{n} !T A_{1} ⊗ ...⊗!T A_{n}⊗!T B ^{u}^{}T B \atop Γ_{1} ⊗ ... ⊗ Γ_{n} ^{w_{1}⊗...⊗w_{n}}^{}T!T A_{1} ⊗ ... ⊗ T!T A_{n} ^{ψ}^{}T (!T A_{1} ⊗ ...⊗!T A_{n}) ^{kleisli(u^{♯})}^{}T B}

D Appendix, operational semantics for LTS_{+Rec}

The I, ⊗, ⊸ fragment

∗ ⟶ ∗  {w ⟶ ∗ u ⟶ c \atop let w be ∗ in u ⟶ c}
{u ⟶ c v ⟶ d \atop u ⊗ v ⟶ c ⊗ d}  {w ⟶ d ⊗ e u[d/x, e/y] ⟶ c \atop let w be x ⊗ y in u ⟶ c}
λx.u ⟶ λx.u  {f ⟶ λx.v u ⟶ d v[d/x] ⟶ c \atop fu ⟶ c}

The &, ⊕ fragment

(u, v) ⟶ (u, v)  {w ⟶ (u, v) u ⟶ c \atop fst(w) ⟶ c}  {w ⟶ (u, v) v ⟶ c \atop snd(w) ⟶ c}
{w ⟶ d \atop inl(w) ⟶ inl(d)}  {w ⟶ e \atop inr(w) ⟶ inr(e)}
w ⟶ inl(d) u[d/x] ⟶ c

case w of inl(x) => u | inr(y) => v ⟶ c

w ⟶ inr(e) u[e/y] ⟶ c
case w of inl(x) => u | inr(y) => v ⟶ c

The ! fragment

w_{1} ⟶ c_{1} , ..., w_{n} ⟶ c_{n}
let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in !u ⟶ let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !u
u ⟶ let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in !v v[c_{1}/x_{1}, ..., c_{n}/x_{n}] ⟶ c

derelict(u) ⟶ c

w ⟶ d u[d/x, d/y] ⟶ c

copy w as x, y in u ⟶ c

w ⟶ d u ⟶ c discard w in u ⟶ c

Other rules

w_{1} ⟶ c_{1} , ..., w_{n} ⟶ c_{n} u[c_{1}/x_{1}, ..., c_{n}/x_{n}][!(let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in recz.u)/z] ⟶ c let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in recz.u ⟶ c

E Appendix, proof of the Soundness Theorem

Theorem E.1 (Soundness Theorem) Given a closed term u s.t. u ⟶ c, then [[u]] = [[c]].

Proof. Induction in the derivation of u ⟶ c. I will only cover the most interesting case, namely the case where the last used rule is: w_{1} ⟶ c_{1} , ..., w_{n} ⟶ c_{n} u[c_{1}/x_{1}, ..., c_{n}/x_{n}][!(let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in recz.u)/z] ⟶ c

let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in recz.u ⟶ c

Due to previous results, we know that for every r ∈ {1, ..., n} there exists a h_{r} : I → T A_{r} such that [[c_{r}]] = γ(h_{r}); η. We therefore have:

[[let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in recz.u]] =

[I ≅ ⊗_{r}I ^{⊗_{r}[[c_{r}]]}^{}⊗_{r} T!T A_{r} ^{ψ}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] =
[I ≅ ⊗_{r}I ^{⊗_{r}(γ(h_{r});η)}^{}⊗_{r} T!T A_{r} ^{ψ}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] =
[I ≅ ⊗_{r}I ^{⊗_{r}γ(h_{r})}^{}⊗_{r}!T A_{r} ^{⊗_{r}η}^{}⊗_{r} T!T A_{r} ^{ψ}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] =
[I ≅ ⊗_{r}I ^{⊗_{r}γ(h_{r})}^{}⊗_{r}!T A_{r} ^{η}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] =
[I ≅ ⊗_{r}I ^{⊗_{r}γ(h_{r})}^{}⊗_{r}!T A_{r} ^{[[u]]^{♯}}^{}T A]

Now, to prove the result is a matter of direct computation: [[c]] =^{∗} [[u[c_{1}/x_{1}, ..., c_{n}/x_{n}][!(let c_{1}, ..., c_{n} be x_{1}, ..., x_{n} in recz.u)/z]]] = [I ≅ (⊗_{r}I) ⊗ I ^{(⊗_{r}γ(h_{r}))⊗γ(≅;(⊗_{r}γ(h_{r}));[[u]]^{♯})}^{}(⊗_{r}!T A_{r})⊗!T A ^{[[u]]}^{}T A] = [I ≅ (⊗_{r}I) ⊗ I ^{(⊗_{r}γ(h_{r}))⊗(≅;(⊗_{r}γ(h_{r}));γ([[u]]^{♯}))}^{}(⊗_{r}!T A_{r})⊗!T A ^{[[u]]}^{}T A] = [I ≅ (⊗_{r}I) ⊗ I ^{(⊗_{r}γ(h_{r}))⊗(≅;(⊗_{r}γ(h_{r}))}^{}(⊗_{r}!T A_{r}) ⊗ (⊗_{r}!T A_{r}) ^{(Id⊗γ([[u]]^{♯}));[[u]]}^{}T A] = [I ≅ (⊗_{r}I) ⊗ (⊗_{r}I) ^{(⊗_{r}γ(h_{r}))⊗(⊗_{r}γ(h_{r}))}^{}(⊗_{r}!T A_{r}) ⊗ (⊗_{r}!T A_{r}) ^{(Id⊗γ([[u]]^{♯}));[[u]]}^{}T A] = [I ≅ ⊗_{r}I ^{⊗_{r}(≅;(γ(h_{r})⊗γ(h_{r})))}^{}⊗_{r} (!T A_{r}⊗!T A_{r}) ≅ (⊗_{r}!T A_{r}) ⊗ (⊗_{r}!T A_{r}) ^{(Id⊗γ([[u]]^{♯}));[[u]]}^{}T A] = [I ≅ ⊗_{r}I ^{⊗_{r}(γ(h_{r});d)}^{}⊗_{r} (!T A_{r}⊗!T A_{r}) ≅ (⊗_{r}!T A_{r}) ⊗ (⊗_{r}!T A_{r}) ^{(Id⊗γ([[u]]^{♯}));[[u]]}^{}T A] = [I ≅ ⊗_{r}I ^{⊗_{r}γ(h_{r})}^{}⊗_{r}!T A_{r} ^{D}^{}(⊗_{r}!T A_{r}) ⊗ (⊗_{r}!T A_{r}) ^{(Id⊗γ([[u]]^{♯}));[[u]]}^{}T A] =^{∗∗} [I ≅ ⊗_{r}I ^{⊗_{r}γ(h_{r})}^{}⊗_{r}!T A_{r} ^{[[u]]^{♯}}^{}T A] = [I ≅ ⊗_{r}I ^{⊗_{r}[[c_{r}]]}^{}⊗_{r} T!T A_{r} ^{ψ}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] =^{∗} [I ≅ ⊗_{r}I ^{⊗_{r}[[w_{r}]]}^{}⊗_{r} T!T A_{r} ^{ψ}^{}T (⊗_{r}!T A_{r}) ^{kleisli([[u]]^{♯})}^{}T A] = [[let w_{1}, ..., w_{n} be x_{1}, ..., x_{n} in recz.u]]

* Cf. the induction hypothesis. ** We are here using the fact that [[u]]^{♯} is a linear fixpoint of [[u]]. □

F Appendix, proof of the Approximation Lemma

Lemma F.1 (Approximation Lemma) Let x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : C be given. Let J be a finite set s.t. for all j ∈ J we are given ⊢ v_{j} : B_{j} and f_{j} ∈ hom(I, [[B_{j}]]) with the property that f_{j}; η ≲_{B_{j}} v_{j}. Moreover, assume that for each j we have a variable z_{j}, s.t. for all i, k ∈ J we have i ≠ k ⇒ z_{i} ≠ z_{k}, s.t. {x_{1}, ..., x_{n}} ⊆ {z_{j}| j ∈ J}, and s.t. for all r ∈ {1, ..., n} and j ∈ J we have x_{r} = z_{j} ⇒ A_{r} = B_{j}. We then have:

[I ≅ I ⊗ ... ⊗ I ^{f_{j_{1}}⊗...⊗f_{jn}}^{}[[A_{1}]] ⊗ ... ⊗ [[A_{n}]] ^{[[u]]}^{}T [[C]]] ≲_{C} u[..., v_{j}/z_{j}, ...]

where for all r in {1, ..., n} we have chosen j_{r} s.t. x_{r} = z_{j_{r}}.

Proof. If 1 ≤ p ≤ q ≤ n and Γ = x_{p} : A_{p}, ..., x_{q} : A_{q}, that is, it is a subsequence of x_{1} : A_{1}, ..., x_{n} : A_{n}, we will then define f_{Γ} : I → Γ to be the following morphism:

[I ≅ I ⊗ ... ⊗ I ^{f_{jp}⊗...⊗f_{jq}}^{}A_{p} ⊗ ... ⊗ A_{q}]

We proceed by induction in the derivation of x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : C. We will without loss of generality assume that none of the variables {z_{j}| j ∈ J} are bound in u.

I will only cover the most interesting case, namely the case where the last used rule is:

Γ_{1} ⊢ w_{1} :!A_{1} , ..., Γ_{m} ⊢ w_{m} :!A_{m} x_{1} :!A_{1}, ..., x_{m} :!A_{m}, z :!B ⊢ v : B
Γ_{1}, ..., Γ_{m} ⊢ let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v : B

We want to prove that ⋆_{1} ≲_{B} (let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v)[..., v_{j}/z_{j}, ...] where ⋆_{1} is the following morphism:

[I ≅ ⊗_{l}I ^{⊗_{l}f_{Γ_{l}}}^{}⊗_{l} Γ_{l} ^{⊗_{l}[[w_{l}]]}^{}⊗_{l} T!T A_{l} ^{ψ}^{}T (⊗_{l}!T A_{l}) ^{kleisli([[v]]^{♯})}^{}T B]

where l is in {1, ..., m}. Now, assume that ⋆_{1} ≠⊥. We then have for every l:

[I ^{f_{Γ_{l}}}^{}Γ_{l} ^{[[w_{l}]]}^{}T!T A_{l}] = [I ^{k_{l}}^{}!T A_{l} ^{η}^{}T!T A_{l}]

for some k_{l} : I →!T A_{l}. We now apply the induction hypothesis on Γ_{l} ⊢ w_{l} :!A_{l} and get for every l:

w_{l}[..., v_{j}/z_{j}, ...] ⟶ c_{l}  and  k_{l} ≲_{!A_{l}}^{∘} c_{l}

for some c_{l} ∈ C_{!A_{l}}. This entails that for every l we have k_{l} = γ(h_{l}) for some h_{l} : I → T A_{l}. Thus:

⋆_{1} =
[I ≅ ⊗_{l}I ^{⊗_{l}γ(h_{l})}^{}⊗_{l}!T A_{l} ^{⊗_{l}η}^{}⊗_{l} T!T A_{l} ^{ψ}^{}T (⊗_{l}!T A_{l}) ^{kleisli([[v]]^{♯})}^{}T B] =
[I ≅ ⊗_{l}I ^{⊗_{l}γ(h_{l})}^{}⊗_{l}!T A_{l} ^{[[v]]^{♯}}^{}T B] =
[I ≅ ⊗_{l}I ^{⊗_{l}γ(h_{l})}^{}⊗_{l}!T A_{l} ^{⨆_{n∈ω} Φ^{n}(⊥)}^{}T B] =
[I ^{⨆_{n∈ω}(≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥))}^{}T B]

where Φ is the continous function from hom(!T A_{1} ⊗ ...⊗!T A_{m}, T B) to itself, induced by the morphism [[u]]. Now, due to the Approximation Lemma, it is enough to show that for all n in ω:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥)}^{}T B] ≲_{B} (let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v)[..., v_{j}/z_{j}, ...]

We will prove this by induction in n. The assertion is true in the case n = 0 because any point followed by a bottom element is a bottom element. Let a number n be given and assume that the assertion is true in case of this n. We then want to show that the assertion is true in case of n + 1.

First a small initial calculation:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥)}^{}T B] ≠⊥

entails due to the inner IH that there exists a d in C_{B} such that:

(let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v)[..., v_{j}/z_{j}, ...] ⟶ d

But the rules for the evaluation relation then gives us:

let c_{1}, ..., c_{m} be x_{1}, ..., x_{m} in recz.v ⟶ d

The conclusion of the initial calculation is that:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥)}^{}T B] ≲_{B} let c_{1}, ..., c_{m} be x_{1}, ..., x_{m} in recz.v

But then the definition of the ≲_{!B}^{∘} relation entails that:

[I ^{γ(≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥))}^{}!T B] ≲_{!B}^{∘}!(let c_{1}, ..., c_{m} be x_{1}, ..., x_{m} in recz.v)

We can now use the outer IH on x_{1} :!A_{1}, ..., x_{m} :!A_{m}, z :!B ⊢ v : B to obtaim:

⋆_{2} ≲_{B} v[c_{1}/x_{1}, ..., c_{m}/x_{m}][!(let c_{1}, ..., c_{m} be x_{1}, ..., x_{m} in recz.v)/z]

where ⋆_{2} is defined to be the morphism:

[I ≅ I ⊗ ... ⊗ I ⊗ I ^{γ(h_{1})⊗...⊗γ(h_{m})⊗γ(≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥))}^{}!T A_{1} ⊗ ...⊗!T A_{m}⊗!T B ^{[[v]]}^{}T B]

Moreover:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n+1}(⊥)}^{}T B] =

[I ≅ ⊗_{l}I ^{⊗_{l}γ(h_{l})}^{}⊗_{l}!T A_{l} ^{⊗_{l}d}^{}⊗_{l} (!T A_{l}⊗!T A_{l}) ≅ (⊗_{l}!T A_{l}) ⊗ (⊗_{l}!T A_{l}) ^{(Id⊗γ(Φ^{n}(⊥)));[[v]]}^{}T B] =

[I ≅ ⊗_{l}I ^{⊗_{l}(≅;(γ(h_{l})⊗γ(h_{l})))}^{}⊗_{l} (!T A_{l}⊗!T A_{l}) ≅ (⊗_{l}!T A_{l}) ⊗ (⊗_{l}!T A_{l}) ^{(Id⊗γ(Φ^{n}(⊥)));[[v]]}^{}T B] =

[I ≅ I ⊗ I ^{≅⊗≅}^{}(⊗_{l}I) ⊗ (⊗_{l}I) ^{(⊗_{l}γ(h_{l}))⊗(⊗_{l}γ(h_{l}))}^{}(⊗_{l}!T A_{l}) ⊗ (⊗_{l}!T A_{l}) ^{(Id⊗γ(Φ^{n}(⊥)));[[v]]}^{}T B] =

[I ≅ I ⊗ I ^{≅⊗Id}^{}(⊗_{l}I) ⊗ I ^{(⊗_{l}γ(h_{l}))⊗Id}^{}(⊗_{l}!T A_{l}) ⊗ I ^{(Id⊗γ(≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥)));[[v]]}^{}T B] =

[I ≅ (⊗_{l}I) ⊗ I ^{(⊗_{l}γ(h_{l}))⊗Id}^{}(⊗_{l}!T A_{l}) ⊗ I ^{(Id⊗γ(≅;(⊗_{l}γ(h_{l}));Φ^{n}(⊥)));[[v]]}^{}T B] = [I ^{⋆_{2}}^{}T B] Now, our final calculation:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n+1}(⊥)}^{}T B] ≠⊥

entails that:

v[c_{1}/x_{1}, ..., c_{m}/x_{m}][!(let c_{1}, ..., c_{m} be x_{1}, ..., x_{m} in recz.v)/z] ⟶ c

for some c. But the rules for the evaluation relation then gives us:

(let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v)[..., v_{j}/z_{j}, ...] ⟶ c

Hence:

[I ^{≅;(⊗_{l}γ(h_{l}));Φ^{n+1}(⊥)}^{}T B] ≲_{B} (let w_{1}, ..., w_{m} be x_{1}, ..., x_{m} in recz.v)[..., v_{j}/z_{j}, ...] which finishes the proof that the above mentioned assertion is true in case of n + 1. □

G Appendix, categorical prerequisites

G.1 Monoidal categories

Definition G.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 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.

G.2 Monads

Definition G.2 A monad (T, η, μ) on C is a functor T : C → C, and two natural transformations:

η : Id_{C} → T μ : T T → T

such that the following diagrams commute:

[figure: T T T; T μ; T T; T T; μT; μ; T; μ; T; ηT; T T; T η; T; Id_{T}; Id_{T}; T; μ]

Definition G.3 Let (C, I, ⊗, α, λ, ρ) be a monoidal category and (T, η, μ) a monad on C. The monad is called strong iff there is a “strength” natural transformation t : (−) ⊗ T (+) → T (− ⊗ +) s.t. the following diagrams commute:

[figure: A ⊗ (B ⊗ T C); Id ⊗ t; A ⊗ T (B ⊗ C); t; T (A ⊗ (B ⊗ C)); (A ⊗ B) ⊗ T C; α; t; T ((A ⊗ B) ⊗ C); T α; I ⊗ T A; t; T (I ⊗ A); λ; T A; T λ]

[figure: A ⊗ B; Id ⊗ η; A ⊗ T B; η; T (A ⊗ B); t; A ⊗ T T B; t; T (A ⊗ T B); T t; T T (A ⊗ B); A ⊗ T B; Id ⊗ μ; t; T (A ⊗ B); μ]

The usual definition of a map between monads assume that the domain and codomain monads are on the same category. The following is a generalisation without this assumption.

Definition G.4 A functor of monads from a monad (T, η, μ) on C to a monad (T′, η′, μ′) on C′ is a functor F : C → C′ and a natural transformation σ : T′F → F T s.t. the following diagrams commute:

[figure: F; F η; T′F; η′F; σ; F T; T′T′F; T′σ; T′F T; σT; F T T; T′F; μ′F; σ; F T; F μ]

Definition G.5 Let (T, η, μ, t) be a strong monad on a monoidal category (C, I, ⊗) and (T′, η′, μ′, t′) a strong monad on a monoidal category (C′, I′, ⊗′). A functor of monads (F, σ) from (T, η, μ) to (T′, η′, μ′) is a functor of strong monads iff F is monoidal and the following diagram commutes:

[figure: F A ⊗′ T′F B; F A ⊗′ σ; F A ⊗′ F T B; n; F (A ⊗ T B); T′(F A ⊗′ F B); t′; T′n; T′F (A ⊗ B); σ; F T (A ⊗ B); F t]

where n is the natural transformation giving monoidal structure to F.

G.3 Comonads

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

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

such that the following diagrams commute:

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

Definition G.7 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 hom_{C_{!}}(A, B) = hom_{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-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.

RS-94-16 Lars Arge. External-Storage Data Structures for Plane-Sweep Algorithms. June 1994, 37 pp.

RS-94-15 Mogens Nielsen and Glynn Winskel. Petri Nets and Bisimulations. May 1994, 36 pp.

RS-94-14 Nils Klarlund. The Limit View of In�nite Computations. May 1994, 16 pp. To appear in the LNCS proceedings of Concur ’94, LNCS, 1994.

RS-94-13 Glynn Winskel. Stable Bistructure Models of PCF. May 1994, 26 pp. Preliminary draft. Invited lecture for MFCS ’94. To appear in the proceedings of MFCS ’94, LNCS, 1994.