BRICS RS-95-13 T. Bra� uner: The Girard Translation Extended with Recursion

BRICS

Basic Research in Computer Science

The Girard Translation Extended with Recursion

Torben Bra� uner

BRICS Report Series RS-95-13 ISSN 0909-0878 February 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, 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

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

The Girard Translation Extended with Recursion^{∗}

Torben Braüner

BRICS^{†}

Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C, Denmark Internet: tor@daimi.aau.dk

Abstract

This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the λ^{rec}-calculus and the linear λ^{rec}-calculus respectively, are given sound categorical interpretations. The embedding of proofs of IL into proofs of ILL given by the Girard Translation is extended with the rules for recursion, such that an embedding of terms of the λ^{rec}-calculus into terms of the linear λ^{rec}-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.

∗Full version of paper to appear in Proceedings of CSL ’94, LNCS 933, 1995.

† Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Contents

1 Introduction 4

2 The Categorical Picture 6 2.1 Previous Work and Related Results . . . . . . . . . . . . . . . . . . . . . . 6 2.2 How to deal with parameters . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Fixpoints in Cartesian Categories . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 Linear Fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.5 Generalisation of Linear Fixpoints . . . . . . . . . . . . . . . . . . . . . . . 24 2.6 Concrete Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

3 The λ-Calculus 27 3.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.2 The Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . . . . . . . 28 3.3 Categorical Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

4 The Linear λ-Calculus 30 4.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.2 The Curry-Howard Isomorphism . . . . . . . . . . . . . . . . . . . . . . . . 31 4.3 Categorical Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

5 The Girard Translation 32 5.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.2 Soundness with Respect to Categorical Semantics . . . . . . . . . . . . . . 32

6 Extensions with Finite Sums 37 6.1 The λ-Calculus Extended with Finite Sums . . . . . . . . . . . . . . . . . 37 6.2 The linear λ-Calculus Extended with Finite Sums . . . . . . . . . . . . . . 38 6.3 The Girard Translation Extended with Finite Sums . . . . . . . . . . . . . 38

7 Extensions with Recursion 40 7.1 The λ^{rec}-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 7.2 The linear λ^{rec}-Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 7.3 The Girard Translation Extended with Recursion . . . . . . . . . . . . . . 42 7.4 The Choice of Rule for Recursion in the linear λ^{rec}-Calculus . . . . . . . . 43

A Appendix, The λ^{rec}-Calculus with Categorical Semantics 48

B Appendix, Natural Deduction Formulation of IL (Extended with Recursion) 50

C Appendix, The linear λ^{rec}-Calculus with Categorical Semantics 51 D Appendix, Natural Deduction Formulation of ILL (Extended with Re-

cursion) 54

E Appendix, The Girard Translation (Extended with Recursion) 56

F Appendix, (Linear) Fixpoint Objects 58 F.1 Fixpoint Objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 F.2 Linear Fixpoint Objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 F.3 Linear Fixpoint Objects and the Intrinsic Preorder . . . . . . . . . . . . . 67

G Appendix, Remarks on Recursion at the Level of Types 77

1 Introduction

Linear Logic was discovered by J.-Y. Girard in 1987 and published in the 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. This paper deals with a Curry-Howard interpretation of the intuitionistic fragment of Linear Logic, appropriate for recursion.

The original Curry-Howard isomorphism, [How80], relates the natural deduction formulation of IL to the λ-calculus; formulas correspond to types, proofs to terms, and normalisation of proofs to reduction of terms. This is dealt with in [GLT89] and in [Abr90]; the first emphasizes the logic side of the isomorphism, the second the computational side. The fundamental idea of categorical logic is that formulas are interpreted as objects, proof-rules as natural operations on maps, and proofs as maps. We can give a sound interpretation of IL in a cartesian closed category, so given the above mentioned Curry-Howard isomorphism, this induces a sound categorical interpretation of the λ-calculus; types are interpreted as objects, typing rules as natural operations on arrows, and derivations of type assignments as maps.

ILL can be given a Curry-Howard interpretation in the same way as the Curry-Howard interpretation of IL. In [Abr90] the first Curry-Howard interpretation of ILL is introduced. The resulting term language is essentially a refinement of the usual λ-calculus where copying and discarding of values is written explicitly in the terms. One of the rules of this system has the property that it forces ! to be isomorphic to !! in any reasonable categorical interpretation, as pointed out in [Wad91]. In 1992 this was remedied by the authors of [BBdPH92] (and by the author of this paper) by changing the rule in an appropriate way, and by discovering a natural deduction formulation equivalent to the Gentzen style formulation of ILL (the hitherto known natural deduction formulation, [Mac91] did not possess that property). This work settled the question about how to interpret ILL via a Curry-Howard isomorphism. The Curry-Howard interpretation of ILL, the linear λcalculus, is in [BBdPH92] given a sound categorical interpretation.

The [Gir87] paper introduced the Girard Translation which embeds IL into ILL. This translation works at the level of formulas as well as at the level of proofs. The Girard Translation at the level of proofs induce an embedding of terms of the λ-calculus into terms of the linear λ-calculus via the Curry-Howard isomorphisms. The embedding preserves β reductions. At the semantic level, a categorical model for the linear λ-calculus, that is, a linear category C with finite products, induces a categorical model for the λ-calculus, that is, a cartesian closed category. This is the category of free coalgebras with respect to the comonad on C. So, given a categorical model for the linear λ-calculus, we can interpret the linear λ-calculus as well as the λ-calculus. The embedding of terms is shown to be sound with respect to the categorical interpretations, that is, it is shown to correspond to the adjunction between C and the category of free coalgebras in a precise way, which is a categorical generalisation of a result in [Gir87] showing that the Girard Translation is sound with respect to interpretation in the category of coherence spaces and linear stable functions.

We can give a sound categorical interpretation of the linear λ-calculus extended with finite sums using a linear category with finite products and finite sums. The category of free coalgebras induced by a linear category with finite products and finite sums has weak finite sums, and moreover, the weak finite sums satisfy certain additional conditions making it possible to give a categorical interpretation of the λ-calculus extended with finite sums, which is sound with respect to β and η reductions. Note that we give a sound interpretation using weak finite sums satisfying certain additional conditions, and not by using finite sums. This is a categorical generalisation of the sound interpretation given in [GLT89], where the category of coherence spaces and stable functions is used; a category that has weak finite sums, but not finite sums. We also have that the Curry-Howard isomorphisms and the Girard Translation still work in a way such that the induced embedding of terms is shown to be sound with respect to the categorical interpretations.

The above mentioned Curry-Howard isomorphisms will in the present paper be extended to deal with the λ-calculus and the linear λ-calculus extended with rules for recursion, the λ^{rec}-calculus and the linear λ^{rec}-calculus. The Girard Translation at the level of proofs is extended with the rules for recursion such that an embedding of terms of the λ^{rec}- calculus into terms of the linear λ^{rec}-calculus is induced. The embedding preserves the reduction rule for recursion. At the semantic level, a sound categorical model for the linear λ^{rec}-calculus, that is, a linear category C with finite products and a parametrised linear fixpoint operator, induces a sound categorical model for the λ^{rec}-calculus, that is, a cartesian closed category with a parametrised fixpoint operator, and moreover, the embedding of terms is shown to be sound with respect to the categorical interpretations.

An appendix on linear fixpoint objects is included for the sake of completeness. A linear fixpoint object is essentially a linear version of a fixpoint object in a cartesian closed category with a strong monad, [CP90]. It is shown that a linear category with a linear fixpoint object induces a unique parametrised linear fixpoint operator satisfying a linear version of Plotkin’s Axiom. It is moreover shown how certain axioms entails that the linear fixpoint of a map is the least upper bound of an appropriate increasing chain with respect to the intrinsic preorder. This makes the induced coKleisli category rational, [AJM95] with respect to the partial order obtained as the quotient of the intrinsic preorder. Thus, we have paved the way for an adequacy result; this topic will be dealt with elsewhere in details.

We have moreover included an appendix with some remarks on recursion at the level of types.

The extensions of IL and ILL with rules for recursion makes every formula provable, so they should not be understood as having logical meaning. Neither should the extension of the Girard Translation and the extensions of the Curry-Howard isomorphisms be understood as having logical meaning. The role of the extensions are to extend the translation from terms in the λ-calculus to terms in the linear λ-calculus to a translation from terms in the λ^{rec}-calculus to terms in the linear λ^{rec}-calculus.

It is shown in [HP90] that a cartesian closed category with finite sums and a fixpoint operator is inconsistent, that is, it is equivalent to the category consisting of one object and one arrow. But the category of CPOs and strict continuous functions is a consistent linear category with finite sums and a linear fixpoint operator; so the presence of a linear fixpoint operator in a linear category is consistent with the presence of finite sums. Thus, the inconsistency of recursion with this standard construct vanish when we go to a linear context, which is in accordance with [Plo93].

In [MRA93] a different approach to recursion in a linear context is taken. The (I, ⊗, ⊸) fragment of the linear λ-calculus is extended with natural numbers, corresponding to a weak natural numbers object in the categorical model. The discussion above implies that this approach is consistent with ours.

In what follows we will frequently abuse the use of notation by applying the same notation to denote the same kind of structure in different categories.

2 The Categorical Picture

2.1 Previous Work and Related Results

In what follows, we need the notion of a categorical model for the (I, ⊗, ⊸,!) fragment of ILL as defined in [BBdPH92]:

Definition 2.1 A !-category is a symmetric monoidal category (C, I, ⊗) equipped with:

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

2. Monoidal natural transformations e :!(−) → I and d :!(−) →!(−)⊗!(−) such that

(a) e_{A} and d_{A} are maps of coalgebras,

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

(c) maps between free coalgebras are maps between cocommutative comonoids.

A linear category is a !-category where each functor (−)⊗A has a right adjoint A ⊸ (−).

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  \overline{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}).

We also need the notion of a generalised coKleisli operator, as defined in [BBdPH92]:

Definition 2.2 Given a map f :!A_{1} ⊗ ...⊗!A_{n} → B in a !-category, we define γ(f) to be the composite

!A_{1} ⊗ ...⊗!A_{n} ^{δ_{A_{1}}⊗...⊗δ_{An}}^{}!!A_{1} ⊗ ...⊗!!A_{n} ^{m_{A_{1},...,An}}^{}!(!A_{1} ⊗ ...⊗!A_{n}) ^{!f}^{}!B

In case n = 1 this definition is consistent with the usual coKleisli operator. Note that the definition of γ does not assume the presence of finite products. In [See89] another notion of a categorical model for ILL is defined where the induced generalised coKleisli operator relies on the existence of finite products.

Given a category C equipped with a comonad (!, ε, δ), the coEilenberg-Moore category, C^{!}, is the category of coalgebras. We have an adjunction U^{!} ⊣ F^{!} between C^{!} and C; the functor U^{!} : C^{!} → C simply forgets the coalgebra structure, while the functor F^{!} : C → C^{!} takes an object B to the coalgebra (!B, δ), and a map f : B → C to the map of coalgebras !f : (!B, δ) → (!C, δ). The adjunction between the functors U^{!} and F^{!} is given by the following natural bijection between maps:

ϕ_{(A,h),B} : C^{!}((A, h), F^{!}B) ≅ C(U^{!}(A, h), B)

where ϕ(f) = f; ε_{B} : A → B and ϕ^{−1}(g) = h; !g : (A, h) → (!B, δ). Note that if (A, h) is equal to (!A_{1}, δ) ⊗ ... ⊗ (!A_{n}, δ), then ϕ^{−1} coincides with the generalised coKleisli operator γ. The category of free coalgebras is the full subcategory of C^{!} whose objects are free coalgebras, that is, coalgebras of the kind (!B, δ). We will denote the category of free coalgebras by F ree(C^{!}) in what follows. The adjunction U^{!} ⊣ F^{!} can be restricted to an adjunction between F ree(C^{!}) and C. Note that F ree(C^{!}) 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 F ree(C^{!}).

Definition 2.3 Let C be a category equipped with a comonad (!, ε, δ). A map of free coalgebras is called linear iff it is in the image of F^{!}.

It is shown in [Bie94] that a symmetric monoidal comonad (!, ε, δ, m_{I}, m) on a symmetric monoidal category (C, I, ⊗) induces a symmetric monoidal structure on C^{!}; the unit I of the tensor product is given by the coalgebra (I, m_{I}), and given two coalgebras (A, k) and (B, h), their tensor product (A, k)⊗(B, h) is given by the coalgebra (A⊗B, (k⊗h); m_{A,B}). If moreover C is a !-category, then the symmetric monoidal structure on C^{!} is a finite product structure, that is, I is a terminal object, and (A, k) ⊗ (B, h) is a binary product of (A, k) and (B, h) when equipped with (A⊗(h; e_{B})); ≅ and ((k; e_{A})⊗B); ≅ as projections. Given (A, k), a unique map from (A, k) to I is given by k; e_{A}, and given maps f : (C, l) → (A, k) and g : (C, l) → (B, h), a unique map from (C, l) to (A, k) ⊗ (B, h) making the appropriate diagrams commute is given by l; d_{C}; (e_{C} ⊗ e_{C}); (f ⊗ g).

Now, assume that a symmetric monoidal closed category (C, I, ⊗, ⊸) is equipped with a symmetric monoidal comonad (!, ε, δ, m_{I}, m). Then C^{!} has a symmetric monoidal structure, as mentioned above, and moreover, it is shown in [Bie94] that every free coalgebra is exponentiable with respect to the monoidal structure on C^{!}. The internal-hom object (A, h) ⇒ (!B, δ) of (A, h) and (!B, δ) is given by (!(A ⊸ B), δ), and we have the following bijections between maps such that each is natural in (C, k):

C^{!}((C, k) ⊗ (A, h), (!B, δ)) = C^{!}((C, k) ⊗ (A, h), F^{!}B)
≅ C(U^{!}((C, k) ⊗ (A, h)), B)  U^{!} ⊣ F^{!}
= C(U^{!}(C, k) ⊗ A, B)
≅ C(U^{!}(C, k), A ⊸ B)  (−) ⊗ A ⊣ A ⊸ (−)
≅ C^{!}((C, k), F^{!}(A ⊸ B))  U^{!} ⊣ F^{!}
= C^{!}((C, k), (!(A ⊸ B), δ))
= C^{!}((C, k), (A, h) ⇒ (!B, δ))

Definition 2.4 Let C be a !-category. We will say that F ree(C^{!}) is closed under finite products iff the terminal object I in C^{!} is isomorphic to a free coalgebra, and given two free coalgebras (!A, δ) and (!B, δ), their product (!A, δ) ⊗ (!B, δ) in C^{!} is isomorphic to a free coalgebra.

Proposition 2.5 Let C be a !-category. The category F ree(C^{!}) is closed under finite products iff F ree(C^{!}) has finite products (1, ×) such that 1 is a terminal object in C^{!} and such that (!A, δ) × (!B, δ) is a binary product of (!A, δ) and (!B, δ) in C^{!}.

Proof. Straightforward calculation. □

If C is a !-category such that F ree(C^{!}) is closed under finite products, then Proposition 2.5 entails that we have an isomorphism n_{I} : I → 1 and a natural isomorphism n_{(!A,δ),(!B,δ)} : (!A, δ) ⊗ (!B, δ) → (!A, δ) × (!B, δ) because diagrams of the finite products (1, ×) on F ree(C^{!}) are universal in C^{!}.

If C is a linear category such that F ree(C^{!}) is closed under finite products, then the internal-hom objects induce a cartesian closed structure on F ree(C^{!}). The finite products (1, ×) is given by the assumption that F ree(C^{!}) is closed under finite products, cf. Proposition 2.5, and an appropriate bijection between maps is given by the following composite of bijections:

C^{!}((!C, δ) × (!A, δ), (!B, δ)) ≅ C^{!}((!C, δ) ⊗ (!A, δ), (!B, δ))  composition with n
≅ C^{!}((!C, δ), (!A, δ) ⇒ (!B, δ))  (!B, δ) is exponentiable

Since the composite of bijections is natural in (!C, δ), it follows from the Pointwise Adjointness Theorem, [BW90] that (!A, δ) ⇒ (−) can be extended to a right adjoint to (−) × (!A, δ). Moreover, we have that

Proposition 2.6 Let C be a linear category such that F ree(C^{!}) is closed under finite products. Given a map f : A → B, then the map

(!C, δ) ⇒ F^{!}(f) : (!C, δ) ⇒ F^{!}(A) ⟶ (!C, δ) ⇒ F^{!}(B)

is equal to F^{!}(Id ⊸ f) and thus linear.

Proof. The following calculation proves the result:

(!C, δ) ⇒ F^{!}(f) = λ(eval; F^{!}(f))  def. of ⇒
= ϕ^{−1}(λ(ϕ(n; n^{−1}; ϕ^{−1}(λ^{−1}(ϕ(Id))); F^{!}(f))))  def. of λ and eval
= ϕ^{−1}(λ(ϕ(ϕ^{−1}(λ^{−1}(ϕ(Id))); F^{!}(f))))
= ϕ^{−1}(λ(λ^{−1}(ϕ(Id)); f))
= ϕ^{−1}(ϕ(Id); (Id ⊸ f))
= F^{!}(Id ⊸ f)

□

Proposition 2.7 Let C be a linear category such that F ree(C^{!}) is closed under finite products. Given a map of free coalgebras f : (!A, δ) → (!B, δ), then the map

f ⇒ (!C, δ) : (!B, δ) ⇒ (!C, δ) ⟶ (!A, δ) ⇒ (!C, δ)

is equal to F^{!}(f ⊸ Id) and thus linear.

Proof. The following calculation proves the result:

f ⇒ (!C, δ) = λ((Id × f); eval)  def. of ⇒
= ϕ^{−1}(λ(ϕ(n^{−1}; (Id × f); n; ϕ^{−1}(λ^{−1}(ϕ(Id))))))  def. of λ and eval
= ϕ^{−1}(λ(ϕ((Id ⊗ f); ϕ^{−1}(λ^{−1}(ϕ(Id))))))
= ϕ^{−1}(λ((Id ⊗ f); λ^{−1}(ϕ(Id))))
= ϕ^{−1}(λ((ϕ(Id) ⊗ f); eval))
= ϕ^{−1}(ϕ(Id); λ((Id ⊗ f); eval))
= ϕ^{−1}(ϕ(Id); (f ⊸ Id))  def. of ⊸
= F^{!}(f ⊸ Id)

□

Now, under which circumstances is F ree(C^{!}) closed under finite products? The following observation induces a sufficient condition:

Proposition 2.8 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 products × then (!(A × B), δ) is a binary product of (!A, δ) and (!B, δ) in C^{!}.

Proof. The free functor F^{!} : C → C^{!} preserves finite products because it has a left adjoint, so a terminal object 1 in C is sent into a terminal object (!1, δ) in C^{!}, and a product diagram A ← A × B → B in C is sent into a product diagram (!A, δ) ← (!(A × B), δ) → (!B, δ) in C^{!}. □

We will for later use note a couple of facts following from the proof of Proposition 2.8. The following bijections

C^{!}((C, k), (!1, δ)) = C^{!}((C, k), F^{!}1)
≅ C(U^{!}(C, k), 1)  U^{!} ⊣ F^{!}
= C(C, 1)

make (!1, δ) a terminal object, and the following bijections

C^{!}((C, k), (!A, δ)) × C^{!}((C, k), (!B, δ)) = C^{!}((C, k), F^{!}A) × C^{!}((C, k), F^{!}B)
≅ C(U^{!}(C, k), A) × C(U^{!}(C, k), B)  U^{!} ⊣ F^{!}
≅ C(U^{!}(C, k), A × B)
≅ C^{!}((C, k), F^{!}(A × B))  U^{!} ⊣ F^{!}
= C^{!}((C, k), (!(A × B), δ))

make (!A, δ) ← (!(A × B), δ) → (!B, δ) a product diagram.

If C is a !-category with finite products, then Proposition 2.8 entails that F ree(C^{!}) is closed under finite products. This induce an isomorphism n_{1} : I →!1, and a natural isomorphism n_{A,B} :!A⊗!B →!(A × B). It can be shown that the map n_{1} and the natural isomorphism n makes ! a symmetric monoidal functor from (C, 1, ×) to (C, I, ⊗). Given these isomorphisms, we can define a model for ILL as described in [See89]. Calculations show that the way the isomorphisms are defined and the universal properties of I and (!A, δ) ⊗ (!B, δ) in C^{!} forces ! to take the cocommutative comonoid structure with respect to the finite products to the cocommutative comonoid structure with respect to the symmetric monoidal structure, that is, e_{A} is equal to the composite

!A ^{!<>}^{}!1 ^{n^{−1}}^{}I

and d_{A} is equal to the composite

!A ^{!Δ}^{}!(A × A) ^{n^{−1}}^{}!A⊗!A

If C is a category with a comonad (!, ε, δ), then an initial object 0 in C induces a weak initial object in F ree(C^{!}) and binary sums + in C induce weak binary sums in F ree(C^{!}), as pointed out in [Bie94]. The weak initial object 0 is given by the free coalgebra (!0, δ), and given two free coalgebras (!A, δ) and (!B, δ), their weak binary sum (!A, δ) + (!B, δ) is given by the free coalgebra (!(!A+!B), δ) when equipped with δ; !in_{1} and δ; !in_{2} as injections. Given a free coalgebra (!C, δ), a map from 0 to (!C, δ) is given by ![], and given maps f : (!A, δ) → (!C, δ) and g : (!B, δ) → (!C, δ), a map from (!A, δ) + (!B, δ) to (!C, δ) making the appropriate diagrams commute is given by ![(f; ε), (g; ε)]. One can actually show more than that:

Proposition 2.9 Let C be a category with a comonad. If C has an initial object 0, then the family of maps of free coalgebras [] : 0 → (!C, δ) induced by the weak initial object is natural in (!C, δ) with respect to linear maps. If C has binary sums +, then the operation on maps of free coalgebras

[−, +] : C^{!}((!A, δ), (!C, δ)) × C^{!}((!B, δ), (!C, δ)) → C^{!}((!A, δ) + (!B, δ), (!C, δ))

induced by the weak binary sums is natural in (!C, δ) with respect to linear maps.

Proof. Let a map h : C → D be given. Then

[]; !h = ![]; !h  def. of [] in F ree(C^{!})
= ![]
= []  def. of [] in F ree(C^{!})

and given maps f : (!A, δ) → (!C, δ) and g : (!B, δ) → (!C, δ), we have

[f, g]; !h = ![(f; ε), (g; ε)]; !h  def. of [−, +] in F ree(C^{!})
= ![(f; ε; h), (g; ε; h)]
= ![(f; !h; ε), (g; !h; ε)]
= [(f; !h), (g; !h)]  def. of [−, +] in F ree(C^{!})

□

Proposition 2.10 Let C be a category with a comonad. If C has an initial object 0, then the map of free coalgebras [] : 0 → 0 induced by the weak initial object is equal to the identity. If C has binary sums +, then the map of free coalgebras

[in_{1}, in_{2}] : (!A, δ) + (!B, δ) → (!A, δ) + (!B, δ)

induced by the weak binary sums is equal to the identity.

Proof. Straightforward calculation. □

The last two results might seem ad hoc, but it turns out that they are suffucint to give a categorical interpretation of the λ-calculus extended with finite sums which is sound with respect to β and η reductions.

2.2 How to deal with parameters

Before considering fixpoints, we need some results enabling us to deal with parameters. Let C be a !-category. With any object A one may associate a comonad (S^{A}, ε^{A}, δ^{A}). The functor S^{A} is given by !A ⊗ (−), a component ε_{B}^{A} is given by

S^{A}B =!A ⊗ B ^{e_{A}⊗B}^{}I ⊗ B ≅ B

and a component δ_{B}^{A} is given by the composite

S^{A}B =!A ⊗ B ^{d_{A}⊗B}^{}(!A⊗!A) ⊗ B ≅!A ⊗ (!A ⊗ B) = S^{A}S^{A}B

We will in what follows show that the functor S^{A} together with the natural transformations ε^{A} and δ^{A} indeed is a comonad. Commutativity of the following diagram

[figure: S^{A}; δ^{A}; S^{A}S^{A}; S^{A}S^{A}; δ^{A}; S^{A}δ^{A}; S^{A}S^{A}S^{A}; δ^{A}S^{A}]

follows from commutativity of the following diagram

[figure: !A ⊗ B; d ⊗ B; (!A⊗!A) ⊗ B; ≅; !A ⊗ (!A ⊗ B)]

[figure: 1.; ((!A⊗!A)⊗!A) ⊗ B; (d ⊗ Id) ⊗ B; ≅; (!A⊗!A) ⊗ (!A ⊗ B); d ⊗ (Id ⊗ B)]

[figure: (!A⊗!A) ⊗ B; d ⊗ B; (Id ⊗ d) ⊗ B; (!A ⊗ (!A⊗!A)) ⊗ B; ≅ ⊗B]

[figure: !A ⊗ (!A ⊗ B); ≅; Id ⊗ (d ⊗ B); !A ⊗ ((!A⊗!A) ⊗ B); ≅; Id⊗ ≅; !A ⊗ (!A ⊗ (!A ⊗ B)); ≅]

1. d is part of a comonoid.

Commutativity of the following diagram

S^{A}

[figure: Id; Id]
[figure: S^{A}; S^{A}ε^{A}; S^{A}S^{A}; δ^{A}; ε^{A}S^{A}; S^{A}]

follows from commutativity of the following two diagrams

!A ⊗ B ^{_{}Id}  !A ⊗ B
[figure: Id]  1.
[figure: !A ⊗ B; ≅ ⊗B; (!A ⊗ I) ⊗ B; ≅ ⊗B; (Id ⊗ e) ⊗ B; (!A⊗!A) ⊗ B; d ⊗ B]

[figure: !A ⊗ B; Id; Id⊗ ≅; !A ⊗ (I ⊗ B); ≅; Id ⊗ (e ⊗ B); !A ⊗ (!A ⊗ B); ≅]

1. e is part of a comonoid.

!A ⊗ B  \overline{Id  ^{}}!A ⊗ B
1.  [figure: Id]
[figure: (!A⊗!A) ⊗ B; d ⊗ B; (e ⊗ Id) ⊗ B; (I⊗!A) ⊗ B; ≅ ⊗B; ≅ ⊗B; !A ⊗ B]

[figure: !A ⊗ (!A ⊗ B); ≅; e ⊗ (Id ⊗ B); I ⊗ (!A ⊗ B); ≅; ≅; !A ⊗ B; Id]

1. e is part of a comonoid.

Moreover, we have a distributive law λ^{A} : S^{A}! →!S^{A} of the comonad (!, ε, δ) over the comonad (S^{A}, ε^{A}, δ^{A}), [BW85]. A component λ_{B}^{A} is given by the composite:

S^{A}!B =!A⊗!B ^{δ_{A}⊗Id}^{}!!A⊗!B ^{m}^{}!(!A ⊗ B) =!S^{A}B

We will in what follows show that the natural transformation λ indeed is a distributive law. Commutativity of the following diagram

S^{A}!  \overline{λ^{A}  ^{}}!S^{A}
[figure: ε^{A}!; !ε^{A}]

!

follows from commutativity of the following diagram

[figure: !A⊗!B; δ ⊗ Id; !!A⊗!B; m; !(!A ⊗ B)]

1.

[figure: I⊗!B; e ⊗ Id; m_{I} ⊗ Id; !I⊗!B; !e ⊗ Id; m; !(I ⊗ B); !(e ⊗ B)]
[figure: ≅; 2.; ! ≅]
!B

1. e is a map of coalgebras. 2. ! is monoidal. Commutativity of the following diagram

S^{A}!  \overline{λ^{A}  ^{}}!S^{A}
[figure: S^{A}ε; εS^{A}]
S^{A}

follows from commutativity of the following diagram

[figure: !A⊗!B; δ ⊗ Id; !!A⊗!B; m; !(!A ⊗ B)]
[figure: Id ⊗ ε; 1.; ε]
!A ⊗ B^{ε ⊗ ε^{}}

1. ε is monoidal. Commutativity of the following diagram

[figure: S^{A}!; λ^{A}; !S^{A}; S^{A}S^{A}!; δ^{A}!; S^{A}λ^{A}; S^{A}!S^{A}; λ^{A}S^{A}; !S^{A}S^{A}; !δ^{A}]

[figure: !A⊗!B; δ ⊗ Id; !!A⊗!B; m; !(!A ⊗ B)]

1.

[figure: (!A⊗!A)⊗!B; d ⊗ Id; (δ ⊗ δ) ⊗ Id; (!!A⊗!!A)⊗!B; m ⊗ Id; !(!A⊗!A)⊗!B; !d ⊗ Id; m; !((!A⊗!A) ⊗ B); !(d ⊗ Id)]

2.

[figure: !A ⊗ (!A⊗!B); ≅; δ ⊗ (δ ⊗ Id); !!A ⊗ (!!A⊗!B); ≅; Id ⊗ m; !!A⊗!(!A ⊗ B); m; !(!A ⊗ (!A ⊗ B)); ! ≅]

1. d is a map of coalgebras. 2. ! is monoidal. Commutativity of the following diagram

[figure: S^{A}!; λ^{A}; !S^{A}; S^{A}!!; S^{A}δ; λ^{A}!; !S^{A}!; !λ^{A}; !!S^{A}; δS^{A}]

follows from commutativity of the following diagram

[figure: !A⊗!B; δ ⊗ Id; !!A⊗!B; m; !(!A ⊗ B)]

[figure: !!A⊗!!B; δ ⊗ δ; !δ ⊗ Id; !!!A⊗!!B; δ ⊗ δ; 1.]

[figure: !(!A⊗!B); m; !(δ ⊗ Id); !(!!A⊗!B); m; !m; !!(!A ⊗ B); δ]

1. δ is monoidal. This induce a lifting of the comonad (S^{A}, ε^{A}, δ^{A}) to C^{!}, [BW85], that is, a comonad (S^{A∗}, ε^{A∗}, δ^{A∗}) on C^{!} such that

1. U^{!}S^{A∗} = S^{A}U^{!} 2. U^{!}ε^{A∗} = ε^{A}U^{!}

3. U^{!}δ^{A∗} = δ^{A}U^{!}

The only part of the comonad (S^{A∗}, ε^{A∗}, δ^{A∗}) that is not determined by these conditions is the structure map of S^{A∗}(B, h), which is given by the composite

S^{A}B ^{S^{A}(h)}^{}S^{A}!B ^{λ_{B}^{A}}^{}!S^{A}B

Moreover, we have an adjunction between C_{S^{A}} and C_{S^{A∗}}^{!} such that the right (left) adjoints of the following diagram commute:

\begin{matrix}C_{S^{A∗}}^{!} & [figure: \underline{F_{S^{A∗}}}; ⊤; U_{S^{A∗}}] & C^{!} \\ C_{S^{A}} & ^{Ũ^{!}^{}}⊣ F̃^{!} & [figure: \underline{F_{S^{A}}}; ⊤; U_{S^{A}}] & C & ^{U^{!}^{}}⊣ F^{!} \end{matrix}

The functor Ũ^{!} simply forgets the coalgebra structure. Given an object B in C_{S^{A}}, which has the same objects as C, then F̃^{!}B is given by F^{!}C. An appropriate bijection ϕ̃_{(B,h),C} between maps is given by the following composite of bijections

C_{S^{A∗}}^{!}((B, h), F̃^{!}C) = C_{S^{A∗}}^{!}((B, h), F^{!}C)
= C^{!}(S^{A∗}(B, h), F^{!}C)  U_{S^{A∗}} ⊣ F_{S^{A∗}}
= C(U^{!}S^{A∗}(B, h), C)  U^{!} ⊣ F^{!}
= C(S^{A}U^{!}(B, h), C)  condition 1.
= C_{S^{A}}(U^{!}(B, h), C)  U_{S^{A}} ⊣ F_{S^{A}}
= C_{S^{A}}(Ũ^{!}(B, h), C)

Since the composite of bijections is natural in (B, h), it follows from the Pointwise Adjointness Theorem, [BW90] that F̃^{!} can be extended to a right adjoint to Ũ^{!}. Given a map f : B → C in C_{S^{A}}, that is, a map f : S^{A}B → C in C, then the map F̃^{!}(f) is equal to the composite

S^{A∗}F̃^{!}B = (S^{A}!B, S^{A}(δ); λ^{A}) ^{λ^{A}}^{}(!S^{A}B, δ) ^{!f}^{}(!C, δ) = F̃^{!}C

The comonad on C_{S^{A}} induced by the adjunction Ũ^{!} ⊣ F̃^{!} will be denoted (˜!, ε̃, δ̃); it has the following properties

1. ˜!F_{S^{A}} = F_{S^{A}}!

2. ε̃F_{S^{A}} = F_{S^{A}}ε

3. δ̃F_{S^{A}} = F_{S^{A}}δ

Note that the construction of the adjunction Ũ^{!} ⊣ F̃^{!} making the mentioned diagrams commute could have been done with an arbitrary distributive law of one comonad over another comonad.

Now, with any object D in a cartesian category (D, ×, 1) we may associate a comonad, [Sim92]; the functor part is given by D × (−), a component of the counit is given by

D × B ^{π_{2}}^{}B

and a component of the comultiplication is given by

D × B ^{<π_{1},Id>}^{}D × (D × B)

which is equal to the composite

D × B ^{Δ×Id}^{}(D × D) × B ≅ D × (D × B)

If C is a !-category, then C^{!} has the cartesian structure (⊗, I), and it turns out that the comonad induced by the object (!A, δ) of C^{!} by using this construction is the same as (S^{A∗}, ε^{A∗}, δ^{A∗}).

The functor F_{S^{A∗}} : C^{!} → C_{S^{A∗}}^{!} preserves limits because it has a left adjoint, so I is a terminal object in C_{S^{A∗}}^{!}. We will not assume that the category C_{S^{A}} has a terminal object, but the following weaker notion will do:

Definition 2.11 A pre !-category is a category C together with an object I, a comonad (!, ε, δ), and a map m_{I} : I →!I such that the following diagrams commute

[figure: I; m_{I}; !I; Id; I; ε; !; m_{I}; !I; !I; m_{I}; !m_{I}; !!I; δ]

This is simply the definition of a monoidal comonad on a monoidal category where the bifunctor part has been left out. This enables us to define the generalised coKleisli operator γ in the nullary and the unary case, Definition 2.2. A !-category is obviously a pre !-category, and moreover, it is straightforward to check that the category C_{S^{A}} together with the object I, the comonad (˜!, ε̃, δ̃), and the map F_{S^{A}}(m_{I}) constitutes a pre !-category. We will for later use note that given a map g : I → C in C, then γ(F_{S^{A}}(g)) = F_{S^{A}}(γ(g)), and similarly, given a map f :!B → C in C, then γ(F_{S^{A}}(f)) = F_{S^{A}}(γ(f)).

2.3 Fixpoints in Cartesian Categories

The main concern of this subsection will be a parametrised version of fixpoints in cartesian categories as introduced in [Law69].

Definition 2.12 Let C be a category with a terminal object 1. A map f^{♯} : 1 → B is a fixpoint of the map f : B → B iff f^{♯} = f^{♯}; f. A fixpoint operator is an operation on maps

(−)_{B}^{♯} : C(B, B) ⟶ C(1, B)

such that f^{♯} is a fixpoint of f for any map f : B → B.

Definition 2.13 Let (C, ×, 1) be a cartesian category. A map f^{♯} : A → B is a parametrised fixpoint of the map f : A × B → B iff f^{♯} is equal to the composite

A ^{Δ}^{}A × A ^{A×f^{♯}}^{}A × B ^{f}^{}B

A parametrised fixpoint operator is an operation on maps

(−)_{A,B}^{♯} : C(A × B, B) ⟶ C(A, B)

such that f^{♯} is a parametrised fixpoint of f for any map f : A × B → B. A parametrised fixpoint operator is natural if the operation is natural in A.

Note how the diagonal map Δ_{A} : A → A × A is used to copy parameters.

Proposition 2.14 Let (C, ×, 1) be a cartesian category. A map f^{♯} : A → B is a parametrised fixpoint of the map f : A × B → B iff the map ≅; f^{♯} : A × 1 → B is a fixpoint of f : A × B → B in C_{A×(−)}, thus, to give a parametrised fixpoint operator on C is equivalent to give a fixpoint operator on each category C_{A×(−)}.

Proof. Note that 1 is a terminal object in C_{A×(−)}. The result follows from straightforward calculation. □

We can deal with internal fixpoint operators if the category is closed with respect to the cartesian structure:

Definition 2.15 Let (C, ×, 1, ⇒) be a cartesian closed category. An internal fixpoint operator is a family of maps Y_{B} : B ⇒ B → B such that λ(f); Y_{B} is a parametrised fixpoint of f for any map f : A × B → B.

Now, one can show that a cartesian closed category has a parametrised fixpoint operator iff it has an internal fixpoint operator, [Poi92], but we will show here a more informative result:

Proposition 2.16 There is a bijective correspondence between natural parametrised fixpoint operators and internal fixpoint operators in a cartesian closed category.

Proof. Assume that C has a natural parametrised fixpoint operator (−)^{♯}, and define a map Y = eval^{♯} for every object. Let a map f : A × B → B be given, then

λ(f); Y = λ(f); eval^{♯}  def. of Y
= ((λ(f) × B); eval)^{♯}
= f^{♯}

which entails that λ(f); Y is a parametrised fixpoint of f. The construction of internal fixpoint operators from natural parametrised fixpoint operators is clearly injective. Conversely, assume that Y is an internal fixpoint operator on C, and define an operation on maps λ(−); Y. This is a natural parametrised fixpoint operator because λ(f); Y is a parametrised fixpoint of f for any map f : A × B → B, and naturality of the operation follows from naturality of λ. The construction of natural parametrised fixpoint operators from internal fixpoint operators is injective because the following calculation

\begin{aligned}λ(eval); Y & = & Id; Y \\ & = & Y \end{aligned}

shows that the internal fixpoint operator induced by λ(−); Y is equal to Y. □

2.4 Linear Fixpoints

We will now consider fixpoints in a linear context. The previous definition of fixpoints can not be used because it assumes the presence of finite products.

Definition 2.17 Let C be a pre !-category. A map f^{♯} : I → B is a linear fixpoint of the map f :!B → B iff f^{♯} = γ(f^{♯}); f. A linear fixpoint operator is an operation on maps

(−)_{B}^{♯} : C(!B, B) ⟶ C(I, B)

such that f^{♯} is a linear fixpoint of f for any map f :!B → B.

We get back Definition 2.12 if we equip a category with a terminal object with the identity functor and the identity map.

Definition 2.18 Let C be a !-category. A map f^{♯} :!A → B is a parametrised linear fixpoint of the map f :!A⊗!B → B iff f^{♯} is equal to the composite

!A ^{d}^{}!A⊗!A ^{Id⊗γ(f^{♯})}^{}!A⊗!B ^{f}^{}B

A parametrised linear fixpoint operator is an operation on maps

(−)_{A,B}^{♯} : C(!A⊗!B, B) ⟶ C(!A, B)

such that f^{♯} is a parametrised linear fixpoint of f for any map f :!A⊗!B → B. A parametrised linear fixpoint operator is natural if the operation is natural in !A with respect to maps of free coalgebras.

Note that maps of free coalgebras is the same as maps in the image of γ. We get back Definition 2.13 if we equip a cartesian category with the identity comonad and the natural transformation induced by the diagonal maps. The definition of a parametrised linear fixpoint is simply an extension of the definition of parametrised fixpoints in a cartesian category to a linear context, where we have only a “diagonal map” d_{A} for objects of the shape !A.

Proposition 2.19 Let C be a !-category. A map f^{♯} :!A → B is a parametrised linear fixpoint of the map f :!A⊗!B → B iff the map ≅; f^{♯} :!A ⊗ I → B is a linear fixpoint of f :!A⊗!B → B in C_{S^{A}}, thus, to give a parametrised linear fixpoint operator on C is equivalent to give a linear fixpoint operator on each category C_{S^{A}}.

Proof. Note that we consider C_{S^{A}} as a pre !-category. The result follows from some straightforward calculation. □

The definition of a linear fixpoint in C_{S^{A}} is essentially the definition of a fixpoint in C_{S^{A∗}}^{!} stated in terms of maps of C_{S^{A}}, which gives us the following results:

Lemma 2.20 Let C be a !-category. A map h : (!A, δ) ⊗ I → (!B, δ) is a fixpoint of a map f : (!A, δ) ⊗ (!B, δ) → (!B, δ) in C_{S^{A∗}}^{!} iff ϕ̃(h) :!A ⊗ I → B is a linear fixpoint of ϕ̃(f) :!A⊗!B → B in C_{S^{A}}, thus, to give a linear fixpoint operator on C_{S^{A}} is equivalent to give a fixpoint operator on C_{S^{A∗}}^{!} restricted to free coalgebras.

Proof. Note that we consider C_{S^{A∗}}^{!} together with the terminal object I and we consider C_{S^{A}} as a pre !-category. The following calculation, where composition is in C_{S^{A}}, proves the result:

h is a fixpoint of f iff h = h; f
iff h = ϕ̃^{−1}(ϕ̃(h)); f
iff ϕ̃(h) = ϕ̃(ϕ̃^{−1}(ϕ̃(h)); f)
iff ϕ̃(h) = ϕ̃^{−1}(ϕ̃(h)); ϕ̃(f)
iff ϕ̃(h) = γ(ϕ̃(h)); ϕ̃(f)  *
iff ϕ̃(h) is a linear fixpoint of ϕ̃(f)

* The underlying map of ϕ̃^{−1}(ϕ̃(h)) is equal to S^{A}(m_{I}); λ^{A}; !ϕ̃(h) because S^{A}(m_{I}); λ^{A} is structure map for the coalgebra S^{A∗}I. But λ^{A}; !ϕ̃(h) is equal to ˜!ϕ̃(h), and S^{A}(m_{I});˜!ϕ̃(h) is equal to F_{S^{A}}(m_{I});˜!ϕ̃(h) where composition is in C_{S^{A}}. Thus, ϕ̃^{−1}(ϕ̃(h)) is equal to γ(ϕ̃(h)). □ Lemma 2.21 Let C be a !-category such that F ree(C^{!}) is closed under finite products. A map h : (!A, δ) ⊗ I → (!B, δ) is a fixpoint of a map f : (!A, δ) ⊗ (!B, δ) → (!B, δ) in C_{S^{A}}^{!} iff the composite

(!A, δ) × 1 ^{n^{−1}}^{}(!A, δ) ⊗ 1 ^{Id⊗n_{1}^{−1}}^{}(!A, δ) ⊗ I ^{h}^{}(!B, δ)

is a fixpoint of the composite

(!A, δ) × (!B, δ) ^{n^{−1}}^{}(!A, δ) ⊗ (!B, δ) ^{f}^{}(!B, δ)

in F ree(C^{!})_{(!A,δ)×(−)}, thus, to give a fixpoint operator on F ree(C^{!})_{(!A,δ)×(−)} is equivalent to give a fixpoint operator on C_{S^{A∗}}^{!} restricted to free coalgebras.

Proof. Note that we consider C_{S^{A∗}}^{!} together with the terminal object I and note that F ree(C^{!}) has finite products (×, 1), Proposition 2.5, which makes 1 a terminal object in F ree(C^{!})_{(!A,δ)×(−)}. The following calculation proves the result:

n^{−1}; (Id ⊗ n_{1}^{−1}); h is a fixpoint of n^{−1}; f in F ree(C^{!})_{(!A,δ)×(−)} iff n^{−1}; (Id ⊗ n_{1}^{−1}); h =< π_{1}, Id >; (Id × (n^{−1}; (Id ⊗ n_{1}^{−1}); h)); n^{−1}; f iff

h = (Id ⊗ n_{1}); n; < π_{1}, Id >; (Id × (n^{−1}; (Id ⊗ n_{1}^{−1}); h)); n^{−1}; f iff  *

h =< π_{1}, Id >; (Id ⊗ h); f h is a fixpoint of f in C_{S^{A}}^{!}

* We obtain the map < g, k > in C^{!} by composing the map < g, k > in F ree(C^{!}) with n^{−1}, and similarly, we obtain the projection map π_{1} in C^{!} by composing the projection map π_{1} in F ree(C^{!}) with n. □

Theorem 2.22 Let C be a !-category such that F ree(C^{!}) is closed under finite products. There is a bijective correspondence between (natural) parametrised fixpoint operators on F ree(C^{!}) and (natural) parametrised linear fixpoint operators on C.

Proof. Note that F ree(C^{!}) has finite products (×, 1), Proposition 2.5. To give a parametrised fixpoint operator on F ree(C^{!}) is equivalent to give a fixpoint operator on each F ree(C^{!})_{(!A,δ)×(−)}, Proposition 2.14, which is equivalent to give a fixpoint operator on each C_{S^{A∗}}^{!} restricted to free coalgebras, Lemma 2.21, which is equivalent to give a linear fixpoint operator on each category C_{S^{A}}, Lemma 2.20, which is equivalent to give a parametrised linear fixpoint operator on C, Proposition 2.19. It can be shown that a parametrised fixpoint operator on F ree(C^{!}) is natural iff the corresponding parametrised linear fixpoint operators on C is natural. □

We can deal with internal linear fixpoint operators if our category is closed with respect to the monoidal structure:

Definition 2.23 Let C be a linear category. An internal linear fixpoint operator is a family of maps Y_{B} :!(!B ⊸ B) → B such that γ(λ(f)); Y_{B} is a parametrised linear fixpoint of f for any map f :!A⊗!B → B.

We get back Definition 2.15 if we equip a cartesian closed category with the identity comonad and the natural transformation induced by the diagonal maps. One can show that a linear category has a parametrised linear fixpoint operator iff it has an internal linear fixpoint operator, which would be a generalisation of the result saying that a cartesian closed category has a parametrised fixpoint operator iff it has an internal fixpoint operator. We will here show a more informative result, which is a generalisation of Proposition 2.16:

Proposition 2.24 There is a bijective correspondence between natural parametrised linear fixpoint operators and internal linear fixpoint operators in a linear category.

Proof. Assume that C has a natural parametrised linear fixpoint operator (−)^{♯}, and define a map Y = ((ε ⊗ Id); eval)^{♯} for every object. Let a map f :!A⊗!B → B be given, then

γ(λ(f)); Y = γ(λ(f)); ((ε ⊗ Id); eval)^{♯}  def. of Y
= ((γ(λ(f)) ⊗ Id); (ε ⊗ Id); eval)^{♯}
= ((λ(f) ⊗ Id); eval)^{♯}
= f^{♯}

which entails that γ(λ(f)); Y is a parametrised linear fixpoint of f. The construction of internal linear fixpoint operators from natural parametrised linear fixpoint operators is clearly injective. Conversely, assume that Y is an internal linear fixpoint operator on C, and define the operation on maps γ(λ(−)); Y. This is a natural parametrised linear fixpoint operator; the map γ(λ(f)); Y is a parametrised linear fixpoint of f for any map f :!A⊗!B → B, and given a map h :!A′ → A, we have

\begin{aligned}γ(h); γ(λ(f)); Y & = & γ(γ(h); λ(f)); Y \\ & = & γ(λ((γ(h) ⊗ Id); f)); Y \end{aligned}

so the operation is natural in !A with respect to maps in the image of γ. The construction of natural parametrised linear fixpoint operators from internal linear fixpoint operators is injective because the following calculation

γ(λ((ε ⊗ Id); eval)); Y = γ(λ((ε ⊗ Id); λ^{−1}(Id))); Y
= γ(λ(λ^{−1}(ε))); Y
= γ(ε); Y
= Id; Y
= Y

shows that the internal linear fixpoint operator induced by γ(λ(−)); Y is equal to Y. □

Theorem 2.25 Let C be a linear category such that F ree(C^{!}) is closed under finite products. There is a bijective correspondence between internal fixpoint operators in F ree(C^{!}) and internal linear fixpoint operators in C.

Proof. Follows from Proposition 2.16, Theorem 2.22 and Proposition 2.24. □

This result can also be derived from the following theorem, which is a consequence of the fact that the definition of an internal linear fixpoint operator in C is essentially the definition of an internal fixpoint operator in F ree(C^{!}) stated in terms of maps in C:

Theorem 2.26 Let C be a linear category such that F ree(C^{!}) is closed under finite products. A family of maps Y : (!B, δ) ⇒ (!B, δ) → (!B, δ) is an internal fixpoint operator in F ree(C^{!}) iff the family of maps ϕ(Y) :!(!B ⊸ B) → B is an internal linear fixpoint operator in C.

Proof. Note that F ree(C^{!}) has finite products (×, 1), Proposition 2.5. We will use the observation that we have a bijection between C(!A⊗!B, B) and F ree(C^{!})((!A, δ) × (!B, δ), (!B, δ)), namely the operation n^{−1}; ϕ^{−1}(−). We will also use the result that a map f : (!A, δ) ⊗ (!B, δ) → (!B, δ) has the same parametrised fixpoints in C^{!} as the composite

(!A, δ) × (!B, δ) ^{n^{−1}}^{}(!A, δ) ⊗ (!B, δ) ^{f}^{}(!B, δ)

has in F ree(C^{!}), Lemma 2.21. Now, Y is an internal fixpoint operator in F ree(C^{!}) iff for any map f :!A⊗!B → B we have that λ(n^{−1}; ϕ^{−1}(f)); Y is a parametrised fixpoint of ϕ^{−1}(f). But we have

λ(n^{−1}; ϕ^{−1}(f)); Y is a par. fixpoint of ϕ^{−1}(f) iff  def. of λ in F ree(C^{!})

ϕ^{−1}(λ(ϕ(n; n^{−1}; ϕ^{−1}(f)))); Y is a par. fixpoint of ϕ^{−1}(f) iff

ϕ^{−1}(λ(f)); Y is a par. fixpoint of ϕ^{−1}(f) iff  *

ϕ(ϕ^{−1}(λ(f)); Y) is a par. linear fixpoint of f iff

γ(λ(f)); ϕ(Y) is a par. linear fixpoint of f iff

* Proposition 2.14, Lemma 2.20, and Proposition 2.19. Thus, Y is an internal fixpoint operator in F ree(C^{!}) iff for any map f :!A⊗!B → B we have that γ(λ(f)); ϕ(Y) is a parametrised linear fixpoint of f, which is the definition of an internal linear fixpoint operator applied to ϕ(Y). □

2.5 Generalisation of Linear Fixpoints

The definition of linear fixpoints can be generalised to an arbitrary number of parameters. We first need a generalisation of the natural transformation d:

Definition 2.27 Let C be a !-category. We define D_{A_{1},...,A_{n}} to be the composite

!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}

Proposition 2.28 Let C be a !-category. The underlying map of the diagonal map

(!A_{1}, δ) ⊗ ... ⊗ (!A_{n}, δ) ^{Δ}^{}(!A_{1}, δ) ⊗ ... ⊗ (!A_{n}, δ) ⊗ (!A_{1}, δ) ⊗ ... ⊗ (!A_{n}, δ)

in C^{!} is equal to D.

Proof. The following calculation proves the result:

Δ = (⊗_{i}δ); m; d; (ε ⊗ ε)  def. of Δ in C^{!}
= (⊗_{i}δ); (⊗_{i}d); ≅; (m ⊗ m); (ε ⊗ ε)  d is monoidal
= (⊗_{i}δ); (⊗_{i}d); ≅; ((⊗_{i}ε) ⊗ (⊗_{i}ε))  ε is monoidal
= (⊗_{i}δ); (⊗_{i}d); (⊗_{i}(ε ⊗ ε)); ≅  δ is a map of comonoids
= (⊗_{i}d); (⊗_{i}(δ ⊗ δ)); (⊗_{i}(ε ⊗ ε)); ≅
= (⊗_{i}d); ≅
= D  def. of D

□

Definition 2.29 (Generalisation) Let C be a !-category. A map f^{♯} :!A_{1} ⊗ ...⊗!A_{n} → B is a parametrised linear fixpoint of the map f :!A_{1} ⊗ ...⊗!A_{n}⊗!B → B iff f^{♯} is equal to the composite

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

A parametrised linear fixpoint operator is an operation on maps (−)^{♯} such that f^{♯} is a parametrised linear fixpoint of f for any map f :!A_{1} ⊗ ...⊗!A_{n}⊗!B → B. A parametrised linear fixpoint operator is natural if the operation is natural in !A_{1} ⊗ ...⊗!A_{n} with respect to maps of coalgebras.

We get back the original definition, Definition 2.18, with the restriction that n = 1. The generalisation can be shown to be equivalent to the original definition in a !-category where F ree(C^{!}) is closed under finite products.

Definition 2.30 (Generalisation) Let C be a linear category. An internal linear fixpoint operator is a family of maps Y_{B} :!(!B ⊸ B) → B such that γ(λ(f)); Y_{B} is a parametrised linear fixpoint of f for any map f :!A_{1} ⊗ ...⊗!A_{n}⊗!B → B.

We get back the original definition, Definition 2.23, with the restriction that n = 1. This generalisation can be shown to be equivalent to the original definition in a linear category where F ree(C^{!}) is closed under finite products.

2.6 Concrete Models

An example of a linear category with finite products and finite sums is the category of CPOs and strict continuous functions; the symmetric monoidal structure is given by the smash product, the internal-hom is given by the strict continuous function space, and the comonad is given by the lift operation. This category has an internal linear fixpoint operator because the induced category of free coalgebras is equivalent to the category of CPOs and continuous functions; a cartesian closed category with an internal fixpoint operator. The internal fixpoint operator

B ⇒ B ^{Y}^{}B

in the category of CPOs and continuous functions is defined as Y (f) = ⊔_{n∈ω}f^{n}(⊥), which entails that the induced internal linear fixpoint operator

!(!B ⊸ B) ^{Y}^{}B

in the category of CPOs and strict continuous functions works as follows: a map f ∈!(!B ⊸ B) is either equal to ⊥ or corresponds to a map in !B ⊸ B. If f =⊥, then Y (f) =⊥. If f corresponds to a map in !B ⊸ B, then this map corresponds to a map f′ ∈ B ⇒ B and Y (f) = Y (f′) = ⊔_{n∈ω}f^{′n}(⊥). It should be noted that the category of CPOs and strict continuous functions is a model for Intuitionistic Relevant Logic in the sense of [Jac], that is, there is a natural transformation d : (−) → (−) ⊗ (−) making appropriate diagrams commute.

Another example of a linear category with finite products and finite sums is the category of dI domains and linear stable functions. This category has an internal linear fixpoint operator because the induced category of free coalgebras is equivalent to the category of dI domains and stable functions; a cartesian closed category with an internal fixpoint operator.

In [Bra94b] a third example of a linear category with finite products is given; namely the category of dI domains and non-empty-join preserving stable functions. This category has an internal linear fixpoint operator because the induced category of free coalgebras is equivalent to the category of dI domains and stable functions; a cartesian closed category with an internal fixpoint operator. The category of dI domains and non-empty-join preserving stable functions does not have finite sums, but if we extend it to the category of bottomless dI domains and non-empty-join preserving stable functions, then we obtain a linear category with finite products and finite sums, but lose the internal linear fixpoint operator. This is so because the induced category of free coalgebras is equivalent to the category of bottomless dI domains and stable functions; a cartesian closed category with finite sums, which is easily seen not to have an internal fixpoint operator. The reader is invited to figure out how a fixpoint of the twist map [in_{2}, in_{1}] : 1+1 → 1+1 might look in this category. The result that a cartesian closed category with finite sums and a fixpoint operator is inconsistent, [HP90], also implies that the category of bottomless dI domains and non-empty-join preserving stable functions can not have a fixpoint operator. It should be noted that the category of dI domains and non-empty-join preserving stable functions as well as the category of bottomless dI domains and non-empty-join preserving stable functions are models of Intuitionistic Affine Logic in the sense of [Jac], that is, the units of the tensor products are terminal objects.

A fourth example of a linear category with finite products and finite sums is the category of coherence spaces and linear stable functions, [GLT89]. This category has an internal linear fixpoint operator because the induced category of free coalgebras is equivalent to the category of coherence spaces and stable functions; a cartesian closed category with an internal fixpoint operator.

3 The λ-Calculus

3.1 Definition

Types are given by the grammar s ::= t | s∧s | s ⇒ s. The metavariables A, B, C, D will range over types. Terms are given by the grammar

t ::= x |
<> | < t, t > | fst(t) | snd(t) |
λx^{A}.t | tt

where x is a variable that ranges over terms. The metavariables f, u, v, w will range over terms. Rules for assignment of types to terms are given in Appendix A (which also contains the rules for assignment of categorical semantics). Type assignments have the form of sequents x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A where x_{1}, ..., x_{n} are pairwise distinct variables. We will frequently write Γ instead of x_{1} : A_{1}, ..., x_{n} : A_{n} or A_{1}, ..., A_{n}. The notation will be abused when necessary; Γ ⊢ u : A can mean either the sequent itself or a certain derivation of the sequent, and the name of a rule, for example (Ax), can mean either the rule itself or a certain instance of the rule. The actual interpretation is to be decided by the context. From now on, we will consider only typable terms. 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. The λ-calculus satisfies the following properties:

Lemma 3.1 If Γ ⊢ u : A is derived by a certain derivation, then for any derivable Γ ⊢ u : B we have A = B.

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

Proposition 3.2 If Γ ⊢ u : A is derivable, then the rule instance above the sequent is uniquely determined.

Proof. Use Lemma 3.1 to check each case. □

Lemma 3.3 If Γ_{1}, Γ_{2} ⊢ u : A is derived by a certain derivation and the variables in Γ_{1}, Γ_{2} and Λ are pairwise distinct, then Γ_{1}, Λ, Γ_{2} ⊢ u : A is derivable too.

Proof. Induction in the derivation of Γ_{1}, Γ_{2} ⊢ u : A. □

Lemma 3.4 (Substitution Property) If Γ ⊢ u : A and Γ, x : A, Λ ⊢ v : B are derived by certain derivations, then Γ, Λ ⊢ v[u/x] : B is derivable too.

Proof. Induction in the derivation of Γ, x : A, Λ ⊢ v : B. We need Lemma 3.3 to the (Ax) case. □

3.2 The Curry-Howard Isomorphism

The Curry-Howard isomorphism says that formulas corresponds to types, proofs to terms, and normalisation of proofs to reduction of terms. In what follows, we need a natural deduction formulation of IL as given in Appendix B. The relation between formulas of IL and types of the λ-calculus is obvious. The idea of the Curry-Howard isomorphism on the level of proofs is that proof-rules can be “decorated” with terms such that the term induced by a proof encodes the proof. An appropriate term language for this purpose is in the case of IL the λ-calculus. It turns out that we get the rules for assigning types to terms in the λ-calculus if we decorate the proof-rules of IL with terms in an appropriate way. We can obviously recover the proof-rules if we take the typing rules of the λ-calculus and remove the terms. We get the Curry-Howard isomorphism on the level of proofs as follows: given a proof of A_{1}, ..., A_{n} ⊢ A, 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} ⊢ u : A, that is, a term u of type A. Conversely, if one has a derivable sequent x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A, there is an easy way to get a proof of A_{1}, ..., A_{n} ⊢ A; erase all terms in the derivation of the type assignment. The two processes are each other’s inverses modulo renaming of variables. The isomorphism on the level of proofs is essentially given by Proposition 3.2. The Curry-Howard isomorphism on the level of normalisation says that a normalisation step followed by application of the Curry-Howard isomorphism on the level of proofs, yields the same term as application of the Curry-Howard isomorphism on the level of proofs followed by the reduction step corresponding to the normalisation step. This is dealt with in details in [GLT89].

3.3 Categorical Semantics

Given a cartesian closed category, we define a categorical interpretation of the λ-calculus; types are interpreted as objects, typing rules as natural operations on arrows, and derivations of type assignments as maps. A derivable sequent

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

is interpreted as a map

[[A_{1}]] × ... × [[A_{n}]] ^{[[x_{1}:A_{1},...,x_{n}:A_{n}⊢u:B]]}^{}[[B]]

by induction in its derivation cf. the operations on arrows (corresponding to the typing rules) given in Appendix A. Note that the derivation of the sequent is uniquely determined, Proposition 3.2, so it makes sense to speak of the interpretation of a derivable sequent without mentioning its derivation explicitly. It can be shown that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents. In what follows, we will omit the [[ −]] brackets when appropriate.

Lemma 3.5 If Γ_{1}, Γ_{2} ⊢ u : A is derived by a certain derivation and the variables in Γ_{1}, Γ_{2} and Λ are pairwise distinct, then Γ_{1}, Λ, Γ_{2} ⊢ u : A is derivable too with the interpretation

Γ_{1} × Λ × Γ_{2} ^{π_{1}×Γ_{2}}^{}Γ_{1} × Γ_{2} ^{[[Γ_{1},Γ_{2}⊢u:A]]}^{}A

Proof. Induction in the derivation of Γ_{1}, Γ_{2} ⊢ u : A. All cases except (Ax) are covered by the observation that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the left hand sides of the sequents. We need direct calculation to the (Ax) case. □

The following extension of Lemma 3.4 essentially says how substitution relates to composition:

Lemma 3.6 If Γ ⊢ u : A and Γ, x : A, Λ ⊢ v : B are derived by certain derivations, then Γ, Λ ⊢ v[u/x] : B is derivable too with the interpretation

Γ × Λ ^{Δ×Λ}^{}Γ × Γ × Λ ^{Γ×[[Γ⊢u:A]]×Λ}^{}Γ × A × Λ ^{[[Γ,x:A,Λ⊢v:B]]}^{}B

Proof. Induction in the derivation of Γ, x : A, Λ ⊢ v : B. All cases except (Ax) are covered by the observation that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the left hand sides of the sequents. We need Lemma 3.5 to the (Ax) case. □

It can be shown by using Lemma 3.6 that the interpretation is sound with respect to the usual reduction rules for terms of the λ-calculus, that is, interpretation is preserved by application of reduction rules.

4 The Linear λ-Calculus

4.1 Definition

Types are given by the grammar s ::= I | 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 |
<> | < t, t > | fst(t) | snd(t) |
λx^{A}.t | tt |

let t, ..., t be x_{1}, ..., x_{n} in !t | derelict(t) | discard t in t | copy t as x, y in t

where x is a variable that ranges over terms, and t, ..., t means a sequence of n occurrences of t. Rules for assignment of types to terms are given in Appendix C. Type assignments have the form of sequents x_{1} : A_{1}, ..., x_{n} : A_{n} − u : A where x_{1}, ..., x_{n} are pairwise distinct variables. A Girardian turnstyle − is used to distinguish sequents in the linear λ-calculus from sequents in the λ-calculus, where the usual turnstyle ⊢ is used. 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. The linear λ-calculus is essentially the same as the calculus given in [BBdPH92]. From now on, we will consider only typable terms. The expression \overline{w} means w_{1}, ..., w_{n}, the expression

copy \overline{w} as \overline{x}, \overline{y} in u

mean

copy w_{1} as x_{1}, y_{1} in (...copy w_{n} as x_{n}, y_{n} in u...)

and the expression

discard \overline{w} in u

mean

discard w_{1} in (...discard w_{n} in u...)

respectively. The linear λ-calculus satisfies the following properties:

Lemma 4.1 If Γ − u : A is derived by a certain derivation, then for any derivable Γ′ − u : B, where the assumptions in Γ′ is a permutation of the assumptions in Γ, we have A = B.

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

Proposition 4.2 If Γ − u : A is derivable, then the first rule instance above the sequent which is different from an instance of (Ex) is uniquely determined up to permutation of assumptions.

Proof. Use Lemma 4.1 to check each case. □

Lemma 4.3 (Substitution Property) If Γ − u : A and Δ, x : A, Λ − v : B are derived by certain derivations and 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. □

4.2 The Curry-Howard Isomorphism

In what follows, we need a natural deduction formulation of ILL as given in Appendix D. ILL corresponds to the linear λ-calculus via a Curry-Howard isomorphism in the same way as IL corresponds to the λ-calculus; we get the rules for assigning types to terms in the linear λ-calculus if we decorate the proof-rules of ILL with terms in an appropriate way, and conversely, we recover the proof-rules if we remove the terms from the typing rules. The isomorphism on the level of proofs is essentially given by Proposition 4.2.

4.3 Categorical Semantics

Given a linear category with finite products, we define a categorical interpretation of the linear λ-calculus; a derivable sequent

x_{1} : A_{1}, ..., x_{n} : A_{n} − u : B

is interpreted as a map

[[A_{1}]] ⊗ ... ⊗ [[A_{n}]] ^{[[x_{1}:A_{1},...,x_{n}:A_{n} − u:B]]}^{}[[B]]

by induction in its derivation cf. the operations on arrows given in Appendix C. Note that the derivation of the sequent is uniquely determined up to permutation of assumptions, Proposition 4.2, so it makes sense to speak of the interpretation of a derivable sequent without mentioning its derivation explicitly. It can be shown that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents. The interpretation of the linear λ-calculus is the same as the interpretation given in [BBdPH92]. The following extension of Lemma 4.3 does essentially say that substitution corresponds to composition:

Lemma 4.4 If Γ − u : A and Δ, x : A, Λ − v : B are derived by certain derivations and the variables in Γ and Δ, Λ are pairwise distinct, then Δ, Γ, Λ − v[u/x] : B is derivable too with the interpretation

Δ ⊗ Γ ⊗ Λ ^{Δ⊗[[Γ − u:A]]⊗Λ}^{}Δ ⊗ A ⊗ Λ ^{[[Δ,x:A,Λ − v:B]]}^{}B

Proof. Induction in the derivation of Δ, x : A, Λ − v : B. All cases except (Ax) are covered by the observation that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the left hand sides of the sequents. The (Ax) case is trivial. □

It can be shown by using Lemma 4.4 that the interpretation is sound with respect to the usual reduction rules for terms of the linear λ-calculus, [BBdPH92].

5 The Girard Translation

5.1 Definition

The [Gir87] paper introduced the Girard Translation which embeds IL into ILL. We will state the Girard Translation in terms of the natural deduction formulations of IL and ILL given in Appendix B and Appendix D. At the level of formulas the Girard Translation is defined inductively as follows:

• t^{o} = ⊤

• (A ∧ B)^{o} = A^{o}&B^{o}

• (A ⇒ B)^{o} =!A^{o} ⊸ B^{o}

At the level of proofs the Girard Translation translates a proof of A_{1}, ..., A_{n} ⊢ B into a proof of !A_{1}^{o}, ...,!A_{n}^{o} − B^{o}. The Girard Translation at the level of proofs is stated in Appendix E. The translation is sound with respect to provability in the sense that A_{1}, ..., A_{n} ⊢ B is provable (in IL) iff !A_{1}^{o}, ...,!A_{n}^{o} − B^{o} is provable (in ILL), [Gir87], and moreover, the translation preserves β reductions, [Bie94]. The translation induces a translation from types and derivable sequents in the λ-calculus to types and derivable sequents in the linear λ-calculus cf. the Curry-Howard isomorphisms; a sequent x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A is translated into a sequent (x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : A)^{o} of the shape x_{1} :!A_{1}^{o}, ..., x_{n} :!A_{n}^{o} − u′ : A^{o} where u′ encodes the translation of the proof encoded by u. An inductive definition of the translation from derivable sequents in the λ-calculus to derivable sequents in the linear λ-calculus can be obtained simply by decorating the rules in the definition of the extended Girard Translation (in Appendix E) appropriately with terms.

5.2 Soundness with Respect to Categorical Semantics

If C is a linear category with finite products, then F ree(C^{!}) is a cartesian closed category, as previous results show. We can therefore interpret types and derivable sequents in the λ-calculus as objects and arrows in F ree(C^{!}). It turns out that the interpretation of a type can be written in a simple way using the Girard Translation at the level of types:

Proposition 5.1 Let C be a linear category with finite products. If a type A of the λcalculus is interpreted in F ree(C^{!}), and the type A^{o} of the linear λ-calculus is interpreted in C, then [[A]] = (![[A^{o}]], δ).

Proof. Induction in A, we proceed case by case.

[[t]] = (!1, δ)
= (![[⊤]], δ)
= (![[t^{o}]], δ)
[[B ∧ C]] = [[B]] × [[C]]
= (![[B^{o}]], δ) × (![[C^{o}]], δ)  IH
= (!([[B^{o}]] × [[C^{o}]]), δ)
= (![[B^{o}&C^{o}]], δ)
= (![[(B ∧ C)^{o}]], δ)
[[B ⇒ C]] = [[B]] ⇒ [[C]]
= (![[B^{o}]], δ) ⇒ (![[C^{o}]], δ)  IH
= (!(![[B^{o}]] ⊸ [[C^{o}]]), δ)
= (![[!B^{o} ⊸ C^{o}]], δ)
= (![[(B ⇒ C)^{o}]], δ)

□

Let the following composite of bijections be denoted by lin:

C^{!}([[A_{1}]] × ... × [[A_{n}]], [[B]]) = C^{!}((![[A_{1}^{o}]], δ) × ... × (![[A_{n}^{o}]], δ), (![[B^{o}]], δ))  Prop. 5.1
≅ C^{!}((![[A_{1}^{o}]], δ) ⊗ ... ⊗ (![[A_{n}^{o}]], δ), (![[B^{o}]], δ))  comp. with n
= C^{!}((![[A_{1}^{o}]], δ) ⊗ ... ⊗ (![[A_{n}^{o}]], δ), F^{!}[[B^{o}]])
≅ C(U^{!}((![[A_{1}^{o}]], δ) ⊗ ... ⊗ (![[A_{n}^{o}]], δ)), [[B^{o}]])  U^{!} ⊣ F^{!}
= C(![[A_{1}^{o}]] ⊗ ...⊗![[A_{n}^{o}]], [[B^{o}]])

We are now ready to state a result showing that the Girard Translation is sound with respect to the above mentioned categorical interpretations. The result essentially says that the Girard Translation corresponds to the adjunction between F ree(C^{!}) and C, or to be precise, to the function lin. Recall that (x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : B)^{o} is a derivable sequent in the linear λ-calculus of the shape x_{1} :!A_{1}^{o}, ..., x_{n} :!A_{n}^{o} − u′ : B^{o}.

Theorem 5.2 (Soundness) Let C be a linear category with finite products. If

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

is a derivable sequent in the λ-calculus, then

lin([[x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : B]]) = [[(x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : B)^{o}]]

Proof. Induction in the derivation of x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ u : B, we proceed case by case. In what follows we will disregard terms, and only consider the underlying proofs.

The (Ax) case. The proof

\begin{aligned}& (Ax) \\ A_{1}, ..., A_{n} ⊢ A_{q} \end{aligned}

is translated into the proof

\begin{aligned}& (Ax) \\ !A_{q}^{o} −!A_{q}^{o} \end{aligned}

(Der)

!A_{q}^{o} − A_{q}^{o} = (W eak) and (Ex) !A_{1}^{o}, ...,!A_{n}^{o} − A_{q}^{o}

The following calculation shows the wanted result:

lin([[A_{1}, ..., A_{n} ⊢ A_{q}]]) = n; π_{q}; ε
= π_{q}; ε  *
= (e ⊗ ... ⊗ e⊗!A_{q}^{o} ⊗ e ⊗ ... ⊗ e); ≅; ε  def. of π_{q} in C^{!}
= [[!A_{1}^{o}, ...,!A_{n}^{o} − A_{q}^{o}]]

* We obtain the projection map π_{q} in C^{!} by composing the projection map π_{q} in F ree(C^{!}) with n.

The (t_{I}) case. The proof

\begin{aligned}& (t_{I}) \\ Γ ⊢ t \end{aligned}

is translated into the proof

\begin{aligned}& (⊤_{I}) \\ !Γ^{o} − ⊤ \end{aligned}

The following calculation shows the wanted result:

lin([[Γ ⊢ t]]) = n; <>; ε
= n; γ(<>); ε  def. of <> in F ree(C^{!})
= <>
= [[!Γ^{o} − ⊤]]

The (∧_{I}) case. The proof

Γ ⊢ A Γ ⊢ B ; (∧_{I}) ; Γ ⊢ A ∧ B

is translated into the proof

!Γ^{o} − A^{o} !Γ^{o} − B^{o}
(&_{I})
!Γ^{o} − A^{o}&B^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ A ∧ B]]) = n; < [[Γ ⊢ A]], [[Γ ⊢ B]] >; ε
= n; ϕ^{−1}(< ϕ([[Γ ⊢ A]]), ϕ([[Γ ⊢ B]]) >); ε  def. of < −, + >
= < (n; [[Γ ⊢ A]]; ε), (n; [[Γ ⊢ B]]; ε) >
= < lin([[Γ ⊢ A]]), lin([[Γ ⊢ B]]) >
= < [[!Γ^{o} − A^{o}]], [[!Γ^{o} − B^{o}]] >  IH
= [[!A_{1}^{o}, ...,!A_{n}^{o} − A^{o}&B^{o}]]

The (∧_{E1}) case. The proof

Γ ⊢ A ∧ B ; (∧_{E1}) ; Γ ⊢ A

is translated into the proof

!Γ^{o} − A^{o}&B^{o} ; (&_{E1}) ; !Γ^{o} − A^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ A]]) = n; [[Γ ⊢ A ∧ B]]; π_{1}; ε
= n; [[Γ ⊢ A ∧ B]]; !π_{1}; ε  def. of π_{1} in F ree(C^{!})
= n; [[Γ ⊢ A ∧ B]]; ε; π_{1}
= lin([[Γ ⊢ A ∧ B]]); π_{1}
= [[!Γ^{o} − A^{o}&B^{o}]]; π_{1}  IH
= [[!Γ^{o} − A^{o}]]

The (∧_{E2}) case is analogous to the (∧_{E1}) case. The (⇒_{I}) case. The proof

Γ, A ⊢ B ; (⇒_{I}) ; Γ ⊢ A ⇒ B

is translated into the proof

!Γ^{o},!A^{o} − B^{o}
(⊸_{I})
!Γ^{o} −!A^{o} ⊸ B^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ A ⇒ B]]) = n; λ([[Γ, A ⊢ B]]); ε
= n; ϕ^{−1}(λ(ϕ(n; [[Γ, A ⊢ B]]))); ε  def. of λ in F ree(C^{!})
= n; λ(n; [[Γ, A ⊢ B]]; ε)
= λ((n ⊗ Id); n; [[Γ, A ⊢ B]]; ε)
= λ(n; [[Γ, A ⊢ B]]; ε)  *
= λ(lin([[Γ, A ⊢ B]]))
= λ([[!Γ^{o},!A^{o} − B^{o}]])  IH
= [[!Γ^{o} −!A^{o} ⊸ B^{o}]]

* Because n makes ! a monoidal functor from (C, 1, ×) to (C, I, ⊗).

The (⇒_{E}) case. The derivation

Γ ⊢ A ⇒ B Γ ⊢ A
(⇒_{E})
Γ ⊢ B

is translated into the proof

!Γ^{o} −!A^{o} ⊸ B^{o} !Γ^{o} − A^{o} ; (!_{I}) ; !Γ^{o} −!A^{o}

(⊸_{E})
!Γ^{o},!Γ^{o} − B^{o}
= (Con) and (Ex)
!Γ^{o} − B^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ B]]) = n; < [[Γ ⊢ A ⇒ B]], [[Γ ⊢ A]] >; eval; ε
= n; < [[Γ ⊢ A ⇒ B]], [[Γ ⊢ A]] >; n^{−1}; ϕ^{−1}(λ^{−1}(ϕ(Id))); ε  def. of eval
= < (n; [[Γ ⊢ A ⇒ B]]), (n; [[Γ ⊢ A]]) >; n^{−1}; (ε ⊗ Id); eval
= < (n; [[Γ ⊢ A ⇒ B]]), (n; [[Γ ⊢ A]]) >; (ε ⊗ Id); eval  *
= D; ((n; [[Γ ⊢ A ⇒ B]]) ⊗ (n; [[Γ ⊢ A]])); (ε ⊗ Id); eval  **
= D; ((n; [[Γ ⊢ A ⇒ B]]; ε) ⊗ γ(n; [[Γ ⊢ A]]; ε)); eval
= D; (lin([[Γ ⊢ A ⇒ B]]) ⊗ γ(lin([[Γ ⊢ A]]))); eval
= D; ([[!Γ^{o} −!A^{o} ⊸ B^{o}]] ⊗ γ([[!Γ^{o} − A^{o}]])); eval  IH
= [[!Γ^{o} − B^{o}]]

* We obtain a map < f, g > in C^{!} by composing the map < f, g > in F ree(C^{!}) with n^{−1}. ** Definition of < −, + > in C^{!}, Definition 2.27 and Proposition 2.28. □

Note that if we consider proofs instead of derivable sequents, then we get a soundness result in the usual proof-theoretic sense. Recall that (A_{1}, ..., A_{n} ⊢ B)^{o} is a proof of !A_{1}^{o}, ...,!A_{n}^{o} − B^{o} in ILL.

Corollary 5.3 Let C be a linear category with finite products. If A_{1}, ..., A_{n} ⊢ B is a proof in IL, then

lin([[A_{1}, ..., A_{n} ⊢ B]]) = [[(A_{1}, ..., A_{n} ⊢ B)^{o}]]

Proof. Use Theorem 5.2 and the Curry-Howard isomorphism. □

This Corollary is a categorical generalisation of a result in [Gir87] showing that the Girard Translation is sound with respect to interpretation in a concrete category, namely the category of coherence spaces and linear stable functions.

6 Extensions with Finite Sums

6.1 The λ-Calculus Extended with Finite Sums

The λ-calculus can be extended with finite sums, that is, we have additional types f | s ∨ s, additional terms

[]^{C}(t) | inl^{A∨B}(t) | inr^{A∨B}(t) | case t of inl(x) => t | inr(y) => t

and typing rules as given in Appendix A. We still have Lemma 3.1, Proposition 3.2, Lemma 3.3, Lemma 3.4, and the Curry-Howard isomorphism.

We could give a categorical interpretation using a cartesian closed category with finite sums such that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents, such that Lemma 3.6 still holds, and such that the interpretation is sound with respect to the usual reduction rules, [GLT89]. The (∨_{E}) rule should then be interpreted using a natural isomorphism Γ × (A + B) ≅ (Γ × A) + (Γ × B) coming from the observation that the functor Γ × (−) has a right adjoint, and thus preserves sums. But a cartesian closed category with finite sums together with a fixpoint operator, [HP90], so we will instead assume that we have a cartesian closed category C with weak finite sums (0, +) such that

1. the operation [−, +] : C(A, Γ ⇒ C) × C(B, Γ ⇒ C) → C(A + B, Γ ⇒ C) is natural in Γ,

2. the map [] : 0 → 0 induced by the weak initial object is equal to the identity, and the map [in_{1}, in_{2}] : (!A, δ) + (!B, δ) → (!A, δ) + (!B, δ) induced by the weak binary sum is equal to the identity.

We are then able to give a categorical interpretation, cf. Appendix A, such that the operations on arrows induced by the typing rules are natural in the interpretation of Γ, and such that Lemma 3.5 and Lemma 3.6 still hold. If the weak finite sums are finite sums in the usual sense, then the above mentioned conditions 1. and 2.are satisfied, and the interpretation will coincide with the one given by the isomorphism Γ × (A + B) ≅ (Γ × A) + (Γ × B). It takes little calculation to see that the operation on arrows induced by the (∨_{E}) rule is natural in Γ. Let a map h : Δ → Γ be given, then

h; < Γ, w >; (Γ × [λ(u), λ(v)]); eval =
< Δ, (h; w) >; (Δ × [λ(u), λ(v)]); (h × (Γ ⇒ C)); eval =
< Δ, (h; w) >; (Δ × [λ(u), λ(v)]); (Δ × (h ⇒ C)); eval =
< Δ, (h; w) >; (Δ × [(λ(u); (h ⇒ C)), (λ(v); (h ⇒ C))]); eval =
< Δ, (h; w) >; (Δ × [λ((h × A); u), λ((h × B); v)]); eval

This categorical interpretation can be shown to be sound with respect to β and η reductions, [GLT89]. It might be a surprise that we do not need finite sums to give a sound categorical interpretation with respect to η reductions, but the two statements in the above mentioned condition 2. corresponds case by case to the two η reductions

[]^{C}(w) ⇝ w case w of inl(x) => inl(x) | inr(y) => inr(y) ⇝ w

The operation on arrows induced by the (∨_{E}) rule is not necessarily natural in C. This entails that the categorical interpretation will be sound only with respect to commuting conversions with the property that the operation on arrows induced by the (∨_{E}) rule is natural in C with respect to the interpretation of the typing rule corresponding to the conversion, [GLT89].

6.2 The linear λ-Calculus Extended with Finite Sums

The linear λ-calculus can be extended with finite sums, that is, we have additional types 0 | s ⊕ s, additional terms

[]^{C}(t) | inl^{A⊕B}(t) | inr^{A⊕B}(t) | case t of inl(x) => t | inr(y) => t

and rules for assignment of types to terms as given in Appendix C. We still have Lemma 4.1, Proposition 4.2, Lemma 4.3, and the Curry-Howard isomorphism.

We can give a categorical interpretation using a linear category with finite products and finite sums (0, +), cf. Appendix C, such that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents, and such that Lemma 4.4 still holds. The natural isomorphism Γ ⊗ (A + B) ≅ (Γ ⊗ A) + (Γ ⊗ B) comes from the observation that the functor Γ ⊗ (−) has a right adjoint, and thus preserves sums. The categorical interpretation is sound with respect to the usual reduction rules.

6.3 The Girard Translation Extended with Finite Sums

The Girard Translation still works if we extend it with finite sums. At the level of formulas, the extension is given by:

• f^{o} = 0

• (A ∨ B)^{o} =!A^{o}⊕!B^{o}

At the level of proofs, the extended Girard Translation is stated in Appendix E. The translation is still sound with respect to provability, [Gir87], and it still preserves β reductions, [Bie94].

If C is a linear category with finite products and finite sums, then F ree(C^{!}) is a cartesian closed category with weak finite sums such that the above mentioned conditions 1. and 2. are satisfied, cf. Proposition 2.9, Proposition 2.7, and Proposition 2.10. We can therefore interpret types and derivable sequents in the λ-calculus extended with finite sums as objects and arrows in F ree(C^{!}).

The categorical interpretation is sound with respect to β and η reductions, and it is sound with respect to commuting conversions with the property that the operation on arrows induced by the (∨_{E}) rule is natural in C with respect to the interpretation of the typing rule corresponding to the conversion, as mentioned above. It follows from Proposition 2.9 and Proposition 2.6 that the operation on arrows induced by the (∨_{E}) rule is natural in C with respect to linear maps, so the categorical interpretation is sound with respect to commuting conversions with the property that the interpretation of the typing rule corresponding to the conversion is linear.

We still have Proposition 5.1, as the following addition to the proof shows:

[[f]] = (!0, δ)
= (![[0]], δ)
= (![[f^{o}]], δ)
[[B ∨ C]] = [[B]] + [[C]]
= (![[B^{o}]], δ) + (![[C^{o}]], δ)  IH
= (!(![[B^{o}]]+![[C^{o}]]), δ)
= (![[!B^{o}⊕!C^{o}]], δ)
= (![[(B ∨ C)^{o}]], δ)

□

We also still have Theorem 5.2 (Soundness), as the following addition to the proof shows:

The (f_{E}) case. The proof

Γ ⊢ f ; (f_{E}) ; Γ ⊢ C

is translated into the proof

!Γ^{o} − 0 ; (0_{E}) ; !Γ^{o} − C^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ C]]) = n; [[Γ ⊢ f]]; []; ε
= n; [[Γ ⊢ f]]; ![]; ε  def. of [] in F ree(C^{!})
= n; [[Γ ⊢ f]]; ε; []
= lin([[Γ ⊢ f]]); []
= [[!Γ^{o} − 0]]; []  IH
= [[!Γ^{o} − C^{o}]]

The (∨_{I1}) case. The proof

Γ ⊢ A ; (∨_{I1}) ; Γ ⊢ A ∨ B

is translated into the proof

!Γ^{o} − A^{o} ; (!_{I}) ; !Γ^{o} −!A^{o}

(⊕_{I1})

!Γ^{o} −!A^{o}⊕!B^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ A ∨ B]]) = n; [[Γ ⊢ A]]; in_{1}; ε
= n; [[Γ ⊢ A]]; δ; !in_{1}; ε  def. of in_{1} in F ree(C^{!})
= n; [[Γ ⊢ A]]; δ; !ε; in_{1}
= γ(n; [[Γ ⊢ A]]); !ε; in_{1}
= γ(n; [[Γ ⊢ A]]; ε); in_{1}
= γ(lin([[Γ ⊢ A]])); in_{1}
= γ([[!Γ^{o} − A^{o}]]); in_{1}  IH
= [[!Γ^{o} −!A^{o}⊕!B^{o}]]

The (∨_{I1}) case is analogous to the (∨_{I1}) case.

The (∨_{E}) case. The proof

Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C
(∨_{E})
Γ ⊢ C

is translated into the proof

!Γ^{o} −!A^{o}⊕!B^{o} !Γ^{o},!A^{o} − C^{o} !Γ^{o},!B^{o} − C^{o}
(⊕_{E})
!Γ^{o},!Γ^{o} − C^{o}
= (Con) and (Ex)
!Γ^{o} − C^{o}

It can be shown by using IH and a lot of algebraic manipulations that lin([[Γ ⊢ C]]) = [[!Γ^{o} − C^{o}]]. □

We still have Corollary 5.3 which corresponds to the fact that the result in [Gir87] showing that the Girard Translation is sound with respect to interpretation in the category of coherence spaces and linear stable functions includes finite sums.

7 Extensions with Recursion

7.1 The λ^{rec}-Calculus

The λ-calculus can be extended with recursion, that is, we have an additional term

recx^{A}.t and a typing rule as given in Appendix A. The extension with recursion will be called the λ^{rec}-calculus. The term and the typing rule for recursion given here can also be found in [Win93]. We still have Lemma 3.1, Proposition 3.2, Lemma 3.3, and Lemma 3.4.

The usual reduction rules for terms of the λ-calculus, [GLT89] can be extended with a reduction rule for the term corresponding to recursion:

recx^{A}.u ⇝ u[recx^{A}.u/x]

By using Lemma 3.4, we see that the rule satisfies “Subject Reduction”, that is, typing is preserved by an application of the reduction rule. Instead of equipping the λ^{rec}-calculus with the mentioned reduction rules, one could define an operational semantics in natural semantics style. This is done in [Win93].

The Curry-Howard isomorphism on the level of proofs can be extended to include the term and the rule for recursion, that is, we have a bijective correspondence between proofs in IL, extended with the rule for recursion as given in Appendix B, and derivable sequents of the λ^{rec}-calculus.

Given a cartesian closed category with an internal fixpoint operator as in Definition 2.15, we extend the categorical interpretation of the λ-calculus to include the rule for recursion, cf. Appendix A, such that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents (where we consider naturality of the operation on arrows corresponding to recursion as naturality in the interpretation of Γ), and such that Lemma 3.5 and Lemma 3.6 still hold.

By using Lemma 3.6, it can be shown that the interpretation is sound with respect to the reduction rule for the term corresponding to recursion. This is so because the reduction rule is essentially a syntactic restatement of the defining equation of a parametrised fixpoint in Definition 2.13.

7.2 The linear λ^{rec}-Calculus

The linear λ-calculus can be extended with recursion, that is, we have an additional term

let t, ..., t be x_{1}, ..., x_{n} in recz^{!A}.t

and a typing rule as given in Appendix C. The extension with recursion will be called the linear λ^{rec}-calculus. We still have Lemma 4.1, Proposition 4.2, and Lemma 4.3.

The reduction rules for terms of the linear λ-calculus, [BBdPH92], can be extended with a reduction rule for the term corresponding to recursion:

let \overline{w} be \overline{x} in recz^{!A}.u ⇝ copy \overline{w} as \overline{x}, \overline{x′′} in (u[let \overline{x′′} be \overline{x′} in !(let \overline{x′} be \overline{x} in recz^{!A}.u)/z])

By using Lemma 4.3, we see that the rule satisfies “Subject Reduction”. Instead of equipping the linear λ^{rec}-calculus with the mentioned reduction rules, one could define an operational semantics in natural semantics style. This is dealt with in [Bra94a].

The Curry-Howard isomorphism on the level of proofs can also be extended in the ILL case to include the term and the rule for recursion, that is, we have a bijective correspondence between proofs in ILL, extended with the rule for recursion as given in Appendix D, and derivable sequents of the linear λ^{rec}-calculus.

Given a linear category with finite products and a (generalised) internal linear fixpoint operator as in Definition 2.30, we extend the categorical interpretation of the linear λcalculus to include the rule for recursion, cf. Appendix C, such that the operations on arrows induced by the typing rules are natural in the interpretation of the unchanged components of the sequents (where we consider naturality of the operation on arrows corresponding to recursion as naturality in the interpretation of Γ_{1}, ..., Γ_{n}), and such that Lemma 4.4 still holds.

By using Lemma 4.4, it can be shown that the interpretation is sound with respect to the reduction rule for the term corresponding to recursion. This is so because the reduction rule is essentially a syntactic restatement of the defining equation of a (generalised) parametrised linear fixpoint in Definition 2.29.

7.3 The Girard Translation Extended with Recursion

The Girard Translation still works if we extend it with the rules for recursion given in Appendix B and Appendix D. The extended Girard Translation at the level of proofs is stated in Appendix E. The translation preserves the reduction rule for recursion. The translation induces a translation from types and derivable sequents in the λ^{rec}-calculus to types and derivable sequents in the linear λ^{rec}-calculus cf. the extended Curry-Howard isomorphisms.

If C is a linear category with finite products and a (generalised) internal linear fixpoint operator, then F ree(C^{!}) is a cartesian closed category with an internal fixpoint operator, as previous results show. We can therefore interpret types and derivable sequents in the λ^{rec}-calculus as objects and arrows in F ree(C^{!}). We obviously still have Proposition 5.1; and Theorem 5.2 (Soundness) also still holds, as the following addition to the proof shows:

The proof

Γ, B ⊢ B ; (Rec) ; Γ ⊢ B

is translated into the proof

!Γ^{o},!B^{o} − B^{o} ; (Rec) ; !Γ^{o} − B^{o}

The following calculation shows the wanted result:

lin([[Γ ⊢ B]]) = n; λ([[Γ, B, ⊢ B]]); Y; ε
= n; ϕ^{−1}(λ(ϕ(n; [[Γ, B, ⊢ B]]))); ϕ^{−1}(Y); ε  def. of λ and Y in F ree(C^{!})
= γ(n; λ(n; [[Γ, B, ⊢ B]]; ε)); Y
= γ(λ((n ⊗ Id); n; [[Γ, B, ⊢ B]]; ε)); Y
= γ(λ(n; [[Γ, B, ⊢ B]]; ε)); Y  *
= γ(λ(lin([[Γ, B, ⊢ B]]))); Y
= γ(λ([[!Γ^{o},!B^{o} − B^{o}]])); Y  IH
= [[!Γ^{o} − B^{o}]]

* Because n makes ! a monoidal functor from (C, 1, ×) to (C, I, ⊗). □

7.4 The Choice of Rule for Recursion in the linear λ^{rec}-Calculus

The first demand to an extension of the linear λ-calculus with recursion is that it must enable the existing Curry-Howard isomorphism to be extended, as is the case with the extension of the λ-calculus with recursion. Secondly, the Girard Translation must still work with the extensions, and moreover, the translation must preserve the reduction rule for recursion.

The the choice of rules for recursion is best explained in terms of Gentzen style formulations of IL and ILL. In natural deduction style we have introduction and elimination rules for each type constructor. In Gentzen style we have two introduction rules for each type constructor; a constructor can be introduced on each side of the sequent, and moreover, we have the cut rule. The Girard Translation translation for Gentzen style formulations of IL and ILL is similar to the translation for the natural deduction style formulations given in Appendix E, except the case with the cut rule:

Γ ⊢ A Γ, A ⊢ C ; (Cut) ; Γ ⊢ C ↦ !Γ^{o} − A^{o} ; (!_{R}) ; !Γ^{o} −!A^{o} !Γ^{o},!A^{o} − C^{o}

(Cut)
!Γ^{o},!Γ^{o} − C^{o}
= (Con) and (Ex)
!Γ^{o} − C^{o}

Now, we will ensure that the Girard Translation still works with the rules for recursion by taking the rule for recursion in the extended ILL in Gentzen style to be the image under the translation of the rule for recursion in the extended IL in Gentzen style (note that the rule for recursion in the extended IL in Gentzen style is the same as in the natural deduction formulation, the λ^{rec}-Calculus). We thus obtain the extended translation as follows:

Γ, B ⊢ B ; (Rec) ; Γ ⊢ B  ↦  !Γ^{o},!B^{o} − B^{o} ; (Rec) ; !Γ^{o} − B^{o}

When decorated appropriately with terms, it is easy to see that these rules enable the existing Curry-Howard isomorphisms for IL and ILL to be extended. We also want the translation to preserve the reduction rule for recursion, which in the extended IL looks as follows:

Γ, B ⊢ B ; (Rec) ; Γ ⊢ B  ⇝  Γ, B ⊢ B ; (Rec) ; Γ ⊢ B Γ, B ⊢ B ; (Cut) ; Γ ⊢ B

corresponding to

recx.u ⇝ u[recx.u/x]

when the rules are decorated with terms. We will ensure that the Girard Translation preserves the reduction rule for recursion by taking the reduction rule for recursion in the extended ILL to be the image under the translation of the reduction rule for recursion in the extended IL. We thus obtain the reduction rule for recursion in the extended ILL as follows:

!Γ^{o},!B^{o} − B^{o} ; (Rec) ; !Γ^{o} − B^{o}

⇝ !Γ^{o},!B^{o} − B^{o} ; (Rec) ; !Γ^{o} − B^{o} ; (!_{R}) ; !Γ^{o} −!B^{o} !Γ^{o},!B^{o} − B^{o}

(Cut)
!Γ^{o},!Γ^{o} − B^{o}
= (Con) and (Ex)
!Γ^{o} − B^{o}

corresponding to

let \overline{y} be \overline{x} in recz.u ⇝ copy \overline{y} as \overline{x}, \overline{x′′} in (u[let \overline{x′′} be \overline{x′} in !(let \overline{x′} be \overline{x} in recz.u)/z])

when the rules are decorated with terms.

The above mentioned rule for recursion in the extended ILL is appropriate for a Gentzen style formulation, but we lose the Substitution Property if we add it to a natural deduction formulation of ILL. This problem is similar to the problem with the (!_{R}) rule, [Wad91]. The solution is similar too; we generalise the rule for recursion to the one given in Appendix D. The above mentioned reduction rule for recursion in the extended ILL in Gentzen style corresponds to the one given in the natural deduction formulation, the linear λ^{rec}-calculus.

Recursion in the linear λ^{rec}-calculus is essentially the image under the Girard Translation of recursion in the λ^{rec}-calculus, that is, it is essentially recursion in the IL fragment of ILL. Speaking in semantical terms, then parametrised linear fixpoints are parametrised fixpoints in F ree(C^{!}). When looking at particular models of ILL, for example the category of CPOs and strict continuous functions, there does not seem to be a general method to find non-trivial fixpoints of arbitrary maps; there only seems to be a general method for maps corresponding to maps of free coalgebras. This is evidence that it is not possible to define recursion in the linear λ-calculus in a way that is more general that the one given in the present paper.

Acknowledgements. I am grateful to my supervisor, Glynn Winskel, for his guidance and support. Thanks to Valeria de Paiva for discussions on linear logic and for comments on this paper at various stages of its history. Thanks also to Gavin Bierman for comments on an early version of this paper and for a Girardian turnstyle macro. Thanks to Claudio Hermida for advice on categorical matters and thanks to Francois Lamarche for a discussion on linear fixpoint objects. I have used Paul Taylor’s macros to produce the diagrams and proof-rules.

References

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

[AJM95] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Manuscript, 1995.

[AM94] S. Abramsky and G. McCusker. Games for recursive types. Manuscript, 1994.

[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] G. Bierman. On Intuitionistic Linear Logic. PhD thesis, Computer Laboratory, University of Cambridge, 1994.

[Bra94a] T. Braüner. A general adequacy result for a linear functional language. Technical Report BRICS-RS-94-22, BRICS, Department of Computer Science, University of Aarhus, aug 1994. Manuscript presented at MFPS ’94.

[Bra94b] T. Braüner. A model of intuitionistic affine logic from stable domain theory. In Proceedings of ICALP ’94, LNCS, volume 820. Springer-Verlag, 1994.

[BW85] M. Barr and C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

[BW90] M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1990.

[CP90] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations. In 5th LICS Conference. IEEE, 1990.

[Fio94] M. P. Fiore. First steps on the representation of domains. Manuscript, 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.

[HO94] J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF. Manuscript, 1994.

[How80] W. A. Howard. The formulae-as-type notion of construction. In J. R. Hindley and J. P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.

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

[Lam] F. Lamarche. Dialectics: a model of linear logic and PCF. Submitted to MSCS.

[Law69] F. W. Lawvere. Diagonal arguments and cartesian closed categories. In P. Hilton, editor, Category Theory, Homology Theory and their Applications II, LNM, volume 92. Springer-Verlag, 1969.

[Mac91] I. Mackie. Lilac : A Functional Programming Language Based on Linear Logic. M.Sc. thesis, Imperial College, 1991.

[MRA93] I. Mackie, L. Román, and S. Abramsky. An internal language for autonomous categories. Journal of Applied Categorical Structures, 1, 1993.

[Mul92] P. S. Mulry. Strong monads, algebras and fixed points. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Application of Categories in Computer Science, volume 177. London Mathematical Society Lecture Notes Series, 1992.

[Plo93] G. D. Plotkin. Type theory and recursion (extended abstract). In 8th LICS Conference. IEEE, 1993.

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

[Sim92] A. Simpson. Recursive types in kleisli categories. Manuscript, 1992.

[Wad91] P. 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, The λ^{rec}-Calculus with Categorical Semantics

Axiom

\begin{aligned}& (Ax) \\ x_{1} : A_{1}, ..., x_{n} : A_{n} ⊢ x_{q} : A_{q} \end{aligned} A_{1} × ... × A_{n} ^{π_{q}}^{}A_{q}

Logical Rules, the (t, ∧, ⇒) Fragment

\begin{aligned}& (t_{I}) \\ Γ ⊢<>: t \end{aligned}  Γ ^{<>}^{}1
Γ ⊢ u : A Γ ⊢ v : B ; (∧_{I}) ; Γ ⊢< u, v >: A ∧ B  {Γ ^{u}^{}A Γ ^{v}^{}B \atop Γ ^{<u,v>}^{}A × B}
Γ ⊢ u : A ∧ B ; (∧_{E1}) ; Γ ⊢ fst(u) : A  {Γ ^{u}^{}A × B \atop Γ ^{u}^{}A × B ^{π_{1}}^{}A}
Γ ⊢ u : A ∧ B ; (∧_{E2}) ; Γ ⊢ snd(u) : B  {Γ ^{u}^{}A × B \atop Γ ^{u}^{}A × B ^{π_{2}}^{}B}
Γ, x : A ⊢ u : B ; (⇒_{I}) ; Γ ⊢ λx^{A}.u : A ⇒ B  {Γ × A ^{u}^{}B \atop Γ ^{λ(u)}^{}A ⇒ B}
Γ ⊢ f : A ⇒ B Γ ⊢ u : A ; (⇒_{E}) ; Γ ⊢ fu : B {Γ ^{f}^{}A ⇒ B Γ ^{u}^{}A \atop Γ ^{<f,u>}^{}(A ⇒ B) × A ^{eval}^{}B}

Logical Rules, the (f, ∨) Fragment

Γ ⊢ w : f ; (f_{E}) ; Γ ⊢ []^{C}(w) : C  {Γ ^{w}^{}0 \atop Γ ^{w}^{}0 ^{[]}^{}C}
Γ ⊢ u : A ; (∨_{I1}) ; Γ ⊢ inl^{A∨B}(u) : A ∨ B {Γ ^{u}^{}A \atop Γ ^{u}^{}A ^{in_{1}}^{}A + B}

Γ ⊢ u : B ; (∨_{I2}) ; Γ ⊢ inr^{A∨B}(u) : A ∨ B {Γ ^{u}^{}B \atop Γ ^{u}^{}B ^{in_{2}}^{}A + B}

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

(∨_{E})

Γ ⊢ case w of inl(x) => u | inr(y) => v : C

Γ ^{w}^{}A + B Γ × A ^{u}^{}C Γ × B ^{v}^{}C

Γ ^{<Γ,w>}^{}Γ × (A + B) ^{Γ×[λ(u),λ(v)]}^{}Γ × (Γ ⇒ C) ^{eval}^{}C

Rule for Recursion

Γ, x : B ⊢ u : B ; (Rec) ; Γ ⊢ recx^{B}.u : B {Γ × B ^{u}^{}B \atop Γ ^{λ(u)}^{}B ⇒ B ^{Y}^{}B}

B Appendix, Natural Deduction Formulation of IL (Extended with Recursion)

Axiom

\begin{aligned}& (Ax) \\ A_{1}, ..., A_{n} ⊢ A_{q} \end{aligned}

Logical Rules, the (t, ∧, ⇒) Fragment

\begin{aligned}& (t_{I}) \\ Γ ⊢ t \end{aligned}

Γ ⊢ A Γ ⊢ B ; (∧_{I}) ; Γ ⊢ A ∧ B Γ ⊢ A ∧ B ; (∧_{E1}) ; Γ ⊢ A Γ ⊢ A ∧ B ; (∧_{E2}) ; Γ ⊢ B
Γ, A ⊢ B ; (⇒_{I}) ; Γ ⊢ A ⇒ B  Γ ⊢ A ⇒ B Γ ⊢ A ; (⇒_{E}) ; Γ ⊢ B

Logical Rules, the (f, ∨) Fragment

Γ ⊢ f ; (f_{E}) ; Γ ⊢ C

Γ ⊢ A ; (∨_{I1}) ; Γ ⊢ A ∨ B Γ ⊢ B ; (∨_{I2}) ; Γ ⊢ A ∨ B Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C ; (∨_{E}) ; Γ ⊢ C

Rule for Recursion

Γ, B ⊢ B ; (Rec) ; Γ ⊢ B

C Appendix, The linear λ^{rec}-Calculus with Categorical Semantics

Axiom

\begin{aligned}& (Ax) \\ x : A − x : A \end{aligned} A ^{A}^{}A

Structural Rule

Γ, x : A, y : B, Δ − u : C ; (Ex) ; Γ, y : B, x : A, Δ − u : C Γ ⊗ A ⊗ B ⊗ Δ ^{u}^{}C

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

Logical Rules, the (I, ⊗, ⊤, &, ⊸,!) Fragment

\begin{aligned}& (I_{I}) \\ − ∗ : I \end{aligned}  I ^{I}^{}I

Λ − w : I Γ − u : A

(I_{E})

Γ, Λ − let w be ∗ in u : A

{Λ ^{w}^{}I Γ ^{u}^{}A \atop Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ I ≅ Γ ^{u}^{}A}

Γ − u : A Δ − v : B ; (⊗_{I}) ; Γ, Δ − u ⊗ v : A ⊗ B  {Γ ^{u}^{}A Δ ^{v}^{}B \atop Γ ⊗ Δ ^{u⊗v}^{}A ⊗ B}

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

(⊗_{E})
Γ, Λ − let w be x ⊗ y in u : C

{Λ ^{w}^{}A ⊗ B Γ ⊗ A ⊗ B ^{u}^{}C \atop Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ A ⊗ B ^{u}^{}C}

\begin{aligned}& (⊤_{I}) \\ Γ − <>: ⊤ \end{aligned}  Γ ^{<>}^{}1

Γ − u : A Γ − v : B ; (&_{I}) ; Γ − < u, v >: A&B  {Γ ^{u}^{}A Γ ^{v}^{}B \atop Γ ^{<u,v>}^{}A × B}

Λ − u : A&B ; (&_{E1}) ; Λ − fst(u) : A  {Λ ^{u}^{}A × B \atop Λ ^{u}^{}A × B ^{π_{1}}^{}A}

Λ − u : A&B ; (&_{E2}) ; Λ − snd(u) : B  {Λ ^{u}^{}A × B \atop Λ ^{u}^{}A × B ^{π_{2}}^{}B}

Γ, x : A − u : B ; (⊸_{I}) ; Γ − λx^{A}.u : A ⊸ B  {Γ ⊗ A ^{u}^{}B \atop Γ ^{λ(u)}^{}A ⊸ B}

Λ − f : A ⊸ B Δ − u : A ; (⊸_{E}) ; Λ, Δ − fu : B  {Λ ^{f}^{}A ⊸ B Δ ^{u}^{}A \atop Λ ⊗ Δ ^{f⊗u}^{}(A ⊸ B) ⊗ A ^{eval}^{}B}

Γ_{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

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

Λ − u :!A
(Der)

Λ − derelict(u) : A

{Λ ^{u}^{}!A \atop Λ ^{u}^{}!A ^{ε}^{}A}

Λ − w :!A Γ, x :!A, y :!A − u : B

(Con)

Γ, Λ − copy w as x, y in u : B

Λ ^{w}^{}!A Γ⊗!A⊗!A ^{u}^{}B
Γ ⊗ Λ ^{Γ⊗w}^{}Γ⊗!A ^{Γ⊗d}^{}Γ⊗!A⊗!A ^{u}^{}B

Λ − w :!A Γ − u : B

(W eak)

Γ, Λ − discard w in u : B

Λ ^{w}^{}!A Γ ^{u}^{}B
Γ ⊗ Λ ^{Γ⊗w}^{}Γ⊗!A ^{Γ⊗e}^{}Γ ⊗ I ^{≅}^{}Γ ^{u}^{}B

Logical Rules, the (0, ⊕) Fragment

Λ − w : 0 ; (0_{E}) ; Λ − []^{C}(w) : C  {Λ ^{w}^{}0 \atop Λ ^{w}^{}0 ^{[]}^{}C}

Γ − u : A ; (⊕_{I1}) ; Γ − inl^{A⊕B}(u) : A ⊕ B {Γ ^{u}^{}A \atop Γ ^{u}^{}A ^{in_{1}}^{}A + B}

Γ − u : B ; (⊕_{I2}) ; Γ − inr^{A⊕B}(u) : A ⊕ B {Γ ^{u}^{}B \atop Γ ^{u}^{}B ^{in_{2}}^{}A + B}

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

(⊕_{E})

Γ, Λ − case w of inl(x) => u | inr(y) => v : C

Λ ^{w}^{}A + B Γ ⊗ A ^{u}^{}C Γ ⊗ B ^{v}^{}C

Γ ⊗ Λ ^{Γ⊗w}^{}Γ ⊗ (A + B) ≅ (Γ ⊗ A) + (Γ ⊗ B) ^{[u,v]}^{}C

Rule for Recursion

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

(Rec)

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

{Γ_{1} ^{w_{1}}^{}!A_{1} , ..., Γ_{n} ^{w_{n}}^{}!A_{n} !A_{1} ⊗ ...⊗!A_{n}⊗!B ^{u}^{}B \atop Γ_{1} ⊗ ... ⊗ Γ_{n} ^{w_{1}⊗...⊗w_{n}}^{}!A_{1} ⊗ ...⊗!A_{n} ^{γ(λ(u))}^{}!(!B ⊸ B) ^{Y}^{}B}

D Appendix, Natural Deduction Formulation of ILL (Extended with Recursion)

Axiom

\begin{aligned}& (Ax) \\ A − A \end{aligned}

Structural Rule

Γ, A, B, Δ − C

(Ex)

Γ, B, A, Δ − C

Logical Rules, the (I, ⊗, ⊤, &, ⊸,!) Fragment

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

\begin{aligned}& (⊤_{I}) \\ Γ − ⊤ \end{aligned}

Γ − A Γ − B ; (&_{I}) ; Γ − A&B  Λ − A&B ; (&_{E1}) ; Λ − A Λ − A&B ; (&_{E2}) ; Λ − B
Γ, A − B ; (⊸_{I}) ; Γ − A ⊸ B  Λ − A ⊸ B Δ − A ; (⊸_{E}) ; Λ, Δ − B
Γ_{1} −!A_{1} , ..., Γ_{n} −!A_{n} !A_{1}, ...,!A_{n} − A ; (!_{I}) ; Γ_{1}, ..., Γ_{n} −!A  Λ −!A ; (Der) ; Λ − A
Λ −!A Γ,!A,!A − B
(Con)
Γ, Λ − B
Λ −!A Γ − B
(W eak)
Γ, Λ − B

Logical Rules, the (0, ⊕) Fragment

Λ − 0 ; (0_{E}) ; Λ − C

Γ − A ; (⊕_{I1}) ; Γ − A ⊕ B Γ − B ; (⊕_{I2}) ; Γ − A ⊕ B Λ − A ⊕ B Γ, A − C Γ, B − C ; (⊕_{E}) ; Γ, Λ − C

Rule for Recursion

Γ_{1} −!A_{1} , ..., Γ_{n} −!A_{n} !A_{1}, ...,!A_{n},!B − B

(Rec)
Γ_{1}, ..., Γ_{n} − B

E Appendix, The Girard Translation (Extended with Recursion)

A proof of A_{1}, ..., A_{n} ⊢ B is translated into a proof of !A_{1}^{o}, ...,!A_{n}^{o} − B^{o} by induction in the proof of A_{1}, ..., A_{n} ⊢ B. Special cases of rules will be used in the definition when appropriate (for example in the case of (Rec)). A double bar means a number of applications of a rule.

Axiom

\begin{aligned}& (Ax) \\ A_{1}, ..., A_{n} ⊢ A_{q} \end{aligned}  ↦  \begin{aligned}& (Ax) \\ !A_{q}^{o} −!A_{q}^{o} \end{aligned} ; (Der) ; !A_{q}^{o} − A_{q}^{o} ; = (W eak) and (Ex) ; !A_{1}^{o}, ...,!A_{n}^{o} − A_{q}^{o}

Logical Rules, the (t, ∧, ⇒) Fragment

\begin{aligned}& (t_{I}) \\ Γ ⊢ t \end{aligned}  ↦  \begin{aligned}& (⊤_{I}) \\ !Γ^{o} − ⊤ \end{aligned}

Γ ⊢ A Γ ⊢ B ; (∧_{I}) ; Γ ⊢ A ∧ B  ↦  !Γ^{o} − A^{o} !Γ^{o} − B^{o} ; (&_{I}) ; !Γ^{o} − A^{o}&B^{o}

Γ ⊢ A ∧ B ; (∧_{E1}) ; Γ ⊢ A  ↦  !Γ^{o} − A^{o}&B^{o} ; (&_{E1}) ; !Γ^{o} − A^{o}

Γ ⊢ A ∧ B ; (∧_{E2}) ; Γ ⊢ B  ↦  !Γ^{o} − A^{o}&B^{o} ; (&_{E2}) ; !Γ^{o} − B^{o}

Γ, A ⊢ B ; (⇒_{I}) ; Γ ⊢ A ⇒ B  ↦  !Γ^{o},!A^{o} − B^{o} ; (⊸_{I}) ; !Γ^{o} −!A^{o} ⊸ B^{o}

Γ ⊢ A ⇒ B Γ ⊢ A ; (⇒_{E}) ; Γ ⊢ B ↦ !Γ^{o} −!A^{o} ⊸ B^{o} !Γ^{o} − A^{o} ; (!_{I}) ; !Γ^{o} −!A^{o}

(⊸_{E})
!Γ^{o},!Γ^{o} − B^{o}
= (Con) and (Ex)
!Γ^{o} − B^{o}

Logical Rules, the (f, ⊕) Fragment

Γ ⊢ f ; (f_{E}) ; Γ ⊢ C  ↦  !Γ^{o} − 0 ; (0_{E}) ; !Γ^{o} − C^{o}

Γ ⊢ A ; (∨_{I1}) ; Γ ⊢ A ∨ B  ↦  !Γ^{o} − A^{o} ; (!_{I}) ; !Γ^{o} −!A^{o} ; (⊕_{I1}) ; !Γ^{o} −!A^{o}⊕!B^{o}

Γ ⊢ B ; (∨_{I2}) ; Γ ⊢ A ∨ B  ↦  !Γ^{o} − B^{o} ; (!_{I}) ; !Γ^{o} −!B^{o} ; (⊕_{I2}) ; !Γ^{o} −!A^{o}⊕!B^{o}

Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C ; (∨_{E}) ; Γ ⊢ C  ↦

!Γ^{o} −!A^{o}⊕!B^{o} !Γ^{o},!A^{o} − C^{o} !Γ^{o},!B^{o} − C^{o}

(⊕_{E})

!Γ^{o},!Γ^{o} − C^{o} = (Con) and (Ex)

!Γ^{o} − C^{o}

Rule for Recursion

Γ, B ⊢ B ; (Rec) ; Γ ⊢ B  ↦  !Γ^{o},!B^{o} − B^{o} ; (Rec) ; !Γ^{o} − B^{o}

F Appendix, (Linear) Fixpoint Objects

F.1 Fixpoint Objects

Let C be a linear category such that F ree(C^{!}) is closed under finite products. The category F ree(C^{!}) is cartesian closed as shown above, and moreover, it has a strong monad (T, η, μ, t) induced by the adjunction U^{!} ⊣ F^{!}. The functor T is given by F^{!}U^{!}, a component η_{(!A,δ)} is given by

(!A, δ) ^{δ_{A}}^{}(!!A, δ) = T (!A, δ)

and a component μ_{(!A,δ)} is given by

T T (!A, δ) = (!!!A, δ) ^{!ε_{!A}}^{}(!!A, δ) = T (!A, δ)

A cartesian closed category with a strong monad enables us to define a fixpoint object, [CP90]. We will not give the original definition here, but instead the following equivalent definition, [Mul92].

Definition F.1 A fixpoint object in a cartesian closed category with a strong monad is

1. an initial T -algebra σ_{Z} : T Z → Z,

2. a map ∞ : 1 → Z which is an equaliser of η_{Z}; σ_{Z} and Id_{Z}.

It is shown in [Mul92] that there is a parametrised fixpoint operator restricted to underlying objects of Eilenberg-Moore T-algebras in a cartesian closed category with a strong monad and a fixpoint object.

If we consider F ree(C^{!}), then every object (!A, δ) can be equipped with a map h_{(!A,δ)} making it an Eilenberg-Moore T-algebra, namely the map

T (!A, δ) = (!!A, δ) ^{!ε_{A}}^{}(!A, δ)

It is obviously a map of free coalgebras, and it is straightforward to check that the the following diagrams commute

[figure: (!A, δ); η; T (!A, δ); Id; (!A, δ); h; T T (!A, δ); μ; T (!A, δ); T (!A, δ); T h; h; (!A, δ); h]

so it is an Eilenberg-Moore T-algebra. We conclude that if F ree(C^{!}) has a fixpoint object, then it has a parametrised fixpoint operator, which is equivalent to C having a parametrised linear fixpoint operator.

It should be remarked that the category of CPOs and continuous functions, which is equivalent to the category of free coalgebras induced by category of CPOs and strict continuous functions, has a fixpoint object, namely the vertical natural numbers.

F.2 Linear Fixpoint Objects

We have above given an account af a parametrised linear fixpoint operator in C in terms of a fixpoint object in F ree(C^{!}). It is actually possible to give an account af a parametrised linear fixpoint operator in terms of something similar to a fixpoint object that lives in the same category as where the parametrised linear fixpoint operator lives, namely C. The definition of a linear fixpoint object exploits an initial !-algebra as suggested in [Lam].

Definition F.2 A linear fixpoint object in a pre !-category C is

1. an initial !-algebra σ_{Z} :!Z → Z,

2. a map ∞ : I → Z such that γ(∞) is an equaliser of γ(σ_{Z}) and Id_{!Z}.

Note that γ(f) = γ(f); γ(σ_{Z}) iff f = γ(f); σ_{Z} for any map f : I → Z. Given a !-algebra g :!A → A, then we define It(g) : Z → A to be a unique map making

[figure: !Z; σ; Z; !A; !It(g); g; A; It(g)]

commute.

It should be remarked that the category of CPOs and strict continuous functions as well as the category of dI domains and linear stable functions has a linear fixpoint object, namely the vertical natural numbers.

We will use the rest of this subsection to show that a linear fixpoint object on a linear category induces a unique parametrised linear fixpoint operator satisfying a linear version of Plotkin’s Axiom. This is essentially a linear version of an analogous result given in [Sim92] which says that a fixpoint object under certain conditions induces a unique parametrised fixpoint operator satisfying Plotkin’s Axiom. Now, Plotkin’s Axiom is especially simple in the context of a pre !-category:

Definition F.3 A linear fixpoint operator (−)^{♯} on a pre !-category C satisfies Plotkin’s Axiom iff whenever we have maps f :!B → B, g :!C → C, and h : B → C such that the following diagram commutes

[figure: !B; f; B; !C; !h; g; C; h]

then the following diagram commutes too

I  \overline{f^{♯} ^{}}B
[figure: g^{♯}]
C^{^{}h}

Lemma F.4 Let C be a pre !-category with a linear fixpoint operator (−)^{♯} satisfying Plotkin’s Axiom. The diagram

I  \overline{ε_{B}^{♯} ^{}}B
[figure: ε_{C}^{♯}]
C^{^{}h}

commutes for any map h : B → C.

Proof. The result follows from commutativity of

[figure: !B; ε_{B}; B; !C; !h; ε_{C}; C; h]

cf. Plotkin’s Axiom. □

Lemma F.5 Let C be a pre !-category with a linear fixpoint object (σ_{Z}, ∞) with the property that whenever we have a map f : I → Z such that γ(f) equalises γ(σ_{Z}) and Id_{!Z} then f = ∞. Then C has a unique linear fixpoint operator (−)^{♯} satisfying Plotkin’s Axiom.

Proof. Given a map f :!B → B define f^{♯} = ∞; It(f). Commutativity of the following diagram shows that f^{♯} indeed is a linear fixpoint of f

!I ^{_{}m_{I}}  I

[figure: !Z; !∞; σ; Z; ∞]

[figure: !B; !It(f); f; B; It(f)]

We will now show that the linear fixpoint operator (−)^{♯} satisfies Plotkin’s Axiom, so assume that we have maps f :!B → B, g :!C → C, and h : B → C making the first diagram in Definition F.3 commute. The diagram

!Z  \overline{σ ^{}}Z

[figure: !B; !It(f); f; B; It(f)]

[figure: !C; !h; g; C; h]

commutes, so we have It(g) = It(f); h, which entails that the last diagram in Definition F.3 commutes.

We will now show that the linear fixpoint operator (−)^{♯} is the unique one which satisfies Plotkin’s Axiom, so assume that (−)^{♯′} is an arbitrary linear fixpoint operator satisfying Plotkin’s Axiom and let a map f :!B → B be given. We will then show that f^{♯′} = f^{♯}.

The following diagram commutes

[figure: !Z; σ; Z; !B; !It(f); f; B; It(f)]

which entails that the following diagram commutes

I  \overline{σ^{♯′} ^{}}Z
[figure: f^{♯′}]
B^{^{}It(f)}

because (−)^{♯′} is assumed to satisfy Plotkin’s Axiom. But σ^{♯′} = γ(σ^{♯′}); σ which entails that σ^{♯′} = ∞ cf. the assumption, and we conclude that f^{♯′} = f^{♯}. □

Let C be a pre !-category with a linear fixpoint object (σ_{Z}, ∞). If the pre !-category C is part of a !-category, then it is straightforward to check that whenever we have a map f : I → Z such that γ(f) equalises γ(σ_{Z}) and Id_{!Z} then we automatically have f = ∞. Thus, the corresponding extra condition of Lemma F.5 vanishes.

We will show an analogous result for parametrised linear fixpoint operators, so here is a parametrised version of Plotkin’s Axiom:

Definition F.6 A parametrised linear fixpoint operator (−)^{♯} on a !-category C satisfies Plotkin’s Axiom iff whenever we have maps f :!A⊗!B → B, g :!A⊗!C → C, and h :!A ⊗ B → C such that the following diagram commutes

[figure: !A⊗!B; d ⊗ Id; (!A⊗!A)⊗!B ≅!A ⊗ (!A⊗!B); Id ⊗ f; !A ⊗ B]

(!A⊗!A)⊗!B^{^{}d ⊗ Id}

!A ⊗ (!A⊗!B)^{^{}≅}

!A ⊗ (!!A⊗!B)^{^{}Id ⊗ (δ ⊗ Id)}

!A⊗!(!A ⊗ B)^{^{}Id ⊗ m}

[figure: !A⊗!C; Id⊗!h; g; C; h]

then the following diagram commutes too

[figure: !A; d; !A⊗!A; Id ⊗ f^{♯}; !A ⊗ B]
[figure: g^{♯}; h]
C

Lemma F.7 Let C be a linear category with an initial !-algebra σ_{Z} :!Z → Z. Given a map f :!A⊗!B → B there is a unique map IT (f) :!A ⊗ Z → B making the following diagram commute

!A⊗!Z  \overline{Id ⊗ σ_{}}!A ⊗ Z

(!A⊗!A)⊗!Z^{d ⊗ Id^{}}

!A ⊗ (!A⊗!Z)^{≅^{}}

!A ⊗ (!!A⊗!Z)^{Id ⊗ (δ ⊗ Id)^{}}

!A⊗!(!A ⊗ Z)^{Id ⊗ m^{}}

[figure: !A⊗!B; Id⊗!IT (f); f; B; IT (f)]

Proof. Let a map f :!A⊗!B → B be given. We have to show that there is a unique map IT (f) :!A ⊗ Z → B making the wanted diagram commute. We first define H_{1} to be the composite

!(!A ⊸ B)⊗!A ^{Id⊗d}^{}!(!A ⊸ B) ⊗ (!A⊗!A) ≅ (!(!A ⊸ B)⊗!A)⊗!A

we then define H_{2} to be the composite

!(!A ⊸ B)⊗!A ^{Id⊗δ}^{}!(!A ⊸ B)⊗!!A ^{m}^{}!((!A ⊸ B)⊗!A) ^{!eval}^{}!B

and finally, we define IT (f) to be a unique map making the following diagram commute

[figure: !Z; σ; Z; !(!A ⊸ B); !λ(≅; IT (f)); λ(H_{1}; (H_{2} ⊗ Id); ≅; f); !A ⊸ B; λ(≅; IT (f))]

where we use that the operation λ(≅; (−)) from C(!A ⊗ Z, B) to C(Z,!A ⊸ B) is a bijection. We will now show that IT (f) is a unique map making the wanted diagram commute by showing that the operation ≅; λ^{−1}(−) from C(!Z,!A ⊸ B) to C(!A⊗!Z, B), which is a bijection, applied to each of the two paths in the defining diagram for IT (f) yields each of the two paths in the wanted diagram. Firstly, we have that

≅; λ^{−1}(σ; λ(≅; IT (f))) = (Id ⊗ σ); IT (f)

Secondly, we have that

≅; λ^{−1}(!λ(≅; IT (f)); λ(H_{1}; (H_{2} ⊗ Id); ≅; f)) = ≅; (!λ(≅; IT (f)) ⊗ Id); H_{1}; (H_{2} ⊗ Id); ≅; f =

≅; (Id ⊗ d); ≅; ((Id ⊗ δ) ⊗ Id); (m ⊗ Id); (! ≅ ⊗Id); (!IT (f) ⊗ Id); ≅; f =  *
≅; (Id ⊗ d); ≅; (≅ ⊗Id); ≅; (Id ⊗ (δ ⊗ Id)); (Id ⊗ m); (Id⊗!IT (f)); f =  **

(d ⊗ Id); ≅; (Id ⊗ (δ ⊗ Id)); (Id ⊗ m); (Id⊗!IT (f)); f

* cf. commutativity of the following diagram

[figure: (!Z⊗!A)⊗!A; (Id ⊗ δ) ⊗ Id; (!Z⊗!!A)⊗!A; m ⊗ Id; !(Z⊗!A)⊗!A]

1.

[figure: (!A⊗!Z)⊗!A; ≅ ⊗Id; (δ ⊗ Id) ⊗ Id; (!!A⊗!Z)⊗!A; ≅ ⊗Id; m ⊗ Id; !(!A ⊗ Z)⊗!A; ! ≅ ⊗Id]

[figure: !A ⊗ (!A⊗!Z); ≅; Id ⊗ (δ ⊗ Id); !A ⊗ (!!A⊗!Z); ≅; !B⊗!A; !IT (f) ⊗ Id]

[figure: !A⊗!(!A ⊗ Z); Id ⊗ m; Id⊗!IT (f); !A⊗!B; ≅]

1. ! is symmetric monoidal.

** cf. commutativity of the following diagram

!A⊗!Z  \overline{≅ ^{}}!Z⊗!A
[figure: d ⊗ Id; 1.]
[figure: (!A⊗!A)⊗!Z; ≅ ⊗Id; (!A⊗!A)⊗!Z; d ⊗ Id; ≅; !Z ⊗ (!A⊗!A); Id ⊗ d]

!A ⊗ (!A⊗!Z)^{≅^{}}

!A ⊗ (!Z⊗!A)^{Id⊗ ≅^{}}

[figure: !A ⊗ (!A⊗!Z); ≅; ≅; (!A⊗!Z)⊗!A; ≅; ≅ ⊗Id; (!Z⊗!A)⊗!A; ≅]

1. d is part of a commutative comonoid. □

Lemma F.8 Let C be a linear category with a linear fixpoint object (σ_{Z}, ∞). Then (F_{S^{A}}(σ_{Z}), F_{S^{A}}(∞)) is a linear fixpoint object on C_{S^{A}} with the property that whenever we have a map f :!A ⊗ I → Z in C_{S^{A}} such that γ(f) equalises γ(σ_{Z}) and Id_{!Z} in C_{S^{A}} then f = F_{S^{A}}(∞).

Proof. Note that we consider C_{S^{A}} as a pre !-category. The map F_{S^{A}}(σ_{Z}) is an initial ˜!-algebra, Lemma F.7. The functor F_{S^{A}} has a left adjoint, which entails that it preserves limits, so F_{S^{A}}(∞) is an equaliser of F_{S^{A}}(γ(σ_{Z})) and Id_{˜!Z} in C_{S^{A}}. But F_{S^{A}}(γ(σ_{Z})) = γ(F_{S^{A}}(σ_{Z})), so (F_{S^{A}}(σ_{Z}), F_{S^{A}}(∞)) is a linear fixpoint object in C_{S^{A}}. We moreover have to show that whenever we have a map f :!A ⊗ I → Z such that γ(f) equalises γ(σ_{Z}) and Id_{!Z} in C_{S^{A}} then f = F_{S^{A}}(∞), which amounts to show that the unique map h :!A ⊗ I → I such that γ(f) = h; γ(F_{S^{A}}(∞)) in C_{S^{A}} is equal to Id_{I} in C_{S^{A}}. Now, γ(f) = h; γ(F_{S^{A}}(∞)) in C_{S^{A}}, which entails that γ(f); F_{S^{A}}(e) = h; γ(F_{S^{A}}(∞)); F_{S^{A}}(e) in C_{S^{A}}. The following calculation shows that RHS is equal to h

γ(F_{S^{A}}(∞)); F_{S^{A}}(e) = F_{S^{A}}(γ(∞)); F_{S^{A}}(e)
= F_{S^{A}}(γ(∞); e)
= F_{S^{A}}(Id)  e is monoidal
= Id

and the following calculation shows that LHS, that is, γ(f); F_{S^{A}}(e), where composition is in C_{S^{A}}, is equal to Id_{I} in C_{S^{A}}

δ^{A}; S^{A}(γ(f)); ε^{A}; e = γ(f); e
= δ^{A}; S^{A}(ε^{A}; m_{I}); λ; !f; e
= S^{A}(m_{I}); λ; e
= (δ ⊗ m_{I}); m; e
= ((δ; e) ⊗ I); ≅  e is monoidal
= (e ⊗ I); ≅  δ is a map of comonoids
= ε^{A}

We conclude that h is equal to Id_{I} in C_{S^{A}}, and thus, f = F_{S^{A}}(∞). □

Theorem F.9 A linear category C with a linear fixpoint object (σ_{Z}, ∞) has a unique parametrised linear fixpoint operator satisfying Plotkin’s Axiom. The parametrised linear fixpoint operator is natural.

Proof. Each category C_{S^{A}}, considered as a pre !-category, has a linear fixpoint object satisfying the extra conditions of Lemma F.5, cf. Lemma F.8. This entails that each category C_{S^{A}} has a unique linear fixpoint operator satisfying Plotkin’s Axiom, Lemma F.5. But to give a linear fixpoint operator on each category C_{S^{A}} is equivalent to give a parametrised linear fixpoint operator on C, Proposition 2.19, and moreover, it is straightforward to see that the linear fixpoint operator on each category C_{S^{A}} satisfies Plotkin’s Axiom iff the corresponding parametrised linear fixpoint operator on C satisfies the parametrised version of Plotkin’s Axiom. The parametrised linear fixpoint operator on C can be shown to be natural. □

F.3 Linear Fixpoint Objects and the Intrinsic Preorder

This subsection should be seen in light of recent work in Axiomatic Domain Theory, [Fio94] where an objective has been to find non-order-theoretic axioms inducing CPO-enrichment on a cartesian closed category. It is, however, the case that a weaker assumption than CPO-enrichment will do if one wants to give an adequate semantics to PCF, namely that of rationality, [AJM95].

Definition F.10 A poset-enriched cartesian closed category C is pointed if each poset C(B, C) has a bottom element ⊥_{B,C} such that f; ⊥_{B,C}=⊥_{A,C} for any map f : A → B.

Definition F.11 Let C be a pointed poset-enriched cartesian closed category. Given a map f : A × B → B, we define a map f^{n} : A → B inductively as

\begin{matrix}f^{0} =⊥_{A,B} \\ f^{n+1} = Δ; (A × f^{n}); f \end{matrix}

Definition F.12 A poset-enriched cartesian closed category C is rational if it is pointed and moreover for every map f : A × B → B the increasing chain {f^{n}|n ∈ ω} has a least upper bound f^{♯} : A → B with the property that g; f^{♯}; h is a least upper bound for the increasing chain {g; f^{n}; h|n ∈ ω} for any maps g : C → A and h : B → D.

The difference is essentially that CPO-enrichment assumes the existence of least upper bounds of arbitrary increasing chains whereas only certain increasing chains are assumed to have least upper bounds in a rational category. It is in this subsection shown how certain axioms entails that the linear fixpoint of a map is a least upper bound of an appropriate increasing chain with respect to the intrinsic preorder. This entails that the induced coKleisli category is rational with respect to the partial order obtained as the quotient of the intrinsic preorder. We first need a couple of definitions from [HO94].

Definition F.13 Let C be a symmetric monoidal closed category. A notion of observables O associates to each object A a set O_{A} of subsets of C(I, A) with the property that if S ∈ O_{B} and g : A → B, then {h : I → A|h; g ∈ O_{B}} ∈ O_{A}.

Given a map f : A → B in a symmetric monoidal closed category, then ⌜f⌝ : I → A ⊸ B is equal to λ(≅; f).

Definition F.14 Let C be a symmetric monoidal closed category with a notion of observables O. The observational preorder ≲ on each C(A, B) is defined as follows

f ≲ g ⇔ ∀R ∈ O_{A⊸B}.⌜f⌝ ∈ R ⇒ ⌜g⌝ ∈ R

The following result can be found in [HO94].

Proposition F.15 A symmetric monoidal closed category C with a notion of observables is preorder-enriched with respect to the induced observational preorder.

Proof. [HO94]. □

In what follows, we will be dealing with an object Σ and a map ⊤ : I → Σ in a symmetric monoidal closed category. The object Σ should be thought of as the Sierpinsky space with the map ⊤ representing the top element. One should in most concrete cases take Σ to be equal to I and ⊤ to be equal to Id_{I}; this is for example the case in the category of CPOs and strict continuous functions and in the category of dI domains and linear stable functions.

Definition F.16 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. For each object A we define

O_{A} = {O_{f}|f :!A → Σ}

where

O_{f} = {h : I → A|γ(h); f = ⊤}

This is a notion of observables because

{h : I → A|h; g ∈ O_{k}} = {h : I → A|γ(h; g); k = ⊤}
= {h : I → A|γ(h); !g; k = ⊤}
= O_{!g;k}

where g : A → B and k :!B → Σ

Definition F.17 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. The intuitionistic intrinsic preorder ≲ on each C(A, B) is defined as the observational preorder induced by O, that is,

f ≲ g ⇔ ∀h :!(A ⊸ B) → Σ.γ(⌜f⌝); h = ⊤ ⇒ γ(⌜g⌝); h = ⊤

Proposition F.18 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. If f, g : I → A, then

f ≲ g ⇔ ∀h :!A → Σ.γ(f); h = ⊤ ⇒ γ(g); h = ⊤

Proof. Note that the two maps

A ^{λ(≅)}^{}I ⊸ A

and

I ⊸ A ^{≅}^{}(I ⊸ A) ⊗ I ^{eval}^{}A

makes A and I ⊸ A isomorphic. The result follows from the observation that f = ⌜f⌝; ≅; eval, and thus γ(f) = γ(⌜f⌝); !(≅; eval), for any map f : I → A. □

Proposition F.19 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. The symmetric monoidal closed category (C, I, ⊗, ⊸) is preorderenriched with respect to the intuitionistic intrinsic preorder.

Proof. Proposition F.15. □

Proposition F.20 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. The functor ! is preorder-enriched with respect to the intuitionistic intrinsic preorder.

Proof. Let maps f, g : A → B such that f ≲ g be given. Consider the map

!(A ⊸ B)⊗!A ^{m}^{}!((A ⊸ B) ⊗ A) ^{!eval}^{}!B

We have that

γ(⌜f⌝); λ(m,!eval) = λ((γ(⌜f⌝)⊗!A); m,!eval)
= λ((m_{I}⊗!A); m,! ≅; !f)
= λ(≅; !f)  ! is monoidal
= ⌜!f⌝

and similarly for g. Thus

γ(⌜!f⌝); h = ⊤  ⇔
γ(⌜f⌝); γ(λ(m,!eval)); h = ⊤ ⇒
γ(⌜g⌝); γ(λ(m,!eval)); h = ⊤ ⇔
γ(⌜!f⌝); h = ⊤

where h :!(!A ⊸!B) → Σ and we conclude that !f ≲!g. □

The following notion of observables is in [HO94] called termination to specified value.

Definition F.21 Let C be a symmetric monoidal closed category. Assume that an object Σ and a map ⊤ : I → Σ is given. For each object A we define

O′_{A} = {O′_{f}|f : A → Σ}

where

O′_{f} = {h : I → A|h; f = ⊤}

This is a notion of observables, as mentioned in [HO94], because

\begin{aligned}\{h : I → A|h; g ∈ O′_{k}\} & = & \{h : I → A|h; g; k = ⊤\} \\ & = & O′_{g;k} \end{aligned}

where g : A → B and k : B → Σ

Definition F.22 Let C be a symmetric monoidal closed category. Assume that an object Σ and a map ⊤ : I → Σ is given. The linear intrinsic preorder ≲′ on each C(A, B) is defined as the observational preorder induced by O′, that is,

f ≲′ g ⇔ ∀h : A ⊸ B → Σ.⌜f⌝; h = ⊤ ⇒ ⌜g⌝; h = ⊤

Proposition F.23 Let C be a symmetric monoidal closed category. Assume that an object Σ and a map ⊤ : I → Σ is given. If f, g : I → A, then

f ≲′ g ⇔ ∀h : A → Σ.f; h = ⊤ ⇒ g; h = ⊤

Proof. Analogous to the proof of Proposition F.18. □

Proposition F.24 A symmetric monoidal closed category C with a given object Σ and a given map ⊤ : I → Σ is preorder-enriched with respect to the linear intrinsic preorder.

Proof. Proposition F.15. □

Definition F.25 Let C be a linear category with a linear fixpoint operator. For any pair of objects A and B we define a map ⊥_{A,B}: A → B as

A ^{≅}^{}I ⊗ A ^{λ^{−1}(ε_{A⊸B}^{♯})}^{}B

Proposition F.26 Let C be a linear category with a linear fixpoint operator satisfying Plotkin’s Axiom. For any object A we have ⊥_{I,A}= ε_{A}^{♯}.

Proof. The result follows from Lemma F.4. □

So ⊥_{I,A} is a linear fixpoint of ε_{A}, that is, a fixpoint of Id_{A} in the coKleisli category.

Proposition F.27 Let C be a linear category with a linear fixpoint operator satisfying Plotkin’s Axiom. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. The map ⊥_{A,B} is a bottom element of C(A, B) with respect to the linear intrinsic preorder.

Proof. We have ε_{A⊸B}^{♯}; h = ε_{Σ}^{♯} cf. Lemma F.4, and therefore ε_{A⊸B}^{♯}; h ≠ ⊤, for any map h : A ⊸ B → Σ. □

Proposition F.28 Let C be a linear category with a linear fixpoint operator satisfying Plotkin’s Axiom. We have ⊥_{A,B}; f =⊥_{A,C} for any map f : B → C.

Proof. The result follows from Lemma F.4. □

Proposition F.29 Let C be a linear category with a linear fixpoint object. We have f; ⊥_{B,C}=⊥_{A,C} for any map f : A → B.

Proof. Let a map f : A → B be given. We have commutativity of

!Z  \overline{σ  ^{}}Z

[figure: !(B ⊸ C); !It(ε_{B⊸C}); ε_{B⊸C}; B ⊸ C; It(ε_{B⊸C})]

[figure: !(A ⊸ C); !(f ⊸ C); ε_{A⊸C}; A ⊸ C; f ⊸ C]

which entails that It(ε_{B⊸C}); (f ⊸ C) = It(ε_{A⊸C}), so

f; ⊥_{B,C} = f; ≅; λ^{−1}(∞; It(ε_{B⊸C}))
= ≅; (I ⊗ f); ((∞; It(ε_{B⊸C})) ⊗ B); eval
= ≅; ((∞; It(ε_{B⊸C})) ⊗ A); ((f ⊸ C) ⊗ A); eval
= ≅; λ^{−1}(∞; It(ε_{B⊸C}); (f ⊸ C))
= ≅; λ^{−1}(∞; It(ε_{A⊸C}))
= ⊥_{A,C}

□

Proposition F.30 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. We have ≲⊆≲′.

Proof. The result follows from the observation that ⌜f⌝ = γ(⌜f⌝); ε for any map f : A → B. □

Now, ! is preorder-enriched with respect to ≲, and ⊥ is a bottom element with respect to ≲′, so we would like the two orders to coinside.

Definition F.31 Let C be a linear category. Assume that an object Σ and a map ⊤ : I → Σ is given. Axiom 1 is satisfied iff we for any maps f, g : I → A have that

∀h : A → Σ.f; h = ⊤ ⇒ g; h = ⊤

implies

∀h :!A → Σ.γ(f); h = ⊤ ⇒ γ(g); h = ⊤

It should be remarked that the category of CPOs and strict continuous functions as well as the category of dI domains and linear stable functions satisfies Axiom 1.

Proposition F.32 A linear category with a given object Σ and a given map ⊤ : I → Σ satisfies Axiom 1 iff ≲=≲′.

Proof. Proposition F.23, Proposition F.18, and Proposition F.30. □

This proposition enables us to blur the distinction between the intuitionistic intrinsic preorder and the linear intrinsic preorder whenever Axiom 1 is satisfied.

Definition F.33 Let C be a linear category with a linear fixpoint object. For any number n we define a map \underline{n} : I → Z inductively as

\begin{matrix}\underline{0} =⊥_{I,Z} \\ \underline{n + 1} = γ(\underline{n}); σ \end{matrix}

and for any number n we define a map \overline{\underline{n}} :!I → Z inductively as

\begin{matrix}\overline{\underline{0}} = ε_{I}; ∞ \\ \overline{\underline{n + 1}} = γ(\overline{\underline{n}}); σ \end{matrix}

The underlying idea of the following lemma stems from [Fio94], where it is used to show that ∞ is greater that or equal to \underline{n} with respect to the path preorder.

Lemma F.34 Let C be a linear category with a linear fixpoint object. The diagram

I
[figure: ∞]
[figure: !I; γ(Id); \overline{\underline{n}}; Z]
[figure: \underline{n}]
I^{γ(⊥)}

commutes for any number n.

Proof. Induction in n. The case n = 0 is clearly true. Assume the lemma is true for n, then commutativity of

I  \overline{Id ^{}}I
[figure: γ(∞); ∞]
[figure: !I; γ(Id); γ(\overline{\underline{n}}); !Z; σ; Z]
[figure: γ(\underline{n})]
I^{γ(⊥)}

shows that the lemma is true for n + 1. □

Lemma F.35 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 is satisfied. The map ∞ is an upper bound for the increasing chain \{\underline{n}|n ∈ ω\} in C(I, Z) with respect to the intrinsic preorder.

Proof. First note that the chain is increasing because \underline{0} ≲ \underline{1} and monotenicity of γ(−); σ. We have γ(⊥) ≲ γ(Id) because ⊥≲ Id and monotenicity of γ; this entails that \underline{n} ≲ ∞ cf. Lemma F.34. □

Definition F.36 Let C be a linear category with a linear fixpoint operator. Given a map f :!A → A, we define a map f^{n} : I → A inductively as

\begin{matrix}f^{0} =⊥_{I,A} \\ f^{n+1} = γ(f^{n}); f \end{matrix}

Lemma F.37 Let C be a linear category with a linear fixpoint object. Given a map f :!A → A, we have f^{n} = \underline{n}; It(f).

Proof. Induction in n. The case n = 0 is clearly true. Assume the lemma is true for n, then

\underline{n + 1}; It(f) = γ(\underline{n}); σ; It(f)
= γ(\underline{n}); !It(f); f
= γ(\underline{n}; It(f)); f
= γ(f^{n}); f
= f^{n+1}

shows that the lemma is true for n + 1. □

Theorem F.38 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 is satisfied. Given maps f :!A → A and g :!A → B, then γ(f^{♯}); g is an upper bound for the increasing chain {γ(f^{n}); g|n ∈ ω} in C(I, B) with respect to the intrinsic preorder.

Proof. First note that the chain is increasing because f^{n} = \underline{n}; It(f) and the observation that γ((−); It(f)); g is monotone. The same observation makes γ(f^{♯}); g an upper bound because f^{♯} = ∞; It(f). □

Corollary F.39 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 is satisfied. Given maps f :!A → A and g : A → B, then f^{♯}; g is an upper bound for the increasing chain {f^{n}; g|n ∈ ω} in C(I, B) with respect to the intrinsic preorder.

Proof. Immediate from Theorem F.38. □

Definition F.40 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given. Axiom 2 is satisfied iff for any h : Z → Σ with the property that ∞; h = ⊤ there is a number n such that \underline{n}; h = ⊤.

It should be remarked that the category of CPOs and strict continuous functions as well as the category of dI domains and linear stable functions satisfies Axiom 2.

Theorem F.41 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 and Axiom 2 are satisfied. Given maps f :!A → A and g :!A → B, then γ(f^{♯}); g is a least upper bound for the increasing chain {γ(f^{n}); g|n ∈ ω} in C(I, B) with respect to the intrinsic preorder.

Proof. Theorem F.38 shows that γ(f^{♯}); g is an upper bound. Now, let an arbitrary upper bound k : I → B and a map h : B → Σ such that γ(f^{♯}); g; h = ⊤ be given. We have

γ(f^{♯}); g; h = γ(∞); !It(f); g; h
= γ(∞); σ; σ^{−1}; !It(f); g; h  Lambek’s Lemma
= ∞; σ^{−1}; !It(f); g; h

which entails that there is a number n such that \underline{n}; σ^{−1}; !It(f); g; h = ⊤ cf. Axiom 2. The case n = 0 is precluded by the assumption that ⊤ ≠ ε_{Σ}^{♯} and Proposition F.26, so we can assume that n > 0. We then have

\begin{aligned}\underline{n}; σ^{−1}; !It(f); g; h & = & γ(\underline{n − 1}); σ; σ^{−1}; !It(f); g; h \\ & = & γ(f^{n−1}); g; h \end{aligned}

so k; h = ⊤ because γ(f^{n−1}); g ≲ k. We conclude that γ(f^{♯}); g ≲ k. □

Corollary F.42 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 and Axiom 2 are satisfied. Given maps f :!A → A and g : A → B, then f^{♯}; g is a least upper bound for the increasing chain {f^{n}; g|n ∈ ω} in C(I, B) with respect to the intrinsic preorder.

Proof. Immediate from Theorem F.41. □

Definition F.43 Let C be a linear category with a linear fixpoint operator. Given a map f :!A⊗!B → B, we define a map f^{n} :!A → B inductively as

\begin{matrix}f^{0} =⊥_{!A,B} \\ f^{n+1} = d; (Id ⊗ γ(f^{n})); f \end{matrix}

Theorem F.44 Let C be a linear category with a linear fixpoint object. Assume that an object Σ and a map ⊤ : I → Σ is given such that ⊤ ≠ ε_{Σ}^{♯}. Assume Axiom 1 and Axiom 2 are satisfied. Given maps f :!A⊗!B → B, g :!C → A and h :!B → D, then γ(g); γ(f^{♯}); h is a least upper bound for the increasing chain {γ(g); γ(f^{n}); h|n ∈ ω} in C(!C, D) with respect to the intrinsic preorder.

Proof. Follows from Theorem F.41.

□

Now, the preorder-enrichment on C induces a preorder-enrichment on the coKleisli category, and it is straightforward to check that Theorem F.44 entails that the quotient of coKleisli category with respect to the preorder is rational.

G Appendix, Remarks on Recursion at the Level of Types

The λ-calculus can be extended with recursion at the level of types, that is, we have additional types X | μX.s, where X is a variable that ranges over types, additional terms

abs(t) | rep(t)

and the following typing rules in natural deduction style

Γ ⊢ t : A[μX.A/X] ; (μ_{I}) ; Γ ⊢ abs(t) : μX.A  Γ ⊢ t : μX.A ; (μ_{E}) ; Γ ⊢ rep(t) : A[μX.A/X]

The above mentioned terms and typing rules can also be found in [Win93]. The usual reduction rules for terms of the λ-calculus can be extended with a reduction rule for the term corresponding to recursion at the level of types:

rep(abs(t)) ⇝ t

We are then able to define recursion at the level of terms in the λ^{rec}-calculus, as given in the present paper. Given a derivation

Γ, z : B ⊢ u : B

we let C be an abbreviation for the type μX.(X ⇒ B), and

Γ ⊢ α : C

an abbreviation for the derivation

{Γ, z : B ⊢ u : B \atop Γ ⊢ λz.u : B ⇒ B}  \begin{matrix}\begin{matrix}x : C ⊢ x : C \\ x : C ⊢ rep(x) : C ⇒ B \end{matrix} & x : C ⊢ x : C \\ x : C ⊢ rep(x)x : B \end{matrix}
∗
Γ, x : C ⊢ (λz.u)(rep(x)x) : B
Γ ⊢ λx.((λz.u)(rep(x)x)) : C ⇒ B
Γ ⊢ abs(λx.((λz.u)(rep(x)x))) : C

* We have here used a multiplicative version of the (⇒_{E}) rule, which is admissible in the λ-calculus. We define

Γ ⊢ recz.u : B

to be an abbreviation for the derivation

{Γ ⊢ α : C \atop Γ ⊢ rep(α) : C ⇒ B} Γ ⊢ α : C

Γ ⊢ rep(α)α : B

and we get the reduction rule for recursion at the level of terms in the λ^{rec}-calculus as follows:

recz.u = rep(α)α
= rep(abs(λx.((λz.u)(rep(x)x))))α
⇝ (λx.((λz.u)(rep(x)x)))α
⇝ (λz.u)(rep(α)α)
⇝ u[(rep(α)α)/z]
= u[recz.u/z]

by using a lazy reduction strategy. This is essentially a syntactic restatement of a result in [Law69] saying that if f : C → C ⇒ B is a weakly point-surjective map in a cartesian closed category, then every endomap on B has a fixpoint.

Now, we want to have recursion at the level of types in the linear λ-calculus. Certain models of ILL have the property that they admit solution of recursive domain equations corresponding to type constructs. The category of CPOs ond strict continuous functions, and the category of dI domains and join preserving stable functions both have that property. Another example is the category of games given in [AM94]. The fact that one can solve recursive domain equations corresponding to type constructs in such models, suggests that we should take recursion at the level of types in the linear λ-calculus to have the same typing and reduction rules as in the λ-calculus case. Note that recursion at the level of types takes place in the full ILL, and not only in the IL fragment of ILL, as it is the case with recursion at the level of terms. The Girard Translation still works when IL and ILL both are extended with recursion at the level of types, and moreover, the translation preserves the reduction rule for recursion.

We are able to define recursion at the level of terms in the linear λ^{rec}-calculus, as given in the present paper, when we take recursion at the level of types to have the same typing and reduction rules as in the λ-calculus case. Given a derivation

\overline{x :!A}, z :!B − u : B

where \overline{x :!A} is an abbreviation for x_{1} :!A_{1}, ..., x_{n} :!A_{n}, we let C be an abbreviation for the type μX.(!X ⊸ B), and

\overline{x :!A} − α : C

an abbreviation for the derivation

\overline{x :!A}, z :!B − u : B \overline{x :!A} − λz.u :!B ⊸ B

x :!C − x :!C
x :!C − derelict(x) : C
x :!C − rep(derelict(x)) :!C ⊸ B

y :!C − y :!C
x :!C, y :!C − rep(derelict(x))y : B
x′ :!C − copy x′ as x, y in (rep(derelict(x))y) : B
x′′ :!C − let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y)) :!B
\overline{x :!A}, x′′ :!C − (λz.u)let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y)) : B
\overline{x :!A} − λx′′.((λz.u)let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y))) :!C ⊸ B
\overline{x :!A} − abs(λx′′.((λz.u)let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y)))) : C

Now, we define

\overline{y′′ :!A} − let \overline{y′′} be \overline{x} in recz.u : B

to be an abbreviation for the derivation

{\overline{x :!A} − α : C \atop \overline{x :!A} − rep(α) :!C ⊸ B}  {\overline{x :!A} − α : C \atop \overline{y′ :!A} − let \overline{y′} be \overline{x} in !α :!C}
\overline{x :!A}, \overline{y′ :!A} − rep(α)let \overline{y′} be \overline{x} in !α : B
\overline{y′′ :!A} − copy \overline{y′′} as \overline{x}, \overline{y′} in (rep(α)let \overline{y′} be \overline{x} in !α) : B

and we have

rep(α)let \overline{y′} be \overline{x} in !α = rep(abs(λx′′.((λz.u)let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y)))))let \overline{y′} be \overline{x} in !α = (λx′′.((λz.u)let x′′ be x′ in !(copy x′ as x, y in (rep(derelict(x))y))))let \overline{y′} be \overline{x} in !α ⇝ (λz.u)let (let \overline{y′} be \overline{x} in !α) be x′ in !(copy x′ as x, y in (rep(derelict(x))y)) ⇝ (λz.u)let \overline{y′} be \overline{y′′} in !(copy (let \overline{y′′} be \overline{x} in !α) as x, y in (rep(derelict(x))y)) ⇝ (λz.u)let \overline{y′} be \overline{y′′} in !(copy \overline{y′′} as \overline{x}, \overline{y′} in (rep(derelict(let \overline{x} be \overline{x} in !α))let \overline{y′} be \overline{x} in !α)) ⇝ (λz.u)let \overline{y′} be \overline{y′′} in !(copy \overline{y′′} as \overline{x}, \overline{y′} in (rep(α)let \overline{y′} be \overline{x} in !α)) ⇝ u[let \overline{y′} be \overline{y′′} in !(copy \overline{y′′} as \overline{x}, \overline{y′} in (rep(α)let \overline{y′} be \overline{x} in !α))/z]

which entails that we get the reduction rule for recursion at the level of terms in the linear λ^{rec}-calculus:

let \overline{y′′} be \overline{x} in recz.u ⇝ copy \overline{y′′} as \overline{x}, \overline{y′} in (u[let \overline{y′} be \overline{y′′} in !(let \overline{y′′} be \overline{x} in recz.u)/z])

One might note that if we extend the !-free fragment of the linear λ-calculus with the above mentioned typing and reduction rules for recursion, then we get a system which is strongly normalising because the underlying proof of a term shrinks during each reduction step (so reduction will actually be linear in the size of the underlying proof).

Recent Publications in the BRICS Report Series

RS-95-13 Torben Bra� uner. The Girard Translation Extended with Recursion. February 1995. 79 pp. Full version of paper to appear in Proceedings of CSL ’94, LNCS 933, 1995.

RS-95-12 Gerth St�lting Brodal. Fast Meldable Priority Queues. February 1995. 12 pp.

RS-95-11 Alberto Apostolico and Dany Breslauer. An Optimal O(log log n) Time Parallel Algorithm for Detecting all Squares in a String. February 1995. 18 pp. To appear in SIAM Journal on Computing.

RS-95-10 Dany Breslauer and Devdatt P. Dubhashi. Transforming Comparison Model Lower Bounds to the Parallel-Random-Access-Machine. February 1995. 11 pp.

RS-95-9 Lars R. Knudsen. Partial and Higher Order Differentials and Applications to the DES. February 1995. 24 pp.

RS-95-8 Ole I. Hougaard, Michael I. Schwartzbach, and Hosein Askari. Type Inference of Turbo Pascal. February 1995. 19 pp.

RS-95-7 David A. Basin and Nils Klarlund. Hardware Veri�cation using Monadic Second-Order Logic. January 1995. 13 pp.

RS-95-6 Igor Walukiewicz. A Complete Deductive System for the μ-Calculus. January 1995. 39 pp.

RS-95-5 Luca Aceto and Anna Ing� olfsd� ottir. A Complete Equational Axiomatization for Pre�x Iteration with Silent Steps. January 1995. 27 pp.

RS-95-4 Mogens Nielsen and Glynn Winskel. Petri Nets and Bisimulations. January 1995. 36 pp. To appear in TCS.

RS-95-3 Anna Ing� olfsd� ottir. A Semantic Theory for Value�Passing Processes, Late Approach, Part I: A Denotational Model and Its Complete Axiomatization. January 1995. 37 pp.

RS-95-2 Franc�ois Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. January 1995. 21 pp.