Theory and Applications of Categories, Vol. 17, No. 3, 2006, pp. 30–48.

A PARIGOT-STYLE LINEAR λ-CALCULUS FOR FULL INTUITIONISTIC LINEAR LOGIC

VALERIA DE PAIVA AND EIKE RITTER

Abstract. This paper describes a natural deduction formulation for Full Intuitionistic Linear Logic (FILL), an intriguing variation of multiplicative linear logic, due to Hyland and de Paiva. The system FILL resembles intuitionistic logic, in that all its connectives are independent, but resembles classical logic in that its sequent-calculus formulation has intrinsic multiple conclusions. From the intrinsic multiple conclusions comes the inspiration to modify Parigot’s natural deduction systems for classical logic, to produce a natural deduction formulation and a term assignment system for FILL.

1. Introduction

This paper describes a natural deduction formulation for Full Intuitionistic Linear Logic (FILL), a variant of Linear Logic, first described by Hyland and de Paiva [HdP93]. The system FILL has all the multiplicative connectives of classical linear logic [Gir95], but it is not involutive: the double-negation A^{⊥⊥} is not the same as A, as is the case in classical linear logic. The system FILL has arisen from its categorical model, the Dialectica construction [dP89], which can be seen as a variant of the Chu construction [Bar96].

Weakly distributive categories [CS97] with a right adjoint to the tensor product but without negation provide another sound and complete model for FILL. Furthermore, for every weakly distributive category modelling FILL one can identify a *-autonomous subcategory which models classical linear logic. This subcategory corresponds to all objects for which ¬¬A and A are isomorphic. This shows that FILL can be seen as classical linear logic without involutive negation.

A sequent-style calculus for FILL has been presented in [BdP98]. Our natural deduction formulation of FILL is based on Pym and Ritter’s extension [RP01] of Parigot’s λμ natural deduction system [Par92] for (propositional) classical logic. Their extension, called λμν, was used to provide a term calculus for a multiplicative version of disjunction in classical logic. We provide a term-calculus for FILL based on λμν, which we call FILL_{μ} and prove its basic proof-theoretical properties.

A PARIGOT-STYLE LINEAR λ-CALCULUS FOR FULL INTUITIONISTIC LINEAR LOGIC 31

We first recall the system FILL, in its sequent-style formulation due to Braüner and de Paiva [BdP98]. Then we recap the main ideas of Parigot’s system λμ, as well as Pym and Ritter’s extension λμν. In the next section we introduce our natural deduction term calculus for FILL, based on λμ, called FILL_{μ} and prove its main proof theoretical properties. Finally we show that the relationship between FILL_{μ} and FILL is as expected: all derivations of the sequent calculus FILL can be seen as terms of the FILL_{μ} calculus. Conversely all decorations can be removed from FILL_{μ}-terms to yield sequent-calculus FILL derivations.

Received by the editors 2003-10-31 and, in revised form, 2005-02-28.

Published on 2006-12-16 in the volume Chu spaces: theory and applications.

2000 Mathematics Subject Classification: 03B20.

Key words and phrases: linear logic, λμ-calculus, Curry-Howard isomorphism.

\begin{matrix}c \\ ◯ \end{matrix} Valeria de Paiva and Eike Ritter, 2006. Permission to copy for private use granted.

2. The system FILL

The system FILL is a variant of (multiplicative) linear logic proposed in [HdP93] whose logical connectives are all independent, that is, they are not interderivable, as they are in (multiplicative) classical linear logic. The relationship between FILL and classical linear logic is somewhat analogous to the relationship between intuitionistic logic and classical logic. In classical logic all the connectives can be expressed in terms of implication and negation, whereas in intuitionistic logic, conjunction, disjunction and implication are all independent connectives. Only negation is defined in terms of implication and the constant ⊥ for falsum. In FILL the linear negation A^{⊥} is defined as A−∘⊥ and it is not an involution, thus A ⊢ A^{⊥⊥} but not vice-versa, as is the case in classical linear logic.

Hyland and de Paiva only deal with the multiplicative fragment of FILL. We will do the same here, but following the dependency-style formulation of Braüner and de Paiva [BdP98]. Formulae of FILL are defined by the grammar:

S ::= S ⊗ S | I | S⅋S | ⊥ | S−∘S

The sequent calculus rules for FILL are as follows, where the asterisk ∗ in the implication right rule indicates the side-condition that A does not depend on any formula in Δ (see below).

A ⊢ A

Γ, A, B ⊢ Δ ; ⊗_{L} ; Γ, A ⊗ B ⊢ Δ Γ ⊢ A, Δ Γ′ ⊢ B, Δ′

⊗_{R}
Γ, Γ′ ⊢ A ⊗ B, Δ, Δ′
Γ ⊢ Δ ; I_{L} ; Γ, I ⊢ Δ  \begin{aligned}& I_{R} \\ ⊢ I \end{aligned}

Γ, A ⊢ Δ Γ′, B ⊢ Δ′
⅋_{L}

Γ, Γ′, A⅋B ⊢ Δ, Δ′

Γ ⊢ A, B, Δ ; ⅋_{R} ; Γ ⊢ A⅋B, Δ

\begin{aligned}& ⊥_{L} \\ ⊥ ⊢ \end{aligned}  Γ ⊢ Δ ; ⊥_{R} ; Γ ⊢ ⊥, Δ

Γ ⊢ A, Δ Γ′, B ⊢ Δ′ −∘_{L}

Γ, Γ′, A−∘B ⊢ Δ, Δ′

\begin{matrix}Γ, A ⊢ B, Δ \\ −∘ & R & * \\ Γ ⊢ A−∘B, Δ \end{matrix}

To explain the side-condition on the implication right rule, we need a notion of dependency, relating formulae occurrences. Basically we must define, given a proof of a sequent Γ, B ⊢ A, Δ, in classical linear logic when the succedent formula occurrence A depends on the antecedent formula occurrence B. This notion of dependency between formulae occurrences in the sequent, when properly defined, allows us to express the constructive property that characterizes FILL. Intuitively we can say that “genuine” dependencies start in axioms, constants do not introduce dependencies and dependencies “percolate” through a proof as expected. The formal definition of the set of dependencies Dep_{τ}(A) in a proof [BdP98] is recalled in the appendix.

Summing up: the implication right rule in classical linear logic (like the one in classical logic) allows any (linear) implications whatsoever. The implication right rule in intuitionistic linear logic enforces the existence of a single conclusion on the sequent. The implication right rule for FILL is more liberal than a single formula in the consequent, but more restricted than the classical linear logic rule.

3. The system λμν

The λμ-calculus was introduced by Parigot [Par92] and extended to deal with multiplicative disjunction by Pym and Ritter [RPW00a, RPW00b]. In this section, we briefly recap both λμ and Pym and Ritter’s extension λμν.

The original λμ-calculus provides a term calculus for the implicational fragment of classical propositional natural deduction: i.e., realizers for a calculus in which multiple conclusioned sequents can be derived. The typing judgements in the λμ-calculus are of the form Γ ⊢ t: A , Δ, where Γ is a context familiar from the typed λ-calculus and Δ is a context containing types indexed by names, α, β, …, distinct from variables. These types are written as A^{α}, etc.. The relationship of this typing judgement with classical logic, the “propositions-as-types correspondence”, is simply stated as follows: there is a term t such that the judgement

x_{1}: A_{1}, …, x_{m}: A_{m} ⊢ t: A, B_{1}^{β_{1}}, …, B_{n}^{β_{n}}

is provable in the λμ-calculus if and only if

A_{1} ∧ … ∧ A_{m} ∧ ¬B_{1} ∧ … ∧ ¬B_{n} → A

is a classical propositional tautology.

The intuition for this term calculus is that each λμ-sequent has exactly one active, or principal, formula, A, on the right-hand side, i.e., the leftmost one, which is the formula upon which all introduction and elimination rules operate. This formula is the type of the term t. The basic grammar of λμ terms is as follows:

t ::= x | λx: A . t | tt | [α]t | μα . t.

The corresponding inference rules of the λμ-calculus are given below.

Γ, x: A ⊢ x: A, Δ Ax
\begin{matrix}Γ, x: A ⊢ t: B, Δ \\ Γ ⊢ λx: A.t: A → B, Δ \end{matrix} → I \begin{matrix}Γ ⊢ t: A → B, Δ Γ ⊢ s: A, Δ \\ Γ ⊢ ts: B, Δ \end{matrix} → E
\begin{matrix}Γ ⊢ t: A, Δ \\ Γ ⊢ [α]t: ⊥, A^{α}, Δ \end{matrix} freeze  \begin{matrix}Γ ⊢ t: ⊥, A^{α}, Δ \\ Γ ⊢ μα.t: A, Δ \end{matrix} unfreeze

In the rules freeze and unfreeze the type-name pair A^{α} may already be contained in Δ. If it is, the rule freeze models contraction and the rule unfreeze models weakening on the right hand side of the sequent. A context Γ is a set of pairs x: A, where x is a variable and A is a type, and a context Δ is a set of pairs A^{α}, where A is a type and α a name. We require that no name and no variable occurs twice in any given context.

The term [α]t realizes the introduction of a name. The term μα.[β]t realizes the exchange operation:

\frac{Γ ⊢ t: B, A^{α}, Δ}{Γ ⊢ μα.[β]t: A, B^{β}, Δ} Exchange

i.e., if A^{α} was part of “side-context” of the succedent before the exchange, then A is the principal formula of the succedent after the exchange. Taken together, these terms also provide a notation for the realizers of contractions and weakenings on the right of a multiple-conclusioned calculus. It is easy to detect whether a formula B^{β} in the righthand side of the sequent is, in fact, superfluous, i.e., there is a derivation of Γ ⊢ t: A, Δ′ where Δ′ does not contain B. The formula B is superfluous if β is not a free name in t. The negation of a formula A is modelled in the λμ-calculus as A → ⊥, and the two rules for ⊥ express the fact that ⊥ can be added and removed to the succedent at any time.

Pym and Ritter’s variation on λμ presented below has two aspects. Firstly, in addition to implicational types, they include both conjunctive (product) and disjunctive (disjoint sum) types. The addition of the conjunctive types follows the standard method for adding products to the simply-typed λ-calculus and is omitted. The addition of disjunctive types requires a more subtle approach. The key point in the addition of disjunctive types is naturally explained in the setting of the multiple-conclusioned sequent calculus. Their formulation, based on that found in Gentzen’s classical sequent calculus LK [Gen34] and also in Dummett’s multiple-conclusioned intuitionistic sequent calculus [Dum80] exploits the presence of multiple conclusions via the introduction rule for disjunctions.

\frac{Γ ⊢ A_{1}, A_{2}, Δ}{Γ ⊢ A_{1} ∨ A_{2}, Δ}.

For the λμ-calculus, the latter formulation presents a new difficulty. Suppose the λμ-sequent

Γ ⊢ t: A, B^{β}, Δ

is to be the premiss of the ∨I rule. In forming the disjunctive active formula A ∨ B, we move the named formula B^{β} from the context to the active position. Consequently, ∨I is formulated as a binding operation and we introduce the following additional constructs, to form the grammar of λμν-terms:

t ::= ⟨β⟩t | νβ . t.

The term νβ . t introduces a disjunction and the term ⟨β⟩t eliminates one. The associated inference rules are given by

\begin{matrix}Γ ⊢ t: A, B^{β}, Δ \\ Γ ⊢ νβ.t: A ∨ B, Δ \end{matrix} ∨ I \begin{matrix}Γ ⊢ t: A ∨ B, Δ \\ Γ ⊢ ⟨β⟩t: A, B^{β}, Δ \end{matrix} ∨ E

The definition of the reduction rules requires not only the standard substitution t[s/x], but also a substitution for names t[s/[α]u], which intuitively indicates the term t with all occurrences of a subterm of the form [α]u replaced by s.

Parigot gives only reduction rules for β-reduction. Pym and Ritter also provide ηrules as expansions, meaning that each term of functional type is transformed into a λ-abstraction, each term of product type into a pair and each term of sum type into a term νβ.t′. These η-rules generate critical pairs which give rise to additional reduction rules. All the reduction rules are collected in the appendix.

The system described by Pym and Ritter satisfy two key properties of reduction systems: namely confluence and strong normalization. Local confluence is the property that any two one-step reducts of a term have a common reduct and confluence is the property that any two reducts of a term have a common reduct. Normalization is the property that any term has a terminating reduction sequence and strong normalization is the property that all reduction sequences for any given term terminate. Both local confluence and strong normalization were proved by Pym and Ritter in the paper cited.

4. A natural deduction system for FILL

We use the λμ-calculus as a blueprint to provide a natural deduction version for FILL, which we call FILL_{μ}. Since the λμ-calculus calculus was originally developed for classical logic, we need a modification to be able to use it for FILL. FILL arises from classical linear logic via a restriction, that is similar to the one turning intuitionistic logic into a subsystem of classical logic, discussed in [RPW00a]. The main difference between classical and intuitionistic (propositional) systems is the implication right rule, where the intuitionistic restriction is that the right-hand side consists of a single formula and the classical rule has no restrictions. Hence a classical derivation is intuitionistic if for all instances of the implication right rule all side formulae on the right-hand side of the sequent arise by weakening. In Pym and Ritter [RPW00a] a syntactic criterion for a λμ-term to satisfy this condition is given. They define a notion of weakening occurrence of a λμ-name, with the intention that if a name has got only weakening occurrences in a term, the corresponding formula in the right-hand side arises by weakening. For FILL_{μ} we have to capture dependencies rather than terms which arise by weakening or not. Hence we decorate types with the list of variables which they depend on and restate the linear implication right rule accordingly.

As a consequence FILL_{μ} has judgements of the form

Γ ⊢ M: A^{σ}, α_{1}: A_{1}^{σ_{1}}, …, α_{n}: A_{n}^{σ_{n}}

where σ, σ_{1}, … stand for decorations on types and α … for names. As we need to keep track of how dependencies are propagated, the decorations are not only variables but are given by the grammar

σ ::= x | λx.σ | σσ | σ⊗σ | Fst(σ) | Snd(σ) | σ⅋σ | l(σ) | r(σ) | nodep

We have the following reduction relation on decorations:

\begin{matrix}(λx.τ)σ & ⇝ & τ[σ/x] \\ Fst(σ⊗τ) & ⇝ & σ \\ Snd(σ⊗τ) & ⇝ & τ \\ l(σ⅋τ) & ⇝ & σ \\ r(σ⅋τ) & ⇝ & τ \end{matrix}

Decorations can be seen as terms in a suitable simply-typed λ-calculus. Hence there exists a unique normal form for decorations. ¿From now on, we assume that all decorations are in normal form.

The typing judgements of FILL_{μ} are the following ones:

x: A ⊢ x: A^{x}
\begin{matrix}Γ, x: A ⊢ M: B^{τ}, Δ \\ Γ ⊢ λx: A.M: (A−∘B)^{λx.τ}, Δ \end{matrix} x ∉ NF (Δ)

\begin{matrix}Γ_{1} ⊢ M_{1}: (A−∘B)^{σ} Γ_{2} ⊢ M_{2}: B^{τ}, Δ_{1} \\ Γ_{1}, Γ_{2} ⊢ MN: B^{στ}, Δ_{1}, Δ_{2} \end{matrix}

Γ_{1} ⊢ M_{1}: A^{σ}, Δ_{1} Γ_{2} ⊢ M_{2}: B^{τ}, Δ_{2} Γ_{1}, Γ_{2} ⊢ M⊗N: (A⊗B)^{σ⊗τ}, Δ_{1}, Δ_{2}

Γ_{1} ⊢ M_{1}: A⊗B^{σ}, Δ_{1} Γ_{2}, x: A, y: B ⊢ M_{2}: C^{τ}, Δ_{2} Γ_{1}, Γ_{2} ⊢ let M be x⊗y in N: (C, Δ_{2})^{[Fst(σ)/x,Snd(σ)/y]}, Δ_{1}

                            ⊢ ∗: I^{nodep}

Γ_{1} ⊢ M: I^{σ}, Δ_{1} Γ_{2} ⊢ N: A^{σ}, Δ_{2} Γ_{1}, Γ_{2} ⊢ let M be ∗ in N: A^{σ}, Δ_{1}, Δ_{2}

\begin{matrix}Γ_{1} ⊢ M: A^{σ}, α: B^{τ}, Δ \\ Γ ⊢ να.M: (A⅋B)^{σ⅋τ}, Δ \end{matrix}

\begin{matrix}Γ ⊢ M: (A⅋B)^{σ}, Δ \\ Γ ⊢ ⟨α⟩M: A^{l(σ)}, α: B^{r(σ)}, Δ \end{matrix} α ∉ Δ

Γ ⊢ M: A^{σ}, Δ Γ ⊢ [α]M: ⊥^{nodep}, α: A^{σ}, Δ

\begin{matrix}Γ ⊢ M: ⊥^{σ}, α: A^{τ}, Δ \\ Γ ⊢ μα.M: A^{τ}, Δ: \end{matrix}

The important restriction in the typing rules is the side condition x ∉ NF (Δ) in the linear implication right rule, meaning that the variable x does not appear in the decorations of Δ. This condition captures the essence of FILL: the formulae in Δ do not depend on the formula A.

The definition of the reduction rules requires not only the standard substitution t[s/x], but also a substitution for names t[s/[α]u], which intuitively indicates the term t with all occurrences of a subterm of the form [α]u replaced by s. To define this notion, we need the notion of a term with holes. Such a term C with holes of type A is a FILL_{μ}-term which may have also the additional term constructor with the rule Γ ⊢ : A, Δ. The term C(u) denotes the term C with the holes textually (with possible variable capture) replaced by u. Then we define t[C(u)/[α]u], where α is a name and u is a metavariable, by

\begin{aligned}x[C(u)/[α]u] & = & x \\ ([α]t)[C(u)/[α]u] & = & C(t[C(u)/[α]u]) \\ (⟨α⟩t)[[C(u)/[α]u]] & = & μγ.C(μα.[γ]⟨α⟩t[C(u)/[α]u]) \end{aligned}

and define t[C(u)/[α]u] on all other expressions t by pushing the replacement inside.

We need the usual substitution lemma for the FILL_{μ}-calculus. As we have not only substitution for variables, but also for names, we obtain several cases for the lemma, in the same way as in the λμν-calculus.

4.1. Lemma.

(i) Assume Γ_{1}, x: A ⊢ M: B, Δ_{1} and Γ_{2} ⊢ N: A^{σ}, Δ_{2}. Then we have also Γ_{1}, Γ_{2} ⊢ M[N/x]: (B, Δ_{1}, Δ_{2})[σ/x].

(ii) Assume Γ_{1} ⊢ M: A, α: (B−∘C)^{σ}, Δ_{1} and Γ_{2} ⊢ N: B^{τ}, Δ_{2}. Then we have also Γ_{1}, Γ_{2} ⊢ M[[β]RN/[α]R]: A, β: C^{στ}, Δ_{1}, Δ_{2}).

(iii) Assume Γ_{1} ⊢ μα.M: (A⊗B)^{σ}, Δ_{1} and

Γ_{2}, x: A, y: B ⊢ N: (C, Δ_{2})[Fst(σ)/x, Snd(σ)/y] .

Then also Γ_{1}, Γ_{2} ⊢ μβ.M[[β]let R be x⊗y in N/[α]R]: C, Δ_{1}, Δ_{2}.

(iv) Assume Γ ⊢ M: A, α: (B⅋C)^{σ}, Δ_{1}. Then we have also

Γ ⊢ M[[β]⟨γ⟩N/[α]N]: A, β: B^{l(σ)}, γ: C^{r(σ)}, Δ .

Proof. Induction over the structure of M.

We have the following reduction rules in addition to the standard β-reduction rules:

(μα.M)N ⇝ M[[β]UN/[α]U]
⟨β⟩μα.M ⇝ M[[γ]⟨β⟩N/[α]N]
(let M be x⊗y in N)R ⇝ let M be x⊗y in NR
⟨α⟩(let M be x⊗y in N) ⇝ let M be x⊗y in ⟨α⟩N
letlet M_{1} be x_{1}⊗y_{1} in N_{1} be x_{2}⊗y_{2} in N_{2} ⇝ let M_{1} be x_{1}⊗y_{1}

                                             inlet N_{1} be x_{2}⊗y_{2} in N_{2}

μα.let M be x⊗y in N ⇝ let M be x⊗y in μα.N
if α ∉ F N(M)

These rules correspond to commuting conversions in the sequent calculus which are necessary to obtain cut-elimination. We will call these rules ζ-rules, and we will use the term βζ-reduction for a β-or a ζ-reduction.

Now we can show the property usually called subject reduction.

4.2. Proposition. Assume M is a FILL_{μ}-term, and M ⇝ N. Then N is also a FILL_{μ}- term.

Proof. Consider each reduction in turn. All β-rules are done via the appropriate substitution lemma.

Now we turn to the proof that FILL_{μ} with the βζ-reductions is strongly normalising and confluent. The strong normalisation and confluence of λμ-calculus is instrumental in this proof, as is the subject reduction for FILL_{μ}.

4.3. Theorem. The calculus FILL_{μ} with βζ-reductions is strongly normalising and confluent.

Proof. We start by showing strong normalisation. Firstly, we define an embedding of FILL_{μ} into the λμν-calculus by replacing a tensor term M⊗N with the product term ⟨M, N⟩ and the term let M be x⊗y in N with the substitution N[π(M)/x, π′(M)/y]. This embedding only creates more β-redexes, and two terms which are equal modulo ζredexes are mapped to equal λμν-terms. Hence any infinite sequence of βζ-reductions contains only a finite number of β-reductions, and there is a term M such that all further reductions are ζ-reductions. Secondly, we define a weight of a syntax tree by assigning 2 to all nodes except a let-node, which is assigned the weight 1. The weight of a tree where the left-hand side has weight w_{1}, the right-hand side has weight w_{2} and the node has weight w, is w + 2w_{1} + w_{2}. It is now easy to see that the weight of the left-hand side of any ζ-rule is bigger than the weight of the right-hand side. The fact that the weight of the left-hand side is higher than the weight of the right-hand side ensures that the left-hand side of rules which push let-constructors from the left-hand side of the syntax tree to the right-hand side of the syntax tree has a higher weight than the right-hand side of such a rule. The lower weight of the let-constructors ensures that also the left-hand side of rules which push let-constructors down the syntax tree has a higher weight than the right-hand side. Hence there is no infinite sequence of ζ-reductions. Hence there is also no infinite sequence of βζ-reductions.

Now we turn to confluence. Local confluence can be shown by considering all critical pairs, and strong normalization then implies confluence.

5. Relating FILL and FILL_{μ}

Next we show that FILL_{μ} proves exactly the same theorems as FILL. For this, we show how to translate FILL_{μ}-derivations to λμ-calculus-terms. We do this by induction over the structure of FILL_{μ}-derivations. Note that as FILL is given by a sequent calculus, this translation does a translation from a sequent calculus into natural deduction as well.

In the translation below the decorations are ignored. The reason is that they are not necessary for the definition of the translation but only to ensure that the result of the translation of a FILL-derivation is a FILL_{μ}-term.

We shall use the following notation: if ϕ is a derivation whose last rule is R applied to the derivations ϕ_{1}, …, ϕ_{n}, we write (ϕ_{1}, …, ϕ_{n}); R for ϕ.

5.1. Definition. Let ϕ: Γ ⊢ A, Δ be a FILL sequent derivation and suppose that each occurrence of a formula in Γ and Δ has a label, i.e., the contexts Γ and Δ satisfy Γ = x_{1}: A_{1}, …, x_{n}: A_{n} and Δ = B_{1}^{β_{1}}, …, B_{m}^{β^{m}}. (These labels turn into variables and names in the FILL_{μ}-calculus, hence we also use them for the derivations.) We define a FILL_{μ}-term ϕ^{fl} satisfying Γ ⊢ ϕ^{fl}: A, Δ by induction over the structure of ϕ as follows (note the clause for the exchange rule):

Axiom: Suppose ϕ : x: A ⊢ A, Δ is an axiom, then ϕ^{fl} =^{def} x;

Exchange: Suppose ϕ: Γ ⊢ A, B^{β}, Δ, and

ϕ′ = ϕ; exc: Γ ⊢ B, A^{α}, Δ.

We define ϕ^{′fl} to be μβ.[α]ϕ^{fl}, where α is a name which does not occur freely in ϕ^{fl};

⊗L: Suppose we have the derivation

ϕ: Γ, x: A, y: B ⊢ A, Δ
⊗L,
ϕ; ⊗L: Γ, z: A⊗B ⊢ A, Δ

then the corresponding λμ-term is

ϕ; ⊗L^{fl} =^{def} let x⊗y be z in ϕ^{fl};

⊗R: Suppose we have the derivation

ϕ: Γ_{1} ⊢ A, Δ_{1} ψ: Γ_{2} ⊢ B, Δ_{2}
⊗R,
(ϕ, ψ); R: Γ_{1}, Γ_{2} ⊢ A⊗B, Δ_{1}, Δ_{2}

then we define

(ϕ, ψ); ⊗R^{fl} =^{def} ϕ^{fl}⊗ψ^{fl};

I L: Suppose we have the derivation

Γ ⊢ Δ ; I L ; Γ, I ⊢ Δ

then we define

ϕ; I L^{fl} =^{def} let x be ∗ in ϕ^{fl} ;

I R: Suppose we have the derivation

\begin{aligned}& I R \\ ⊢ I \end{aligned}

then we define

I R^{fl} =^{def} ∗ ;

−∘L: Suppose we have the derivation

ϕ: Γ_{1} ⊢ A, Δ_{1} ψ: Γ_{2}, w: B ⊢ C, Δ_{2}

−∘L

(ϕ, ψ); −∘L: Γ_{1}, Γ_{2}, x: A−∘B ⊢ C, Δ_{1}, Δ_{2}

then we define (ϕ, ψ); −∘L^{fl} to be ψ^{fl}[xϕ^{fl}/w];

−∘R: Suppose we have the derivation

ϕ: Γ, x: A ⊢ B, Δ

−∘R

ϕ; −∘R: Γ ⊢ A−∘B, Δ

then we define [[ϕ; −∘R]] to be λx: A.[[ϕ]];

⅋R: Assume we have a derivation

{ϕ: Γ ⊢ A, B^{β}, Δ \atop ϕ; ⅋R: Γ ⊢ A⅋B, Δ}

then we define ϕ; ⅋R^{fl} = νβ.[[ϕ]];

⅋L: Assume we have a derivation

ϕ_{1}: Γ_{1}, x: A ⊢ Δ_{1} ϕ_{2}: Γ_{2}, y: B ⊢ Δ_{2}
⅋L
(ϕ_{1}, ϕ_{2}); ⅋L: Γ_{1}, z: A⅋B ⊢ Δ_{1}, Δ_{2}
Then (ϕ_{1}, ϕ_{2}; ⅋L)^{fl} is the FILL_{μ}-term
ϕ_{1}^{fl}[μα.[γ][μβ.[α]⟨β⟩z/y]/x] ;

⊥L: Suppose we have the derivation

\begin{aligned}& ⊥ L \\ ⊥ ⊢ \end{aligned}

then we define

⊥ L^{fl} =^{def} μα.x ;

⊥R: Suppose we have the derivation

Γ ⊢ Δ ; ⊥ R ; Γ ⊢ ⊥, Δ

then we define

ϕ; ⊥R^{fl} =^{def} [α]ϕ^{fl} .

So far we have not used the decorations at all, neither for FILL nor for FILL_{μ}. They are important when we show that the translation of a FILL-derivation is a FILL_{μ}-term. In particular, the restriction of the −∘R-rule is captured by the side condition of the rule for λ-abstraction of FILL_{μ}.

5.2. Theorem. Assume ϕ: Γ ⊢ Δ is a FILL-derivation. Then ϕ^{fl} is a FILL_{μ}-term.

Proof. Induction over the derivation.

As an example for a FILL-derivation which is not an intuitionistic derivation consider the derivation

u: A ⊢ A^{u} v: B ⊢ B^{v} ; ⅋L ; z: A⅋B ⊢ A^{l(z)}, B^{r(z)} x: C ⊢ C^{x}

⊗R

z: A⅋B, x: C ⊢ (A⊗C)^{l(z)⊗x}, B^{r(z)}

⊢ R

z: A⅋B ⊢ (C−∘(A⊗C))^{λx.l(z)⊗x}, B^{r(z)}

The corresponding FILL_{μ}-term is

z: A⅋B ⊢ λx.(⟨β⟩z)⊗x: (C−∘(A⊗C))^{λx.l(z)⊗x}, β: B^{r(z)}

The crucial point is that the name β depends only on z and not on x. This ensures that this term is a FILL_{μ}-term. This derivation is not an intuitionistic derivation, which can be derived syntactically from the fact that the operator ⟨β⟩ is applied to a variable. This means that there is a second formula on the RHS when the −∘R-rule is applied.

In the other direction, we define a translation from FILL_{μ}-terms to FILL-derivation by induction over the structure of FILL_{μ}-terms. Again, the decorations are not used in the definition of the translation, only in the proof that the translation transforms FILL_{μ}-terms to FILL-derivations.

x: Assume x: A ⊢ x: A. Then the derivation x^{lf} is given by

A ⊢ A ;

μα.M: Assume M^{lf} = ϕ: Γ ⊢ ⊥, A, Δ. Then μα.M^{lf} is the derivation

{ϕ \atop Γ ⊢ ⊥, A, Δ}  \begin{aligned}& ⊥L \\ ⊥ ⊢ \end{aligned}
cut ;
Γ ⊢ A, Δ

[α]M: Assume M^{lf} = ϕ: Γ ⊢ A, Δ. Then [α]M^{lf} is the derivation

{ϕ \atop Γ ⊢ A, Δ} ; ⊥R ; ; Γ ⊢ ⊥, A, Δ

λx: A.M: Assume M^{lf} = ϕ: Γ, A ⊢ B, Δ. Then λx: A.M^{lf} is the derivation

\begin{matrix}ϕ \\ Γ ⊢ A−∘B, Δ \end{matrix} −∘R;

MN: Assume M^{lf} = ϕ, N^{lf} = ψ, Γ_{1} ⊢ M: A−∘B, Δ_{1} and Γ_{2} ⊢ N: A, Δ_{2}. Then MN^{lf} is the derivation

{ϕ \atop Γ_{1} ⊢ A−∘B, Δ_{1}}  {Γ_{2} ⊢ A, Δ_{2}  A ⊢ A B ⊢ B ; −∘L ; A−∘B, A ⊢ B \atop Γ_{2}, A−∘B ⊢ B, Δ_{2}}
cut ;
Γ_{1}, Γ_{2} ⊢ B, Δ_{1}, Δ_{2}

M⊗N: Assume M^{lf} = ϕ: Γ_{1} ⊢ A, Δ_{1}, and N^{lf} = ψ: Γ_{2} ⊢ B, Δ_{2}. Then M⊗N^{lf} is the

derivation

Γ_{1} ⊢ A, Δ_{1} Γ_{2} ⊢ B, Δ_{2}
⊗R ;
Γ_{1}, Γ_{2} ⊢ A⊗B, Δ_{1}, Δ_{2}

let M be x⊗y in N: Assume that M and N satisfy M^{lf} = ϕ: Γ_{1} ⊢ A⊗B, Δ_{1}, and N^{lf} = ψ: Γ_{2}, A, B ⊢ C, Δ_{2}. Then let M be x⊗y in N^{lf} is the derivation

{ϕ \atop Γ_{1} ⊢ A⊗B, Δ_{1}}  Γ_{2}, A, B ⊢ C, Δ_{2} ; ⊗L ; Γ_{2}, A⊗B ⊢ C, Δ_{2}
cut ;
Γ_{1}, Γ_{2} ⊢ C, Δ_{1}, Δ_{2}

∗: ∗^{lf} = I R;

let M be ∗ in N: Assume M^{lf} = ϕ: Γ_{1} ⊢ I, Δ_{1}, and N^{lf} = ψ: Γ_{2} ⊢ A, Δ_{2}. Then let M be ∗ in N^{lf} is the derivation

{ϕ \atop Γ_{1} ⊢ I, Δ_{1}}  Γ_{2} ⊢ C, Δ_{2} ; I L ; Γ_{2}, I ⊢ C, Δ_{2}
cut ;
Γ_{1}, Γ_{2} ⊢ C, Δ_{1}, Δ_{2}

να.M: Assume M^{lf} = ϕ: Γ ⊢ A, B, Δ. Then να.M^{lf} is the derivation

ϕ ; ⅋R ; ; Γ ⊢ A⅋B, Δ

⟨α⟩M: Assume M^{lf} = ϕ: Γ ⊢ A⅋B, Δ. Then ⟨α⟩M^{lf} is the derivation

{ϕ \atop Γ ⊢ A⅋B, Δ}  A ⊢ A B ⊢ B ; ⅋L ; A⅋B ⊢ A, B
cut .
Γ ⊢ A, B, Δ

We have the expected theorem:

5.3. Theorem. Assume Γ ⊢ M: A, Δ is FILL_{μ}-term. Then the derivation M^{lf} is a FILLderivation.

Proof. Induction over the structure of M.

6. A sound semantics for FILL_{μ}

So far we have only established that FILL and FILL_{μ} are logically equivalent, i.e., they prove the same theorems. In this section we show that they are not equivalent as far as proofs are concerned. The reason is that the ν-construction in FILL_{μ} does not provide co-products. In fact, in [RP01] we show that if the ν-construction is a co-product, then the calculus is trivial in the sense that in any semantic model all terms of the same type are interpreted by the same element in the model.

However, we can show that weakly distributive categories with a right adjoint to the tensor product but without negation (which we call full linear categories) are a sound model of the FILL_{μ}-calculus. The reason is that the handling of dependencies which was crucial for the semantics of FILL also works for FILL_{μ}.

We now present the soundness proof, following closely [HdP93]. We repeat here the notion of independence from [HdP93].

6.1. Definition. Suppose that we have a map of the form f: A⊗B → C⅋D in a weakly distributive category L. We say that the object C is independent of B (for f) if there exists an object E of L and maps g: A → C⅋E and h: E⊗B → D such that the composite (1_{C}⅋h)∘δ∘(g⊗1_{B}) is equal to f, where δ is the weak distributivity with domain (C⅋E)⊗B and co-domain C⅋(E⊗B).

Now we show that this notion of independence is compatible with linear function spaces.

6.2. Lemma. Suppose we have a map f: A⊗B → C⅋D in a full linear category L. If C is independent of B for f, then there exists a morphism \overline{f}: A → C⅋(B−∘D).

The operation f ↦ \overline{f} is crucial for defining the categorical semantics of λ-abstraction. However, we need another lemma, which states that this operation preserves other independences.

6.3. Lemma. Suppose we have a map f: A⊗B⊗C → D⅋E⅋F in a full linear category L. Suppose also that D⅋E is independent of C for f so that we have a map \overline{f}: A⊗B → D⅋E⅋(C−∘F). Then

(i) If F is independent of B for f, then C−∘F is independent of B for \overline{f};

(ii) If E is independent of B for f, then E is independent of B for \overline{f}.

Now we can define the semantics of FILL_{μ}by induction over the structure of derivations. The clause for λ-abstraction requires a lemma to show that this definition is well-formed. We do this immediately afterwards.

6.4. Definition. By induction over the structure of derivations, we define the semantics of FILL_{μ}in a weakly distributive category as follows:

Types: The type constructors of FILL_{μ}are modelled by the corresponding categorical constructions;

x: [[x]] = Id;

⊗: Assume [[t_{1}]] = f: Γ_{1} → A_{1} and [[t_{2}]] = f_{2}: Γ_{1} → A_{2}. Then define [[t_{1}⊗t_{2}]] to be

Γ_{1}⊗Γ_{2} ⟶^{f_{1}⊗f_{2}} (A_{1}⅋Δ_{1})⊗(A_{2}⅋Δ_{2}) ⟶^{δ} (A_{1}⊗(A_{1}⅋Δ_{2}))⅋Δ_{1}

⟶^{π∘(δ⅋1)} (A_{1}⊗A_{2})⅋Δ_{1}⅋Δ_{2} ;

44  VALERIA DE PAIVA AND EIKE RITTER

let t be a⊗b in s: Assume [[t]]: Γ_{1} → A⊗B, Δ_{1} and [[s]]: Γ_{2}⊗A⊗B → C⅋Δ_{2}. Then

[[let t be a⊗b in s]] is defined as

Γ_{1}⊗Γ_{2} ⟶^{[[t]]⊗1} ((A⊗B)⅋Δ_{1})⊗Γ_{2} ⟶^{δ} Δ_{1}⅋(A⊗B⊗Γ_{2}) ⟶^{1⅋[[s]]} C⅋Δ_{1}⅋Δ_{2} ;

λ-abstraction: Assume [[t]]: Γ⊗A → B⅋Δ. Define [[λa: A.t]] to be \overline{[[t]]}; ts: Assume [[t]]: Γ_{1} → (A−∘B)⅋Δ_{1} and [[s]]: Γ_{2} → A⅋Δ_{2}. Then define [[ts]] to be

Γ_{1}⊗Γ_{2} ⟶^{[[t]]⊗[[s]]} (A−∘B⅋Δ_{1})⊗(A⅋Δ_{2}) ⟶^{δ} ((A−∘B⅋Δ_{1})⊗A)⅋Δ_{2}

⟶^{δ⅋1} (A−∘B⊗A)⅋Δ_{1}⅋Δ_{2} ⟶^{App⅋Id} B⅋Δ_{1}⅋Δ_{2} ;

μα.t: Assume Γ ⊢ t: ⊥, α: B^{τ}, Δ. Then [[μα.t]] is defined to be the morphism u∘[[t]], where

u is the unit of ⅋; [α]t: Assume Γ ⊢ t: A, Δ. Then [[[α]t]] is defined to by u^{−1} ∘ [[M]]; να.t: [[να.t]] = [[t]]; ⟨α⟩t: [[⟨α⟩t]] = [[t]].

Well-definedness of the semantics requires the following lemma, which shows that the category-theoretic notion of independence captures the syntactic notion of independence in FILL_{μ}. 6.5. Lemma. Assume Γ, x: C ⊢ t: A, Δ, and assume also that x does not appear in Δ. Then Δ is independent for C in [[t]]. Proof. Induction over the structure of t. Lemmata 6.2 and 6.3 are used for the λabstraction.

Now the soundness proof is routine. 6.6. Theorem.

(i) Assume Γ ⊢ t: A, Δ. Then [[t]] is a morphism from [[Γ]] to [[A]]⅋[[Δ]]; (ii) Assume t = s. Then also [[t]] = [[s]]. Proof. Induction over the derivation.

7. Conclusions

We have shown how to produce a Natural Deduction formulation for FILL, called FILL_{μ}, using a modification of Pym and Ritter’s λμν-calculus, itself an extension of Parigot’s λμ-calculus.

The process of transforming Parigot’s λμ-calculus into Pym and Ritter’s λμν-calculus and finally into FILL_{μ}-terms is complicated, but it works and provides a Curry-Howard correspondence for full intuitionistic linear logic. We can prove not only the essential properties of subject reduction and strong normalization for the FILL_{μ}-calculus but also that this really corresponds to the original (sequent-style) formulation of FILL. But given the somewhat convoluted process, we wonder if something simpler might work as well. This is part of our proposal for future work.

The interested reader may wonder how the terms of the FILL_{μ}-calculus relate to the terms of the classical linear λ-calculus, described by Bierman[Bie99]. The classical linear λ-calculus also arises from considering Parigot’s ideas in the context of linear logic. But since Bierman is dealing with classical linear logic, he can adapt Parigot’s ideas more directly. We believe, and this must be checked, that restricting FILL_{μ} to classical linear logic we obtain a calculus equivalent to the classical linear λ-calculus.

Two other question also suggest themselves. Firstly, since the restriction that characterizes FILL was also considered recently by Crolard [Cro04], in the context of modelling co-routines that do not access the local environment of other co-routines, we wonder whether our new term assignment for FILL can be used to model linear co-routines with the same non-interfering property. Secondly, Pratt [Pra03] presents a calculus for Chuspaces which has two kinds of variables with equal status, one for (positive) assumptions and for (negative) evidence against a formula. He shows that this so-called “dialectic calculus” captures proofs of bi-implicational mulplicative linear logic but does not present reduction rules for this calculus. It would be interesting to check how this dialectic calculus relates to our FILL_{μ} calculus.

Appendix A: Dependencies in FILL

.1. Definition. Let τ be a proof in CLL whose end-sequent is Γ ⊢ Δ and where A is a formula occurrence in Δ. The immediate subproofs of τ are denoted by τ_{i}. We define the set Dep_{τ}(A) (the formulae occurrences of Γ that A depends on, in the proof τ) by induction on τ. The definition is by cases in accordance with the table in Figure 1.

If the derivation τ ends in the sequent Γ ⊢ Δ, and B and A are formula occurrences in Γ and Δ respectively, then we say that A depends on B in τ iff B ∈ Dep_{τ}(A). If τ and τ′ are two derivations ending in the sequent Γ ⊢ Δ in CLL, we say that the end-sequent of τ has the same dependencies as the end-sequent of τ′ iff we for any formula occurrence C in Γ and any formula occurrence A in Δ, we have that A depends on C in τ iff A depends on C in τ′. Similarly say that the end-sequent of τ has fewer dependencies than the end-sequent of τ′ iff we for any formula occurrence C in Γ and any formula occurrence

46  VALERIA DE PAIVA AND EIKE RITTER

\begin{aligned}& Ax \\ A ⊢ A \end{aligned}  Dep_{τ} (A) = A

Γ ⊢ B, Δ Γ′, B ⊢ Δ′

Cut
Γ′, Γ ⊢ Δ′, Δ

Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A) & if A ∈ Δ \\ Dep_{τ_{2}}(A)[\{B\} ↦ Dep_{τ_{1}}(B)] & if A ∈ Δ′ \end{matrix}

Γ, B, C ⊢ Δ ; ⊗_{L} ; Γ, B ⊗ C ⊢ Δ  Dep_{τ} (A) = Dep_{τ_{1}}(A)[{B, C} ↦ {B ⊗ C}]

Γ ⊢ B, Δ Γ′ ⊢ C, Δ′

⊗_{R}

Γ, Γ′ ⊢ B ⊗ C, Δ, Δ′

Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A) & if A ∈ Δ \\ Dep_{τ_{2}}(A) & if A ∈ Δ′ \\ Dep_{τ_{1}}(B) ∪ Dep_{τ_{2}}(C) & if A = B ⊗ C \end{matrix}

Γ ⊢ Δ ; I_{L} ; Γ, I ⊢ Δ  Dep_{τ} (A) = Dep_{τ_{1}}(A)

\begin{aligned}& I_{R} \\ ⊢ I \end{aligned}  Dep_{τ} (I) = ∅

Γ, B ⊢ Δ Γ′, C ⊢ Δ′

⅋_{L}

Γ, Γ′, B⅋C ⊢ Δ, Δ′

Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A)[\{B\} ↦ \{B⅋C\}] & if A ∈ Δ \\ Dep_{τ_{2}}(A)[\{C\} ↦ \{B⅋C\}] & if A ∈ Δ′ \end{matrix}

Γ ⊢ B, C, Δ ; ⅋_{R} ; Γ ⊢ B⅋C, Δ  Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A) & if A ∈ Δ \\ Dep_{τ_{1}}(B) ∪ Dep_{τ_{1}}(C) & if A = B⅋C \end{matrix}

\begin{aligned}& ⊥_{L} \\ ⊥ ⊢ \end{aligned}  nothing to define

Γ ⊢ Δ ; ⊥_{R} ; Γ ⊢ ⊥, Δ  Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A) & if A ∈ Δ \\ ∅ & if A = ⊥ \end{matrix}

Γ ⊢ B, Δ Γ′, C ⊢ Δ′ −∘_{L}

Γ, Γ′, B−∘C ⊢ Δ, Δ′

Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{2}}(A)[\{C\} ↦ \{B−∘C\} ∪ Dep_{τ_{1}}(B)] \\ if A ∈ Δ′ \\ Dep_{τ_{1}}(A) \\ if A ∈ Δ \end{matrix}

\begin{matrix}Γ, B ⊢ C, Δ \\ −∘ & R \\ Γ ⊢ B−∘C, Δ \end{matrix}  Dep_{τ} (A) = \{ \begin{matrix}Dep_{τ_{1}}(A)[\{B\} ↦ ∅] & if A ∈ Δ \\ Dep_{τ_{1}}(C)[\{B\} ↦ ∅] & if A = B−∘C \end{matrix}

Figure 1: Definition of dependencies Dep_{τ}(A)

A in Δ have that A depends on C in τ entails that A depends on C in τ′.

Appendix B: Reduction rules of the λμν-calculus

β  (λx: A.t)s ⇝ t[s/x]
η^{→}  t ⇝ λx: A.tx
ζ^{⊃} (μα^{A→B}.t)s ⇝ μβ^{B}.t[[β]us/[α]u]
(μα^{A→⊥}.t)s ⇝ t[us/[α]u]
η^{μ}  μα.[α]s ⇝ s if α not free in s
β^{μ}  [γ](μα.s) ⇝ s[γ/α]
β^{∧}  π(⟨t, s⟩) ⇝ t
π′(⟨t, s⟩) ⇝ s
η^{∧}  t ⇝ ⟨π(t), π′(t)⟩
ζ^{∧} π(μα^{A∧B}.s) ⇝ μβ^{A}.s[[β]π(u)/[α]u]
π(μα^{⊥∧B}.s) ⇝ s[π(u)/[α]u]
π′(μα^{A∧B}.s) ⇝ μγ^{B}.s[[γ]π′(u)/[α]u]
π′(μα^{A∧⊥}.s) ⇝ s[π′(u)/[α]u]
β^{∨}  ⟨β⟩(να.s) ⇝ s[β/α]
η^{∨}  t ⇝ να.⟨α⟩t
ζ^{∨}  ⟨β⟩μγ.t ⇝ μα.t[[α]⟨β⟩s/[γ]s]
⟨β⟩μγ^{⊥∨B} ⇝ t[⟨β⟩s/[γ]s]

Standard variable-capture are conditions assumed. In the η-rules we assume that t is neither a λ-abstraction nor a product nor a term να.t′ and that t does not occur as the first argument of an application, of a projection π or π′ or of some term ⟨β⟩ . In the η−∘-, η^{∧}- and η^{∨}-rules. In the η^{→}-, η^{∧}- and η^{∨}-rule we also assume that t is of function type, product type and sum type respectively.

References

[Bar96] M. Barr. The Chu construction. Theory and Applications of Categories, 2:17–35, 1996.

[BdP98] Torben Braüner and Valeria de Paiva. A formulation of linear logic based on dependency-relations. In Proc. of Computer Science Logic ’97, Lecture Notes in Computer Science. Springer Verlag, 1998.

[Bie99] G. Bierman. A classical linear lambda calculus. Theoretical Computer Science, 227(1–2):43–78, 1999.

[Cro04] T. Crolard. A formulae-as-types interpretation of subtractive logic. Journal of Logic and Computation, 14(4):529–570, 2004.

[CS97] J.R.B. Cockett and R.A.G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133–173, 1997.

[dP89] V.C.V de Paiva. A dialectica-like model of linear logic. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science. Springer, 1989.

[Dum80] M. Dummett. Elements of Intuitionism. OUP, Oxford, 1980.

[Gen34] G. Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, pages 176–210, 405–431., 1934.

[Gir95] J.-Y. Girard. Linear logic: its syntax and semantics. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 1–42. Cambridge University Press, 1995. London Mathematical Society Lecture Note Series 222, Proceedings of the 1993 Workshop on Linear Logic, Cornell Univesity, Ithaca.

[HdP93] M. Hyland and V. de Paiva. Full intuitionistic linear logic (extended abstract). Annals of Pure and Applied Logic, 64(3):273–291, 1993.

[Par92] M. Parigot. λμ-calculus: an algorithmic interpretation of classical natural deduction. In Proc. Logic Progr. and Automatic Reasoning, St. Petersburg, pages 190–201. Lecture Notes in Computer Science No. 624, Berlin, Heidelberg, New York, 1992.

[Pra03] V. Pratt. Chu spaces as a semantic bridge between linear logic and mathematics,. Theoretical Computer Science, 294:439–471, 2003.

[RP01] E. Ritter and D. Pym. On the semantics of classical disjunction. Journal of Pure and Applied Algebra, 159:315–338, 2001.

[RPW00a] E. Ritter, D. Pym, and L. A. Wallen. On the intuitionistic force of classical search. Journal of Logic and Computation, 10(2):173–207, 2000.

[RPW00b] E. Ritter, D. Pym, and L.A. Wallen. Proof-terms for classical and intuitionistic logic. Theoretical Computer Science, 232(1–2):299–333, 2000.

Palo Alto Research Center USA

School of Computer Science University of Birmingham, UK

Email: paiva@parc.com
      E.Ritter@cs.bham.ac.uk

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/17/3/17-03.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: mbarr@barrs.org

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com

Ezra Getzler, Northwestern University: getzler(at)math(dot)northwestern(dot)edu

Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca