BRICS RS-02-48 Nygaard & Winskel: Linearity in Process Languages BRICS

Basic Research in Computer Science

Linearity in Process Languages

Mikkel Nygaard Glynn Winskel BRICS Report Series RS-02-48 ISSN 0909-0878 December 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Mikkel Nygaard & Glynn Winskel.

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 BRICS Report Series publications. 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@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/48/

Linearity in Process Languages

Mikkel Nygaard  Glynn Winskel
BRICS^{∗}  Computer Laboratory
University of Aarhus University of Cambridge

Abstract The meaning and mathematical consequences of linearity (managing without a presumed ability to copy) are studied for a path-based model of processes which is also a model of affine-linear logic. This connection yields an affine-linear language for processes, automatically respecting open-map bisimulation, in which a range of process operations can be expressed. An operational semantics is provided for the tensor fragment of the language. Different ways to make assemblies of processes lead to different choices of exponential, some of which respect bisimulation.

1 Path-based models of processes

In distributed computation it can be hard or impossible for a process to copy a process, while it is generally easy for a process to ignore another process. For this reason an operation on processes associated with distributed computation often has the following property: a computation path of the process arising from the application of the operation to an input process has resulted from at most one computation path of the input process. As we will see, this property expresses that the operation is an affine linear map within a model of linear logic, a fact which carries many consequences.

This article presents a model of processes based on computation paths and so can make precise the sense in which many process operations are associated with linear maps, investigates the consequences of linearity for the important equivalence of bisimulation, and delineates the boundaries of linearity with respect to one, fairly broad, mathematical model, in which processes are represented as presheaves.

∗

Basic Research in Computer Science (www.brics.dk),

funded by the Danish National Research Foundation.

Of course some process operations do involve sending and copying code, which can give rise to maps which are not linear. The presheaf model exposes how different degrees of copying lead to different kinds of nonlinear maps, some respecting bisimulation, others not.

Consider processes which, like those of CCS [17] and CSP [10], can perform simple atomic actions, one at a time, among which might be actions of synchronisation. An old idea is to represent the nondeterministic behaviour of such a process as a “collection” of the computation paths it can perform. The trace model [10] and tree model [16] of processes are based on different ideas of what this means. A trace set of a process simply expresses whether or not a finite sequence of actions, a trace, is possible for the process. A tree expresses not only what paths are present but also how paths are subpaths, or restrictions, of others, thus keeping track of nondeterministic branching. This data, what paths are present and how they restrict to smaller paths, is precisely that caught in a presheaf over a category in which the objects are path shapes and the maps express how one path shape can extend to another. In the category of all such presheaves we can view the tree as a colimit of its paths—another kind of “collection” of its paths.

To illustrate the idea, suppose that actions are drawn from some alphabet L, and consider processes whose computation paths have the shape of strings of actions, so members of L^{∗}. The substring ordering ≤ makes L^{∗} a partial order, and so a category with an arrow from s to t precisely when s ≤ t. A presheaf over L^{∗} is a functor from the opposite category (L^{∗})^{op}, where all the arrows are reversed, to the category of sets and functions Set. When thinking of a presheaf X as representing a process, for a string s, the set X(s) is the set of computation paths of shape s that the process can perform, and, when s ≤ t, the function X(s, t) : X(t) → X(s) tells how paths of shape t restrict to subpaths of shape s.

Suppose that we replace the category of sets used in the definition of presheaves by the simple subcategory 2, consisting of the empty set, ∅, and the singleton set, 1, with the only non-identity map being ∅ ⊆ 1. A functor X from (L^{∗})^{op} to 2 is the same as a monotonic function from the reverse order (L^{∗})^{op} to the order 2, so that if s ≤ t then X(t) ≤ X(s). When thinking of X as representing a process, X(s) = 1 means that the process can perform a path of shape s while X(s) = ∅ means that it can’t. If X(t) = 1 and s ≤ t, then X(s) = 1. The functor X is a characteristic function for a trace set.

So trees and trace sets arise as variants of a common idea, that of representing a process as a generalised characteristic function, in the form of a functor from path shapes to measures of the extent to which the path shapes can be realised by the process.

In what follows, we want to broaden computation paths to have more general shapes than sequences of atomic actions, to allow actions to occur concurrently in a computation path, and for individual actions to have a more complicated structure. Later on, processes will be allocated types; the type of a process will specify the kind of computation path shapes it can perform.

2 Processes as presheaves

Let ℙ be a small category. The category of presheaves over ℙ, written ℙ̂, is the category [ℙ^{op}, Set] with objects the functors from ℙ^{op} to the category of sets, and maps the natural transformations between them. In our applications, ℙ is thought of as consisting of computation-path shapes where a map e : p → q expresses how p is extended to q.

A presheaf category has all limits and colimits given pointwise, at a particular object, by the corresponding limits or colimits of sets. In particular, a presheaf category has all sums (coproducts) of presheaves; the sum Σ_{i∈I}X_{i} of presheaves X_{i} over ℙ has a contribution Σ_{i∈I}X_{i}(p), the disjoint union of sets, at p ∈ ℙ. The empty sum of presheaves is the presheaf ∅ with empty contribution at each p ∈ ℙ. In process terms, a sum of presheaves represents a nondeterministic sum of processes.

2.1 A linear category of presheaf models

A category of presheaves, ℙ̂, is accompanied by the Yoneda embedding, a functor y_{ℙ} : ℙ → ℙ̂, which fully and faithfully embeds ℙ in ℙ̂. For every object p of ℙ, the Yoneda embedding yields y_{ℙ}(p) = ℙ(−, p). Presheaves isomorphic to images of objects of ℙ under the Yoneda embedding are called representables.

Via the Yoneda embedding we can regard ℙ essentially as a full subcategory of ℙ̂. Moreover, ℙ̂ is characterized (up to equivalence of categories) as the free colimit completion of ℙ. In other words, y_{ℙ} satisfies the universal property that for any functor F : ℙ → E, where E is a category with all colimits, there is a colimit-preserving functor G : ℙ̂ → E, determined to within isomorphism, such that F ≅ G ∘ y_{ℙ}—see e.g. [15], p. 43:

\xymatrix{ℙ \ar[r]^{y_{ℙ}} \ar[dr]_{F}^{≅} & ℙ̂ \ar[d]^{G} \\  & E}

The proof rests on the fact that any presheaf is a colimit of representables. We will use an “inner product” notation and describe G above as F · −.

In particular, we can take E to be a presheaf category ℚ̂. As the universal property suggests, colimit-preserving functors between presheaf categories are useful. Define the category Lin to consist of small categories ℙ, ℚ, … with maps G : ℙ → ℚ the colimit-preserving functors ℙ̂ → ℚ̂.

By the universal property, colimit-preserving functors G : ℙ̂ → ℚ̂ correspond to within isomorphism to functors F : ℙ → ℚ̂, and such functors are in 1-1 correspondence with profunctors F̄ : ℙ −↦ ℚ. Recall that the category of profunctors from ℙ to ℚ, written Prof(ℙ, ℚ), is the functor category [ℙ × ℚ^{op}, Set], which clearly equals the category of presheaves { \atop ℙ^{op} × ℚ}, and is isomorphic to the functor category [ℙ, ℚ̂]. We thus have the chain of equivalences:

Lin(ℙ, ℚ) ≃ [ℙ, ℚ̂] ≅ Prof(ℙ, ℚ) = { \atop ℙ^{op} × ℚ} .

The more symmetric, relational presentation via profunctors exposes an involution central in understanding Lin as a categorical model of classical linear logic. The involution of linear logic, ℙ^{⊥}, on an object ℙ, is given by ℙ^{op}; clearly presheaves over ℙ^{op} × ℚ correspond to presheaves over (ℚ^{op})^{op} × ℙ^{op}, showing how maps G : ℙ → ℚ correspond to maps G^{⊥} : ℚ^{op} → ℙ^{op} in Lin. The tensor product of ℙ and ℚ is given by the product of small categories ℙ × ℚ and the function space from ℙ to ℚ by ℙ^{op} × ℚ. On objects ℙ and ℚ, products (written ℙ & ℚ) and coproducts are both given by ℙ + ℚ, the disjoint juxtaposition of ℙ and ℚ. As for the exponential ! of linear logic, there’s room for choice—see Section 7.

Linear maps preserve colimits. The colimit of the empty diagram is ∅, to be thought of as a nil process, which is unable to perform any computation path. So linear maps, unlike many process operations, always send the nil process to the nil process. We could extend to maps from !ℙ to ℚ, for objects ℙ and ℚ in Lin, but by the properties of the exponential, this would allow arbitrary copying of the argument process. All we often need is to allow maps to ignore their arguments and this can be got much more cheaply, by moving to a model of affine linear logic.

2.2 An affine-linear category of presheaf models

Many operations associated with process languages do not preserve sums, so arbitrary colimits. Prefixing operations only preserve connected colimits, that is, colimits of nonempty connected diagrams. Prefixing operations derive from the functor ⌊−⌋ : ℙ̂ → ℙ̂_{⊥}. The category ℙ_{⊥} comprises ℙ together with a new initial object ⊥. The functor ⌊−⌋ adjoins a “root” to a presheaf X in ℙ̂ in the sense that ⌊X⌋(p) is a copy of X(p) for any p in ℙ, while ⌊X⌋(⊥) is a singleton set {∗}, the new root being ∗; the restriction maps are extended so that restriction to ⊥ sends elements to ∗. A map from X to Y in ℙ̂ is sent to its obvious extension from ⌊X⌋ to ⌊Y ⌋ in ℙ̂_{⊥}. Presheaves that to within isomorphism can be obtained as images under ⌊−⌋ are called rooted [12].

Proposition 2.1 Any presheaf Y in ℙ̂_{⊥} has a decomposition as a sum of rooted presheaves Y ≅ Σ_{i∈Y (⊥)}⌊Y_{i}⌋, where, for i ∈ Y (⊥), the presheaf Y_{i} in ℙ̂ is, to within isomorphism, given as

Y_{i}(p) = {x ∈ Y (p) | (Y!_{p})x = i}

where !_{p} is the unique arrow ⊥ → p in ℙ_{⊥}.

Intuitively, thinking of presheaves as processes, the presheaves Y_{i}, where i ∈ Y (⊥), in the decomposition of Y are those processes that Y can become after performing the initial action ⊥.

The strict Yoneda embedding j_{ℙ} : ℙ_{⊥} → ℙ̂, sends ⊥ to ∅ and elsewhere acts like y_{ℙ}. The presheaf category ℙ̂ with j_{ℙ} is a free connected-colimit completion of ℙ_{⊥}. Together they satisfy the universal property that for any functor F : ℙ_{⊥} → E, where E is a category with all connected colimits, there is a connected-colimit preserving functor F^{†} : ℙ̂ → E, determined to within isomorphism, such that F ≅ F^{†} ∘ j_{ℙ}:

\xymatrix{ℙ_{⊥} \ar[r]^{j_{ℙ}} \ar[dr]_{F}^{≅} & ℙ̂ \ar[d]^{F^{†}} \\  & E}

The central observation on which the proof relies is that any presheaf over ℙ is a connected colimit of representables (images under y_{ℙ}) together with ∅, the empty presheaf.

The universal property suggests the importance of connected-colimit preserving functors. Define Aff to be the category consisting of small categories ℙ, ℚ, …, with maps G : ℙ → ℚ the connected-colimit preserving functors ℙ̂ → ℚ̂. It has Lin in which the maps preserve arbitrary colimits as a subcategory, one which shares the same objects. We can easily characterise those maps in Aff which are in Lin:

Proposition 2.2 Suppose G : ℙ̂ → ℚ̂ is a functor which preserves connected colimits. The following properties are equivalent: (i) G preserves all colimits; (ii) G preserves all coproducts (sums); (iii) G is strict, i.e., G(∅) = ∅.

Because ℙ̂ is the free connected-colimit completion of ℙ_{⊥}, we obtain the equivalence Aff(ℙ, ℚ) ≃ [ℙ_{⊥}, ℚ̂], and consequently the equivalence

Aff(ℙ, ℚ) ≃ Lin(ℙ_{⊥}, ℚ) .

The equivalence is part of an adjunction between Aff and Lin regarded as 2-categories, in which the 2-cells are natural transformations. We can easily extend lifting to a 2-functor (−)_{⊥} : Aff → Lin; for G : ℙ → ℚ in Aff, the functor G_{⊥} : ℙ_{⊥} → ℚ_{⊥} in Lin takes Y ∈ ℙ̂_{⊥} with decomposition Σ_{i∈Y (⊥)}⌊Y_{i}⌋ to G_{⊥}(Y) = Σ_{i∈Y (⊥)}⌊G(Y_{i})⌋. Lifting restricts to a 2-comonad on Lin with Aff as its coKleisli category. The comonad (−)_{⊥} has turned the model of linear logic Lin into a model Aff of affine linear logic (where the tensor unit is terminal).

2.3 Bisimulation

Bisimulation between presheaves is derived from the notion of open map between presheaves [11, 12].

A morphism h : X → Y, between presheaves X, Y over ℙ, is open iff for all morphisms e : p → q in ℙ_{⊥}, any commuting square (on the left below) can be split into two commuting triangles (on the right):

\xymatrix{j_{ℙ}(p) \ar[r]^{x} \ar[d]_{j_{ℙ}(e)} & X \ar[d]^{h} & j_{ℙ}(p) \ar[r]^{x} \ar[d]_{j_{ℙ}(e)} & X \ar[d]^{h} \\ j_{ℙ}(q) \ar[r]_{y} & Y & j_{ℙ}(q) \ar[r]_{y} \ar@{.>}[ur]^{z} & Y}

That the square commutes means that the path h ∘ x in Y can be extended via e to a path y in Y. That the two triangles commute means that the path x can be extended via e to a path z in X which matches y.

Open maps are a generalisation of functional bisimulations, or zig-zag morphisms, known from transition systems [12]. Presheaves in ℙ̂ are bisimilar iff there is a span of open maps between them.^{1}

The preservation of connected colimits by a functor between presheaf categories is sufficient to ensure that it preserves open maps and bisimulation.

Proposition 2.3 [8] Let G : ℙ̂ → ℚ̂ be any connected-colimit preserving functor between presheaf categories. Then G preserves open maps and openmap bisimulation.

1We have chosen here to develop the definition of open map from the strict Yoneda embedding rather than the Yoneda embedding. Maps between presheaves are open w.r.t.

strict Yoneda iff they are surjective and open w.r.t. Yoneda.

3 Constructions for path orders

The constructions in Aff below form the basis of a denotational semantics of the affine-linear process language presented in Section 4. The types and open terms of that language will be interpreted, respectively, as objects and arrows of Aff. Actually, only the full subcategory of path orders, small partial order categories, is needed, and we’ll simplify the discussion accordingly, treating denotations of types as though they were just partial orders. (In fact, all the constructions can be imitated for a domain analogue of presheaf categories, in which Set is replaced by 2 and processes denote trace sets—see Section 1 and [19].)

3.1 Sums and fixed points

Each path order ℙ is associated with (nondeterministic) sum operations, a map Σ : &_{i∈I} ℙ → ℙ in Aff taking a tuple ⟨X_{i}⟩_{i∈I} to the sum (coproduct) Σ_{i∈I}X_{i} in ℙ̂. The empty sum yields ∅ ∈ ℙ̂. Finite sums, of size k, are typically written as X_{1} + ⋯ + X_{k}.

For path orders ℙ and ℚ, the category Aff(ℙ, ℚ), being equivalent to { \atop (ℙ_{⊥})^{op} × ℚ}, has all colimits and in particular all ω-colimits. Any operation G : Aff(ℙ, ℚ) → Aff(ℙ, ℚ) which preserves connected colimits will have a fixed point fix G : ℙ → ℚ, a map in Aff. We will build up the denotation of fixed points out of composition in Aff. The composition G ∘ F of maps F in Aff(ℙ, ℚ) and G in Aff(ℚ, ℝ), being got as the application G(F (−)), preserves connected colimits in the argument F and colimits in G.

3.2 Tensor

The tensor product ℙ⊗ℚ of path orders ℙ, ℚ is given by the set (ℙ_{⊥} ×ℚ_{⊥})\ {(⊥, ⊥)}, ordered coordinatewise.

Let F : ℙ → ℙ′ and G : ℚ → ℚ′. We define F ⊗ G : ℙ ⊗ ℚ → ℙ′ ⊗ ℚ′ as the extension (cf. Section 2.2) H^{†} of a functor H : (ℙ ⊗ ℚ)_{⊥} → { \atop ℙ′ ⊗ ℚ′}. Notice that (ℙ⊗ℚ)_{⊥} ≅ ℙ_{⊥}×ℚ_{⊥} and so we can define H : ℙ_{⊥}×ℚ_{⊥} → { \atop ℙ′ ⊗ ℚ′} by taking

(H(p, q))(p′, q′) = ⌊F (j_{ℙ}p)⌋(p′) × ⌊G(j_{ℚ}q)⌋(q′)

for p ∈ ℙ_{⊥}, q ∈ ℚ_{⊥} and (p′, q′) ∈ ℙ′ ⊗ ℚ′.

The unit for tensor is the empty path order 𝕆. Objects X ∈ ℙ̂ correspond to maps X̃ : 𝕆 → ℙ sending ∅ to X. Given X ∈ ℙ̂ and Y ∈ ℚ̂ we define X ⊗ Y ∈ { \atop ℙ ⊗ ℚ} to be the element pointed to by X̃ ⊗ Ỹ : 𝕆 → ℙ ⊗ ℚ.

3.3 Function space

The function space of path orders ℙ ⊸ ℚ is given by the product of partial orders (ℙ_{⊥})^{op} × ℚ.

We have the following chain of isomorphisms:

\begin{matrix}ℙ ⊗ ℚ ⊸ ℝ = ((ℙ ⊗ ℚ)_{⊥})^{op} × ℝ \\ ≅ (ℙ_{⊥})^{op} × (ℚ_{⊥})^{op} × ℝ ≅ ℙ ⊸ (ℚ ⊸ ℝ) . \end{matrix}

So that { \atop ℙ ⊗ ℚ ⊸ ℝ} ≅ { \atop ℙ ⊸ (ℚ ⊸ ℝ)}. Thus there is a 1-1 correspondence curry from maps ℙ ⊗ ℚ → ℝ to maps ℙ → (ℚ ⊸ ℝ) in Aff; its inverse is called uncurry. We obtain application, app : (ℙ ⊸ ℚ) ⊗ ℙ → ℚ, as uncurry(1_{ℙ⊸ℚ}).

We shall write t u for the application of t of type ℙ ⊸ ℚ to u of type ℙ. The ability to curry justifies the formation of terms λx.t of type ℙ ⊸ ℚ by lambda abstraction where t of type ℚ is a term with free variable x of type ℙ.

3.4 Products

The product of path orders ℙ & ℚ is given by the disjoint union of ℙ and ℚ. An object of { \atop ℙ & ℚ} can be identified with a pair (X, Y), with X ∈ ℙ̂ and Y ∈ ℚ̂, which provides the projections π_{1} : ℙ & ℚ → ℙ and π_{2} : ℙ & ℚ → ℚ. More general, not just binary, products &_{i∈I} ℙ_{i} with projections π_{j}, for j ∈ I, are defined similarly. From the universal property of products, a collection of maps F_{i} : ℙ → ℙ_{i}, for i ∈ I, can be tupled together to form a unique map ⟨F_{i}⟩_{i∈I} : ℙ → &_{i∈I} ℙ_{i} with the property that π_{j} ∘ ⟨F_{i}⟩_{i∈I} = F_{j} for all j ∈ I. The empty product is given by 𝕆 and as the terminal object is associated with unique maps !_{ℙ} : ℙ → 𝕆, constantly ∅, for any path order ℙ.

Because there are empty presheaves we can define maps in Lin from products to tensors of path orders. For instance, in the binary case, σ : ℙ & ℚ → ℙ ⊗ ℚ in Lin is specified by (X, Y) ↦ (X ⊗ ∅) + (∅ ⊗ Y). The composition of such a map with the diagonal map of the product, viz.

δ_{ℙ} : ℙ ⟶^{diag} ℙ & ℙ ⟶^{σ} ℙ ⊗ ℙ

takes X to (X ⊗ ∅) + (∅ ⊗ X) and gives a weak form of diagonal map. Analogously, one can define general weak diagonal maps δ_{ℙ}_{k} : ℙ → ℙ⊗⋯⊗ℙ in Lin from ℙ to k copies of ℙ tensored together. Weak diagonal maps allow the same argument to be used in several different, though incompatible, ways.

3.5 Prefixed sums

The category Aff does not have coproducts (since all constant functors are maps of Aff there can be no initial object, so empty coproduct). However, we can build a useful sum in Aff with the help of the coproduct of Lin and lifting. Let ℙ_{α}, for α ∈ A, be a family of path orders. As their prefixed sum, Σ_{α∈A}αℙ_{α}, we take the disjoint union of the path orders ℙ_{α}_{⊥}, over the underlying set ⋃_{α∈A}{α}×ℙ_{α}_{⊥}; the latter path order forms a coproduct in Lin with the obvious injections in_{β} : ℙ_{β}_{⊥} → Σ_{α∈A}αℙ_{α}, for β ∈ A. The injections β : ℙ_{β} → Σ_{α∈A}αℙ_{α} in Aff, for β ∈ A, are defined to be the compositions β = in_{β}⌊−⌋. Finite prefixed sums are written α_{1}ℙ_{1} + ⋯ + α_{k}ℙ_{k}.

This construction is not a coproduct in Aff. However, it does satisfy a weaker property analogous to the universal property of a coproduct. Suppose F_{α} : ℙ_{α} → ℚ are maps in Aff for all α ∈ A. Then, there is a mediating map F : Σ_{α∈A}αℙ_{α} → ℚ in Lin determined to within isomorphism such that F ∘ α = F_{α} for all α ∈ A.

Suppose that the family of maps F_{α} : ℙ_{α} → ℚ, with α ∈ A, has the property that each F_{α} is constantly ∅ whenever α ∈ A is different from β and that F_{β} is H : ℙ_{β} → ℚ. Write H_{@β} : Σ_{α∈A}αℙ_{α} → ℚ for a choice of mediating map in Lin.

If a term t of type ℚ with free variable x of type ℙ_{β} denotes H : ℙ_{β} → ℚ in Aff and u is of type Σ_{α∈A}αℙ_{α}, then we shall write [u > β x ⇒ t] for H_{@β}(u). This construction “tests” or matches u against the pattern β x and passes the results of successful matches for x on to t; the possibly multiple results of successful matches are then summed together.

Because prefixed sum is not a coproduct we do not have that tensor distributes over prefixed sum. However there is a map dist : ℚ ⊗ Σ_{α∈A}αℙ_{α} → Σ_{α∈A}α(ℚ ⊗ ℙ_{α}) in Aff, expressing a form of distributivity, given as the extension H^{†} of the functor

\begin{matrix}H : ℚ_{⊥} × (Σ_{α∈A}αℙ_{α})_{⊥} → { \atop Σ_{α∈A}α(ℚ ⊗ ℙ_{α})} \\ H(q, (α, p)) = y_{Σ_{α∈A}α(ℚ⊗ℙ_{α})}(α, (q, p)), H(q, ⊥) = ∅ . \end{matrix}

3.6 Recursive type definitions

In modelling a process language like CCS but where processes are passed at channels a ∈ A, we require the “least” path orders that satisfy the following equations:

ℙ = τℙ + Σ_{a}a!ℂ + Σ_{a}a?𝔽 ℂ = ℙ ⊗ ℙ 𝔽 = ℙ ⊸ ℙ .

We can solve such recursive equations for path orders by several techniques, ranging from the sophisticated method of [7], providing inductive and coinductive characterisations, to simple methods essentially based on inductive definitions. Paralleling [14], path orders under the order

ℙ ⊴ ℚ ⟺ ℙ ⊆ ℚ and (∀p, p′ ∈ ℙ. p ≤_{ℙ} p′ ⟺ p ≤_{ℚ} p′)

form a (large) cpo with respect to which all the constructions we have just seen can be made Scott continuous. Solutions to equations like those above are then obtained as (simultaneous) least fixed points.

4 An affine-linear language for processes

Assume that path orders are presented using the constructions with the following syntax:

\begin{aligned}𝕋 ::= & 𝕆 | 𝕋_{1} ⊗ 𝕋_{2} | 𝕋_{1} ⊸ 𝕋_{2} | 𝕋_{1} & 𝕋_{2} | Σ_{α∈A}α𝕋_{α} | \\ & P | μ_{j}P_{1}, …, P_{k}.(𝕋_{1}, …, 𝕋_{k}) \end{aligned}

All the constructions have been met earlier with the exception of the notation for recursively defined path orders. P is drawn from a set of variables used in the recursive definition of path orders; μ_{j}P_{1}, …, P_{k}.(𝕋_{1}, …, 𝕋_{k}) stands for the j-component (1 ≤ j ≤ k) of the least solution to the defining equations

P_{1} = 𝕋_{1} , …, P_{k} = 𝕋_{k} ,

in which the expressions 𝕋_{1}, …, 𝕋_{k} may contain the P_{j}’s. We’ll write μP⃗ .𝕋⃗ as an abbreviation for the k-tuple with j-component μ_{j}P_{1}, …, P_{k}.(𝕋_{1}, …, 𝕋_{k}), and confuse a closed expression for a path order with the path order itself.

The operations of Section 3 form the basis of a syntax of terms:

t, u, ⋯::=

x, y, z, … |  (Variables)
∅ | Σ_{i∈I}t_{i} |  (Sums of terms)
rec x.t |  (Recursive definition)
λx.t | t u |  (Abstraction and application)
α t | [u > α x ⇒ t] |  (Injections and match for prefixed sums)

(t, u) | [u > (x, −) ⇒ t] |

[u > (−, x) ⇒ t] | (Pairing and match for products)
t ⊗ u | [u > x ⊗ y ⇒ t] (Tensor operation and match)

The syntax will be subject to typing and linearity constraints. The language is similar to that in [1], being based on a form of pattern matching. Accordingly, variables like x in the match [u > α x ⇒ t] are binding occurrences and bind later occurrences of the variable in the body t. We shall take for granted an understanding of free and bound variables, and substitution on raw terms.

Let ℙ_{1}, …, ℙ_{k}, ℚ be closed expressions for path orders and let the variables x_{1}, …, x_{k} be distinct. A syntactic judgement x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ stands for a map

⟦x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ⟧ : ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} → ℚ

in Aff. We shall typically write Γ, or Δ, for an environment list x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} and most often abbreviate the denotation to ℙ_{1}⊗⋯⊗ℙ_{k} ⟶^{t} ℚ, or even Γ ⟶^{t} ℚ. When the environment list is empty, the corresponding tensor product is the empty path order 𝕆.

An affine-linear language will restrict copying and so substitutions of a common term into distinct variables. The counterpart in the model is the absence of a suitable diagonal map from objects ℙ to ℙ ⊗ ℙ. Consider a term t(x, y), with its free variables x and y shown explicitly, for which

x : ℙ, y : ℙ ⊢ t(x, y) : ℚ ,

corresponding to a map ℙ⊗ℙ ⟶^{t(x, y)} ℚ in Aff. This does not generally entail that x : ℙ ⊢ t(x, x) : ℚ—there may not be a corresponding map in Aff, for example if t(x, y) = x⊗y. There is however a condition on how the variables x and y occur in t which ensures that the judgement x : ℙ ⊢ t(x, x) : ℚ holds and that it denotes the map in Aff obtained as the composition

ℙ ⟶^{δ_{ℙ}} ℙ ⊗ ℙ ⟶^{t(x, y)} ℚ

—using the weak diagonal map seen earlier in Section 3.4. Syntactically, this is assured if the variables x and y are not crossed in t according to the following definition:

Definition 4.1 Let t be a raw term. Say a set of variables V is crossed in t iff there are subterms of t of the form tensor t_{1} ⊗ t_{2}, application (t_{1} t_{2}), or match [t_{1} > p ⇒ t_{2}], for which t has free occurrences of variables from V appearing in both t_{1} and t_{2}.

The term-formation rules for the affine language are listed below alongside their interpretations as constructors on morphisms, taking the morphisms denoted by the premises to that denoted by the conclusion (cf. [2]).

Structural rules:

\overline{x : ℙ ⊢ x : ℙ}  \overline{ℙ ⟶^{1_{ℙ}} ℙ}

\frac{Δ ⊢ t : ℙ}{Γ, Δ ⊢ t : ℙ}  \frac{Δ ⟶^{t} ℙ}{Γ ⊗ Δ ⟶^{!_{Γ} ⊗ t} 𝕆 ⊗ ℙ ≅ ℙ}

\frac{Γ, x : ℙ, y : ℚ, Δ ⊢ t : ℝ}{Γ, y : ℚ, x : ℙ, Δ ⊢ t : ℝ} \frac{Γ ⊗ ℙ ⊗ ℚ ⊗ Δ ⟶^{t} ℝ}{Γ ⊗ ℚ ⊗ ℙ ⊗ Δ ≅ Γ ⊗ ℙ ⊗ ℚ ⊗ Δ ⟶^{t} ℝ}

Recursive path orders:

\frac{Γ ⊢ t : 𝕋_{j}[μP⃗ .𝕋⃗/P⃗]}{Γ ⊢ t : μ_{j}P⃗ .𝕋⃗} ; \frac{Γ ⊢ t : μ_{j}P⃗ .𝕋⃗}{Γ ⊢ t : 𝕋_{j}[μP⃗ .𝕋⃗/P⃗]}

The premise and conclusion are interpreted as the same map because μ_{j}P⃗ .𝕋⃗ and 𝕋_{j}[μP⃗ .𝕋⃗/P⃗] denote equal path orders.

Sums of terms:

\overline{Γ ⊢ ∅ : ℙ}  \overline{Γ ⟶^{∅} ℙ}

\frac{Γ ⊢ t_{i} : ℙ for all i ∈ I}{Γ ⊢ Σ_{i∈I}t_{i} : ℙ} \frac{Γ ⟶^{t_{i}} ℙ for all i ∈ I}{Γ ⟶^{⟨t_{i}⟩_{i∈I}} &_{i∈I} ℙ ⟶^{Σ} ℙ}

Recursive definition:

\frac{Γ, x : ℙ ⊢ t : ℙ \{y, x\} is not crossed in t for any y in Γ.}{Γ ⊢ rec x.t : ℙ} \frac{Γ ⊗ ℙ ⟶^{t} ℙ}{Γ ⟶^{fix G} ℙ}

Here, with F : Γ → ℙ the map G(F) : Γ → ℙ is the composition

Γ ⟶^{δ_{Γ}} Γ ⊗ Γ ⟶^{1_{Γ} ⊗ F} Γ ⊗ ℙ ⟶^{t} ℙ .

Abstraction and application:

\frac{Γ, x : ℙ ⊢ t : ℚ}{Γ ⊢ λx.t : ℙ ⊸ ℚ}  \frac{Γ ⊗ ℙ ⟶^{t} ℚ}{Γ ⟶^{curry t} ℙ ⊸ ℚ}

\frac{Γ ⊢ t : ℙ ⊸ ℚ Δ ⊢ u : ℙ}{Γ, Δ ⊢ t u : ℚ} \frac{Γ ⟶^{t} ℙ ⊸ ℚ Δ ⟶^{u} ℙ}{Γ ⊗ Δ ⟶^{t ⊗ u} (ℙ ⊸ ℚ) ⊗ ℙ ⟶^{app} ℚ}

Injections and match for prefixed sums:

\frac{Γ ⊢ t : ℙ_{β} , where β ∈ A}{Γ ⊢ β t : Σ_{α∈A}αℙ_{α}} \frac{Γ ⟶^{t} ℙ_{β} , where β ∈ A}{Γ ⟶^{t} ℙ_{β} ⟶^{β} Σ_{α∈A}αℙ_{α}}

\frac{Γ, x : ℙ_{β} ⊢ t : ℚ , where β ∈ A Δ ⊢ u : Σ_{α∈A}αℙ_{α}}{Γ, Δ ⊢ [u > β x ⇒ t] : ℚ}

\frac{Γ ⊗ ℙ_{β} ⟶^{t} ℚ , where β ∈ A Δ ⟶^{u} Σ_{α∈A}αℙ_{α}}{Γ ⊗ Δ ⟶^{1_{Γ} ⊗ u} Γ ⊗ Σ_{α∈A}αℙ_{α} ⟶^{t_{@β} ∘ dist} ℚ}

Pairing and match for products:

\frac{Γ ⊢ t : ℙ Γ ⊢ u : ℚ}{Γ ⊢ (t, u) : ℙ & ℚ}  \frac{Γ ⟶^{t} ℙ Γ ⟶^{u} ℚ}{Γ ⟶^{⟨t, u⟩} ℙ & ℚ}

\frac{Γ, x : ℙ ⊢ t : ℝ Δ ⊢ u : ℙ & ℚ}{Γ, Δ ⊢ [u > (x, −) ⇒ t] : ℝ} \frac{Γ ⊗ ℙ ⟶^{t} ℝ Δ ⟶^{u} ℙ & ℚ}{Γ ⊗ Δ ⟶^{1_{Γ} ⊗ (π_{1} ∘ u)} Γ ⊗ ℙ ⟶^{t} ℝ}

\frac{Γ, x : ℚ ⊢ t : ℝ Δ ⊢ u : ℙ & ℚ}{Γ, Δ ⊢ [u > (−, x) ⇒ t] : ℝ} \frac{Γ ⊗ ℚ ⟶^{t} ℝ Δ ⟶^{u} ℙ & ℚ}{Γ ⊗ Δ ⟶^{1_{Γ} ⊗ (π_{2} ∘ u)} Γ ⊗ ℚ ⟶^{t} ℝ}

Tensor operation and match:

\frac{Γ ⊢ t : ℙ Δ ⊢ u : ℚ}{Γ, Δ ⊢ t ⊗ u : ℙ ⊗ ℚ}  \frac{Γ ⟶^{t} ℙ Δ ⟶^{u} ℚ}{Γ ⊗ Δ ⟶^{t ⊗ u} ℙ ⊗ ℚ}

\frac{Γ, x : ℙ, y : ℚ ⊢ t : ℝ Δ ⊢ u : ℙ ⊗ ℚ}{Γ, Δ ⊢ [u > x ⊗ y ⇒ t] : ℝ} \frac{Γ ⊗ ℙ ⊗ ℚ ⟶^{t} ℝ Δ ⟶^{u} ℙ ⊗ ℚ}{Γ ⊗ Δ ⟶^{1_{Γ} ⊗ u} Γ ⊗ ℙ ⊗ ℚ ⟶^{t} ℝ}

Proposition 4.2 Suppose Γ, x : ℙ ⊢ t : ℚ. The set {x} is not crossed in t.

Exploiting the naturality of the various operations used in the semantic definitions, we can prove a general substitution lemma.

Lemma 4.3 (Substitution) Suppose Γ, x_{1} : ℙ, …, x_{k} : ℙ ⊢ t : ℚ and that the set of variables {x_{1}, …, x_{k}} is not crossed in t. Suppose Δ ⊢ u : ℙ where the variables of Γ and Δ are disjoint. Then, Γ, Δ ⊢ t[u/x_{1}, …, u/x_{k}] : ℚ and, (suppressing the types for brevity)

⟦t[u/x_{1}, …, u/x_{k}]⟧ ≅ ⟦t⟧ ∘ (1_{Γ} ⊗ (δ_{ℙ}_{k} ∘ ⟦u⟧)) .

Note that in the case where k = 1, the lemma specialises to ⟦t[u/x]⟧ ≅ ⟦t⟧ ∘ (1_{Γ} ⊗ ⟦u⟧). A particular consequence is that linear application amounts to substitution:

Lemma 4.4 If Γ ⊢ (λx.t) u : ℚ, then Γ ⊢ t[u/x] : ℚ and

⟦Γ ⊢ (λx.t) u : ℚ⟧ ≅ ⟦Γ ⊢ t[u/x] : ℚ⟧ .

Similarly, we have the expected result for recursion:

Lemma 4.5 If Γ ⊢ rec x.t : ℙ, then Γ ⊢ t[rec x.t/x] : ℙ and

⟦Γ ⊢ rec x.t : ℙ⟧ ≅ ⟦Γ ⊢ t[rec x.t/x] : ℙ⟧ .

The next lemma follows directly from the universal properties of prefixed sum (the last property because the mediating map is in Lin):

Lemma 4.6 Properties of prefix match:

(i) ⟦Γ ⊢ [α u > α x ⇒ t] : ℚ⟧ ≅ ⟦Γ ⊢ t[u/x] : ℚ⟧
(ii) ⟦Γ ⊢ [α u > β x ⇒ t] : ℚ⟧ ≅ ∅ if α ≠ β
(iii) ⟦Γ ⊢ [Σ_{i∈I}u_{i} > α x ⇒ t] : ℚ⟧ ≅ ⟦Γ ⊢ Σ_{i∈I}[u_{i} > α x ⇒ t] : ℚ⟧

General patterns It will be convenient for the examples of the next Section to allow general patterns according to

p ::= x | α p | (p, −) | (−, p) | p ⊗ q

—with p being well-formed if all its variables are distinct. A match

[u > p ⇒ t]

is understood inductively as an abbreviation for a term in the affine-linear language, according to

[u > x ⇒ t] ≡ (λx.t) u
[u > α p ⇒ t] ≡ [u > α x ⇒ [x > p ⇒ t]]  x fresh
[u > (p, −) ⇒ t] ≡ [u > (x, −) ⇒ [x > p ⇒ t]]  x fresh
[u > (−, p) ⇒ t] ≡ [u > (−, x) ⇒ [x > p ⇒ t]]  x fresh
[u > p ⊗ q ⇒ t] ≡ [u > x ⊗ y ⇒ [x > p ⇒ [y > q ⇒ t]]] x, y fresh

We write

[u_{1} > p_{1}, …, u_{k} > p_{k} ⇒ t]

as an abbreviation of

[u_{1} > p_{1} ⇒ [⋯ [u_{k} > p_{k} ⇒ t] ⋯]] .

5 Examples

The affine-linear language is remarkably expressive, as the following examples show. Having denotations in Aff, all operations expressible in the language will automatically preserve open-map bisimulation.

5.1 CCS

As in CCS, assume a set of labels A, a complementation operation producing ā from a label a, with ¯ ā = a, and a distinct label τ. We can specify the path order ℙ as

ℙ = τℙ + Σ_{a∈A}aℙ .

Let α range over A ∪ {τ}. The CCS parallel composition can be defined as the following term Par of type ℙ ⊸ (ℙ ⊸ ℙ):

rec P.λx.λy.Σ_{α}[x > α x′ ⇒ α (P x′ y)] +
Σ_{α}[y > α y′ ⇒ α (P x y′)] +
Σ_{a∈A}[x > a x′, y > ā y′ ⇒ τ (P x′ y′)] .

The other CCS operations are easy to encode. Here, open-map bisimulation coincides with strong bisimulation. We can recover the expansion law for general reasons. Write X|Y for Par X Y with X, Y terms of type ℙ. Suppose X = Σ_{α}Σ_{i∈I(α)}α X_{i} and Y = Σ_{α}Σ_{j∈J(α)}α Y_{j}. Using Lemmas 4.5 and 4.4, then Lemma 4.6, we get

X|Y ≅ Σ_{α}[X > α x′ ⇒ α (x′|Y)] +
Σ_{α}[Y > α y′ ⇒ α (X|y′)] +
Σ_{a∈A}[X > a x′, Y > ā y′ ⇒ τ (x′|y′)]
≅ Σ_{α}Σ_{i∈I(α)}α (X_{i}|Y) +
Σ_{α}Σ_{j∈J(α)}α (X|Y_{j}) +
Σ_{a∈A}Σ_{i∈I(a),j∈J(ā)}τ (X_{i}|Y_{j}) .

In similar ways it is easy to express CSP and any parallel composition given by a synchronisation algebra [20] in the affine-linear language.

5.2 A linear higher-order process language

Recall from Section 3.6 the path orders for processes, concretions and abstractions for a higher-order language. We are chiefly interested in the parallel composition of processes, Par_{ℙ,ℙ}, this time of the uncurried type ℙ ⊗ ℙ ⊸ ℙ for clarity. But parallel composition is really a family of mutually dependent operations also including components such as Par_{𝔽,ℂ} of type 𝔽 ⊗ ℂ ⊸ ℙ to say how abstractions compose in parallel with concretions etc. All these components can be tupled together in a product using &, and parallel composition defined as a simultaneous recursive definition whose component at ℙ ⊗ ℙ ⊸ ℙ satisfies

P |Q = Σ_{α}[P > α x ⇒ α (x|Q)] +
Σ_{α}[Q > α y ⇒ α (P |y)] +
Σ_{a}[P > a? f, Q > a! (s ⊗ r) ⇒ τ ((f s)|r)] +
Σ_{a}[P > a! (s ⊗ r), Q > a? f ⇒ τ (r|(f s))] ,

where, e.g., P |Q abbreviates Par_{ℙ,ℙ} (P ⊗ Q). In the summations a ∈ A and α ranges over a!, a?, τ.

5.3 Mobile ambients with public names

We can translate the Ambient Calculus with public names [4] into the affinelinear language, following similar lines to the linear process-passing language above. Assume a fixed set of ambient names n, m, … ∈ N. Following [5], the syntax of ambients is extended beyond just processes (P) to include concretions (C) and abstractions (F):

P ::= ∅ | P |P | rep P | n[P] | in n P | out n P |
open n! P | τ P | mvin n! C | mvout n! C |
open n? P | mvin n? F | x
C ::= P ⊗ P
F ::= λx.P

The notation for actions departs a little from that of [5]. Here some actions are marked with ! and others with ?—active (or inceptive) actions are marked by ! and passive (or receptive) actions by ?. We say actions α and β are complementary iff one has the form open n! or mvin n! while the other is open n? or mvin n? respectively. Complementary actions can synchronise together to form a τ-action. We adopt a slightly different notation for concretions (P ⊗ R instead of ⟨P ⟩R) and abstractions (λx.P instead of (x)P) to make their translation into the affine-linear language clear.

The usual conventions are adopted for variables. Terms are assumed to be linear, in that a variable appears on at most one side of any parallel compositions within the term, and subterms of the form rep P are closed. A replication rep P is intended to behave as P | rep P so readily possesses a recursive definition in the affine-linear language.

Suitable path orders for ambients are given recursively by:

ℙ = τℙ + Σ_{n}in nℙ + Σ_{n}out nℙ + Σ_{n}open n!ℙ +
Σ_{n}mvin n!ℂ + Σ_{n}mvout n!ℂ + Σ_{n}open n?ℙ +
Σ_{n}mvin n?𝔽
ℂ = ℙ ⊗ ℙ
𝔽 = ℙ ⊸ ℙ

Here, n ranges over the set of names N. The eight components of the prefixed sum in the equation for ℙ correspond to eight forms of ambient actions: τ, in n, out n, open n!, mvin n!, mvout n!, open n?, and mvin n?. We obtain the prefixing operations as injections into the appropriate component of the prefixed sum ℙ.

Parallel composition is really a family of operations, one of which is a binary operation between processes but where in addition there are parallel compositions of abstractions with concretions, and even abstractions with processes and concretions with processes. The family of operations

\begin{matrix}(−|−) : 𝔽 ⊗ ℂ ⊸ ℙ, & (−|−) : ℂ ⊗ 𝔽 ⊸ ℙ, \\ (−|−) : 𝔽 ⊗ ℙ ⊸ 𝔽, & (−|−) : ℙ ⊗ 𝔽 ⊸ 𝔽, \\ (−|−) : ℂ ⊗ ℙ ⊸ ℂ, & (−|−) : ℙ ⊗ ℂ ⊸ ℂ \end{matrix}

are defined in a simultaneous recursive definition:

Processes in parallel with processes:

P |Q = Σ_{α}[P > α x ⇒ α (x|Q)] +
Σ_{α}[Q > α y ⇒ α (P |y)] +
Σ_{n}[P > open n! x, Q > open n? y ⇒ τ (x|y)] +
Σ_{n}[P > open n? x, Q > open n! y ⇒ τ (x|y)] +
Σ_{n}[P > mvin n? f, Q > mvin n! (s ⊗ r) ⇒ τ ((f s)|r)] +
Σ_{n}[P > mvin n! (s ⊗ r), Q > mvin n? f ⇒ τ (r|(f s))]

Abstractions in parallel with concretions: F |C = [C > s ⊗ r ⇒ (F s)|r]

Abstractions in parallel with processes: F |P = λx.((F x)|P)

Concretions in parallel with processes: C|P = [C > s ⊗ r ⇒ s ⊗ (r|P)]

The remaining cases are given symmetrically.

Presheaves X, Y over ℙ will have decompositions into rooted components, and by Lemma 4.6, their parallel composition satisfies the obvious expansion law.

Ambient creation can be defined recursively in the affine-linear language:

m[P] = [P > τ x ⇒ τ m[x]] +
Σ_{n}[P > in n x ⇒ mvin n! (m[x] ⊗ ∅)] +
Σ_{n}[P > out n x ⇒ mvout n! (m[x] ⊗ ∅)] +
[P > mvout m! (s ⊗ r) ⇒ τ (s|m[r])] +
open m? P +
mvin m? λy.m[P |y] .

The denotations of ambients are determined by their capabilities: an ambient m[P] can perform the internal (τ) actions of P, enter a parallel ambient (mvin n!) if called upon to do so by an in n-action of P, exit an ambient n (mvout n!) if P so requests through an out n-action, be exited if P so requests through an mvout m!-action, be opened (open m?), or be entered by an ambient (mvin m?); initial actions of other forms are restricted away. Ambient creation is at least as complicated as parallel composition. This should not be surprising given that ambient creation corresponds intuitively to putting a process behind (so in parallel with) a wall or membrane which if unopened mediates in the communications the process can do, converting some actions to others and restricting some others away. The tree-containment structure of ambients is captured in the chain of open m?’s that they can perform.

By the properties of prefix-match (Lemma 4.6), there is an expansion theorem for ambient creation. For X with decomposition X = Σ_{α}Σ_{i∈X(α)}α X_{i}, where α ranges over atomic actions of ambients,

m[X] ≅ Σ_{i∈X(τ)}τ m[X_{i}] +
Σ_{n}Σ_{j∈X(in n)}mvin n! (m[X_{j}] ⊗ ∅) +
Σ_{n}Σ_{k∈X(out n)}mvout n! (m[X_{k}] ⊗ ∅) +
Σ_{l∈X(mvout m!)}[X_{l} > s ⊗ r ⇒ τ (s|m[r])] +
open m?X +
mvin m?(λy.m[X|y]) .

5.4 Nondeterministic dataflow

The affine-linear language allows us to define processes of the kind encountered in treatments of nondeterministic dataflow. Define ℙ recursively so that ℙ = aℙ + bℙ, consisting of streams (or sequences) of a’s and b’s.

The recursively defined process A : ℙ ⊸ ℙ selects and outputs a’s while ignoring all b’s:

A = λx. [x > a x′ ⇒ a (A x′)] + [x > b x′ ⇒ A x′]

The recursively defined process F : ℙ ⊗ ℙ produces two identical, parallel streams of a’s and b’s as output:

F = [F > z_{1} ⊗ z_{2} ⇒ (a z_{1}) ⊗ (a z_{2}) + (b z_{1}) ⊗ (b z_{2})]

The recursively defined process S : ℙ ⊸ (ℙ ⊗ ℙ) separates a stream of a’s and b’s into two streams, the first consisting solely of a’s and the second solely of b’s:

\begin{aligned}S = λx. & [x > a x′, (S x′) > z_{1} ⊗ z_{2} ⇒ (a z_{1}) ⊗ z_{2}] + \\ & [x > b x′, (S x′) > z_{1} ⊗ z_{2} ⇒ z_{1} ⊗ (b z_{2})] \end{aligned}

A subcategory of Aff supports a “trace operation” to represent processes with feedback loops (see [9]). The trace operation is, however, not definable in the present affine-linear language. It can be shown that if the trace operation of [9] were definable in the presheaf semantics, we could obtain (replacing Set by 2) a compositional relational semantics of nondeterministic dataflow with feedback, shown impossible by Brock&Ackerman [3].

6 Operational semantics

We now consider the tensor fragment of the affine-linear language, the fragment obtained by leaving out product (for brevity) and function space (in progress).

We employ the language of general patterns of Section 4. It can be given semantics using judgements of the form

x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊩ p : ℙ

with the x_{i} distinct, interpreted as functors

(ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k})_{⊥} ⟶^{p} ℙ_{⊥}

according to the rules (the rule identifying a recursive type with its unfolding is omitted)

\overline{x : ℙ ⊩ x : ℙ}  \overline{ℙ_{⊥} ⟶^{1} ℙ_{⊥}}

\frac{Π ⊩ p : ℙ_{α} α ∈ A}{Π ⊩ α p : Σ_{α∈A}αℙ_{α}}  \frac{Π_{⊥} ⟶^{p} ℙ_{α}_{⊥} α ∈ A}{Π_{⊥} ⟶^{⌊in_{α} p⌋} (Σ_{α∈A}αℙ_{α})_{⊥}}

\frac{Π ⊩ p : ℙ Λ ⊩ q : ℚ}{Π, Λ ⊩ p ⊗ q : ℙ ⊗ ℚ} \frac{Π_{⊥} ⟶^{p} ℙ_{⊥} Λ_{⊥} ⟶^{q} ℚ_{⊥}}{(Π ⊗ Λ)_{⊥} ⟶^{p × q} (ℙ ⊗ ℚ)_{⊥}}

As there are no rules for weakening or exchange, the environment Π for which Π ⊩ p : ℙ is given uniquely by p and ℙ. We’ll only need the sub-language

p ::= α x | p ⊗ x | x ⊗ p .

Here, the interpretations map into non-⊥ elements and, accordingly, we may view ⟦Π ⊩ p : ℙ⟧ as a functor into ℙ rather than ℙ_{⊥}. We obtain atomic paths as images ⟦Π ⊩ p : ℙ⟧(⊥) ∈ ℙ for which we’ll write

a ::= α ⊥ | a ⊗ ⊥ | ⊥ ⊗ a .

Conversely, for each a we may recover a pattern p_{a} (unique up to variable names) by replacing all ⊥’s of a with distinct variables. We let atomic paths stand for patterns and write

ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} ⊩ a : ℙ

if x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊩ p_{a} : ℙ. Notice that (ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k})_{⊥}, uniquely given by a and ℙ, is isomorphic to the path order above a ∈ ℙ. We’ll write α for α ⊥.

Given ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} ⊩ a : ℙ and ⊢ t : ℙ, we may restrict ⟦⊢ t : ℙ⟧ to (ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k})_{⊥} by applying the map a^{∗} : ℙ → (ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k})_{⊥} of Lin got by composition as X ↦ X(a−). (More generally, we may compose a^{∗} with the maps of Aff interpreting open terms, so making sense of (semantic) expressions like a^{∗}t when ℙ′ ⊩ a : ℙ and Γ ⊢ t : ℙ.) Identifying t with its denotation, we see that a^{∗}t is a presheaf over a lifted path order and therefore has a decomposition as a sum of rooted presheaves by Proposition 2.1. It turns out that each rooted component has the form ⌊t′⌋ for a denotation t′ of a term of type ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k}. Judgements t ⟶^{a} t′ in the operational semantics will express that ⌊t′⌋ is a rooted component of a^{∗}t. In fact, derivations of transitions t ⟶^{a} t′ will be in 1-1 correspondence with components of the decomposition of a^{∗}t.

The operational semantics is informed by isomorphisms saying how to find the rooted components of a^{∗}t. As an example we have the isomorphisms on the left below, suggesting the rules on the right:

\begin{matrix}β^{∗}(α t) ≅ \begin{cases}⌊t⌋ & if α = β \\ ∅ & if α ≠ β \end{cases} & \overline{α t ⟶^{α} t} \\ a^{∗}Σ_{i∈I}t_{i} ≅ Σ_{i∈I}a^{∗}t_{i} & \frac{t_{j} ⟶^{a} t′}{Σ_{i∈I}t_{i} ⟶^{a} t′} j ∈ I \end{matrix}

These rules are for closed terms. In the semantics

a^{∗}[u > x ⊗ y ⇒ t] ≅ [u > x ⊗ y ⇒ a^{∗}t] ,

which suggests that we let t (an open term) take an a-transition in the “environment” u > x ⊗ y. Syntactically, environments e are lists of such matches. An environment “exports” a set of variables; the empty environment exports the empty set, while e, u > x ⊗ y exports what e exports, except the free variables of u, plus x and y. We may formalise this using a judgement

e ⊢ x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k}

(with the x_{i} distinct) which denotes the same presheaf over ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} as [e ⇒ x_{1} ⊗ ⋯ ⊗ x_{k}]. A term t in environment e will be written e ⤇ t. For e ⊢ Γ, Δ and Γ ⊢ t : ℙ, we give the judgement

⊢ e ⤇ t : ℙ; Δ

the same denotation as the term [e ⇒ t ⊗ x_{1} ⊗ ⋯ ⊗ x_{k}] where the x_{i} are now the variables exported by e but not free in t.

Incorporating such environments, the operational rules are:

\frac{e_{1} ⤇ u ⟶^{a ⊗ ⊥} e′_{1} ⤇ u′}{e_{1}, u > x ⊗ y, e_{2} ⤇ x ⟶^{a} e′_{1}, u′ > x ⊗ y, e_{2} ⤇ x}

\frac{e_{1} ⤇ u ⟶^{⊥ ⊗ a} e′_{1} ⤇ u′}{e_{1}, u > x ⊗ y, e_{2} ⤇ y ⟶^{a} e′_{1}, u′ > x ⊗ y, e_{2} ⤇ y}

\frac{e ⤇ t_{j} ⟶^{a} e′ ⤇ t′}{e ⤇ Σ_{i∈I}t_{i} ⟶^{a} e′ ⤇ t′} j ∈ I \frac{e ⤇ t[rec x.t/x] ⟶^{a} e′ ⤇ t′}{e ⤇ rec x.t ⟶^{a} e′ ⤇ t′}

\overline{e ⤇ α t ⟶^{α} e ⤇ t}  \frac{e ⤇ u ⟶^{α} e′ ⤇ u′ e′ ⤇ t[u′/x] ⟶^{a} e′′ ⤇ t′}{e ⤇ [u > α x ⇒ t] ⟶^{a} e′′ ⤇ t′}

\frac{e ⤇ t ⟶^{a} e′ ⤇ t′}{e ⤇ t ⊗ u ⟶^{a ⊗ ⊥} e′ ⤇ t′ ⊗ u}  \frac{e ⤇ u ⟶^{a} e′ ⤇ u′}{e ⤇ t ⊗ u ⟶^{⊥ ⊗ a} e′ ⤇ t ⊗ u′}

\frac{e, u > x ⊗ y ⤇ t ⟶^{a} e′, u′ > x ⊗ y ⤇ t′}{e ⤇ [u > x ⊗ y ⇒ t] ⟶^{a} e′ ⤇ [u′ > x ⊗ y ⇒ t′]}

In the last-mentioned rule, the variables x and y are implicitly renamed to avoid overshadowing of exported variables in the environment e, u > x ⊗ y. The rules are well-typed:

Lemma 6.1 Assume ⊢ e ⤇ t : ℙ; Δ. If e ⤇ t ⟶^{a} e′ ⤇ t′ then ℙ′ ⊩ a : ℙ and ⊢ e′ ⤇ t′ : ℙ′; Δ.

An ordinal size measure can be defined on terms in environments in such a way that transitions are accompanied by a decrease in size if we replace general recursion by finite unfoldings. Building on this fact, we can prove the main result below which says that rooted components correspond to derivations. It is proved by well-founded induction using an order based on the size measure. The induction hypothesis says that for ⊢ e ⤇ t : ℙ; Δ and ℙ′ ⊩ a : ℙ with x⃗ ≡ x_{1} ⊗ ⋯ ⊗ x_{k} any subset of the variables in Δ, we have (a ⊗ ⊥)^{∗}[e ⇒ t ⊗ x⃗] ≅ Σ_{d}⌊[e′ ⇒ t′ ⊗ x⃗]⌋ where d ranges over derivations with conclusion of the form e ⤇ t ⟶^{a} e′ ⤇ t′.

Theorem 6.2 Assume ⊢ t : ℙ and ℙ′ ⊩ a : ℙ. Then a^{∗}t ≅ Σ_{d}⌊t′⌋ where the sum is over all derivations d with conclusion ⤇ t ⟶^{a} ⤇ t′.

As the operational semantics stands it gives an interleaving model of the tensor fragment. We have been able to represent the definable presheaves of the tensor fragment as event structures, a representation in which the tensor operation denotes the simple parallel composition of event structures got by juxtaposition; elements of definable presheaves correspond to finite configurations of the event-structure representation, with restriction in the presheaf matched by restriction to a subconfiguration in the event structure [18]. We are currently working on exhibiting the operational semantics as a transition system with independence [20] in order to strengthen the correspondence with the presheaf semantics begun in Theorem 6.2.

7 Nonlinearity

Of course code can be copied, and this may lead to maps which are not linear. According to the discipline of linear logic, nonlinear maps from ℙ to ℚ are introduced as linear maps from !ℙ to ℚ—the exponential ! applied to ℙ allows arguments from ℙ to be copied and discarded freely.

In the domain model of linear logic (see Section 3) !ℙ can be taken to be the finite-join completion of ℙ. Then, the nonlinear maps in the coKleisli category of ! correspond to Scott continuous functions. A close analogue for presheaf models is to interpret !ℙ as the finite-colimit completion of ℙ. Note that now !ℙ is a category, and no longer just a partial order. With this understanding of !ℙ, it can be shown that ℙ̂ with the inclusion functor !ℙ → ℙ̂ is the free filtered-colimit completion of !ℙ—see [13]. It follows that maps !ℙ → ℚ in Lin correspond, to within isomorphism, to continuous (i.e., filtered-colimit preserving) functors ℙ̂ → ℚ̂. But, unfortunately, continuous functors from ℙ̂ to ℚ̂ need not send open maps to open maps. This raises the question of whether other choices of exponential fit in better with bisimulation.

Bear in mind the intuition that objects of ℙ correspond to the shapes of computation path a process, represented as a presheaf in ℙ̂, might perform. An object of !ℙ should represent a computation path of an assembly of processes each with computation-path shapes in ℙ—the assembly of processes can then be a collection of copies of a process, possibly at different states. If we take !ℙ to be the finite-colimit completion of ℙ, an object of !ℙ, as a finite colimit, would express how paths coincide initially and then branch. One way to understand this object as a computation path of an assembly of processes is that the assembly of processes is not fixed once and for all. Rather the assembly grows as further copies are invoked, and these copies can be made of processes after they have run for a while. The copies can then themselves be run and the resulting processes copied. In this way, by keeping track of the origins of copies, we can account for the identifications of sub-paths.

This intuition suggests exploring other less liberal ways of copying, e.g. without being able to copy after some initial run. We will discover candidates for exponentials !ℙ based on computation-path shapes of simple assemblies of processes, ones built out of indexed families. We start with an example.

7.1 An example

Since both sum and tensor preserve open maps, the functor copy taking a presheaf X over ℙ to the presheaf

copy(X) = 1 + X + X^{2} + ⋯ + X^{k} + ⋯
over  !ℙ = 𝟙 + ℙ + ℙ^{2} + ⋯ + ℙ^{k} + ⋯

will preserve open maps. Here the superscripts abbreviate repeated applications of tensor in Lin. So ℙ^{k} is the product of k copies of the partial order ℙ, in which the objects are k-tuples of objects of ℙ—in particular, 𝟙 is the partial order consisting solely of the empty tuple called 1 above. The presheaf X^{k} comprises k copies of X tensored together, so that X^{k}⟨p_{1}, …, p_{k}⟩ = X(p_{1}) × ⋯ × X(p_{k}).

By supplying “coefficients” we can obtain various nonlinear maps. An appropriate form of polynomial is given by a functor F : !ℙ → ℚ̂, which splits up into a family of functors F_{k} : ℙ^{k} → ℚ̂ , for k ∈ ω. We can extend F to a functor F [−] = F · copy(−) : ℙ̂ → ℚ̂. For X ∈ ℙ̂,

F [X] = F_{0} + F_{1} · X + F_{2} · X^{2} + ⋯ + F_{k} · X^{k} + ⋯

Because F · − is colimit-preserving it preserves open maps. So does copy. Hence F [−] preserves open maps.

Note, that the original polynomial F is not determined to within isomorphism by the functor F [−] it induces. (We can only hope for such uniqueness if we restrict to polynomials which are symmetric, i.e., such that F_{k} ≅ F_{k} ∘ π for all permutations π of the k arguments.)

We write Poly(ℙ, ℚ) for the functor category [!ℙ, ℚ̂] of polynomials from ℙ to ℚ. To compose polynomials F ∈ Poly(ℙ, ℚ) and G ∈ Poly(ℚ, ℝ) we first define F^{!} ∈ Poly(ℙ,!ℚ) by taking F^{!}⟨p_{1}, …, p_{n}⟩⟨q_{1}, …, q_{k}⟩ to be

Σ_{μ⟨s_{1},...,s_{k}⟩=⟨p_{1},...,p_{n}⟩}F s_{1}q_{1} × ⋯ × F s_{k}q_{k} ,

when ⟨p_{1}, …, p_{n}⟩ ∈ !ℙ and ⟨q_{1}, …, q_{k}⟩ ∈ !ℚ. The operation μ : !!ℙ → ℙ flattens, by concatenation, a tuple ⟨s_{1}, …, s_{k}⟩ of tuples s_{r} = ⟨s_{r1}, …, s_{rm_{r}}⟩, for 1 ≤ r ≤ k, down to a tuple

μ⟨s_{1}, …, s_{k}⟩ = ⟨s_{11}, …, s_{1m_{1}}, …, s_{k1}, …, s_{km_{k}}⟩ .

So, the sum is indexed by all ways to partition ⟨p_{1}, …, p_{n}⟩ into tuples ⟨s_{1}, …, s_{k}⟩. Now, we can define the composition of polynomials to be G∘F = G · (F^{!}−) ∈ Poly(ℙ, ℝ). At ⟨p_{1}, …, p_{n}⟩ in !ℙ, G ∘ F ⟨p_{1}, …, p_{n}⟩ equals

Σ_{μ⟨s_{1},...,s_{k}⟩=⟨p_{1},...,p_{n}⟩}G_{k} · F s_{1} × ⋯ × F s_{k} ,

with F s_{1} × ⋯ × F s_{k}⟨q_{1}, …, q_{k}⟩ = F s_{1}q_{1} × ⋯ × F s_{k}q_{k}. This composition is only defined to within isomorphism; polynomials form a bicategory Poly, rather than a category.

Note that !𝕆 = 𝟙. In the special case where F : !𝕆 → ℚ̂, so that F merely points to a presheaf X in ℚ̂, the composition G ∘ F of a polynomial G : !ℚ → ℝ̂ with the polynomial F is isomorphic to G[X]. So certainly compositions of this form preserve open maps and bisimulation.

More generally, the polynomials in Poly(ℙ, ℚ) and Poly(ℚ, ℝ) correspond to presheaves over (!ℙ)^{op} × ℚ and (!ℚ)^{op} × ℝ, respectively. So under this correspondence polynomials are related by open maps and bisimulation. It can be shown that the composition of polynomials in general preserves open maps between polynomials.

However, the present interpretation of ! fails as a candidate for the exponential of linear logic because Poly is not cartesian-closed in any reasonable sense. There is an isomorphism of categories

Poly(ℝ, ℙ & ℚ) ≅ Poly(ℝ, ℙ) × Poly(ℝ, ℚ) ,

natural in ℝ in Lin, showing the sense in which ℙ&ℚ, given by juxtaposition, remains a product in the bicategory of polynomials. There is also clearly an isomorphism of functor categories

[!ℙ ×!ℚ, ℝ̂] ≅ [!ℙ, { \atop (!ℚ)^{op} × ℝ}] .

But, in general, !(ℙ & ℚ) and !ℙ ×!ℚ are not isomorphic, so that (!ℚ)^{op} × ℝ is not a function space for the polynomials with respect to − & −. The difficulty boils down to a lack of symmetry in the current definition of !ℙ, where tuples like ⟨p_{1}, …, p_{k}⟩ and its permutations ⟨p_{π(1)}, …, p_{π(k)}⟩ are not necessarily related by any maps. Nor for that matter, are there any maps from a tuple ⟨p_{1}, …, p_{k}⟩ to a larger tuple ⟨p_{1}, …, p_{k}, …, p_{m}⟩, even though intuitively the larger tuple would be a path of a larger assembly of processes, so arguably an extension of the smaller tuple in which further copies have been invoked.

To allow different kinds of polynomial, polynomials which can take account of the symmetry there exists between different copies and also permit further copies to be invoked as needed, we broaden the picture.

7.2 General polynomials

The example suggests that we take assemblies of processes to be families where we can reindex copies, precisely how being prescribed in 𝕌, a subcategory of sets in which the maps are the possible reindexings. A 𝕌-family of a category A comprises ⟨A_{i}⟩_{i∈I} where i ∈ I, with I an object of 𝕌, index objects A_{i} in A. A map of families (f, e) : ⟨A_{i}⟩_{i∈I} → ⟨A′_{j}⟩_{j∈J} consists of a reindexing function f : I → J in 𝕌 and e = ⟨e_{i}⟩_{i∈I}, a family of maps e_{i} : A_{i} → A′_{f(i)} in A. With the obvious composition we obtain F_{𝕌}(A), the category of 𝕌-families.

Imitating the example, we define the category of polynomials from ℙ to ℚ, Poly_{𝕌}(ℙ, ℚ), to be the functor category [F_{𝕌}(ℙ), ℚ]. Under sufficient conditions, that 𝕌 is small, has a singleton and dependent sum (a functor Σ : F_{𝕌}(𝕌) → 𝕌 collapsing any family of sets in 𝕌 to a set in 𝕌), we can compose polynomials in the manner of the coKleisli construction. For this we need a “distributive law” converting a family of presheaves into a presheaf over families of paths. It can be shown that provided all the maps in 𝕌 (the possible reindexings) are injective, composition of polynomials preserves open maps and bisimulation. If 𝕌 contains the empty set, we can specialise composition, as in the example, to obtain a functor F [−] : ℙ̂ → ℚ̂ from F in Poly_{𝕌}(ℙ, ℚ).

The example is now seen as the special case in which 𝕌 consists of subsets, possibly empty, of positive natural numbers {1, …, n} with identities as the only maps. In the special case in which 𝕌 is the full subcategory of Set consisting of the empty set and a singleton, polynomials amount to functors ℙ_{⊥} → ℚ̂ so to maps in Aff. If we take 𝕌 to be 𝕀 (finite sets with injections), or 𝔹 (finite sets with bijections), we can repair an inadequacy in the example; then, F_{𝕌}(ℙ & ℚ) and F_{𝕌}(ℙ) × F_{𝕌}(ℚ) are isomorphic, so that we obtain a function space for the polynomials with respect to the product − & −. Both F_{𝕀} and F_{𝔹} are good candidates for the exponential !—they also behave well w.r.t. bisimulation.

There is a fly in the ointment however. The complete mathematical story, in which one would see the polynomials as maps in a coKleisli construction, uses bicategories and at least pseudo (co)monads on a biequivalent 2-category. At present this theory, even the definitions, are not sufficiently developed (though remedial work has started with Martin Hyland and John Power).

Acknowledgements A good deal of the background for this work was developed with Gian Luca Cattani for his PhD [6]. Discussions with Martin Hyland and John Power have played a crucial role in the work on nonlinearity.

References

[1] S. Abramsky. Computational interpretation of linear logic. Tech. Report 90/20, Dept. of Computing, Imperial College, 1990.

[2] T. Braüner. An Axiomatic Approach to Adequacy. BRICS Dissertation Series DS-96-4, 1996.

[3] J. Brock and W. Ackerman. Scenarios: A model of non-determinate computation. In Proc. of Formalization of Programming Concepts. LNCS 107, 1981.

[4] L. Cardelli and A. D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. In Proc. POPL’00.

[5] L. Cardelli and A. D. Gordon. A Commitment Relation for the Ambient Calculus. Note, 2000.

[6] G. L. Cattani. Presheaf Models for Concurrency. BRICS Dissertation Series DS-99-1, 1999.

[7] G. L. Cattani, M. Fiore, and G. Winskel. A Theory of Recursive Domains with Applications to Concurrency. In Proc. of LICS ’98.

[8] G. L. Cattani, A. J. Power, and G. Winskel. A categorical axiomatics for bisimulation. In Proc. of CONCUR’98, LNCS 1466, 1998.

[9] T. Hildebrandt, P. Panangaden, and G. Winskel. Relational semantics of nondeterministic dataflow. In Proc. of CONCUR’98, LNCS 1466, 1998.

[10] C. A. R. Hoare. A model for communicating sequential processes. Tech. Report PRG-22, University of Oxford Computing Lab., 1981.

[11] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

[12] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127:164–185, 1996.

[13] G. M. Kelly. Basic concepts of enriched category theory. London Math. Soc. Lecture Note Series 64, CUP, 1982.

[14] K. G. Larsen and G. Winskel. Using information systems to solve recursive domain equations effectively. LNCS 173, 1984.

[15] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic. Springer-Verlag, 1992.

[16] A. R. G. Milner. A Calculus of Communicating Systems. LNCS 92, 1980.

[17] A. R. G. Milner. Communication and concurrency. Prentice Hall, 1989.

[18] M. Nygaard. Towards an Operational Understanding of Presheaf Models. Progress report, University of Aarhus, 2001.

[19] G. Winskel. A Linear Metalanguage for Concurrency. In Proc. AMAST’98, LNCS 1548, 1998.

[20] G. Winskel and M. Nielsen. Models for Concurrency. In Handbook of Logic in Computer Science, Volume 4, OUP, 1995

Recent BRICS Report Series Publications

RS-02-48 Mikkel Nygaard and Glynn Winskel. Linearity in Process Languages. December 2002. 27 pp. Appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, LICS ’02 Proceedings, 2002, pages 433–446.

RS-02-47 Zoltán Ésik. Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators. December 2002. 16 pp. To appear in 6th International Conference, Developments in Language Theory, DLT ’02 Revised Papers, LNCS, 2002.

RS-02-46 Zoltán Ésik and Hans Leiß. Greibach Normal Form in Algebraically Complete Semirings. December 2002. 43 pp. An extended abstract appears in Bradfield, editor, European Association for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O(2.4023^{n}) Using Maximal Independent Sets. December 2002. 6 pp.

RS-02-44 Zoltán Ésik and Zoltán L. Németh. Higher Dimensional Automata. November 2002. 32 pp. A preliminary version appears under the title Automata on Series-Parallel Biposets in Kuich, Rozenberg and Salomaa, editors, 5th International Conference, Developments in Language Theory, DLT ’01 Revised Papers, LNCS 2295, 2001, pages 217–227. This report supersedes the earlier BRICS report RS-01-24.

RS-02-43 Mikkel Christiansen and Emmanuel Fleury. Using IDDs for Packet Filtering. October 2002. 25 pp.

RS-02-42 Luca Aceto, Jens A. Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. Checking Consistency of Pedigree Information is NP-complete (Preliminary Report). October 2002. 16 pp.

RS-02-41 Stephen L. Bloom and Zoltán Ésik. Axiomatizing Omega and Omega-op Powers of Words. October 2002. 16 pp.

RS-02-40 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Note on an Expressiveness Hierarchy for Multi-exit Iteration. September 2002. 8 pp.