BRICS RS-03-43 Nygaard & Winskel: Domain Theory for Concurrency BRICS

Basic Research in Computer Science

Domain Theory for Concurrency

Mikkel Nygaard Glynn Winskel BRICS Report Series RS-03-43 ISSN 0909-0878 December 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, 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/03/43/

Domain Theory for Concurrency

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

Abstract

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency.

1 Introduction

Denotational semantics and domain theory of Scott and Strachey provide a global mathematical setting for sequential computation, and thereby place programming languages in connection with each other; connect with the mathematical worlds of algebra, topology and logic; and inspire programming languages, type disciplines and methods of reasoning.

In concurrent/distributed/interactive computation that global mathematical guidance is missing, and domain theory has had little direct influence on theories of concurrent computation. One reason is that classical domain theory has not scaled up to the more intricate models used there.

∗ Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

Broadly speaking, approaches to concurrency are either based on a specific mathematical model of processes or start from the syntax of a process calculus. Among the variety of models for concurrency, one can discern an increasing use of causal/independence/partial-order models (such as Petri nets and event structures) in which computation paths are partial orders of events. Independence models thread through partial-order model checking [45], security protocols [50], nondeterministic dataflow [17], self-timed circuits [18], term-rewriting, game semantics [3], and the analysis of distributed algorithms [29]. There are a variety of process calculi, most of them based on an operational semantics. Following on from the π-calculus [37, 47], newname generation is central to almost all calculi of topical interest. Many are higher-order (allowing process passing) which presents a challenge in understanding suitable equivalences, of which forms of bisimulation are prevalent.

Theories of concurrency form a rather fragmented picture. Relations between different approaches are often unclear; ideas are rediscovered (for example, special event structures reappear as “strand spaces” in reasoning about security protocols [50, 16]). A lot of energy is used on local optimisations to specific process calculi, optimisations that may obscure connections and the global picture. Research is often “modelling-driven” in the sense that many approaches are based on formalising some feature observed in the computing world; the feature may be general such as locality of computation, or specific as in the study of a particular protocol. But the lessons learnt often remain isolated for lack of the commonality a global framework would provide.

A domain theory which handled higher-order processes, independence models, name-generation, and possessed an operational interpretation would provide a global mathematical framework for most theories of concurrency. In case incorporating independence models into a domain theory seems a tall order, there are now arguments (based on event-structure representations of process denotations—see Sect. 6.4) that the operational semantics associated with a domain theory for concurrency will involve event structures. It should be remarked that a traditional use of powerdomains [46], based on domains of resumptions, will fall short because, insisting on a nondeterministic choice of actions one at a time, it cannot accommodate independence models where computation paths have more structure than strings of actions.

How do we work towards such a domain theory for concurrency? The potentially complicated structure of computation paths suggests building a domain theory directly on computation paths. This line has been followed in what seemed originally to be two different directions, one being Matthew Hennessy’s semantics for CCS with process passing [22], in which a process denotes the set of its computation paths. We’ll call this kind of semantics a path semantics because of its similarity to trace semantics [24]; in both cases, processes denote downwards-closed sets of computation paths and the corresponding notion of process equivalence, called path equivalence, is given by equality of such sets. Computation paths, however, may have more structure than traditional traces, e.g. allowing path semantics to take nondeterministic branching into account in a limited way. For example, path equivalence is related to simulation equivalence in Sect. 3.5 below. The other path-based approach is that of categories of presheaf models [14] in which processes denote mappings from computation paths to sets of “realisers” saying how each computation path may be realised. This extra structure allows the incorporation of complete branching information, and the corresponding notion of process equivalence is a form of bisimulation [26]. The two approaches are variations on a common idea: that a process denotes a form of characteristic function in which the truth values are sets of realisers. A path set may be viewed as a special presheaf that yields at most one realiser for each path.

The study of presheaf models for concurrency has drawn attention to a 2categorical model of linear logic and associated pseudo-comonads [15]. This led to the discovery of two expressive metalanguages for concurrency, one based on an exponential of linear logic (from which one derives a model of intuitionistic logic), the other based on a weakening comonad (from which one derives a model of affine-linear logic). The presheaf semantics led to operational semantics, guided by the idea that derivations of transitions in the operational semantics, associated with paths, should correspond to elements of the presheaf denotations. The presheaf models capture the nondeterministic branching of processes and support notions of bisimulation. But there is a significant overhead in terms of the category theory needed.

In this paper we concentrate on the simpler path semantics of the languages. Path sets give rise to a simpler version of the categorical models, avoiding the 2-categorical structure. Though path sets are considerably simpler than presheaves they furnish models which are sufficiently rich in structure to show how both languages arise from canonical constructions on path sets. The path semantics admits simple proofs of full abstraction, showing that path equivalence coincides with contextual equivalence.

One language, called HOPLA for Higher-Order Process LAnguage [41, 42], derives from an exponential of linear logic. It can be viewed as an extension of the lambda-calculus with CCS-like nondeterministic sum and prefix operations, in which types express the form of computation path of which a process is capable. HOPLA can directly encode calculi like CCS [35], CCS with process passing [22], and mobile ambients with public names [10, 11], and it can be given a straightforward operational semantics supporting a standard bisimulation congruence. We relate the denotational and operational semantics giving pleasingly simple proofs of soundness and adequacy. Full abstraction implies that contextual equivalence coincides with logical equivalence for a fragment of Hennessy-Milner logic, linking up with simulation equivalence [21]. Work is in progress on extending HOPLA with name generation [55].

The other language is here called Affine HOPLA [40] and is based on a weakening comonad that yields a model of affine-linear logic in the sense of Jacobs [25]. This language adds to HOPLA an interesting tensor operation at the price of linearity constraints on the occurrences of variables. The tensor can be understood as a parallel composition of independent processes and allows Affine HOPLA to encode processes of the kind found in treatments of nondeterministic dataflow [27].

We conclude with a discussion of how the results fit within a broader programme of research, towards a fully fledged domain theory for concurrency. Important leads come by moving to categories obtained from presheaves rather than path sets. These categories are very rich in structure. They point towards more expressive languages than HOPLA and Affine HOPLA. In particular, the affine category accommodates the independence model of event structures to the extent of supporting the standard event structure semantics of CCS and related languages [12], as well as the trace of nondeterministic dataflow [23]. In fact, Affine HOPLA can be given an event structure semantics which at first order provides a representation of the presheaf denotations. Nevertheless, it is here we meet the limitations of Affine HOPLA, and HOPLA. They can be shown not to support definitions of the standard event structure semantics of CCS and the trace of nondeterministic dataflow [43].

2 Domain Theory of Path Sets

In the path semantics, processes are intuitively represented as collections of their computation paths. Paths are elements of preorders ℙ, ℚ, … called path orders which function as process types, each describing the set of possible paths for processes of that type together with their sub-path ordering.^{1} A process of type ℙ is then represented as a downwards-closed subset X ⊆ ℙ, called a path set. Path sets ordered by inclusion form the elements of the poset ℙ̂ which we’ll think of as a domain of meanings of processes of type ℙ.

The poset ℙ̂ has many interesting properties. First of all, it is a complete lattice with joins given by union. In the sense of Hennessy and Plotkin [20], ℙ̂ is a “nondeterministic domain”, with joins used to interpret nondeterministic sums of processes. Accordingly, given a family (X_{i})_{i∈I} of elements of ℙ̂, we’ll often write Σ_{i∈I}X_{i} for their join. A typical finite join is written X_{1} + ⋯ + X_{k} while the empty join is the empty path set, the inactive process, written ∅.

1It is possible to work with straight posets rather than preorders—indeed, the mathematics is virtually unaffected by this choice—but preorders will be helpful in dealing with recursive types in Sect. 3.1.

A second important property of ℙ̂ is that any X ∈ ℙ̂ is the join of certain “prime” elements below it; ℙ̂ is a prime algebraic complete lattice [39]. Primes are down-closures y_{ℙ}p = {p′ : p′ ≤_{ℙ} p} of individual elements p ∈ ℙ, representing a process that may perform the computation path p. The map y_{ℙ} reflects as well as preserves order, so that p ≤_{ℙ} p′ iff y_{ℙ}p ⊆ y_{ℙ}p′, and y_{ℙ} thus “embeds” ℙ in ℙ̂. We clearly have y_{ℙ}p ⊆ X iff p ∈ X and prime algebraicity of ℙ̂ amounts to saying that any X ∈ ℙ̂ is the union of its elements:

X = ⋃_{p∈X} y_{ℙ}p .  (1)

Finally, ℙ̂ is characterised abstractly as the free join-completion of ℙ, meaning (i) it is join-complete and (ii) given any join-complete poset C and a monotone map f : ℙ → C, there is a unique join-preserving map f^{†} : ℙ̂ → C such that the diagram on the left below commutes.

\xymatrix{ℙ \ar[r]^{y_{ℙ}} \ar[dr]_{f} & ℙ̂ \ar@{.>}[d]^{f^{†}} \\  & C}  f^{†}X = ⋃_{p∈X} fp .  (2)

We call f^{†} the extension of f along y_{ℙ}. Uniqueness of f^{†} follows from (1).

Notice that we may instantiate C to any poset of the form ℚ̂, drawing our attention to join-preserving maps ℙ̂ → ℚ̂. By the freeness property (2), joinpreserving maps ℙ̂ → ℚ̂ are in bijective correspondence with monotone maps ℙ → ℚ̂. Each element Y of ℚ̂ can be represented using its “characteristic function”, a monotone map f_{Y} : ℚ^{op} → 2 from the opposite order to the simple poset 0 < 1 such that Y = {q : f_{Y} q = 1} and ℚ̂ ≅ [ℚ^{op}, 2]. Uncurrying then yields the following chain:

[ℙ, ℚ̂] ≅ [ℙ, [ℚ^{op}, 2]] ≅ [ℙ × ℚ^{op}, 2] = [(ℙ^{op} × ℚ)^{op}, 2] ≅ { \atop ℙ^{op} × ℚ} . (3)

So the order ℙ^{op} × ℚ provides a function space type. We’ll now investigate what additional type structure is at hand.

2.1 Linear and Continuous Categories

Write Lin for the category with path orders ℙ, ℚ, … as objects and joinpreserving maps ℙ̂ → ℚ̂ as arrows. It turns out Lin has enough structure to be understood as a categorical model of Girard’s linear logic [19, 49]. Accordingly, we’ll call arrows of Lin linear maps.

Linear maps are represented by elements of { \atop ℙ^{op} × ℚ} and so by downwardsclosed subsets of the order ℙ^{op} × ℚ. This relational presentation exposes an involution central in understanding Lin as a categorical model of classical linear logic. The involution of linear logic, yielding ℙ^{⊥} on an object ℙ, is given by ℙ^{op}; clearly, downwards-closed subsets of ℙ^{op} × ℚ correspond to downwards-closed subsets of (ℚ^{op})^{op} × ℙ^{op}, showing how maps ℙ → ℚ correspond to maps ℚ^{⊥} → ℙ^{⊥} in Lin. The tensor product of ℙ and ℚ is given by the product of preorders ℙ × ℚ; the singleton order 𝟙 is a unit for tensor. Linear function space ℙ ⊸ ℚ is then obtained as ℙ^{op} × ℚ. Products ℙ & ℚ are given by ℙ + ℚ, the disjoint juxtaposition of preorders. An element of { \atop ℙ & ℚ} can be identified with a pair (X, Y) with X ∈ ℙ̂ and Y ∈ ℚ̂, which provides the projections π_{1} : ℙ & ℚ → ℙ and π_{2} : ℙ & ℚ → ℚ in Lin. 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 the empty order 𝕆 and, as the terminal object, is associated with unique maps ∅_{ℙ} : ℙ → 𝕆, constantly ∅, for any path order ℙ. All told, Lin is a ∗-autonomous category, so a symmetric monoidal closed category with a dualising object, and has finite products (indeed, all products) as required by Seely’s definition of a model of linear logic [49].

In fact, Lin also has all coproducts, also given on objects ℙ and ℚ by the juxtaposition ℙ+ℚ and so coinciding with products. Injection maps in_{1} : ℙ → ℙ+ℚ and in_{2} : ℚ → ℙ+ℚ in Lin derive from the obvious injections into the disjoint sum of preorders. The empty coproduct is the empty order 𝕆 which is then a zero object. This collapse of products and coproducts highlights that Lin has arbitrary biproducts. Via the isomorphism Lin(ℙ, ℚ) ≅ { \atop ℙ^{op} × ℚ}, each homset of Lin can be seen as a commutative monoid with neutral element the always ∅ map, itself written ∅ : ℙ → ℚ, and sum given by union, written +. Composition in Lin is bilinear in that, given f, f′ : ℙ → ℚ and g, g′ : ℚ → ℝ, we have (g + g′) ∘ (f + f′) = g ∘ f + g ∘ f′ + g′ ∘ f + g′ ∘ f′. Further, given a family of objects (ℙ_{α})_{α∈A}, we have for each β ∈ A a diagram

\xymatrix{ℙ_{β} \ar[r]_{_{in_{β}}} & Σ_{α∈A}ℙ_{α} \ar[l]_{π_{β}}} such that π_{β} ∘ in_{β} = 1_{ℙ_{β}} , π_{β} ∘ in_{α} = ∅ if α ≠ β, and Σ_{α∈A}(in_{α} ∘ π_{α}) = 1_{Σ_{α∈A}ℙ_{α}} . (4)

Processes of type Σ_{α∈A}ℙ_{α} may intuitively perform computation paths in any of the component path orders ℙ_{α}.

We see that Lin is rich in structure. But linear maps alone are too restrictive. Being join-preserving, they in particular preserve the empty join. So, unlike e.g. prefixing, linear maps always send the inactive process ∅ to itself. Looking for a broader notion of maps between nondeterministic domains we follow the discipline of linear logic and consider non-linear maps whose domain is under an exponential, !. One choice of a suitable exponential for Lin is got by taking !ℙ to be the preorder obtained as the free finite-join completion of ℙ. Concretely, !ℙ can be defined to have finite subsets of ℙ as elements with ordering given by ⪯_{ℙ}, defined for arbitrary subsets X, Y of ℙ as follows:

X ⪯_{ℙ} Y ⟺_{def} ∀p ∈ X.∃q ∈ Y. p ≤_{ℙ} q .  (5)

When !ℙ is quotiented by the equivalence induced by the preorder we obtain a poset which is the free finite-join completion of ℙ. By further using the obvious inclusion of this completion into ℙ̂, we get a map i_{ℙ} : !ℙ → ℙ̂ sending a finite set {p_{1}, …, p_{n}} to the join y_{ℙ}p_{1} + ⋯ + y_{ℙ}p_{n}. Such finite sums of primes are the finite (isolated, compact) elements of ℙ̂. The map i_{ℙ} assumes the role of y_{ℙ} above. For any X ∈ ℙ̂ and P ∈ !ℙ, we have i_{ℙ}P ⊆ X iff P ⪯_{ℙ} X, and X is the directed join of the finite elements below it:

X = ⋃_{P ⪯_{ℙ}X} i_{ℙ}P .  (6)

Further, ℙ̂ is the free directed-join completion of !ℙ (also known as the ideal completion of !ℙ). This means that given any monotone map f : !ℙ → C for some directed-join complete poset C, there is a unique directed-join preserving (i.e. Scott continuous) map f^{‡} : ℙ̂ → C such that the diagram below commutes.

\xymatrix{!ℙ \ar[r]^{i_{ℙ}} \ar[dr]_{f} & ℙ̂ \ar@{.>}[d]^{f^{‡}} \\  & C}  f^{‡}X = ⋃_{P ⪯_{ℙ}X} fP .  (7)

Uniqueness of f^{‡}, called the extension of f along i_{ℙ}, follows from (6). As before, we can replace C by a nondeterministic domain ℚ̂ and by the freeness properties (2) and (7), there is a bijective correspondence between linear maps !ℙ → ℚ and continuous maps ℙ̂ → ℚ̂.

We define the category Cts to have path orders ℙ, ℚ, … as objects and continuous maps ℙ̂ → ℚ̂ as arrows. These arrows allow more process operations, including prefixing, to be expressed. The structure of Cts is induced by that of Lin via an adjunction between the two categories.

2.2 An Adjunction

As linear maps are continuous, Cts has Lin as a sub-category, one which shares the same objects. We saw above that there is a bijection

Lin(!ℙ, ℚ) ≅ Cts(ℙ, ℚ) .  (8)

This is in fact natural in ℙ and ℚ so an adjunction with the inclusion Lin ↪ Cts as right adjoint. Via (7) the map y_{!ℙ} : !ℙ → ˆ!ℙ extends to a map η_{ℙ} = y_{!ℙ}^{‡} : ℙ → !ℙ in Cts. Conversely, i_{ℙ} : !ℙ → ℙ̂ extends to a map ε_{ℙ} = i_{ℙ}^{†} : !ℙ → ℙ in Lin using (2). These maps are the unit and counit, respectively, of the adjunction:

η_{ℙ}X = ⋃_{P ⪯_{ℙ}X} y_{!ℙ}P  ε_{ℙ}X = ⋃_{P ∈X} i_{ℙ}P  (9)

The left adjoint is the functor ! : Cts → Lin given on arrows f : ℙ → ℚ by (η_{ℚ} ∘ f ∘ i_{ℙ})^{†} : !ℙ → !ℚ. The bijection (8) then maps g : !ℙ → ℚ in Lin to ḡ = g ∘ η_{ℙ} : ℙ → ℚ in Cts while its inverse maps f : ℙ → ℚ in Cts to f̄ = ε_{ℚ} ∘!f in Lin. We call ḡ and f̄ the transpose of g and f, respectively; of course, transposing twice yields back the original map. As Lin is a subcategory of Cts, the counit is also a map in Cts. We have ε_{ℙ} ∘ η_{ℙ} = 1_{ℙ} and 1_{!ℙ} ≤ η_{ℙ} ∘ ε_{ℙ}, the pointwise order, for all objects ℙ.

Right adjoints preserve products, and so Cts has finite products given as in Lin. Hence, Cts is a symmetric monoidal category like Lin, and in fact, our adjunction is symmetric monoidal (see [31] pp. 251–6). In detail, there are isomorphisms of path orders,

k : 𝟙 ≅ !𝕆 and m_{ℙ,ℚ} : !ℙ ×!ℚ ≅ !(ℙ & ℚ) ,  (10)

with m_{ℙ,ℚ} mapping a pair (P, Q) ∈ !ℙ ×!ℚ to the union in_{1} P ∪ in_{2} Q; any element of !(ℙ & ℚ) can be written on this form. These isomorphisms induce isomorphisms with the same names in Lin with m natural. Moreover, k and m commute with the associativity, symmetry and unit maps of Lin and Cts, such as s_{ℙ,ℚ}^{Lin} : ℙ × ℚ ≅ ℚ × ℙ and r_{ℚ}^{Cts} : ℚ & 𝕆 ≅ ℚ, making ! symmetric monoidal. It then follows [28] that the inclusion Lin ↪ Cts is symmetric monoidal as well, and that the unit and counit are monoidal transformations. Thus, there are maps

l : 𝕆 → 𝟙 and n_{ℙ,ℚ} : ℙ & ℚ → ℙ × ℚ  (11)

in Cts, with n natural, corresponding to k and m above; l maps ∅ to {∗} while n_{ℙ,ℚ} is the extension h^{‡} of the map h(in_{1} P ∪ in_{2} Q) = i_{ℙ}P × i_{ℚ}Q. The unit also makes the diagrams below commute and the counit satisfies similar properties.

\xymatrix{ & ℙ & ℚ \ar@{-->}[dl]_{η_{ℙ}&η_{ℚ}} \ar@{-->}[dr]^{η_{ℙ&ℚ}} &  & 𝕆 \ar[r]^{l} \ar[dr]_{η_{𝕆}} & 𝟙 \ar[d]^{k} \\ !ℙ & !ℚ \ar[r]_{n_{!ℙ,!ℚ}} & !ℙ ×!ℚ \ar[r]_{m_{ℙ,ℚ}} & !(ℙ & ℚ) &  & !𝕆}  (12)

The diagram on the left can be written as str_{ℙ,ℚ} ∘(1_{ℙ}&η_{ℚ}) = η_{ℙ&ℚ} where str, the strength of ! viewed as a monad on Cts, is the natural transformation

\xymatrix{ℙ & !ℚ \ar[r]^{η_{ℙ}&1_{!ℚ}} & !ℙ & !ℚ \ar[r]^{n_{!ℙ,!ℚ}} & !ℙ ×!ℚ \ar[r]^{m_{ℙ,ℚ}} & !(ℙ & ℚ)} .  (13)

Finally, recall that the category Lin is symmetric monoidal closed so that the functor (ℚ ⊸ −) is right adjoint to (− × ℚ) for any object ℚ. Together with the natural isomorphism m this provides a right adjoint (ℚ → −), defined by (!ℚ ⊸ −), to the functor (− & ℚ) in Cts via the chain

Cts(ℙ & ℚ, ℝ) ≅ Lin(!(ℙ & ℚ), ℝ) ≅ Lin(!ℙ ×!ℚ, ℝ) ≅ Lin(!ℙ,!ℚ ⊸ ℝ) ≅ Cts(ℙ,!ℚ ⊸ ℝ) = Cts(ℙ, ℚ → ℝ) (14)

—natural in ℙ and ℝ. This demonstrates that Cts is cartesian closed, as is well known. The adjunction between Lin and Cts now satisfies the conditions put forward by Benton, Bierman, Hyland, and de Paiva for a categorical model of intuitionistic linear logic, strengthening those of Seely [5, 4, 49]; see also [33] for a recent survey of such models.

3 HOPLA

HOPLA is a typed process language directly suggested by the structure of the category Cts [41, 42]. A typing judgement

x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ  (15)

means that a process t yields computation paths in ℚ once processes with computation paths in ℙ_{1}, …, ℙ_{k} are assigned to the variables x_{1}, …, x_{k} respectively.

3.1 Denotational Semantics

Types are given by the grammar

𝕋 ::= 𝕋_{1} → 𝕋_{2} | Σ_{α∈A}𝕋_{α} | !𝕋 | T | μ_{j}T⃗.𝕋⃗ .  (16)

The symbol T is drawn from a set of type variables used in defining recursive types; closed type expressions are interpreted as path orders. Using vector notation, μ_{j}T⃗.𝕋⃗ abbreviates μ_{j}T_{1}, …, T_{k}.(𝕋_{1}, …, 𝕋_{k}) and is interpreted as the j-component, for 1 ≤ j ≤ k, of “the least” solution to the defining equations T_{1} = 𝕋_{1}, …, T_{k} = 𝕋_{k}, in which the expressions 𝕋_{1}, …, 𝕋_{k} may contain the T_{j}’s. What “the least” means will be explained below. We shall write μT⃗.𝕋⃗ as an abbreviation for the k-tuple with j-component μ_{j}T⃗.𝕋⃗, and confuse a closed expression for a path order with the path order itself.

Simultaneous recursive equations for path orders can be solved using information systems [48, 30]. Here, it will be convenient to give a concrete, inductive characterisation based on a language of paths:

p, q ::= P ↦ q | βp | P | abs p .  (17)

Above, P ranges over finite sets of paths. We use P ↦ q as notation for pairs in the function space (!ℙ)^{op} ×ℚ. The language is complemented by formation rules using judgements p : ℙ, meaning that p belongs to ℙ, displayed below alongside rules defining the ordering on ℙ using judgements p ≤_{ℙ} p′. Recall that P ⪯_{ℙ} P′ means ∀p ∈ P.∃p′ ∈ P′. p ≤_{ℙ} p′.

\frac{P : !ℙ q : ℚ}{P ↦ q : ℙ → ℚ}  \frac{P′ ≤_{!ℙ} P q ≤_{ℚ} q′}{P ↦ q ≤_{ℙ→ℚ} P′ ↦ q′}
\frac{p : ℙ_{β} β ∈ A}{βp : Σ_{α∈A}ℙ_{α}}  \frac{p ≤_{ℙ_{β}} p′ βinA}{βp ≤_{Σ_{α∈A}ℙ_{α}} βp′}
\frac{p_{1} : ℙ ⋯ p_{n} : ℙ}{\{p_{1}, …, p_{n}\} : !ℙ}  \frac{P ⪯_{ℙ} P′}{P ≤_{!ℙ} P′}
\frac{p : 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}{abs p : μ_{j}T⃗.𝕋⃗}  \frac{p ≤_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} p′}{abs p ≤_{μ_{j} T⃗.𝕋⃗} abs p′}

(18)

Using information systems as in [30] yields the same representation, except for the tagging with abs in recursive types, done to help in the proof of adequacy in Section 3.4.1. So rather than the straight equality between a recursive type and its unfolding which we are used to from [30], we get an isomorphism abs : 𝕋_{j}[μT⃗.𝕋⃗/T⃗] ≅ μ_{j}T⃗.𝕋⃗ whose inverse we call rep.

The raw syntax of terms is given by

t, u ::= x|rec x.t|Σ_{i∈I}t_{i} |λx.t|t u|βt|π_{β}t|!t|[u > !x ⇒ t]|abs t|rep t . (19)

The variable x in the “match” term [u > !x ⇒ t] is a binding occurrence and so binds 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. The syntax will be subject to typing constraints below.

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

⟦x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ⟧ : ℙ_{1} & ⋯ & ℙ_{k} → ℚ  (20)

in Cts. We’ll write Γ, or Λ, for an environment list x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} and most often abbreviate the denotation to ℙ_{1}&⋯&ℙ_{k} ⟶^{t} ℚ, or Γ ⟶^{t} ℚ, or even ⟦t⟧, suppressing the type information. When the environment list is empty, the corresponding product is the empty path order 𝕆.

The term-formation rules are displayed below alongside their interpretations as constructors on maps of Cts, taking the maps denoted by the premises to that denoted by the conclusion (cf. [8]). We assume that the variables in any environment list are distinct.

Structural rules. The rules handling environment lists (identity, weakening, exchange, and contraction) are given as follows:

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

\frac{Γ ⊢ t : ℚ}{Γ, x : ℙ ⊢ t : ℚ}  \frac{Γ ⟶^{t} ℚ}{Γ & ℙ ⟶^{t&∅_{ℙ}} ℚ & 𝕆 ⟶^{r_{ℚ}^{Cts}} ℚ}  (22)

\frac{Γ, y : ℚ, x : ℙ, Λ ⊢ t : ℝ}{Γ, x : ℙ, y : ℚ, Λ ⊢ t : ℝ}  \frac{Γ & ℚ & ℙ & Λ ⟶^{t} ℝ}{Γ & ℙ & ℚ & Λ ⟶^{t∘(1_{Γ}&s_{ℙ,ℚ}^{Cts} &1_{Λ})} ℝ}  (23)

\frac{Γ, x : ℙ, y : ℙ ⊢ t : ℚ}{Γ, z : ℙ ⊢ t[z/x, z/y] : ℚ}  \frac{Γ & ℙ & ℙ ⟶^{t} ℚ}{Γ & ℙ ⟶^{1_{Γ}&Δ_{ℙ}} Γ & ℙ & ℙ ⟶^{t} ℚ}  (24)

In the formation rule for contraction (24), the variable z must be fresh; the map Δ_{ℙ} is the usual diagonal, given as ⟨1_{ℙ}, 1_{ℙ}⟩.

Recursive definition. Since each ℙ̂ is a complete lattice, it admits least fixedpoints of continuous maps. If f : ℙ̂ → ℙ̂ is continuous, it has a least fixedpoint, fix f ∈ ℙ̂ obtained as ⋃_{n∈ω} f^{n}(∅). This allows us to interpret recursively defined processes:

\frac{Γ, x : ℙ ⊢ t : ℙ}{Γ ⊢ rec x.t : ℙ}  \frac{Γ & ℙ ⟶^{t} ℙ}{Γ ⟶^{fix F} ℙ}  (25)

Here, fix F is the fixpoint in Cts(Γ, ℙ) ≅ { \atop Γ → ℙ} of the continuous operation F mapping g : Γ → ℙ in Cts to the composition

Γ ⟶^{Δ_{Γ}} Γ & Γ ⟶^{1_{Γ}&g} Γ & ℙ ⟶^{t} ℙ .  (26)

Nondeterministic sum. Each path order ℙ is associated with a join operation, Σ : &_{i∈I} ℙ → ℙ in Cts taking a tuple ⟨t_{i}⟩_{i∈I} to the nondeterministic sum Σ_{i∈I}t_{i} in ℙ̂. We’ll write ∅ and t_{1} + ⋯ + t_{k} for finite sums.

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

Function space. As noted at the end of Sect. 2.2, the category Cts is cartesian closed with function space ℙ → ℚ. Thus, there is a 1-1 correspondence curry from maps ℙ & ℚ → ℝ to maps ℙ → (ℚ → ℝ) in Cts; its inverse is called uncurry. We obtain application, app : (ℙ → ℚ) & ℙ → ℚ as uncurry(1_{ℙ→ℚ}).

\frac{Γ, x : ℙ ⊢ t : ℚ}{Γ ⊢ λx.t : ℙ → ℚ}  \frac{Γ & ℙ ⟶^{t} ℚ}{Γ ⟶^{curry t} ℙ → ℚ}  (28)

\frac{Γ ⊢ t : ℙ → ℚ Λ ⊢ u : ℙ}{Γ, Λ ⊢ t u : ℚ}  \frac{Γ ⟶^{t} ℙ → ℚ Λ ⟶^{u} ℙ}{Γ & Λ ⟶^{t&u} (ℙ → ℚ) & ℙ ⟶^{app} ℚ}  (29)

Sum type. The category Cts does not have coproducts, but we can build a useful sum type out of the biproduct of Lin. The properties (4) are obviously also satisfied in Cts, even though the construction is universal only in the subcategory of linear maps because composition is generally not bilinear in Cts. We’ll write 𝕆 and ℙ_{1} +⋯+ℙ_{k} for the empty and finite sum types. The product ℙ_{1} & ℙ_{2} of [41] with pairing (t, u) and projection terms fst t, snd t can be encoded as, respectively, ℙ_{1} + ℙ_{2}, 1t + 2u and π_{1}t, π_{2}t.

\frac{Γ ⊢ t : ℙ_{β} β ∈ A}{Γ ⊢ βt : Σ_{α∈A}ℙ_{α}}  \frac{Γ ⟶^{t} ℙ_{β} β ∈ A}{Γ ⟶^{t} ℙ_{β} ⟶^{in_{β}} Σ_{α∈A}ℙ_{α}}  (30)

\frac{Γ ⊢ t : Σ_{α∈A}ℙ_{α} β ∈ A}{Γ ⊢ π_{β}t : ℙ_{β}}  \frac{Γ ⟶^{t} Σ_{α∈A}ℙ_{α} β ∈ A}{Γ ⟶^{t} Σ_{α∈A}ℙ_{α} ⟶^{π_{β}} ℙ_{β}}  (31)

Prefixing. The adjunction between Lin and Cts provides a type constructor, !(−), for which the unit η_{ℙ} : ℙ → !ℙ and counit ε_{ℙ} : !ℙ → ℙ play a role in interpreting term constructors and deconstructors, respectively. The behaviour of η_{ℙ} with respect to maps of Cts fits that of an anonymous prefix operation. We’ll say that η_{ℙ} maps u of type ℙ to a “prefixed” process !u of type !ℙ; intuitively, the process !u will be able to perform an action, which we call !, before continuing as the process u.

\frac{Γ ⊢ u : ℙ}{Γ ⊢ !u : !ℙ}  \frac{Γ ⟶^{u} ℙ}{Γ ⟶^{u} ℙ ⟶^{η_{ℙ}} !ℙ}  (32)

By the universal property of η_{ℙ}, if t of type ℚ has a free variable of type ℙ, and so is interpreted as a map t : ℙ → ℚ in Cts, then the transpose t̄= ε_{ℚ}∘!t is the unique map !ℙ → ℚ in Lin such that t = t̄∘η_{ℙ}. With u of type !ℙ, we’ll write [u > !x ⇒ t] for t̄u. Intuitively, this construction “tests” or matches u against the pattern !x and passes the results of successful matches for x on to t. Indeed, first prefixing a term u of type ℙ and then matching yields a successful match u for x as t̄(η_{ℙ}u) = tu. By linearity of t̄, the possibly multiple results of successful matches are nondeterministically summed together; the denotations of [Σ_{i∈I}u_{i} > !x ⇒ t] and Σ_{i∈I}[u_{i} > !x ⇒ t] are identical.

The above clearly generalises to the case where u is an open term, but if t has free variables other than x, we need to make use of the strength map given by (13), see Proposition 3.5 below.

\frac{Γ, x : ℙ ⊢ t : ℚ Λ ⊢ u : !ℙ}{Γ, Λ ⊢ [u > !x ⇒ t] : ℚ} \frac{Γ & ℙ ⟶^{t} ℚ Λ ⟶^{u} !ℙ}{Γ & Λ ⟶^{1_{Γ}&u} Γ & !ℙ ⟶^{str_{Γ,ℙ}} !(Γ & ℙ) ⟶^{t̄} ℚ} (33)

Recursive type definitions. Folding and unfolding recursive types is accompanied by term constructors abs and rep:

\frac{Γ ⊢ t : 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}{Γ ⊢ abs t : μ_{j}T⃗.𝕋⃗}  \frac{Γ ⟶^{t} 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}{Γ ⟶^{t} 𝕋_{j}[μT⃗.𝕋⃗/T⃗] ⟶^{abs} μ_{j}T⃗.𝕋⃗}  (34)

\frac{Γ ⊢ t : μ_{j}T⃗.𝕋⃗}{Γ ⊢ rep t : 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}  \frac{Γ ⟶^{t} μ_{j}T⃗.𝕋⃗}{Γ ⟶^{t} μ_{j}T⃗.𝕋⃗ ⟶^{rep} 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}  (35)

3.2 Useful Identities

We provide some technical results about the path semantics which are used in the proofs of full abstraction and soundness below. They are also useful for reasoning about encodings of process calculi, see Sect. 3.6.

Lemma 3.1 (Substitution) Suppose Γ, x : ℙ ⊢ t : ℚ and Λ ⊢ u : ℙ with Γ and Λ disjoint. Then Γ, Λ ⊢ t[u/x] : ℚ with denotation given by the composition

Γ & Λ ⟶^{1_{Γ}&u} Γ & ℙ ⟶^{t} ℚ .  (36)

Corollary 3.2 Application amounts to substitution. In the situation of the substitution lemma, we have ⟦(λx.t) u⟧ = ⟦t[u/x]⟧.

Corollary 3.3 Recursion amounts to unfolding. Suppose Γ, x : ℙ ⊢ t : ℙ. Then Γ ⊢ t[rec x.t/x] : ℙ and ⟦rec x.t⟧ = ⟦t[rec x.t/x]⟧.

Proof. By renaming variables y of Γ to y′ and y′′ we get Γ′, x : ℙ ⊢ t′ : ℙ and Γ′′, x : ℙ ⊢ t′′ : ℙ with Γ′ and Γ′′ disjoint. Then by the substitution lemma, Γ′, Γ′′ ⊢ t′[rec x.t′′/x] : ℙ with denotation given by

Γ′ & Γ′′ ⟶^{1_{Γ′}&rec x.t′′} Γ′ & ℙ ⟶^{t′} ℙ .  (37)

By suitable use of exchange and contraction, substituting y for y′ and y′′, we get Γ ⊢ t[rec x.t/x] : ℙ with denotation

Γ ⟶^{Δ_{Γ}} Γ & Γ ⟶^{1_{Γ}&rec x.t} Γ & ℙ ⟶^{t} ℙ .  (38)

This is the same as F (fix F) where fix F is the denotation of rec x.t, and by property of the fixed-point, F (fix F) = fix F as wanted. □

Proposition 3.4 From the properties of the biproduct we get:

⟦π_{β}(βt)⟧ = ⟦t⟧
⟦π_{α}(βt)⟧ = ∅  if α ≠ β
⟦Σ_{α∈A}α(π_{α}(t))⟧ = ⟦t⟧  where Γ ⊢ t : Σ_{α∈A}ℙ_{α}

(39)

In addition, ⟦β(Σ_{i∈I}t_{i})⟧ = ⟦Σ_{i∈I}(βt_{i})⟧ and ⟦π_{β}(Σ_{i∈I}t_{i})⟧ = ⟦Σ_{i∈I}(π_{β}t_{i})⟧ by linearity of injection and projection.

Proposition 3.5 The prefix match satisfies the properties:

\begin{aligned}⟦[!u > !x ⇒ t]⟧ & = ⟦t[u/x]⟧ \\ ⟦[Σ_{i∈I}u_{i} > !x ⇒ t]⟧ & = ⟦Σ_{i∈I}[u_{i} > !x ⇒ t]⟧ \end{aligned}  (40)

Proof. By the properties of str and t̄, and using the substitution lemma, we have

[!u > !x ⇒ t] = t̄∘ str_{Γ,ℙ} ∘(1_{Γ} & (η_{ℙ} ∘ u))
= t̄∘ str_{Γ,ℙ} ∘(1_{Γ} & η_{ℙ}) ∘ (1_{Γ} & u)
= t̄∘ η_{Γ&ℙ} ∘ (1_{Γ} & u)
= t ∘ (1_{Γ} & u)
= t[u/x] .

(41)

Note that we are e.g. abbreviating ⟦t⟧ to t. Linearity of t̄ and m_{Γ,ℙ} and naturality of n yields

[Σ_{i∈I}u_{i} > !x ⇒ t] = t̄∘ str_{Γ,ℙ} ∘(1_{Γ} & Σ_{i∈I}u_{i})
= t̄∘ m_{Γ,ℙ} ∘ n_{!Γ,!ℙ} ∘ (η_{Γ} & 1_{!ℙ}) ∘ (1_{Γ} & Σ_{i∈I}u_{i})
= t̄∘ m_{Γ,ℙ} ∘ n_{!Γ,!ℙ} ∘ (η_{Γ} & Σ_{i∈I}u_{i})
= t̄∘ m_{Γ,ℙ} ∘ (η_{Γ} × Σ_{i∈I}u_{i}) ∘ n_{Γ,Λ}
= Σ_{i∈I}(t̄∘ m_{Γ,ℙ} ∘ (η_{Γ} × u_{i}) ∘ n_{Γ,Λ})
= Σ_{i∈I}(t̄∘ m_{Γ,ℙ} ∘ n_{!Γ,!ℙ} ∘ (η_{Γ} & u_{i}))
= Σ_{i∈I}[u_{i} > !x ⇒ t]

(42)

—as wanted. □

3.3 Full Abstraction

We define a program to be a closed term t of type !𝕆, the simplest type with at least two values. A (Γ, ℙ)-program context C is a term with holes into which a term t with Γ ⊢ t : ℙ may be put to form a program ⊢ C(t) : !𝕆. The denotational semantics gives rise to a type-respecting contextual preorder [38]:

Definition 3.6 Suppose Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ. We say that t_{1} and t_{2} are related by contextual preorder, written t_{1} ⊏ ∼ t_{2}, iff for all (Γ, ℙ)-program contexts C, we have ⟦C(t_{1})⟧ ≠ ∅ ⟹ ⟦C(t_{2})⟧ ≠ ∅. If both t_{1} ⊏ ∼ t_{2} and t_{2} ⊏ ∼ t_{1}, we say that t_{1} and t_{2} are contextually equivalent.

Contextual equivalence coincides with path equivalence, as do the associated preorders:

Theorem 3.7 (Full abstraction) Suppose Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ. Then

⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ ⟺ t_{1} ⊏ ∼ t_{2} .  (43)

Proof. Suppose ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ and let C be a (Γ, ℙ)-program context with ⟦C(t_{1})⟧ ≠ ∅. As ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ we have ⟦C(t_{2})⟧ ≠ ∅ by compositionality and monotonicity, and so t_{1} ⊏ ∼ t_{2} as wanted.

To prove the converse we define for each path p : ℙ a closed term t_{p} of type ℙ and a (𝕆, ℙ)-program context C_{p} that respectively “realise” and “consume” the path p, by induction on the structure of p.^{2} We’ll also need realisers t′_{P} and consumers C′_{P} of finite sets of paths:

2We have recently become aware that this technique has been applied by Guy McCusker to prove full abstraction for a version of Idealized Algol [32].

t_{P ↦q} ≡_{def} λx.[C′_{P} (x) > !x′ ⇒ t_{q}]
t_{βp} ≡_{def} βt_{p}
t_{P} ≡_{def} !t′_{P}
t_{abs p} ≡_{def} abs t_{p}

C_{P ↦q} ≡_{def} C_{q}(− t′_{P})
C_{βp} ≡_{def} C_{p}(π_{β}−)
C_{P} ≡_{def} [− > !x ⇒ C′_{P} (x)]
C_{abs p} ≡_{def} C_{p}(rep −)

\begin{aligned}t′_{\{p_{1},...,p_{n}\}} & ≡_{def} t_{p_{1}} + ⋯ + t_{p_{n}} \\ C′_{\{p_{1},...,p_{n}\}} & ≡_{def} [C_{p_{1}} > !x_{1} ⇒ ⋯ ⇒ [C_{p_{n}} > !x_{n} ⇒ !∅] ⋯] \end{aligned}

(44)

Note that t′_{∅} ≡ ∅ and C′_{∅} ≡ !∅. Although the syntax of t′_{P} and C′_{P} depends on a choice of permutation of the elements of P, the semantics obtained for different permutations is the same. Indeed, we have (z being a fresh variable):

\begin{aligned}⟦t_{p}⟧ & = y_{ℙ}p \\ ⟦t′_{P} ⟧ & = i_{ℙ}P \end{aligned}  \begin{aligned}⟦λz.C_{p}(z)⟧ & = y_{ℙ→!𝕆}(\{p\} ↦ ∅) \\ ⟦λz.C′_{P} (z)⟧ & = y_{ℙ→!𝕆}(P ↦ ∅) \end{aligned}  (45)

It then follows from the substitution lemma that for any p : ℙ and ⊢ t : ℙ,

p ∈ ⟦t⟧ ⟺ ⟦C_{p}(t)⟧ ≠ ∅ .  (46)

Suppose t_{1} ⊏ ∼ t_{2} with t_{1} and t_{2} closed. Given any p ∈ ⟦t_{1}⟧ we have ⟦C_{p}(t_{1})⟧ ≠ ∅ and so using t_{1} ⊏ ∼ t_{2}, we get ⟦C_{p}(t_{2})⟧ ≠ ∅, so that p ∈ ⟦t_{2}⟧. It follows that ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧.

As for open terms, suppose Γ ≡ x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k}. Writing λx⃗.t_{1} for the closed term λx_{1}. · · · λx_{k}.t_{1} and likewise for t_{2}, we get

\begin{aligned}t_{1} ⊏ ∼ t_{2} & ⟹ & λx⃗.t_{1} ⊏ ∼ λx⃗.t_{2} \\ & ⟹ & ⟦λx⃗.t_{1}⟧ ⊆ ⟦λx⃗.t_{2}⟧ \\ & ⟹ & ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ . \end{aligned}  (47)

The proof is complete. □

3.4 Operational Semantics

HOPLA can be given a straightforward operational semantics [42] using actions defined by the grammar

a ::= u ↦ a | βa | ! | abs a .  (48)

We assign types to actions a using a judgement of the form ℙ : a : ℙ′. Intuitively, after performing the action a, what remains of a computation

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

\frac{ℚ : t[u/x] ⟶^{a} t′}{ℙ → ℚ : λx.t ⟶^{u↦a} t′}  \frac{ℙ → ℚ : t ⟶^{u↦a} t′}{ℚ : t u ⟶^{a} t′}
\frac{ℙ_{β} : t ⟶^{a} t′}{Σ_{α∈A}ℙ_{α} : βt ⟶^{βa} t′}  \frac{Σ_{α∈A}ℙ_{α} : t ⟶^{βa} t′}{ℙ_{β} : π_{β}t ⟶^{a} t′}

\overline{!ℙ : !t ⟶^{!} t}  \frac{!ℙ : u ⟶^{!} u′ ℚ : t[u′/x] ⟶^{a} t′}{ℚ : [u > !x ⇒ t] ⟶^{a} t′}

\frac{𝕋_{j}[μT⃗.𝕋⃗/T⃗] : t ⟶^{a} t′}{μ_{j}T⃗.𝕋⃗ : abs t ⟶^{abs a} t′}  \frac{μ_{j}T⃗.𝕋⃗ : t ⟶^{abs a} t′}{𝕋_{j}[μT⃗.𝕋⃗/T⃗] : rep t ⟶^{a} t′}

Figure 1: Operational rules

path in ℙ is a computation path in ℙ′:

\begin{matrix}\frac{⊢ u : ℙ ℚ : a : ℙ′}{ℙ → ℚ : u ↦ a : ℙ′} & \frac{ℙ_{β} : a : ℙ′ β ∈ A}{Σ_{α∈A}ℙ_{α} : βa : ℙ′} \\ \overline{!ℙ : ! : ℙ} & \frac{𝕋_{j}[μT⃗.𝕋⃗/T⃗] : a : ℙ′}{μ_{j}T⃗.𝕋⃗ : abs a : ℙ′} \end{matrix}  (49)

Notice that in ℙ : a : ℙ′, the type ℙ′ is unique given ℙ and a. The operational rules of Fig. 1 define a relation ℙ : t ⟶^{a} t′ where ⊢ t : ℙ and ℙ : a : ℙ′. By rule induction on the transition rules, we have

Proposition 3.8 If ℙ : t ⟶^{a} t′ with ℙ : a : ℙ′, then ⊢ t′ : ℙ′.

Accordingly, we’ll write ℙ : t ⟶^{a} t′ : ℙ′ when ℙ : t ⟶^{a} t′ and ℙ : a : ℙ′.

3.4.1 Soundness and Adequacy

For ℙ : a : ℙ′ we define a linear map a^{∗} : ℙ → !ℙ′ which intuitively maps a process t of type ℙ to a representation of its possible successors after performing the action a. In order to distinguish between, say, the successor ∅ and no successors, a^{∗} embeds into the type !ℙ′ rather than using ℙ′ itself. For instance, the successors after action ! of the processes !∅ and ∅ are, respectively,

!^{∗}⟦!∅⟧ = 1_{!ℙ}(η_{ℙ}∅) = η_{ℙ}∅ and !^{∗}⟦∅⟧ = 1_{!ℙ}∅ = ∅ .  (50)

It will be convenient to treat a^{∗} as a syntactic operation and so we define a term a^{∗}t such that ⟦a^{∗}t⟧ = a^{∗}⟦t⟧:

(u ↦ a)^{∗} = a^{∗} ∘ app ∘ (− & ⟦u⟧) (βa)^{∗} = a^{∗} ∘ π_{β} !^{∗} = 1_{!ℙ} (abs a)^{∗} = a^{∗} ∘ rep  \begin{aligned}(u ↦ a)^{∗}t & ≡ a^{∗}(t u) \\ (βa)^{∗}t & ≡ a^{∗}(π_{β}t) \\ !^{∗}t & ≡ t \\ (abs a)^{∗}t & ≡ a^{∗}(rep t) \end{aligned}  (51)

The syntactic operation a^{∗} can be viewed as providing a context which reduces a-transitions to !-transitions:

Lemma 3.9 ℙ : t ⟶^{a} t′ : ℙ′ ⟺ !ℙ′ : a^{∗}t ⟶^{!} t′ : ℙ′.

Proof. By structural induction on actions. For the prefix action ! the result is immediate. We present the case for u ↦ a, the two remaining cases being similar. As there is only one operational rule deriving transitions for applications t u we have

ℙ → ℚ : t ⟶^{u↦a} t′ : ℙ′ ⟺ ℚ : t u ⟶^{a} t′ : ℙ′ .  (52)

By the induction hypothesis the right-hand side is equivalent to

!ℙ′ : a^{∗}(t u) ⟶^{!} t′ : ℙ′ ,  (53)

and by definition of (u ↦ a)^{∗}t we are done. □

Writing ℙ : t ⟶^{a} when there exists t′ such that ℙ : t ⟶^{a} t′ : ℙ′, the following are equivalent:

(i) ℙ : t ⟶^{a}  (ii) !ℙ′ : a^{∗}t ⟶^{!}  (iii) !𝕆 : C_{∅}(a^{∗}t) ⟶^{!} .  (54)

Here, C_{∅} is the (𝕆,!ℙ′)-program context [− > !x ⇒ !∅] from the proof of full abstraction.

Thus, observations of general transitions and !-transitions are reducible to observations of !-transitions at type !𝕆. We’ll exploit this below to give an operational formulation of full abstraction.

Proposition 3.10 (Soundness) If ℙ : t ⟶^{a} t′ : ℙ′, then ⟦!t′⟧ ⊆ a^{∗}⟦t⟧.

Proof. By rule-induction on the transition rules, see App. A. □

We obtain an adequacy result using logical relations X ⊴_{ℙ} t between subsets X ⊆ ℙ and closed terms of type ℙ. Intuitively, X ⊴_{ℙ} t means that all paths in X can be “operationally realised” by t. Because of recursive types, these relations cannot be defined by structural induction on the type ℙ and we therefore employ a trick essentially due to Martin-Löf (see [53]). We define auxiliary relations p ϵ_{ℙ} t between paths p : ℙ and closed terms t of type ℙ, by induction on the structure of p:

X ⊴_{ℙ} t ⟺_{def} ∀p ∈ X. p ϵ_{ℙ} t
P ↦ q ϵ_{ℙ→ℚ} t ⟺_{def} ∀u. (P ⊴_{ℙ} u ⟹ q ϵ_{ℚ} t u)
βp ϵ_{Σ_{α∈A}ℙ_{α}} t ⟺_{def} p ϵ_{ℙ_{β}} π_{β}t
P ϵ_{!ℙ} t ⟺_{def} ∃t′. !ℙ : t ⟶^{!} t′ : ℙ and P ⊴_{ℙ} t′
abs p ϵ_{μ_{j} T⃗.𝕋⃗} t ⟺_{def} p ϵ_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} rep t

(55)

Lemma 3.11 (Main Lemma) Suppose ⊢ t : ℙ. Then ⟦t⟧ ⊴_{ℙ} t.

Proof. By structural induction on terms, see App. B. □

Proposition 3.12 (Adequacy) For ⊢ t : !ℙ we have ⟦t⟧ ≠ ∅ ⟺ !ℙ :

t ⟶^{!} .

Proof. The “⇐” direction follows from soundness. Assume ⟦t⟧ ≠ ∅. Then because ⟦t⟧ is a downwards-closed subset of !ℙ which has least element ∅, we must have ∅ ∈ ⟦t⟧. Thus ∅ ϵ_{!ℙ} t by Lemma 3.11, which implies the existence of a term t′ such that !ℙ : t ⟶^{!} t′ : ℙ as wanted. □

By (54), adequacy is equivalent to a^{∗}⟦t⟧ ≠ ∅ ⟺ ℙ : t ⟶^{a} for general terms ⊢ t : ℙ.

3.4.2 Full Abstraction w.r.t. Operational Semantics

Adequacy allows an operational formulation of contextual equivalence. For programs ⊢ t : !𝕆 we have !𝕆 : t ⟶^{!} iff ⟦t⟧ ≠ ∅ by adequacy. Hence, two terms t_{1} and t_{2} with Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ are related by contextual preorder iff for all (Γ, ℙ)-program contexts C, we have !𝕆 : C(t_{1}) ⟶^{!} ⟹ !𝕆 : C(t_{2}) ⟶^{!}.

Full abstraction is often formulated in terms of this operational preorder. With t_{1} and t_{2} as above, the inclusion ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ holds iff for all (Γ, ℙ)- program contexts C, we have !𝕆 : C(t_{1}) ⟶^{!} ⟹ !𝕆 : C(t_{2}) ⟶^{!}.

3.5 Simulation

The operational semantics supports a standard bisimulation [44, 35]:

Definition 3.13 A type-respecting relation R on closed terms is a bisimulation if the following holds. If t_{1} R t_{2} with t_{1}, t_{2} of the same type ℙ, then

1. if ℙ : t_{1} ⟶^{a} t′_{1} : ℙ′, then ℙ : t_{2} ⟶^{a} t′_{2} : ℙ′ for some t′_{2} such that t′_{1} R t′_{2};

2. if ℙ : t_{2} ⟶^{a} t′_{2} : ℙ′, then ℙ : t_{1} ⟶^{a} t′_{1} : ℙ′ for some t′_{1} such that t′_{1} R t′_{2}.

Bisimilarity, written ∼, is the largest bisimulation.

Bisimilarity is a congruence for HOPLA and coincides with notions of applicative bisimilarity [1] and higher order bisimilarity [51]—see [41].

The path semantics does not capture enough of the branching behaviour of processes to characterise bisimilarity (for that, the presheaf semantics is needed, see Sect. 6.1). As an example, the processes !∅ + !!∅ and !!∅ have the same denotation, but are clearly not bisimilar. However, using Hennessy-Milner logic we can link path equivalence to simulation, obtained as in Definition 3.13, but leaving out condition 2. In detail, we consider the fragment of Hennessy-Milner logic given by possibility and finite conjunctions; it is characteristic for simulation equivalence in the case of image-finite processes [21]. With a ranging over actions, formulae are given by

ϕ ::= ⟨a⟩ϕ | ⋀_{i≤n} ϕ_{i} .  (56)

The empty conjunction is written ⊤ and we sometimes write ϕ_{1} ∧ ⋯ ∧ ϕ_{n} for the conjunction ⋀_{i≤n} ϕ_{i}. We type formulae using judgements ϕ : ℙ, the idea being that only processes of type ℙ should be described by formulae of type ℙ.

\frac{ℙ : a : ℙ′ ϕ : ℙ′}{⟨a⟩ϕ : ℙ}  \frac{ϕ_{i} : ℙ all i ≤ n}{⋀_{i≤n} ϕ_{i} : ℙ}  (57)

A typed notion of satisfaction, written t ⊨ ϕ : ℙ, is defined by

t ⊨ ⟨a⟩ϕ : ℙ ⟺_{def} ∃t′. ℙ : t ⟶^{a} t′ : ℙ′ and t′ ⊨ ϕ : ℙ′
t ⊨ ⋀_{i≤n} ϕ_{i} : ℙ ⟺_{def} t ⊨ ϕ_{i} : ℙ for each i ≤ n . (58)

Note that ⊤ : ℙ and t ⊨ ⊤ : ℙ for all terms ⊢ t : ℙ.

Definition 3.14 Suppose ⊢ t_{1} : ℙ and ⊢ t_{2} : ℙ. We say that t_{1} and t_{2} are related by the logical preorder, written t_{1} ⊏ ∼_{L} t_{2}, iff for all formulae ϕ : ℙ we have t_{1} ⊨ ϕ : ℙ ⟹ t_{2} ⊨ ϕ : ℙ. If both t_{1} ⊏ ∼_{L} t_{2} and t_{2} ⊏ ∼_{L} t_{1}, we say that t_{1} and t_{2} are logically equivalent.

Using adequacy and adapting the proof of full abstraction, we can show that logical equivalence coincides with contextual equivalence:

Theorem 3.15 For closed terms t_{1} and t_{2} of the same type ℙ,

t_{1} ⊏ ∼ t_{2} ⟺ t_{1} ⊏ ∼_{L} t_{2} .  (59)

Proof. To each formula ϕ : ℙ we can construct a (𝕆, ℙ)-program context C_{ϕ} with the property that

!𝕆 : C_{ϕ}(t) ⟶^{!} ⟺ t ⊨ ϕ : ℙ .  (60)

Define

C_{⟨u↦a⟩ϕ} ≡_{def} C_{⟨a⟩ϕ}(− u) ,_{C_{⟨βa⟩ϕ} ≡_{def} C_{⟨a⟩ϕ}(π_{β}−) ,} C_{⟨!⟩ϕ} ≡_{def} [− > !x ⇒ C_{ϕ}(x)] ,

C_{⟨abs a⟩ϕ} ≡_{def} C_{⟨a⟩ϕ}(rep −) ,

C_{⋀_{i≤n} ϕ_{i}} ≡_{def} [C_{ϕ_{1}} > !x_{1} ⇒ ⋯ ⇒ [C_{ϕ_{n}} > !x_{n} ⇒ !∅] ⋯] .

(61)

It follows by (60) that t_{1} ⊏ ∼_{L} t_{2} iff for all formulae ϕ : ℙ we have that !𝕆 : C_{ϕ}(t_{1}) ⟶^{!} implies !𝕆 : C_{ϕ}(t_{2}) ⟶^{!}. The direction “⇒” then follows by adequacy.

For the converse, we observe that the program contexts C_{p} used in the full-abstraction proof are all subsumed by the contexts C_{ϕ}. In detail, using the terms t′_{P} realising finite sets of paths, we can define actions ℙ : a_{p} : ℙ′ and formulae ϕ_{p} : ℙ by induction on paths p : ℙ such that C_{p} ≡ C_{⟨a_{p}⟩ϕ_{p}}:

a_{P ↦q} ≡_{def} t′_{P} ↦ a_{q} a_{βp} ≡_{def} βa_{p} a_{P} ≡_{def} ! a_{abs p} ≡_{def} abs a_{p}  ϕ_{P ↦q} ≡_{def} ϕ_{q} ϕ_{βp} ≡_{def} ϕ_{p} ϕ_{P} ≡_{def} ⋀_{p∈P} ⟨a_{p}⟩ϕ_{p} ϕ_{abs p} ≡_{def} ϕ_{p}  (62)

With p : ℙ and ⊢ t : ℙ we obtain p ∈ ⟦t⟧ ⟺ ⟦C_{⟨a_{p}⟩ϕ_{p}}(t)⟧ ≠ ∅ as in the proof of full abstraction, and so by adequacy and (60), we have p ∈ ⟦t⟧ ⟺ t ⊨ ⟨a_{p}⟩ϕ_{p} : ℙ. It follows that t_{1} ⊏ ∼_{L} t_{2} implies ⟦t_{1}⟧ ⊆ ⟦t_{2}⟧, and so t_{1} ⊏ ∼ t_{2}. □

We note that the proof above establishes a link between paths and actions:

p ∈ ⟦t⟧ ⟺ ℙ : t ⟶^{a_{p}} t′ : ℙ′ and t′ ⊨ ϕ_{p} : ℙ′ .  (63)

3.6 Expressive Power

HOPLA does not have many features typical of process calculi built-in, beyond that of a nondeterministic sum and a prefix operation. It is therefore notable that we can express many kinds of concurrent processes in the language. We start by encoding the “prefix-sum” construct of [41], useful for subsequent examples. We’ll dispense with the abstract syntax abs and rep for brevity.

3.6.1 Prefixed Sum

In the original presentation of HOPLA, prefixing and the sum type where part of a single construct, the prefixed sum [41]. Consider a family of types (ℙ_{α})_{α∈A}. Their prefixed sum is the type Σ_{α∈A}α.ℙ_{α} which stands for Σ_{α∈A}!ℙ_{α}. This type describes computation paths in which first an action β ∈ A is performed before resuming as a computation path in ℙ_{β}. We’ll write α_{1}.ℙ_{α_{1}} + ⋯ + α_{k}.ℙ_{α_{k}} for a typical finite prefixed sum. The prefixed sum is associated with prefix operations taking a process t of type ℙ_{β} to β.t ≡_{def} β(!t) of type Σ_{α∈A}α.ℙ_{α} as well as a prefix match [u > β.x ⇒ t] ≡_{def} [π_{β}u > !x ⇒ t], where u has prefix-sum type, x has type ℙ_{β} and t generally involves the variable x.

Proposition 3.16 Using Propositions 3.4 and 3.5, we get:

\begin{aligned}⟦[β.u > β.x ⇒ t]⟧ & = ⟦t[u/x]⟧ \\ ⟦[α.u > β.x ⇒ t]⟧ & = ∅  if α ≠ β \\ ⟦[Σ_{i∈I}u_{i} > β.x ⇒ t]⟧ & = ⟦Σ_{i∈I}[u_{i} > β.x ⇒ t]⟧ \end{aligned}  (64)

Note that the prefixed sum is obtained using the biproduct, so coproduct, of Lin. This implies that prefixed sum is a “weak coproduct” in Cts. Because of the universal property of the coproduct in Lin and using the adjunction between Lin and Cts, there is a chain of isomorphisms

Lin(Σ_{α∈A}!ℙ_{α}, ℚ) ≅ Π_{α∈A}Lin(!ℙ_{α}, ℚ) ≅ Π_{α∈A}Cts(ℙ_{α}, ℚ)  (65)

—natural in ℚ. Hence, linear maps f : Σ_{α∈A}!ℙ_{α} → ℚ from the prefixed sum in Cts are in bijective correspondence with tuples ⟨f_{α}⟩_{α∈A} of maps from the components of the sum to ℚ in Cts. Thus, the prefixed sum is a coproduct in Cts but for the fact that the required mediating morphism is unique only within the subcategory of linear maps.

3.6.2 CCS

As in CCS [35], let N be a set of names and N̄ the set of complemented names {n̄ | n ∈ N}. Let l range over labels L =_{def} N ∪ N̄, with complementation extended to L by taking ¯ n̄ =_{def} n, and let τ be a distinct label. The type of CCS processes can then be specified as the solution to the equation

ℙ = τ.ℙ + Σ_{n∈N}n.ℙ + Σ_{n∈N} n̄.ℙ .  (66)

Below, we let α range over L ∪ {τ}. The terms of CCS are translated into HOPLA by the function H⟦−⟧,

H⟦x⟧ ≡_{def} x H⟦rec x.t⟧ ≡_{def} rec x.H⟦t⟧ H⟦Σ_{i∈I}t_{i}⟧ ≡_{def} Σ_{i∈I}H⟦t_{i}⟧ H⟦α.t⟧ ≡_{def} α.H⟦t⟧  H⟦t|u⟧ ≡_{def} Par H⟦t⟧ H⟦u⟧ H⟦t \ S⟧ ≡_{def} Res_{S} H⟦t⟧ H⟦t[f]⟧ ≡_{def} Rel_{f} H⟦t⟧  (67)

Here, Par : ℙ → (ℙ → ℙ) (curried for convenience), Res_{S} : ℙ → ℙ, and Rel_{f} : ℙ → ℙ are abbreviations for the following recursively defined processes:

Par ≡_{def} rec p.λx.λy.\begin{matrix}Σ_{α}[x > α.x′ ⇒ α.(p x′ y)] + \\ Σ_{α}[y > α.y′ ⇒ α.(p x y′)] + \\ Σ_{l}[x > l.x′ ⇒ [y > l̄.y′ ⇒ τ.(p x′ y′)]] \end{matrix}

Res_{S} ≡_{def} rec r.λx.Σ_{α∉(S∪S̄)}[x > α.x′ ⇒ α.(r x′)]
Rel_{f} ≡_{def} rec r.λx.Σ_{α}[x > α.x′ ⇒ f(α).(r x′)]

(68)

The operational semantics for CCS induced by the translation agrees with that given by Milner:

Proposition 3.17 If t ⟶^{α} t′ is derivable in CCS, then ℙ : H⟦t⟧ ⟶^{α!} H⟦t′⟧ : ℙ. Conversely, if ℙ : H⟦t⟧ ⟶^{a} u : ℙ, then a ≡ α! and u ≡ H⟦t′⟧ for some α, t′ such that t ⟶^{α} t′ according to CCS.

It follows that the translations of two CCS terms are bisimilar in HOPLA iff they are strongly bisimilar in CCS.

We can recover Milner’s expansion law [34] directly from the properties of the prefixed sum. Write t|u for the application Par t u, where t and u are terms of type ℙ. Suppose

⟦t⟧ = ⟦Σ_{α}Σ_{i∈I(α)}α.t_{i}⟧ and ⟦u⟧ = ⟦Σ_{α}Σ_{j∈J(α)}α.u_{j}⟧ .  (69)

Using Corollaries 3.3 and 3.2, then Proposition 3.16, ⟦t|u⟧ equals the denotation of the expansion

Σ_{α}Σ_{i∈I(α)}α.(t_{i}|u) + Σ_{α}Σ_{j∈J(α)}α.(t|u_{j}) + Σ_{l}Σ_{i∈I(l),j∈J(l̄)}τ.(t_{i}|u_{j}) . (70)

3.6.3 Higher-Order CCS

The language considered by Hennessy [22] is like CCS but where processes are passed at channels C; the language can be seen as an extension of Thomsen’s CHOCS [51]. For a translation into HOPLA, we follow Hennessy in defining types that satisfy the equations^{3}

ℙ = τ.ℙ + Σ_{c∈C} c̄.ℂ + Σ_{c∈C}c.𝔽 ℂ = ℙ & ℙ 𝔽 = ℙ → ℙ .  (71)

We are chiefly interested in the parallel composition of processes, Par_{ℙ,ℙ} of type ℙ & ℙ → ℙ. 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 and parallel composition defined as a simultaneous recursive definition. Writing (−|−) for all the components of the solution, the denotation of a parallel composition t|u of processes equals the denotation of the expansion

\begin{matrix}Σ_{α}[t > α.x ⇒ α.(x|u)] + \\ Σ_{α}[u > α.y ⇒ α.(t|y)] + \\ Σ_{c}[t > c.f ⇒ [u > c̄.p ⇒ τ.((f π_{1}p)|π_{2}p)]] + \\ Σ_{c}[t > c̄.p ⇒ [u > c.f ⇒ τ.(π_{2}p|(f π_{1}p))]] . \end{matrix}  (72)

In the summations, c ∈ C and α ranges over labels c, c̄, τ.

The bisimulation induced on higher-order CCS terms is perhaps the one to be expected; a corresponding bisimulation relation is defined like an applicative bisimulation but restricted to the types of processes ℙ, concretions ℂ, and abstractions 𝔽.

In a similar way, we can encode Cardelli and Gordon’s Ambient Calculus with public names [10, 11], see [41]. HOPLA can thus express certain forms of mobility of processes by virtue of allowing process passing. Another kind of mobility, mobility of communication links, arises from name-generation as in the π-calculus [36]. Inspired by HOPLA, Francesco Zappa Nardelli and GW have defined a higher-order process language with name-generation, allowing encodings of full ambient calculus and π-calculus. Bisimulation properties and semantic underpinnings are being developed [55].

3See Page 12 for how to encode the binary product ℙ & ℙ.

4 Linearity

The move from Lin to Cts has allowed us to interpret prefixing. In fact, we can do much the same more cheaply.

The category Cts is obtained from Lin using an exponential which allows arbitrary copying in linear logic. An element P ∈ !ℙ consists of several, possibly no, computation paths of ℙ. An element of the path order !ℙ can therefore be understood intuitively as describing a compound computation path associated with running several copies of a process of type ℙ. Maps ℙ → ℚ of Cts, corresponding to maps !ℙ → ℚ of Lin, allow their input to be copied, as witnessed by the fact that the type system of HOPLA allows contraction.

However, copying is generally restricted in a distributed computation. A communication received is most often the result of a single run of the process communicated with. Of course, process code can be sent and copied. But generally the receiver has no possibility of rewinding or copying the state of an ongoing computation. On the other hand, ignoring another process is often easy. For this reason, many operations of distributed computation have the following property [40]:

Affine linearity: a computation path of the process arising from the application of an operation to an input process has resulted from at most one computation path of the input process.

Note in particular that prefix operations are affine in this sense: if we wish to observe just the initial action of a process !t, no computation path of t is needed, though observing any longer path will involve a (single) computation path of t.

Recall the diagram (2) which says that linear maps ℙ → ℚ are determined by their values on single paths, elements of ℙ. Via the adjunction between Lin and Cts, continuous maps ℙ → ℚ are determined by their values on compound paths in !ℙ (diagram (7)). To summarise:

• linear operations use a single path of the input;

• affine operations use at most one path of the input;

• continuous operations use any number of paths of the input.

Affine maps are defined by their values on singleton copies of paths together with the empty path. Accordingly, affine maps derive from the lifting operation (−)_{⊥} adding a new element ⊥, to be thought of as the empty computation path, below a copy of a path order ℙ to produce a path order ℙ_{⊥}.

Abstractly, ℙ_{⊥} is the empty-join completion of ℙ; concretely, we can take ℙ_{⊥} to contain the empty set, written ⊥, together with singletons {p} for p ∈ ℙ, ordered by ⪯_{ℙ}. There is an obvious inclusion of the empty-join completion of ℙ into ℙ̂, in the form of a map j_{ℙ} : ℙ_{⊥} → ℙ̂ sending ⊥ to ∅ and {p} to y_{ℙ}p. We’ll use P to range over ℙ_{⊥} in what follows. The map j_{ℙ} assumes the role of i_{ℙ}; for any X ∈ ℙ̂ and P ∈ ℙ_{⊥} we have j_{ℙ}P ⊆ X iff P ⪯_{ℙ} X, and from (1) we get

X = ⋃_{p∈X} y_{ℙ}p = ∅ ∪ ⋃_{p∈X} y_{ℙ}p = ⋃_{P ⪯_{ℙ}X} j_{ℙ}P .  (73)

This join is manifestly nonempty and in fact, ℙ̂ is the free closure of ℙ_{⊥} under nonempty joins. This means that given any monotone map f : ℙ_{⊥} → C for some nonempty-join complete poset C, there is a unique nonemptyjoin preserving (i.e. affine) map f^{§} : ℙ̂ → C such that the diagram below commutes:

\xymatrix{ℙ_{⊥} \ar[r]^{j_{ℙ}} \ar[dr]_{f} & ℙ̂ \ar@{.>}[d]^{f^{§}} \\  & C}  f^{§}X = ⋃_{P ⪯_{ℙ}X} fP .  (74)

Uniqueness of f^{§}, called the extension of f along j_{ℙ}, follows from (73). As before, we can replace C by a nondeterministic domain ℚ̂ and by the freeness properties (2) and (74), there is a bijective correspondence between linear maps ℙ_{⊥} → ℚ and affine maps ℙ̂ → ℚ̂.

We define the category Aff to have path orders ℙ, ℚ, … as objects and affine maps ℙ̂ → ℚ̂ as arrows. Again, the structure of Aff is induced by that of Lin via an adjunction between the two categories with the inclusion Lin ↪ Aff (linear maps are affine) as right adjoint:

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

The unit η_{ℙ} : ℙ → ℙ_{⊥} in Aff, the counit ε_{ℙ} : ℙ_{⊥} → ℙ in Lin, and the left adjoint (−)_{⊥} : Aff → Lin are obtained precisely as in Sect. 2.2.

Aff inherits products Σ_{α∈A}ℙ_{α} with weak coproduct properties from Lin in the same way as Cts does. However, unlike Cts, the category Aff is not cartesian closed because ℙ_{⊥} × ℚ_{⊥} and (ℙ & ℚ)_{⊥} are not isomorphic in Lin. On the other hand we can easily define a tensor operation ⊗ on Aff such that the path orders ℙ_{⊥} ×ℚ_{⊥} and (ℙ⊗ℚ)_{⊥} become isomorphic: simply take ℙ⊗ℚ to be (ℙ_{⊥} ×ℚ_{⊥})\{(⊥, ⊥)}. Paths of ℙ⊗ℚ then consist of a (possibly empty) path of ℙ and a (possibly empty) path of ℚ, and so a path set X ∈ { \atop ℙ ⊗ ℚ} can be thought of as a process performing two parallel computation paths, one of type ℙ and one of type ℚ. On arrows f : ℙ → ℙ′ and g : ℚ → ℚ′ in Aff, we define f ⊗ g : ℙ ⊗ ℚ → ℙ′ ⊗ ℚ′ as the extension h^{§} of the map

h : ℙ_{⊥} × ℚ_{⊥} ≅ (ℙ ⊗ ℚ)_{⊥} → { \atop ℙ′ ⊗ ℚ′} defined by

(P′, Q′) ∈ h(P, Q) ⟺ P′ ∈ (η_{ℙ′} ∘ f ∘ j_{ℙ})P and Q′ ∈ (η_{ℚ′} ∘ g ∘ j_{ℚ})Q . (76)

The unit of tensor is the empty path order 𝕆. Elements X ∈ ℙ̂ correspond to maps X̄ : 𝕆 → ℙ in Aff and with Y ∈ ℚ̂, we’ll write X ⊗ Y for the element of { \atop ℙ ⊗ ℚ} pointed to by the map X̄ ⊗ Ȳ. The tensor makes Aff a symmetric monoidal category, and again, the adjunction (75) is symmetric monoidal. The obvious isomorphisms of path orders,

𝟙 ≅ 𝕆_{⊥} and ℙ_{⊥} × ℚ_{⊥} ≅ (ℙ ⊗ ℚ)_{⊥} ,  (77)

induce natural isomorphisms in Lin and we obtain a monoidal strength ℙ ⊗ ℚ_{⊥} → (ℙ ⊗ ℚ)_{⊥} precisely as for Cts.

Finally, the monoidal closed structure of Lin together with the natural isomorphism ℙ_{⊥} × ℚ_{⊥} ≅ (ℙ ⊗ ℚ)_{⊥} provide a right adjoint (ℚ ⊸ −), defined by (ℚ_{⊥} ⊸ −), to the functor (− ⊗ ℚ) in Aff via the chain

Aff(ℙ ⊗ ℚ, ℝ) ≅ Lin((ℙ ⊗ ℚ)_{⊥}, ℝ) ≅ Lin(ℙ_{⊥} × ℚ_{⊥}, ℝ) ≅ Lin(ℙ_{⊥}, ℚ_{⊥} ⊸ ℝ) ≅ Aff(ℙ, ℚ_{⊥} ⊸ ℝ) = Aff(ℙ, ℚ ⊸ ℝ) (78)

—natural in ℙ and ℝ. This demonstrates that Aff is symmetric monoidal closed and since the unit of the tensor is terminal, a model of affine linear logic, as already observed in [25].

5 Affine HOPLA

Affine HOPLA is a typed process language suggested by the structure of Aff [40]. Even though we replace the type constructor !(−) by (−)_{⊥}, we’ll continue to use ! for the action in prefixing.

5.1 Denotational Semantics

Types are given by the grammar

𝕋 ::= 𝕋_{1} ⊸ 𝕋_{2} | 𝕋_{1} ⊗ 𝕋_{2} | Σ_{α∈A}𝕋_{α} | 𝕋_{⊥} | T | μ_{j}T⃗.𝕋⃗ .  (79)

Again, closed type expressions are interpreted as path orders. For the solution of recursive type definitions we proceed as for HOPLA, replacing finite sets of paths by sets P of size at most one, writing ⊥ for the empty set.

p, q ::= P ↦ q | P ⊗ Q | βp | P | abs p  (80)

Here, P ⊗ Q stands for a pair of paths P of ℙ_{⊥} and Q of ℚ_{⊥} where at least one is non-⊥. Formation rules are displayed below alongside rules defining the ordering. Note that all path orders interpreting types of Affine HOPLA are posets because, unlike the exponential, the comonad (−)_{⊥} maps posets to posets.

\frac{P : ℙ_{⊥} q : ℚ}{P ↦ q : ℙ ⊸ ℚ}  \frac{P′ ≤_{ℙ_{⊥}} P q ≤_{ℚ} q′}{P ↦ q ≤_{ℙ⊸ℚ} P′ ↦ q′}
\frac{P : ℙ_{⊥} Q : ℚ_{⊥} (P, Q) ≠ (⊥, ⊥)}{P ⊗ Q : ℙ ⊗ ℚ}  \frac{P ≤_{ℙ_{⊥}} P′ Q ≤_{ℚ_{⊥}} Q′}{P ⊗ Q ≤_{ℙ⊗ℚ} P′ ⊗ Q′}
\frac{p : ℙ_{β} β ∈ A}{βp : Σ_{α∈A}ℙ_{α}}  \frac{p ≤_{ℙ_{β}} p′ β ∈ A}{βp ≤_{Σ_{α∈A}ℙ_{α}} βp′}
\overline{⊥ : ℙ_{⊥}}  \frac{p : ℙ}{\{p\} : ℙ_{⊥}}  \frac{P ⪯_{ℙ} P′}{P ≤_{ℙ_{⊥}} P′}
\frac{p : 𝕋_{j}[μT⃗.𝕋⃗/T⃗]}{abs p : μ_{j}T⃗.𝕋⃗}  \frac{p ≤_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} p′}{abs p ≤_{μ_{j} T⃗.𝕋⃗} abs p′}

(81)

The raw syntax of terms is given by

t, u ::= x | rec x.t | Σ_{i∈I}t_{i} | λx.t | t u | t ⊗ u | [u > x ⊗ y ⇒ t] | αt | π_{α}t | !t | [u > !x ⇒ t] | abs t | rep t .  (82)

The use of a pattern match term for tensor is similar to that in [2]. Let ℙ_{1}, …, ℙ_{k}, ℚ be closed type expressions and x_{1}, …, x_{k} distinct variables. A syntactic judgement x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ stands for a map

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

in Aff. When the environment list is empty, the corresponding tensor product is the empty path order 𝕆. The term-formation rules for Affine HOPLA are very similar to those for HOPLA, replacing & by ⊗ in the handling of environment lists and the type constructors !(−) and → by (−)_{⊥} and ⊸. We discuss the remaining differences in the following.

New rules are introduced for the tensor operation:

\frac{Γ ⊢ t : ℙ Λ ⊢ u : ℚ}{Γ, Λ ⊢ t ⊗ u : ℙ ⊗ ℚ} \frac{Γ ⟶^{t} ℙ Λ ⟶^{u} ℚ}{Γ ⊗ Λ ⟶^{t⊗u} ℙ ⊗ ℚ}  (84)

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

One important difference is the lack of contraction for the affine language. This restricts substitution of a common term into distinct variables, and so copying. The counterpart in the model is the absence of a suitable diagonal map from objects ℙ to ℙ ⊗ ℙ; for example, the map X ↦ X ⊗ X from ℙ̂ to { \atop ℙ ⊗ ℙ} is not in general a map in Aff.^{4} Consider a term t(x, y), with its free variables x and y shown explicitly, for which

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

corresponding to a map ℙ ⊗ ℙ ⟶^{t} ℚ 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. Intuitively, if any computation for t involves both inputs, then x : ℙ ⊢ t(x, x) : ℚ would use the same input twice and therefore cannot be interpreted in Aff. There is a syntactic condition on the occurrences of variables which ensures that in any computation, at most one of a set of variables is used.

Definition 5.1 Let v be a raw term. Say a set of variables V is crossed in v iff there are subterms of v of the form tensor t ⊗ u, application t u, tensor match [u > x ⊗ y ⇒ t], or prefix match [u > !x ⇒ t], for which v has free occurrences of variables from V appearing in both t and u.

If the set {x, y} is not crossed in t(x, y) above, then t uses at most one of its inputs x, y in each computation; semantically, t is interpreted as a map ℙ⊗ℙ → ℚ of Aff which behaves identically on input X⊗Y and X⊗∅+∅⊗Y for all X, Y ∈ ℙ̂. In this case x : ℙ ⊢ t(x, x) : ℚ holds and is interpreted as the composition

ℙ ⟶^{δ_{ℙ}} ℙ ⊗ ℙ ⟶^{t} ℚ  (87)

—where δ_{ℙ} : ℙ → ℙ ⊗ ℙ maps X to X ⊗ ∅ + ∅ ⊗ X. We’ll write δ_{ℙ}^{k} : ℙ → ℙ^{k} for the obvious generalisation to a k-fold tensor product ℙ^{k} = ℙ ⊗ ⋯ ⊗ ℙ.

We can now give the rule for recursively defined processes in Affine HOPLA:

\frac{Γ, x : ℙ ⊢ t : ℙ \{x, y\} not crossed in t for any y in Γ}{Γ ⊢ rec x.t : ℙ}  \frac{Γ ⊗ ℙ ⟶^{t} ℙ}{Γ ⟶^{fix F} ℙ} (88)

Here, fix F is the fixpoint in Aff(Γ, ℙ) ≅ { \atop Γ ⊸ ℙ} of the continuous operation F mapping g : Γ → ℙ in Aff to the composition

Γ ⟶^{δ_{Γ}} Γ ⊗ Γ ⟶^{1_{Γ}⊗g} Γ ⊗ ℙ ⟶^{t} ℙ .  (89)

4To see this, assume that ℙ is the prefixed sum α.𝕆 + β.𝕆 with paths abbreviated to α, β. Confusing paths with the corresponding primes, the nonempty join α + β is sent by X ↦ X ⊗ X to α ⊗ α + β ⊗ β + α ⊗ β + β ⊗ α instead of α ⊗ α + β ⊗ β as would be needed to preserve nonempty joins.

5.2 Useful Identities

Counterparts of the results for HOPLA of Sect. 3.2 can now be proved for Affine HOPLA. In particular, a general substitution lemma can be formulated as follows:

Lemma 5.2 (Substitution) Suppose Γ, x_{1} : ℙ, …, x_{k} : ℙ ⊢ t : ℚ with {x_{1}, …, x_{k}} not crossed in t. If Λ ⊢ u : ℙ with Γ and Λ disjoint, then Γ, Λ ⊢ t[u/x_{1}, …, u/x_{k}] : ℚ with denotation given by the composition

Γ ⊗ Λ ⟶^{1_{Γ}⊗(δ_{ℙ}^{k}∘u)} Γ ⊗ ℙ^{k} ⟶^{t} ℚ .  (90)

An easy induction on typing derivations shows that if Γ, x : ℙ ⊢ t : ℚ, then {x} is not crossed in t, and so the substitution lemma specialises to

Corollary 5.3 If Γ, x : ℙ ⊢ t : ℚ and Λ ⊢ u : ℙ with Γ and Λ disjoint, then we have Γ, Λ ⊢ t[u/x] : ℚ with ⟦(λx.t) u⟧ = ⟦t[u/x]⟧.

Corollary 5.4 Suppose Γ, x : ℙ ⊢ t : ℙ. Then Γ ⊢ t[rec x.t/x] : ℙ with ⟦rec x.t⟧ = ⟦t[rec x.t/x]⟧.

Proof. We proceed as in the proof of Corollary 3.3, obtaining Γ′, x : ℙ ⊢ t′ : ℙ and Γ′′, x : ℙ ⊢ t′′ : ℙ with Γ′ and Γ′′ disjoint by renaming variables y of Γ to y′ and y′′. By the substitution lemma with k = 1, we get Γ′, Γ′′ ⊢ t′[rec x.t′′/x] : ℙ denoting

Γ′ ⊗ Γ′′ ⟶^{1_{Γ′}⊗rec x.t′′} Γ′ ⊗ ℙ ⟶^{t′} ℙ .  (91)

Now, since the sets {x, y} are not crossed in t, the sets {y′, y′′} are not crossed in t′[rec x.t′′/x]. Hence, by repeated use of exchange and the substitution lemma with k = 2, we may perform substitutions [y/y′, y/y′′] to obtain Γ ⊢ t[rec x.t/x] : ℙ with denotation

Γ ⟶^{δ_{Γ}} Γ ⊗ Γ ⟶^{1_{Γ}⊗rec x.t} Γ ⊗ ℙ ⟶^{t} ℙ .  (92)

Again, this is the same as F (fix F) = fix F, the denotation of rec x.t. □

The properties of sums and prefixing are the same as for HOPLA.

Proposition 5.5 The tensor match satisfies

⟦[u_{1} ⊗ u_{2} > x ⊗ y ⇒ t]⟧ = ⟦t[u_{1}/x, u_{2}/y]⟧  (93)
⟦[u > x ⊗ y ⇒ Σ_{i∈I}t_{i}]⟧ = ⟦Σ_{i∈I}[u > x ⊗ y ⇒ t_{i}]⟧  (94)
⟦[Σ_{i∈I}u_{i} > x ⊗ y ⇒ t]⟧ = ⟦Σ_{i∈I}[u_{i} > x ⊗ y ⇒ t]⟧ if I ≠ ∅ (95)

Further, if x_{1} and y_{1} are not free in t, then

⟦[[u_{1} > x_{1} ⊗ y_{1} ⇒ u_{2}] > x_{2} ⊗ y_{2} ⇒ t]⟧ = ⟦[u_{1} > x_{1} ⊗ y_{1} ⇒ [u_{2} > x_{2} ⊗ y_{2} ⇒ t]]⟧ . (96)

Proof. All the properties are consequences of tensor match being interpreted as composition in Aff. Equation (93) follows by exchange and two applications of the substitution lemma. The two distributive properties hold since composition f ∘ g in Aff is linear in f and affine in g. Finally, (96) follows from associativity of composition. □

5.3 Full Abstraction

As for HOPLA, we take a program to be a closed term t of type 𝕆_{⊥}, but because of linearity constraints, program contexts will now have at most one hole. Otherwise, the notion of contextual preorder is the same as in Sect. 3.3. Again, contextual equivalence coincides with path equivalence:

Theorem 5.6 (Full abstraction) For any terms Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ,

⟦t_{1}⟧ ⊆ ⟦t_{2}⟧ ⟺ t_{1} ⊏ ∼ t_{2} .  (97)

Proof. Path “realisers” and “consumers” are defined as in the proof of full abstraction for HOPLA, restricting the terms t′_{P} and C′_{P} to the cases where P has at most one element. Terms corresponding to paths of tensor type are defined by

\begin{aligned}t_{P ⊗Q} & ≡ t′_{P} ⊗ t′_{Q} \\ C_{P ⊗Q} & ≡ [− > x ⊗ y ⇒ [C′_{P} (x) > !x′ ⇒ C′_{Q}(y)]] \end{aligned}  (98)

For any p : ℙ and P : ℙ we then have (z being a fresh variable):

\begin{aligned}⟦t_{p}⟧ & = y_{ℙ}p \\ ⟦t′_{P} ⟧ & = j_{ℙ}P \end{aligned}  \begin{aligned}⟦λz.C_{p}(z)⟧ & = y_{ℙ⊸𝕆_{⊥}}(\{p\} ↦ ∅) \\ ⟦λz.C′_{P} (z)⟧ & = y_{ℙ⊸𝕆_{⊥}}(P ↦ ∅) \end{aligned}  (99)

We can now proceed as in the proof of Theorem 3.7. □

5.4 Expressive Power

Subject to the linearity constraints on variables, Affine HOPLA has much of the expressive power of HOPLA. In particular, the calculi discussed in Sects. 3.6.2 and 3.6.3 can be encoded with the restriction that no variable can occur freely on both sides of a parallel composition. The prefixed sum Σ_{α∈A}α.ℙ_{α} stands for Σ_{α∈A}(ℙ_{α})_{⊥} in Affine HOPLA. Prefixing β.t is still translated into β!t, but now has a different semantics. For example, by replacing !(−) with (−)_{⊥}, the solution of the equation (66) defining the type of CCS processes becomes isomorphic to the partial order of strings over the alphabet of CCS actions. Thus, the semantics of CCS given by the translation into Affine HOPLA is a traditional trace semantics. This is illustrated by the fact that the two CCS processes α.β.∅ + α.γ.∅ and α.(β.∅ + γ.∅) are given the same semantics by the Affine HOPLA translation, but can be told apart by the HOPLA context C_{⟨α⟩(⟨β⟩⊤∧⟨γ⟩⊤)}, see Sect. 3.5.

More interestingly, the tensor type of Affine HOPLA allows us to define processes of the kind encountered in treatments of nondeterministic dataflow [27], something which is not possible using HOPLA. To illustrate, define ℙ recursively as the prefixed sum

ℙ = α.ℙ + β.ℙ ,  (100)

so that ℙ essentially consists of streams (or sequences) of α’s and β’s. We can then define dataflow processes whose properties can be determined from the above results about the denotational semantics—in particular using Proposition 5.5:

• A process A of type ℙ⊗ℙ which produces two identical, parallel streams of α’s and β’s as output:

A ≡ rec p.[p > x ⊗ y ⇒ (α.x ⊗ α.y) + (β.x ⊗ β.y)] .  (101)

The denotation of A is the set of pairs (s, s′) with s and s′ strings of α’s and β’s, such that s is a prefix of s′ or vice versa. Notice the “entanglement” between the two sides of the tensor—choices made on one side affect choice on the other.

• A process B of type ℙ ⊸ (ℙ ⊗ ℙ) which is like A, except it produces its two output streams as copies of the input stream:

B ≡ rec f.λz.\begin{matrix}[z > α.z′ ⇒ [f z′ > x ⊗ y ⇒ α.x ⊗ α.y]] + \\ [z > β.z′ ⇒ [f z′ > x ⊗ y ⇒ β.x ⊗ β.y]] . \end{matrix}  (102)

We have e.g. ⟦B (α.β.∅)⟧ = ⟦α.β.∅ ⊗ α.β.∅⟧ and ⟦B (α.∅ + β.∅)⟧ = ⟦α.∅ ⊗ α.∅ + β.∅ ⊗ β.∅⟧, the latter not containing “cross terms” like α.∅ ⊗ β.∅.

• A process C of type (ℙ ⊗ ℙ) ⊸ ℙ which merges two streams into one:

C ≡ rec f.λz.[z > x ⊗ y ⇒ \begin{matrix}[x > α.x′ ⇒ α.f (y ⊗ x′)] + \\ [x > β.x′ ⇒ β.f (y ⊗ x′)]] . \end{matrix}  (103)

We have e.g. ⟦C (α.α.∅ ⊗ β.β.∅)⟧ = ⟦α.β.α.β.∅⟧.

A “trace operation” to represent dataflow processes with feedback loops is not definable in Affine HOPLA, because then we would have obtained a compositional relational semantics of nondeterministic dataflow with feedback, shown impossible by Brock and Ackerman [9]. However, with a more refined notion of “relation”, which spells out the different ways in which input and output of a dataflow process are related, such a semantics is in fact possible [23].

6 Related Work

We conclude by setting the specific results of this paper in the context of what we see as a promising broader enterprise towards a full domain theory for concurrency.

6.1 Presheaf Semantics

We have investigated the path semantics of HOPLA and Affine HOPLA. In reality HOPLA and Affine HOPLA were discovered within a more informative domain theory than that based on path sets. As remarked earlier, the domain of path sets ℙ̂, of a path order ℙ, is isomorphic to characteristic functions [ℙ^{op}, 2], ordered pointwise. In modelling a process as a path set we are in effect representing a process by a characteristic function from paths to truth values 0 < 1. If instead of these simple truth values we take sets of realisers, replacing 2 by the category of sets Set, we obtain a functor category [ℙ^{op}, Set], whose objects, traditionally called presheaves, provide an alternative “domain” of meanings; now a process denotes a presheaf in which a path is associated with the set of elements standing for the ways in which the path can be realised.

For the presheaf semantics of HOPLA we can obtain a more refined adequacy result than that for the path semantics: Letting ⊢ t : !ℙ, the set of realisers ⟦t⟧(∅) corresponds to the set of derivations of !ℙ : t ⟶^{!} t′ : ℙ. In fact, a guiding principle in designing the operational semantics has been that derivations of transitions of which the actions are essentially paths should correspond to the realisers associated to the path in the denotational semantics; this generally determines the form of rules.

A presheaf captures the nondeterministic branching of a process and a presheaf semantics can support equivalences such as forms of bisimulation which are sensitive to the branching behaviour of processes. Though here our understanding of the role of open maps and open map bisimulation, intrinsic to presheaf models [26], is very incomplete.

The presheaf semantics helps expose a range of possible pseudo comonads with which to interpret !ℙ [15, 40].

6.2 Powerdomains

The adjunction between Lin and Cts, key to our semantics of HOPLA, determines a monad, the monad of the “Hoare powerdomain” [52]. The adjunction between Lin and Cts is of the kind already studied in the early work of Hennessy and Plotkin [20]; they were concerned with adjunctions between categories of nondeterministic cpos and categories of cpos associated with a variety of powerdomains. This was in the days prior to linear logic. But models of linear logic are obtained by cutting down their adjunctions.

Like the model of linear logic formed from Lin and Cts, we expect that each model furnishes a denotational semantics of HOPLA. Presumably there are full abstraction results companion to that here based on detecting the “must” as well as “may” behaviour of processes. Just as there is an abstraction function from the presheaf semantics of HOPLA to its path semantics (induced by sending nonempty sets of realisers to 1 and the empty set to 0), so can we expect other abstraction functions from the presheaf semantics to other powerdomain semantics. But presently all this is conjectural.

Note that this use of powerdomains doesn’t fit the original pattern proposed for handling concurrency via a recursively defined powerdomain of resumptions [46]; rather one defines domains of paths recursively and only then adjoins nondeterminism.

6.3 An Underlying Language?

Most process languages have developed incrementally, based on previously known languages. Even HOPLA and Affine HOPLA are essentially lambdacalculi extended by nondeterministic sum and prefix operations (though the latter are understood as arising from a comonad associated with models of linear logic). Proof theory is beginning to influence ideas on the nature of processes. A recent impetus has been the discovery of linear logic, a discovery founded on the domain theory of coherence spaces with linear and stable maps [19]. Similarly we can hope that a persuasive mathematical model of processes can guide us towards a fuller understanding of processes and their syntax.

We have a rich model in the linear category analogous to Lin but based on presheaves rather than path sets. Just as maps in Lin correspond to relations, the analogous maps correspond to profunctors, a generalisation of relations (see e.g. [7] for an elementary introduction to profunctors, there called “distributors”). The bicategory of profunctors Prof is analogous to Lin.^{5} Like Lin the bicategory Prof has an involution so that maps f : ℙ → ℚ correspond to their dual f^{⊥} : ℚ^{⊥} → ℙ^{⊥}. Indeed, again just as in Lin, a map f : ℙ → ℚ corresponds to a map f′ : ℙ × ℚ^{⊥} → 𝟙, in which we have “dualised” the output to input.

It is because of this duality that open maps and open-map bisimulation for higher-order processes take as much account of input as they do output. Most often two higher-order processes are defined to be bisimilar iff they yield bisimilar outputs on any common input. But this simply won’t do within a type discipline in which all nontrivial output can be “dualised” to input. On the other hand, traditional process languages and their types don’t support this duality.

One line towards understanding open-map bisimulation at higher order is to design a process language in which this duality is present. The language could support the types of Prof extended by a suitable pseudo comonad. Ideally one would obtain a coinductive charactisation of open map bisimulation at higher order based on an operational semantics. (The mathematics for this enterprise is developed in [15].)

6.4 Affine Models

Linear maps alone are too restrictive to support a semantics of processes. To do so they must be moderated through the use of a (pseudo) comonad, the simplest of which is lifting.

There is a category analogous to Aff based on presheaves rather than path sets; its maps preserve connected colimits in presheaf categories [40, 15]. This affine category is host to the semantics of nondeterministic dataflow [23], event-structure semantics of CCS and related languages [12] as well as a semantics for Affine HOPLA.

It came as a recent surprise [43] that the presheaf denotations of firstorder processes in Affine HOPLA can be represented by event structures; the elements of definable presheaves can be understood as finite configurations of an event structure. In more detail, maps definable in Affine HOPLA by open terms can be represented by certain spans of event structures with composition given by pullbacks. This sheds light on the tensor operation and the form of entanglement associated with it, revealing the tensor as a form of parallel composition of event structures and entanglement as a pattern of concurrency/conflict. The event-structure semantics extends to all types, so higher-order processes. Though, as one would expect, the event-structure semantics diverges from the presheaf semantics at higher-order; the eventstructure semantics is analogous to stable domain theory [6].

5The bicategory Prof is equivalent to the 2-category in which maps are colimitpreserving functors between presheaf categories, perhaps a more immediate analogue of Lin.

As mentioned above, we can define a semantics for CCS using Affine HOPLA subject to certain restrictions on occurrences of variables. Unfortunately, one can show the event-structure denotations of Affine HOPLA are too impoverished to coincide with the standard “true concurrency” semantics of CCS as e.g. given in [54]. A language must go beyond Affine HOPLA if it is to express such semantics. Guidelines on what’s lacking in Affine HOPLA can be got from work on presheaf models for concurrency [12], where the ingredients of product of presheaves, pomset augmentation and cartesian liftings (extending the match operators of Affine HOPLA) all play a critical role. This work suggests exploring other event-structure representations, based on more general spans of event structures, and perhaps a new comonad yielding a less rigid form of prefixing.

As a general point, the affine category based on presheaves is very rich in structure and supports a great many mathematical constructions which lie outside the scope of the present syntax of Affine HOPLA.

An operational semantics for the tensor-fragment of Affine HOPLA (leaving out function space) was given in [40]. But it has proved very challenging to extend this to higher order. Linearity obliges us to work with rather complicated environments, and entanglement of terms of tensor type in the execution of processes. (Note that the simplifying equation (95) is not valid in the presheaf semantics, not even up to isomorphism, because there, affine maps preserve connected colimits, and any nontrivial sum is manifestly not connected.) It is the interaction of the environments with higher-order processes which has been problematic in giving an operational semantics to full Affine HOPLA.

However the event-structure denotational semantics of Affine HOPLA suggests an alternative operational semantics obviating the need for complicated environments. It is at the cost of having transitions between open terms. Taking advantage of stability, the configurations of an event structure representing an open term x : ℙ ⊢ t : ℚ, will be associated with both an output q ∈ ℚ and a minimal input, P ∈ ℙ_{⊥} necessary for that output. The idea is that such a configuration will correspond to a derivation in the operational semantics of a transition x : P ⊢ t ⟶^{q} t′ [43].

6.5 Name Generation

Process languages often follow the pioneering work on the π-calculus and allow name generation. HOPLA can be extended to encompass such languages [55]. The extensions are to add a type of names N, function spaces, as well as a type δℙ supporting new-name generation through the abstraction new x.t. The denotational semantics of the extension to name generation is currently being developed; this addresses the question of when function spaces exist in the obvious model (extending that of [13]). There is already an operational semantics; it is like that of HOPLA but given at stages indexed by the current set of names.

Acknowledgments. The authors are glad to take this opportunity, that of Dana Scott’s retirement, to express their indebtedness to Dana Scott for his pioneering and visionary work in logic and computation. GW would like to add his gratitude for many past kindnesses.

References

[1] S. Abramsky. The lazy lambda calculus. In D. Turner, editor. Research Topics in Functional Programming. Addison-Wesley, 1990.

[2] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–57, 1993.

[3] S. Abramsky. Game semantics for programming languages. In Proc. MFCS’97, LNCS 1295.

[4] N. Benton, G. Bierman, V. de Paiva and M. Hyland. Linear λ-calculus and categorical models revisited. In Proc. CSL’92, LNCS 702.

[5] P. N. Benton. A mixed linear and non-linear logic: proofs, terms and models (extended abstract). In Proc. CSL’94, LNCS 933.

[6] G. Berry. Modèles complètement adéquats et stables des lambda-calculs typés. Thèse de Doctorat d’Etat, Université Paris VII, 1979.

[7] F. Borceux. Handbook of Categorical Algebra I. Basic Category Theory. Cambridge University Press, 1994.

[8] T. Bräuner. An Axiomatic Approach to Adequacy. Ph.D. dissertation, University of Aarhus, 1996. BRICS Dissertation Series DS-96-4.

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

[10] L. Cardelli and A. D. Gordon. Anytime, anywhere: modal logics for mobile ambients. In Proc. POPL’00.

[11] L. Cardelli and A. D. Gordon. A commitment relation for the ambient calculus. October 6th, 2000. Available from http://research.

microsoft.com/~adg/.

[12] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In Proc. CSL’96, LNCS 1258.

[13] G. L. Cattani, I. Stark and G. Winskel. Presheaf models for the πcalculus. In Proc. CTCS’97, LNCS 1290.

[14] G. L. Cattani. Presheaf Models for Concurrency. Ph.D. dissertation, University of Aarhus, 1999. BRICS Dissertation Series DS-99-1.

[15] G. L. Cattani and G. Winskel. Profunctors, open maps and bisimulation.

Manuscript, 2003. Available from http://www.cl.cam.ac.uk/~gw104/.

[16] F. Crazzolara and G. Winskel. Events in security protocols. In Proc. 8th ACM Conference on Computer and Communication Security, 2001.

[17] J. B. Dennis. Data flow computation. In M. Broy, editor. Control Flow and Data Flow: Concepts of Distributed Programming. Springer-Verlag, 1985.

[18] S. Furber, editor. Proc. Eighth International Symposium on Asynchronus Circuits and Systems. IEEE, 2002.

[19] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1–102, 1987.

[20] M. C. B. Hennessy and G. D. Plotkin. Full abstraction for a simple parallel programming language. In Proc. MFCS’79, LNCS 74.

[21] M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137–161, 1985.

[22] M. Hennessy. A fully abstract denotational model for higher-order processes. Information and Computation, 112(1):55–95, 1994.

[23] T. Hildebrandt, P. Panangaden and G. Winskel. A relational model of non-deterministic dataflow. In Proc. CONCUR’98, LNCS 1466.

[24] C. A. R. Hoare. Some properties of predicate transformers. Journal of the ACM, 25(3):461–480, 1987.

[25] B. Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69(1):73–106, 1994.

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

[27] G. Kahn. The semantics of a simple language for parallel programming. Information Processing, 74:471–475, 1974.

[28] G. M. Kelly. Doctrinal adjunction. In Proc. Category Seminar. Sydney 1972/73, LNM 420.

[29] L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, 1978.

[30] K. G. Larsen and G. Winskel. Using information systems to solve recursive domain equations effectively. In Proc. Semantics of Data Types, 1984, LNCS 173.

[31] S. Mac Lane. Categories for the Working Mathematician. Second edition, Springer, 1998.

[32] G. McCusker. A fully abstract relational model of Syntactic Control of Interference. In Proc. CSL’02, LNCS 2471.

[33] P.-A. Melliès. Categorical models of linear logic revisited. Submitted to Theoretical Computer Science, 2002.

[34] R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer-Verlag, 1980.

[35] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[36] R. Milner, J. Parrow and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, 100(1):1–77, 1992.

[37] R. Milner. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, 1999.

[38] J. H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, 1968.

[39] M. Nielsen, G. Plotkin and G. Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13(1):85–108, 1981.

[40] M. Nygaard and G. Winskel. Linearity in process languages. In Proc. LICS’02.

[41] M. Nygaard and G. Winskel. HOPLA—a higher-order process language. In Proc. CONCUR’02, LNCS 2421.

[42] M. Nygaard and G. Winskel. Full abstraction for HOPLA. In Proc. CONCUR’03, LNCS 2761.

[43] M. Nygaard. Domain Theory for Concurrency. Ph.D. dissertation, University of Aarhus, 2003.

[44] D. Park. Concurrency and automata on infinite sequences. In Proc. Theoretical Computer Science: 5th GI-Conference, LNCS 104, 1981.

[45] D. A. Peled, V. R. Pratt and G. J. Holzmann, editors. Proc. Partial Order Methods in Verification 1996. DIMACS 29, American Mathematical Society, 1997.

[46] G. Plotkin. A powerdomain construction. SIAM Journal on Computing, 5(3):452–487, 1976.

[47] D. Sangiorgi and D. Walker. The π-calculus. A Theory of Mobile Processes. Cambridge University Press, 2001.

[48] D. S. Scott. Domains for denotational semantics. In Proc. ICALP’82, LNCS 140.

[49] R. A. G. Seely. Linear logic, ∗-autonomous categories and cofree coalgebras. In Proc. Categories in Computer Science and Logic, 1987, Contemporary Mathematics 92.

[50] F. Javier Thayer, J. C. Herzog and J. D. Guttman. Strand spaces: why is a security protocol correct? In Proc. IEEE Symposium on Security and Privacy 1998.

[51] B. Thomsen. A calculus of higher-order communicating systems. In Proc. POPL’89.

[52] G. Winskel. On powerdomains and modality. Theoretical Computer Science, 36:127–137, 1985.

[53] G. Winskel. The Formal Semantics of Programming Languages. An Introduction. The MIT Press, 1993.

[54] G. Winskel and M. Nielsen. Models for concurrency. In S. Abramsky et al, editors. Handbook of Logic in Computer Science. Volume 4. Semantic Modelling. Oxford University Press, 1995.

[55] G. Winskel and F. Zappa Nardelli. Manuscript, 2003.

A Proof of Soundness

We want to show that if ℙ : t ⟶^{a} t′ : ℙ′, then ⟦!t′⟧ ⊆ a^{∗}⟦t⟧. The proof is by rule-induction on the transition rules:

Recursive definition. If ℙ : rec x.t ⟶^{a} t′ : ℙ′ we have ℙ : t[rec x.t/x] ⟶^{a} t′ : ℙ′ as premise. By the induction hypothesis and Corollary 3.3,

⟦!t′⟧ ⊆ a^{∗}⟦t[rec x.t/x]⟧ = a^{∗}⟦rec x.t⟧ .  (104)

Nondeterministic sum. If ℙ : Σ_{i∈I}t_{i} ⟶^{a} t′ : ℙ′ we have the premise ℙ : t_{j} ⟶^{a} t′ : ℙ′ for some j ∈ I. By the induction hypothesis and linearity of a^{∗},

⟦!t′⟧ ⊆ a^{∗}⟦t_{j}⟧ = ⟦a^{∗}t_{j}⟧ ⊆ ⟦Σ_{i∈I}a^{∗}t_{i}⟧ = a^{∗}⟦Σ_{i∈I}t_{i}⟧ .  (105)

Abstraction. If ℙ → ℚ : λx.t ⟶^{u↦a} t′ : ℙ′ we have ℚ : t[u/x] ⟶^{a} t′ : ℙ′ as premise. By the induction hypothesis and Corollary 3.2,

⟦!t′⟧ ⊆ a^{∗}⟦t[u/x]⟧ = a^{∗}⟦(λx.t) u⟧ = (u ↦ a)^{∗}⟦λx.t⟧ .  (106)

Application. If ℚ : t u ⟶^{a} t′ : ℙ′ we have the premise ℙ → ℚ : t ⟶^{u↦a} t′ : ℙ′. By the induction hypothesis,

⟦!t′⟧ ⊆ (u ↦ a)^{∗}⟦t⟧ = a^{∗}⟦t u⟧ .  (107)

Injection. If Σ_{α∈A}ℙ_{α} : βt ⟶^{βa} t′ : ℙ′ we have the premise ℙ_{β} : t ⟶^{a} t′′ : ℙ′. By the induction hypothesis and Proposition 3.4,

⟦!t′⟧ ⊆ a^{∗}⟦t⟧ = a^{∗}⟦π_{β}(βt)⟧ = (βa)^{∗}⟦βt⟧ .  (108)

Projection. If ℙ_{β} : π_{β}t ⟶^{a} t′ : ℙ′ we have the premise Σ_{α∈A}ℙ_{α} : t ⟶^{βa} t′ : ℙ′. By the induction hypothesis,

⟦!t′⟧ ⊆ (βa)^{∗}⟦t⟧ = a^{∗}⟦π_{β}t⟧ .  (109)

Prefixing. Consider the transition !ℙ : !t ⟶^{!} t : ℙ. By definition, !^{∗}⟦!t⟧ = ⟦!t⟧, a subset of itself.

Prefix match. If ℚ : [u > !x ⇒ t] ⟶^{a} t′ : ℙ′ we have the premises !ℙ : u ⟶^{!} u′ : ℙ and ℚ : t[u′/x] ⟶^{a} t′ : ℙ′. By the induction hypothesis for u,

⟦!u′⟧ ⊆ !^{∗}⟦u⟧ = ⟦u⟧  (110)

Now by the induction hypothesis for t, Proposition 3.5 and monotonicity,

⟦!t′⟧ ⊆ a^{∗}⟦t[u′/x]⟧ = a^{∗}⟦[!u′ > !x ⇒ t]⟧ ⊆ a^{∗}⟦[u > !x ⇒ t]⟧ .  (111)

Fold. If μ_{j}T⃗.𝕋⃗ : abs t ⟶^{abs a} t′ : ℙ′ we have the premise 𝕋_{j}[μT⃗.𝕋⃗/T⃗] : t ⟶^{a} t′ : ℙ′. By the induction hypothesis and since abs and rep are inverses,

⟦!t′⟧ ⊆ a^{∗}⟦t⟧ = a^{∗}⟦rep(abs t)⟧ = (abs a)^{∗}⟦abs t⟧ .  (112)

Unfold. If 𝕋_{j}[μT⃗.𝕋⃗/T⃗] : rep t ⟶^{a} t′ : ℙ′ we have the premise μ_{j}T⃗.𝕋⃗ : t ⟶^{abs a} t′ : ℙ′. By the induction hypothesis,

⟦!t′⟧ ⊆ (abs a)^{∗}⟦t⟧ = a^{∗}⟦rep t⟧ .  (113)

The rule-induction is complete. □

B Proof of Adequacy (Main Lemma)

For the proof of Lemma 3.11 we need two technical results, which can both be proved by induction on the structure of paths. One says that ϵ_{ℙ} is closed on the left by ≤_{ℙ}, the other that ϵ_{ℙ} is closed on the right by the relation ⊏ ∼_{1},

defined by t_{1} ⊏ ∼_{1} t_{2} iff ℙ : t_{1} ⟶^{a} t′ : ℙ′ implies ℙ : t_{2} ⟶^{a} t′ : ℙ′.

Lemma B.1 If p ≤_{ℙ} p′ and p′ ϵ_{ℙ} t, then p ϵ_{ℙ} t.

Lemma B.2 If p ϵ_{ℙ} t_{1} and t_{1} ⊏ ∼_{1} t_{2}, then p ϵ_{ℙ} t_{2}.

It follows from Lemma B.1 that for any subset X of ℙ we have X ⊴_{ℙ} t iff the down-closure of X, written X̄, satisfies X̄ ⊴_{ℙ} t.

The proof of Lemma 3.11 proceeds by structural induction on terms using the induction hypothesis

Suppose x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℙ and let ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}}
s_{j} for 1 ≤ j ≤ k. Then ⟦t⟧(X̄_{1}, …, X̄_{k}) ⊴_{ℙ} t[s_{1}/x_{1}, …, s_{k}/x_{k}].

We’ll abbreviate x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} to Γ, (X̄_{1}, …, X̄_{k}) to X, and the substitution [s_{1}/x_{1}, …, s_{k}/x_{k}] to [s]. Lemma B.2 will be used freely below.

Variable. Let Γ ⊢ x_{j} : ℙ_{j}, with j between 1 and k, and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦x_{j}⟧X ⊴_{ℙ_{j}} x_{j}[s]. Now, ⟦x_{j}⟧X = X̄_{j} and x_{j}[s] ≡ s_{j} so this amounts to X̄_{j} ⊴_{ℙ_{j}} s_{j} which by the remarks above is equivalent to X_{j} ⊴_{ℙ_{j}} s_{j}.

Recursive definition. Let Γ ⊢ rec x.t : ℙ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦rec x.t⟧X ⊴_{ℙ} rec x.t[s]. Now, ⟦rec x.t⟧X = (fix F)X where F maps g : Γ → ℙ to the composition

Γ ⟶^{Δ_{Γ}} Γ & Γ ⟶^{1_{Γ}&g} Γ & ℙ ⟶^{t} ℙ .  (114)

We’ll show by induction on n that F^{n}(∅)X ⊴_{ℙ} rec x.t[s] for all n ∈ ω. Having done so we may argue as follows: Since

⟦rec x.t⟧X = (fix F)X = (⋃_{n∈ω} F^{n}∅)X = ⋃_{n∈ω} ((F^{n}∅)X) ,  (115)

we have that p ∈ ⟦rec x.t⟧X implies the existence of an n ∈ ω such that p ∈ (F^{n}∅)X. Therefore ⟦rec x.t⟧X ⊴_{ℙ} rec x.t[s] as wanted.

Basis. Here, (F^{0}∅)X = ∅. By definition of ⊴_{ℙ} we get ∅ ⊴_{ℙ} t for any type ℙ and term ⊢ t : ℙ.

Step. Suppose (F^{n}∅)X ⊴_{ℙ} rec x.t[s]. By the assumption of the lemma, X_{j} ⊴_{ℙ} s_{j} for each 1 ≤ j ≤ k, and so by the induction hypothesis of the structural induction,

⟦t⟧(X, (F^{n}∅)X) ⊴_{ℙ} t[s][rec x.t[s]/x] .  (116)

So if p ∈ (F^{n+1}∅)X, then since (F^{n+1}∅)X = ⟦t⟧(X, (F^{n}∅)X) we have p ϵ_{ℙ} t[s][rec x.t[s]/x]. By the transition rules we have t[s][rec x.t[s]/x] ⊏ ∼_{1} rec x.t[s], and so p ϵ_{ℙ} rec x.t[s]. We conclude (F^{n+1}∅)X ⊴_{ℙ} rec x.t[s] and the mathematical induction is complete.

Nondeterministic sum. Let Γ ⊢ Σ_{i∈I}t_{i} : ℙ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦Σ_{i∈I}t_{i}⟧X ⊴_{ℙ} Σ_{i∈I}t_{i}[s]. Now, ⟦Σ_{i∈I}t_{i}⟧X = Σ_{i∈I}⟦t_{i}⟧X. So if p ∈ ⟦Σ_{i∈I}t_{i}⟧X, there exists j ∈ I with p ∈ ⟦t_{j}⟧X. Using the induction hypothesis for t_{j} we have p ϵ_{ℙ} t_{j}[s]. By the transition rules, t_{j}[s] ⊏ ∼_{1} Σ_{i∈I}t_{i}[s] and so p ϵ_{ℙ} Σ_{i∈I}t_{i}[s] as wanted.

Abstraction. Let Γ ⊢ λx.t : ℙ → ℚ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦λx.t⟧X ⊴_{ℙ→ℚ} (λx.t)[s]. So let P ↦ q ∈ ⟦λx.t⟧X. By the denotational semantics, we then have q ∈ ⟦t⟧(X, i_{ℙ}P). We must show that P ↦ q ϵ_{ℙ→ℚ} (λx.t)[s]. So suppose ⊢ u : ℙ with P ⊴_{ℙ} u. We must then show q ϵ_{ℚ} (λx.t)[s] u. By the transition rules, t[s][u/x] ⊏ ∼_{1} (λx.t)[s] u and so it is sufficient to show q ϵ_{ℚ} t[s][u/x]. Now, by the induction hypothesis, we know that ⟦t⟧(X, i_{ℙ}P) ⊴_{ℚ} t[s][u/x] and so, with q ∈ ⟦t⟧(X, i_{ℙ}P), we are done.

Application. Let Γ ⊢ t u : ℚ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦t u⟧X ⊴_{ℚ} (t u)[s]. So suppose q ∈ ⟦t u⟧X. By the denotational semantics, there exists P ∈ !ℙ such that P ↦ q ∈ ⟦t⟧X and P ⊆ ⟦u⟧X. By the induction hypothesis for t, we have ⟦t⟧X ⊴_{ℙ→ℚ} t[s] and so P ↦ q ϵ_{ℙ→ℚ} t[s]. This means that given any ⊢ u′ : ℙ with P ⊴_{ℙ} u′, we have q ϵ_{ℚ} t[s] u′. Now using the induction hypothesis for u we get that ⟦u⟧X ⊴_{ℙ} u[s] and so, since P ⊆ ⟦u⟧X, we have P ⊴_{ℙ} u[s] so that q ϵ_{ℚ} t[s] u[s] ≡ (t u)[s] as wanted.

Injection. Let Γ ⊢ βt : Σ_{α∈A}ℙ_{α} and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦βt⟧X ⊴_{Σ_{α∈A}ℙ_{α}} (βt)[s]. So suppose βp ∈ ⟦βt⟧X; by the denotational semantics, p ∈ ⟦t⟧X. We must then show that βp ϵ_{Σ_{α∈A}ℙ_{α}} (βt)[s] which means that p ϵ_{ℙ_{β}} π_{β}(βt[s]). By the transition rules, we have t[s] ⊏ ∼_{1} π_{β}(βt[s]) so it is sufficient to show that p ϵ_{ℙ_{β}} t[s]. By the induction hypothesis, ⟦t⟧X ⊴_{ℙ_{β}} t[s] and so, since p ∈ ⟦t⟧X we have p ϵ_{ℙ_{β}} t[s] as wanted.

Projection. Let Γ ⊢ π_{β}t : ℙ_{β} with Γ ⊢ t : Σ_{α∈A}ℙ_{α} and β ∈ A, and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦π_{β}t⟧X ⊴_{ℙ_{β}} π_{β}t[s]. So suppose p ∈ ⟦π_{β}t⟧X; by the denotational semantics, βp ∈ ⟦t⟧X. By the induction hypothesis, ⟦t⟧X ⊴_{Σ_{α∈A}ℙ_{α}} t[s] and so βp ϵ_{Σ_{α∈A}ℙ_{α}} t[s] which means that p ϵ_{ℙ_{β}} π_{β}t[s] as wanted.

Prefixing. Let Γ ⊢ !t : !ℙ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦!t⟧X ⊴_{!ℙ} !t[s]. So suppose P ∈ ⟦!t⟧X; by the denotational semantics, P ⊆ ⟦t⟧X. We must then show that P ϵ_{!ℙ} !t[s], and so since the transition rules provide a derivation !ℙ : !t[s] ⟶^{!} t[s] : ℙ, that P ⊴_{ℙ} t[s]. Now, by the induction hypothesis, ⟦t⟧X ⊴_{ℙ} t[s] and so, since P ⊆ ⟦t⟧X we have P ⊴_{ℙ} t[s] as wanted.

Prefix match. Let Γ ⊢ [u > !x ⇒ t] : ℚ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. By renaming x if necessary, we may assume that x is not one of the x_{j}. We must show that ⟦[u > !x ⇒ t]⟧X ⊴_{ℚ} [u > !x ⇒ t][s]. So suppose q ∈ ⟦[u > !x ⇒ t]⟧X; by the denotational semantics, there exists P ∈ !ℙ such that q ∈ ⟦t⟧(X, i_{ℙ}P) and P ∈ ⟦u⟧X. By the induction hypothesis for u we have ⟦u⟧X ⊴_{!ℙ} u[s] and so since P ∈ ⟦u⟧X, there exists u′ such that !ℙ : u[s] ⟶^{!} u′ : ℙ and P ⊴_{ℙ} u′. Hence, by the induction hypothesis for t we have ⟦t⟧(X, i_{ℙ}P) ⊴_{ℚ} t[s][u′/x] and so since q ∈ ⟦t⟧(X, i_{ℙ}P) we have q ϵ_{ℚ} t[s][u′/x]. Now, by the transition rules, t[s][u′/x] ⊏ ∼_{1} [u > !x ⇒ t][s] and so q ϵ_{ℚ} [u > !x ⇒ t][s] as wanted. Fold. Let Γ ⊢ abs t : μ_{j}T⃗.𝕋⃗ and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦abs t⟧X ⊴_{μ_{j} P⃗ .𝕋⃗} abs t[s]. So suppose abs q ∈ ⟦abs t⟧X such that q ∈ ⟦t⟧X. By the induction hypothesis, q ϵ_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} t[s] and since t[s] ⊏ ∼_{1} rep abs t[s], we have q ϵ_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} rep abs t[s] which means that abs q ϵ_{μ_{j} P⃗ .𝕋⃗} abs t[s] as wanted. Unfold. Let Γ ⊢ rep t : 𝕋_{j}[μT⃗.𝕋⃗/T⃗] and ⊢ s_{j} : ℙ_{j} with X_{j} ⊴_{ℙ_{j}} s_{j} for 1 ≤ j ≤ k. We must show that ⟦rep t⟧X ⊴_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} rep t[s]. So suppose q ∈ ⟦rep t⟧X such that abs q ∈ ⟦t⟧X. By the induction hypothesis, abs q ϵ_{μ_{j} T⃗.𝕋⃗} t[s] and so q ϵ_{𝕋_{j}[μT⃗.𝕋⃗/T⃗]} rep t[s] as wanted.

The structural induction is complete. □

Recent BRICS Report Series Publications

RS-03-43 Mikkel Nygaard and Glynn Winskel. Domain Theory for Concurrency. December 2003. 45 pp. To appear in a Theoretical Computer Science special issue on Domain Theory.

RS-03-42 Mikkel Nygaard and Glynn Winskel. Full Abstraction for HO-PLA. December 2003. 25 pp. Appears in Amadio and Lugiez, editors, Concurrency Theory: 14th International Conference, CONCUR ’03 Proceedings, LNCS 2761, 2003, pages 383–398.

RS-03-41 Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations. December 2003. 21 pp.

RS-03-40 Andrzej Filinski and Henning Korsholm Rohde. A Denotational Account of Untyped Normalization by Evaluation. December 2003. 29 pp.

RS-03-39 Jörg Abendroth. Applying π-Calculus to Practice: An Example of a Unified Security Mechanism. November 2003. 35 pp.

RS-03-38 Henning Böttger, Anders Møller, and Michael I. Schwartzbach. Contracts for Cooperation between Web Service Programmers and HTML Designers. November 2003. 23 pp.

RS-03-37 Claude Crépeau, Paul Dumais, Dominic Mayers, and Louis Salvail. Computational Collapse of Quantum State with Application to Oblivious Transfer. November 2003. 30 pp.

RS-03-36 Ivan B. Damgård, Serge Fehr, Kirill Morozov, and Louis Salvail. Unfair Noisy Channels and Oblivious Transfer. November 2003.

RS-03-35 Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects. November 2003. 31 pp.

RS-03-34 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. CCS with Hennessy’s Merge has no Finite Equational Axiomatization. November 2003. 37 pp.

RS-03-33 Olivier Danvy. A Rational Deconstruction of Landin’s SECD Machine. October 2003. 32 pp. This report supersedes the earlier BRICS report RS-02-53.