BRICS RS-03-42 Nygaard & Winskel: Full Abstraction for HOPLA BRICS

Basic Research in Computer Science

Full Abstraction for HOPLA

Mikkel Nygaard Glynn Winskel BRICS Report Series RS-03-42 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/42/

Full Abstraction for HOPLA

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

Abstract

A fully abstract denotational semantics for the higher-order process language HOPLA is presented. It characterises contextual and logical equivalence, the latter linking up with simulation. The semantics is a clean, domain-theoretic description of processes as downwardsclosed sets of computation paths: the operations of HOPLA arise as syntactic encodings of canonical constructions on such sets; full abstraction is a direct consequence of expressiveness with respect to computation paths; and simple proofs of soundness and adequacy shows correspondence between the denotational and operational semantics.

1 Introduction

HOPLA (Higher-Order Process LAnguage [19]) is an expressive language for higher-order nondeterministic processes. It has a straightforward operational semantics supporting a standard bisimulation congruence, and can directly encode calculi like CCS, higher-order CCS and mobile ambients with public names. The language came out of work on a linear domain theory for concurrency, based on a categorical model of linear logic and associated comonads [4, 18], the comonad used for HOPLA being an exponential ! of linear logic.

The denotational semantics given in [19] interpreted processes as presheaves. Here we consider a “path semantics” for HOPLA which allows us to characterise operationally the distinguishing power of the notion of computation path underlying the presheaf semantics (in contrast to the distinguishing power of the presheaf structure itself). Path semantics is similar to trace semantics [10] in that 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. Indeed, we characterise contextual equivalence for HOPLA as path equivalence and show that this coincides with logical equivalence for a fragment of Hennessy-Milner logic which is characteristic for simulation equivalence in the case of image-finite processes [8].

∗

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

funded by the Danish National Research Foundation.

To increase the expressiveness of HOPLA (for example, to include the type used in [25] for CCS with late value-passing), while still ensuring that every operation in the language has a canonical semantics, we decompose the “prefix-sum” type Σ_{α∈A}α.ℙ_{α} in [19] into a sum type Σ_{α∈A}ℙ_{α} and an anonymous action prefix type !ℙ. The sum type, also a product, is associated with injection (“tagging”) and projection term constructors, βt and π_{β}t for β ∈ A. The prefix type is associated with constructions of prefixing !t and prefix match [u > !x ⇒ t], subsuming the original terms β.t and [u > β.x ⇒ t] using β!t and [π_{β}u > !x ⇒ t].

In Sect. 2 we present a domain theory of path sets, used in Sect. 3 to give a fully abstract denotational semantics to HOPLA. Section 4 presents the operational semantics of HOPLA, essentially that of [19], and relates the denotational and operational semantics with pleasingly simple proofs of soundness and adequacy. Section 5 concludes with a discussion of related and future work.

2 Domain Theory from Path Sets

In the path semantics, processes are represented as collections of 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. A process of type ℙ is then represented as a downwards-closed subset X ⊆ ℙ, called a path set. Path sets X ⊆ ℙ 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 [7], ℙ̂ 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 sometimes 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 ∅.

A second important property of ℙ̂ is that any X ∈ ℙ̂ is the join of certain “prime” elements below it; ℙ̂ is a prime algebraic complete lattice [17]. 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), join-preserving 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 join-pre-serving maps ℙ̂ → ℚ̂ as arrows. It turns out Lin has enough structure to be understood as a categorical model of Girard’s linear logic [5, 23]. 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 as required by Seely’s definition of a model of linear logic [23].

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, i.e. 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 \begin{matrix}= ⋃_{P ⪯_{ℙ}X} y_{!ℙ}P \\ = \{P ∈ !ℙ : P ⪯_{ℙ} X\} \end{matrix} ε_{ℙ}X \begin{matrix}= ⋃_{P ∈X} i_{ℙ}P \\ = \{p ∈ ℙ : ∃P ∈ X. p ∈ P \} \end{matrix} (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 X ⊆ η_{ℙ}(ε_{ℙ}X) for all X ∈ ˆ!ℙ.

Right adjoints preserve products, and so Cts has products given as in Lin. Hence, Cts is a symmetric monoidal category like Lin, and in fact, our adjunction is symmetric monoidal. 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 [14] 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.

In addition, the unit 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 for a categorical model of intuitionistic linear logic, strengthening those of Seely [1, 23]; see also [14] for a recent survey of such models.

3 Denotational Semantics

HOPLA is directly suggested by the structure of Cts. The language is typed with types given by the grammar

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

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. 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 [22, 12]. 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 .  (16)

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 on top of 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′}{β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′}

(17)

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

As an example, consider the type of CCS processes given in [19] as the path order ℙ satisfying ℙ = Σ_{α∈A}!ℙ where A is a set of CCS actions. The elements of ℙ then have the form abs(βP) where β ∈ A and P is a finite set of paths from ℙ. Intuitively, a CCS process can perform such a path if it can perform the action β and, following that, is able to perform each path in P.

The raw syntax of HOPLA 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 . (18)

The variables x in the terms rec x.t, λx.t, and [u > !x ⇒ t] are binding occurrences with scope t. We shall take for granted an understanding of free and bound variables, and substitution on raw terms.

Let ℙ_{1}, …, ℙ_{k}, ℚ be closed type expressions and assume that the variables x_{1}, …, x_{k} are distinct. A syntactic judgement x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ stands for a map ⟦x_{1} : ℙ_{1}, …, x_{k} : ℙ_{k} ⊢ t : ℚ⟧ : ℙ_{1} & ⋯ & ℙ_{k} → ℚ in 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 typing 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. [2]). We assume that the variables in any environment list which appears are distinct.

Structural rules. The rules handling environment lists are given as follows:

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

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

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

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

In the formation rule for contraction (22), 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}(∅). Below, fix f is the fixpoint in Cts(Γ, ℙ) ≅ { \atop Γ → ℙ} of the continuous operation f mapping g : Γ → ℙ in Cts to the composition ⟦t⟧ ∘ (1_{Γ} & g) ∘ Δ_{Γ}.

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

Nondeterministic sum. Each path order ℙ is associated with a join operation, Σ : &_{i∈I} ℙ → ℙ in Cts taking a tuple ⟨t_{i}⟩_{i∈I} to the join Σ_{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} ℙ ⟶^{Σ} ℙ}  (24)

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} ℙ → ℚ}  (25)

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

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 of (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 [19] with pairing (t, u) and projection terms fst t, snd t can be encoded, respectively, as the type ℙ_{1} + ℙ_{2}, and the terms 1t + 2u and π_{1}t, π_{2}t.

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

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

Prefixing. The adjunction between Lin and Cts provides a type constructor, !(−), for which the unit η_{ℙ} : ℙ → !ℙ and counit ε_{ℙ} : !ℙ → ℙ may interpret 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 u.

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

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 (13):

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

Recursive types. 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⃗.𝕋⃗}  (31)

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

3.1 Useful Equivalences

We provide some technical results about the path semantics which are used in the proof of soundness, Proposition 4.3. Proofs can be found in [20].

Lemma 3.1 (Substitution) Suppose Γ, x : ℙ ⊢ t : ℚ and Λ ⊢ u : ℙ with Γ and Λ disjoint. Then Γ, Λ ⊢ t[u/x] : ℚ with denotation given by the composition ⟦t⟧ ∘ (1_{Γ} & ⟦u⟧).

Corollary 3.2 If Γ, x : ℙ ⊢ t : ℙ, then Γ ⊢ t[rec x.t/x] : ℙ and ⟦rec x.t⟧ = ⟦t[rec x.t/x]⟧ so recursion amounts to unfolding.

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

Proposition 3.4 From the properties of the biproduct we get:

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

(33)

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}  (34)

Proposition 3.6 As abs and rep are inverses and linear, we get

⟦rep(abs t)⟧ = ⟦t⟧ ⟦abs(rep t)⟧ = ⟦t⟧  ⟦abs(Σ_{i∈I}t_{i})⟧ = ⟦Σ_{i∈I}(abs t_{i})⟧ ⟦rep(Σ_{i∈I}t_{i})⟧ = ⟦Σ_{i∈I}(rep t_{i})⟧  (35)

3.2 Full Abstraction

We define a program to be a closed term t of type !𝕆. 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 [16]:

Definition 3.7 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.8 (Full Abstraction) Suppose Γ ⊢ t_{1} : ℙ and Γ ⊢ t_{2} : ℙ. Then

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

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.^{1}

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 −) (37)

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

Here, t′_{P} and C′_{P} realise and consume finite sets of paths:

\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}  (38)

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}  (39)

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

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

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}  (41)

The proof is complete. □

4 Operational Semantics

HOPLA can be given an operational semantics using actions defined by

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

We assign types to actions a using a judgement of the form ℙ : a : ℙ′. Intuitively, performing the action a turns a process of type ℙ into a process of type ℙ′.

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

\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

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 : ℙ′.^{2} The operational rules are type-correct:

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

Proof. By rule-induction on the operational rules.

Abstraction. Suppose ℙ → ℚ : λx.t ⟶^{u↦a} t′ is derived from ℚ : t[u/x] ⟶^{a} t′ with ℙ ↦ ℚ : u ↦ a : ℙ′. By typing of actions, we have ⊢ u : ℙ and ℚ : a : ℙ′. The induction hypothesis then yields ⊢ t′ : ℙ′ as wanted. Note also that the substitution t[u/x] is well-formed as x : ℙ ⊢ t : ℚ follows from ⊢ λx.t : ℙ → ℚ by the typing rules.

Application. Suppose ℚ : t u ⟶^{a} t′ is derived from ℙ → ℚ : t ⟶^{u↦a} t′ with ℚ : a : ℙ′. By the premise and typing rules, we have ⊢ t : ℙ → ℚ and ⊢ u : ℙ, such that ℙ → ℚ : u ↦ a : ℙ′. The induction hypothesis then yields ⊢ t′ : ℙ′ as wanted.

Prefixing. Suppose !ℙ : !t ⟶^{!} t with !ℙ : ! : ℙ. Then ⊢ !t : !ℙ and so by the typing rules, ⊢ t : ℙ as wanted.

Prefix match. Suppose ℚ : [u > !x ⇒ t] ⟶^{a} t′ is derived from !ℙ : u ⟶^{!} u′ and ℚ : t[u′/x] ⟶^{a} t′ with ℚ : a : ℙ′. By the induction hypothesis applied to the right premise, we get ⊢ t′ : ℙ′ as wanted. Note also that we have ⊢ u : !ℙ and therefore ⊢ u′ : ℙ by the induction hypothesis for the left premise. Thus, as x : ℙ ⊢ t : ℚ, the substitution t[u′/x] is well-formed.

2The explicit types in the operational rules were missing in the rules given in [19]. They are needed to ensure that the types of t and a agree in transitions.

The remaining cases are handled similarly. □

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

4.1 Soundness and Adequacy

For each action ℙ : 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_{!ℙ}∅ = ∅. 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}  (44)

The role of a^{∗} is to reduce the action a to a prefix action:

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

Proof. By structural induction on a exploiting the fact that there is only one operational rule deriving transitions from each of the constructs application t u, injection βt, and folding abs t so that

\begin{aligned}ℙ → ℚ : t ⟶^{u↦a} t′ : ℙ′ & ⟺ ℚ : t u ⟶^{a} t′ : ℙ′ \\ Σ_{α∈A}ℙ_{α} : t ⟶^{βa} t′ : ℙ′ & ⟺ ℙ_{β} : π_{β}t ⟶^{a} t′ : ℙ′ \\ μ_{j}T⃗.𝕋⃗ : t ⟶^{abs a} t′ : ℙ′ & ⟺ 𝕋_{j}[μT⃗.𝕋⃗/T⃗] : rep t ⟶^{a} t′ : ℙ′ \end{aligned}  (45)

Function space. We argue as follows:

ℙ → ℚ : t ⟶^{u↦a} t′ : ℙ′

⟺ ℚ : t u ⟶^{a} t′ : ℙ′  (by (45))
⟺ !ℙ′ : a^{∗}(t u) ⟶^{!} t′ : ℙ′  (ind. hyp.)
⟺ !ℙ′ : (u ↦ a)^{∗}t ⟶^{!} t′ : ℙ′ (def. of (u ↦ a)^{∗}t)

Sum. We argue as follows:

Σ_{α∈A}ℙ_{α} : t ⟶^{βa} t′ : ℙ′

⟺ ℙ_{β} : π_{β}t ⟶^{a} t′ : ℙ′  (by (45))
⟺ !ℙ′ : a^{∗}(π_{β}t) ⟶^{!} t′ : ℙ′ (ind. hyp.)
⟺ !ℙ′ : (βa)^{∗}t ⟶^{!} t′ : ℙ′ (def. of (βa)^{∗}t)

Prefix. We argue as follows:

\begin{matrix}!ℙ : t ⟶^{!} t′ : ℙ \\ ⟺ & !ℙ : !^{∗}t ⟶^{!} t′ : ℙ & (def. of !^{∗}t) \end{matrix}

Recursion. We argue as follows:

μ_{j}T⃗.𝕋⃗ : t ⟶^{abs a} t′ : ℙ′

⟺ 𝕋_{j}[μT⃗.𝕋⃗/T⃗] : rep t ⟶^{a} t′ : ℙ′ (by (45))
⟺ !ℙ′ : a^{∗}(rep t) ⟶^{!} t′ : ℙ′  (ind. hyp.)
⟺ !ℙ′ : (abs a)^{∗}t ⟶^{!} t′ : ℙ′  (def. of (abs a)^{∗}t)

The structural induction is complete. □

Note that the reduction is done uniformly at all types using deconstructor contexts: application, projection, and unfolding. This explains the somewhat mysterious function space actions u ↦ a. A similar use of labels to carry context information appears e.g. in [6].

Soundness says that the operational notion of “successor” is included in the semantic notion:

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

Proof. By rule-induction on the transition rules. We’ll dispense with the typing information in transitions for clarity.

Recursive definition. Suppose rec x.t ⟶^{a} t′ is derived from t[rec x.t/x] ⟶^{a} t′. By the induction hypothesis and Corollary 3.2,

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

Nondeterministic sum. Suppose Σ_{i∈I}t_{i} ⟶^{a} t′ is derived from 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}⟧ .  (47)

Abstraction. Suppose λx.t ⟶^{u↦a} t′ is derived from t[u/x] ⟶^{a} t′. By the induction hypothesis and Corollary 3.3,

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

Application. Suppose t u ⟶^{a} t′ is derived from t ⟶^{u↦a} t′. By the induction hypothesis,

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

Injection. Suppose βt ⟶^{βa} t′ is derived from t ⟶^{a} t′. By the induction hypothesis and Proposition 3.4,

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

Projection. Suppose π_{β}t ⟶^{a} t′ is derived from t ⟶^{βa} t′. By the induction hypothesis,

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

Prefixing. Consider the transition !t ⟶^{!} t. By definition, ⟦!t⟧ = !^{∗}⟦!t⟧.

Prefix match. Suppose [u > !x ⇒ t] ⟶^{a} t′ is derived from u ⟶^{!} u′ and t[u′/x] ⟶^{a} t′. By the induction hypothesis for u, we have ⟦!u′⟧ ⊆ !^{∗}⟦u⟧ = ⟦u⟧, and so by the induction hypothesis for t, Proposition 3.5, and monotonicity,

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

Fold. Suppose abs t ⟶^{abs a} t′ is derived from t ⟶^{a} t′. By the induction hypothesis and Proposition 3.6,

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

Unfold. Suppose rep t ⟶^{a} t′ is derived from t ⟶^{abs a} t′. By the induction hypothesis,

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

The rule-induction is complete. □

We obtain a corresponding 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 [24], Ch. 13). 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 4.4 Suppose ⊢ t : ℙ. Then ⟦t⟧ ⊴_{ℙ} t.

Proof. 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 4.5 If p ≤_{ℙ} p′ and p′ ϵ_{ℙ} t, then p ϵ_{ℙ} t.

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

It follows from Lemma 4.5 that for any subset X of ℙ we have X ⊴_{ℙ} t iff the down-closure of X, written X̄, satisfies X̄ ⊴_{ℙ} t. Lemma 4.6 will be used freely below.

The proof of the main lemma 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].

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} ℙ .  (56)

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) ,  (57)

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] .  (58)

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] : ℙ, it is enough to show 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. □

Proposition 4.7 (Adequacy) Suppose ⊢ t : ℙ and ℙ : a : ℙ′. Then

a^{∗}⟦t⟧ ≠ ∅ ⟺ ∃t′. ℙ : t ⟶^{a} t′ : ℙ′  (59)

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

ℙ : t ⟶^{a} t′ : ℙ′. □

4.2 Full Abstraction w.r.t. Operational Semantics

Adequacy allows an operational formulation of contextual equivalence. If t is a program, we write t⟶^{!} if there exists t′ such that !𝕆 : t ⟶^{!} t′ : 𝕆. We then 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 the implication C(t_{1})⟶^{!} ⟹ C(t_{2})⟶^{!}.

4.3 Simulation

The path semantics does not capture enough of the branching behaviour of processes to characterise bisimilarity (for that, the presheaf semantics is needed, see [11, 19]). 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. 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 [8]. With a ranging over actions, formulae are given by

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

The empty conjunction is written ⊤. We type formulae using judgements ϕ : ℙ, the idea being that only processes of type ℙ should be described by ϕ : ℙ.

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

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

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

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

Definition 4.8 Closed terms t_{1}, t_{2} of the same type ℙ are related by 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 by adapting the proof of full abstraction, we can show that logical equivalence coincides with contextual equivalence as do the associated preorders:

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

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

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

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

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} ⇒ !∅] ⋯] .

(66)

It follows by (65) 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}  (67)

With p : ℙ and ⊢ t : ℙ we obtain p ∈ ⟦t⟧ iff ⟦C_{⟨a_{p}⟩ϕ_{p}}(t)⟧ ≠ ∅ as in the proof of full abstraction, and so by adequacy and (65), we have p ∈ ⟦t⟧ iff 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} : ℙ′ .  (68)

5 Related and Future Work

Matthew Hennessy’s fully abstract semantics for higher-order CCS [9] is a path semantics, and what we have presented here can be seen as a generalisation of his work via the translation of higher-order CCS into HOPLA, see [19].

The presheaf semantics originally given for HOPLA is a refined version of the path semantics. A path set X ∈ ℙ̂ can be seen to give a “yes/no answer” to the question of whether or not a path p ∈ ℙ can be realised by the process (cf. the representation in Sect. 2 of path sets as monotone maps ℙ^{op} → 2). A presheaf over ℙ is a functor ℙ^{op} → Set to the category of sets and functions, and gives instead a set of “realisers”, saying how a path may be realised. This extra information can be used to obtain refined versions of the proofs of soundness and adequacy, giving hope of extending the full abstraction result to a characterisation of bisimilarity, possibly in terms of open maps [11].

Replacing the exponential ! by a “lifting” comonad yields a model Aff of affine linear logic and an affine version of HOPLA, again with a fully abstract path semantics [20]. The tensor operation of Aff can be understood as a simple parallel composition of event structures [21]. Thus, the affine language holds promise of extending our approach to “independence” models like Petri nets or event structures in which computation paths are partial orders of events. Work is in progress to provide an operational semantics for this language together with results similar to those obtained here [21].

Being a higher-order process language, HOPLA allows process passing and so can express certain forms of mobility, in particular that present in the ambient calculus with public names [3, 19]. Another kind of mobility, mobility of communication links, arises from name-generation as in the πcalculus [15]. 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 [26].

References

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

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

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

[4] G. L. Cattani and G. Winskel. Profunctors, open maps and bisimulation. Manuscript, 2000.

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

[6] A. D. Gordon. Bisimilarity as a theory of functional programming. In Proc. MFPS’95, ENTCS 1.

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

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

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

[10] C. A. R. Hoare. A Model for Communicating Sequential Processes. Technical monograph, PRG-22, University of Oxford Computing Laboratory, 1981.

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

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

[13] G. McCusker. A fully abstract relational model of syntactic control of interference. In Proc. CSL’02, LNCS 2471.

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

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

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

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

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

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

[20] M. Nygaard and G. Winskel. Domain theory for concurrency. Submitted to Theoretical Computer Science, 2003.

[21] M. Nygaard. Domain Theory for Concurrency. PhD dissertation, University of Aarhus, 2003.

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

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

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

[25] G. Winskel. A presheaf semantics of value-passing processes. In Proc. CON-CUR’96, LNCS 1119.

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

Recent BRICS Report Series Publications

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.

RS-03-32 Philipp Gerhardy and Ulrich Kohlenbach. Extracting Herbrand Disjunctions by Functional Interpretation. October 2003. 17 pp.