Logical Methods in Computer Science
Vol. 13(4:9)2017, pp. 1–76
https://lmcs.episciences.org/

Submitted
Published

Jun. 01, 2015
Nov. 15, 2017

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π
(EXPANDED VERSION)

CLOVIS EBERHART a , TOM HIRSCHOWITZ b , AND THOMAS SEILLER c
a,b
c

Univ. Savoie Mont Blanc, CNRS, LAMA, F-73000 Chambéry, France
Department of Computer Science, University of Copenhagen, Copenhagen, Denmark and CNRS,
UMR 7030, Laboratoire d’Informatique de Paris Nord Université Paris 13, Sorbonne Paris Cité,
F-93430 Villetaneuse, France

Abstract. Following previous work on CCS, we propose a compositional model for the
π-calculus in which processes are interpreted as sheaves on certain simple sites. Such
sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau
game semantics. We define an analogue of fair testing equivalence in the model and show
that our interpretation is intensionally fully abstract for it. That is, the interpretation
preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is
fair testing equivalent to the interpretation of some process. The central part of our work
is the construction of our sites, relying on a combinatorial presentation of π-calculus traces
in the spirit of string diagrams.

Contents
1. Introduction
1.1. Causal models and beyond
1.2. Traces and naive concurrent strategies
1.3. Innocence as a sheaf condition
1.4. Main result
1.5. Contributions
1.6. Related work
1.7. Plan
2. Notation and preliminaries
2.1. Basic notation and labelled transition systems
2.2. A π-calculus
2.3. Fair testing equivalence
2.4. Playgrounds

2
2
3
4
5
7
7
8
9
9
10
11
14

Key words and phrases: Programming languages; categorical semantics;presheaf semantics; game semantics;
concurrency; process algebra.
The authors acknowledge support from French ANR projet blancs PiCoq ANR 2010 BLAN 0305 01 and
Récré ANR-11-BS02-0010.

l

LOGICAL METHODS
IN COMPUTER SCIENCE

©
DOI:10.23638/LMCS-13(4:9)2017

CC

C. Eberhart, T. Hirschowitz, and T. Seiller
Creative Commons

2

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

3. A pseudo double category of traces
3.1. String diagrams
3.2. From string diagrams to actions
3.3. From actions to traces
3.4. The main double category
4. Codomain is a fibration
4.1. A factorisation system
4.2. A first ‘fibred’ double category
4.3. Restriction of seeds
4.4. Opliftings
4.5. Restriction of actions
4.6. Restriction of traces
5. A playground for π
5.1. A candidate playground
5.2. Correctness criterion
5.3. A playground
6. A sheaf model
6.1. Strategies and behaviours
6.2. Decomposing behaviours
6.3. Interpretation of π
6.4. Semantic fair testing
7. Intensional full abstraction
7.1. A first graph with testing for behaviours
7.2. A further graph with testing for behaviours
7.3. Intensional full abstraction
7.4. Generalisation
8. Conclusion and future work
References
Appendix A. Proof of Lemma 7.37

17
18
20
22
23
25
25
26
27
29
32
34
37
38
40
45
47
48
50
52
53
54
54
60
62
64
65
65
70

1. Introduction
1.1. Causal models and beyond. Operational semantics of programming languages standardly model the execution of programs as paths in a certain labelled transition system (lts).
Under this interpretation, different possible interleavings of parallel actions yield different
paths. Verification on ltss thus incurs a well-known state explosion problem. Similarly,
causality between various actions, visible in the syntax, is lost in the lts, thus making, e.g.,
error diagnostics difficult [32].
Causal models, originally designed for Petri nets [63] and Milner’s CCS [72], intend to
remedy both problems, but have yet to be applied to full-scale programming languages. They
have recently been extended in two different directions: (1) by Crafa et al. [18] to Milner’s
π-calculus, and (2) by Melliès [57] to Girard’s linear logic. The former extension accounts for
the subtle interaction of channel creation with synchronisation in π, a significant technical
achievement, 30 years after the first causal semantics for CCS. The latter is the first causal

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

3

model for functional languages (inspired by Hyland-Ong’s and Nickau’s games models for
PCF [62, 42]). An important challenge is now the search for a causal model of full-fledged
languages with both concurrent and functional features. Winskel and collaborators are
currently working in this direction, using extensions of Melliès’s approach [67, 73, 14].
In previous work [40, 38, 39], we have proposed a causal model for CCS based on a
different approach. We here push this approach further by applying it to the π-calculus.
1.2. Traces and naive concurrent strategies. In standard causal models, execution
traces essentially consist of partially ordered sets of atomic ‘events’. Our approach relies on
a new notion of trace, which we now briefly sketch. There is first a (straightforward) notion
of position, which is essentially a finite hypergraph whose nodes are thought of as agents,
and whose hyperedges between nodes x1 , . . . , xn are thought of as communication channels
shared by x1 , . . . , xn . There is then a notion of atomic action from one position to another.
The collection of atomic actions is thought of as a ‘rule of the game’. Examples of atomic
actions are: an agent creates a new, private communication channel; an agent forks into
two new agents connected to the same channels; an agent sends some channel a over some
channel b to some other agent. We finally have a notion of trace which allows several atomic
actions to occur, in a way that only retains some minimal causality information between
them. We here mean, e.g., information such as: ‘such agent outputs on such channel only
after having created such other channel’.
The main purpose of our notion of trace is to interpret π-calculus processes as some
kind of strategies over them. Most naively, a strategy on some position X is a prefix-closed
set of ‘accepted’ traces from X. But what should prefix mean in our setting? Well, we may
view traces with initial position X and final position Y as morphisms Y
X. Sequential
composition of traces, denoted by ●, yields an analogue of prefix ordering, defined by t ≤ t ● w.
Strategies as prefix-closed sets of traces however fail to suit our needs on three counts. First,
such naive strategies may not be stable under isomorphism of traces; second, they are bound
to model coarse behavioural equivalences, at least as coarse as may testing equivalence (a.k.a.
trace equivalence); and third, they permit undesirable interaction between players. Let us
examine these issues in more detail.
The first, easy one is that there is an obvious notion of isomorphism between traces,
under which strategies should be closed. The second problem is more serious: until now,
these too naive strategies are not concurrent enough to adequately model CCS or the
π-calculus.
Example 1.1 (Milner’s coffee machines). Consider the CCS processes P = (a.b + a.c) and
Q = a.(b + c). The process P has two ways of inputting on a and then, depending on
the chosen way, inputs on either b or c. The process Q inputs on a and then has both
possibilities of inputting on b or c. They hence exhibit significantly different interactive
behaviour. Both processes, however, accept exactly the same traces (in the standard sense),
namely {, a, ab, ac}, where  denotes the empty trace.
Thus, taking strategies to be prefix-closed sets of traces would prevent us from directly
modelling any reasonably fine behavioural equivalence on processes. Inspired by presheaf
models [45], we remedy both problems at once by passing from prefix-closed sets of traces to
presheaves (of finite sets) on traces. Indeed, in the simple case where traces on X form a mere
poset T(X) by prefix ordering, a prefix-closed set of traces is nothing but a contravariant
functor from T(X) to the ordinal 2, viewed as a category. The latter has two objects 0 and

4

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

1 and just one non-trivial morphism 0 → 1. The idea is that a functor S∶ T(X)op → 2 maps
any trace to 1 when it is accepted, and to 0 otherwise. Furthermore, if t ≤ t′ , i.e., t is a prefix
of t′ , then we have a morphism t → t′ which should be mapped by S to some morphism
S(t′ ) → S(t). If t′ is accepted then S(t′ ) = 1, so this has to be a morphism 1 → S(t).
Because there are no morphisms 1 → 0, this entails S(t) = 1, hence prefix-closedness of the
corresponding strategy. Now in the case where traces form a proper category T(X), whose
morphisms encompass both prefix ordering and isomorphism between traces, considering
functors T(X)op → 2 retains prefix-closedness and solves our first problem: for any t ≅ t′ ,
functoriality imposes S(t) ≅ S(t′ ). Our second problem is then solved by replacing such
functors with presheaves, i.e., functors T(X)op → Set.
Example 1.2. In Example 1.1, the two ways that P has to accept inputting on a may
be reflected by mapping the trace a to some two-element set. More precisely, P may be
modelled by the presheaf S defined on the left and pictured on the right:
⋆
a
a
● S empty otherwise,
● S() = {⋆},
x
x′
● S( ↪ a) = {x ↦ ⋆, x′ ↦ ⋆},
● S(a) = {x, x′ },
c
b
● S(a ↪ ab) = {y ↦ x},
● S(ab) = {y},
′
y
y
.
● S(a ↪ ac) = {y ′ ↦ x′ },
● S(ac) = {y ′ },
Presheaves thus may ‘accept a trace in several ways’: the trace a is here accepted in two
ways, x and x′ . The process Q is of course modelled by equating x and x′ .
As it turns out, we actually only need finitely many ways of accepting each trace. Thus,
we arrive at a first sensible notion of strategy given by presheaves of finite sets, i.e., functors
T(X)op → set, where set denotes the category with as objects all finite subsets of N, with all
maps between them. We call them (naive) strategies in the sequel. (Please note that set is
equivalent to the category of all finite sets.)
Notation 1.3. For any C, let ̃
C denote the category of presheaves of finite sets over C.
1.3. Innocence as a sheaf condition. The third problem evoked above is that functors
T(X)op → set allow some undesirable behaviours. Intuitively, in π just as in CCS, agents
should not have any control over the routing of messages.
Example 1.4. Consider a position X with three agents x, y, and z sharing a communication
channel a, and a strategy S accepting (1) the trace where x outputs on a, (2) the trace
where y inputs on a, and (3) the trace where z inputs on a. Then, both synchronisations
should be accepted by S. However, one easily constructs a naive strategy in which one is
refused (see Example 6.2).
In order to rectify this deficiency, we enrich strategies with ‘local’ information. The idea
is that a strategy should not only accept or refuse traces on the whole position X, but also
traces on all possible subpositions of X. Moreover, this local information should fit together
coherently.
Example 1.5. Consider the position X of Example 1.4. Any strategy on X should now in
particular include independent strategies for each of the three agents x, y, and z. Coherence
means that in order for a trace to be accepted, it should be enough for it to be ‘locally
accepted’, i.e., at every stage in the trace, each agent should approve what they see of the

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

5

next action. E.g., if the next action is a synchronisation x  y with x outputting and y
inputting on some channel a, then all that is required for the synchronisation to be accepted
is that x accepts to output and y accepts to input. Consequently, if some other agent z also
accepts to input on a at this stage, then the synchronisation x  z is also accepted.

We call this putative coherence condition innocence by analogy with Hyland and Ong’s
notion [42]. In order to formalise it, we first extend our category of traces T(X) on X with
new objects representing traces on subpositions of X. We also add new morphisms, which
are about ‘locality’. Indeed, standardly, plays form a poset for the prefix ordering, but here
we want to enrich this, e.g., by embedding traces on subpositions of X into traces on X.
Example 1.6. Consider a position X with two agents x1 and x2 . There is a trace t on X
in which both agents fork. Consider now the subposition Y of X consisting solely of x1 and
the trace t′ on Y in which x1 merely forks. There is a morphism t′ → t in our new category.
This extended category, TX , yields an intermediate notion of strategy, given by functors
Top
X → set. Among the new objects, we have in particular traces on just one agent of X
obtained by sequentially composing atomic actions whose final position again consists of
one agent. We call this particular kind of trace a view. Views are the most ‘local’ kind of
objects in TX . They form a full subcategory VX of TX .
Example 1.7. If X merely consists of an agent x linked to n communication channels,
consider the atomic action given by x forking into two new agents, say x1 and x2 . This
action, viewed as an object of TX has three subobjects which are views: (1) the ‘identity’
view, in which nothing happens, (2) πnl , which represents the left-hand branch (to x1 ), (3)
and πnr , which represents the right-hand branch (to x2 ).
The inclusion VX ↪ TX induces a simple Grothendieck topology [54] on TX , which
amounts to decreeing that any trace is covered by its views. We finally call any S∶ Top
X → set
innocent precisely when it is a sheaf for this Grothendieck topology. In particular, giving
an innocent presheaf on TX is equivalent (up to isomorphism) to separately giving an
innocent presheaf for each agent of X, which rules out the undesirable behaviour described
in Example 1.4.
Sheaves on TX form a category SX , which is small thanks to our use of set instead of Set.
They furthermore map back to naive strategies, i.e., presheaves on T(X), by forgetting the
local information. Finally, because the considered topology is particularly simple, sheaves
̃
are equivalent to presheaves on views, i.e., SX ≃ V
X (recalling Notation 1.3). In summary,
we have three categories of strategies: naive strategies are presheaves on the ‘global’ category
of traces T(X), innocent strategies SX are sheaves on the extended category of traces TX ,
and so-called behaviours BX are presheaves on the category of views VX . The last two are
̃
equivalent, and we furthermore have an adjunction T(X)

SX .
We use both sides of the equivalence: behaviours directly lead to our compositional
interpretation ⟦−⟧∶ Pi → S of π-calculus processes, and innocent strategies are used below as
the basis for our semantic definition of fair testing equivalence.
1.4. Main result. What should we do in order to demonstrate adequacy of our model? By
definition, causal models expose some intensional information. Hence, equality is generally
much finer than any reasonable behavioural equivalence, so we should not base our main
result on it. On the other hand, causal models are supposed to be ‘compositional’, i.e., to

6

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

come equipped with an interpretation of syntactic operations in the model. A natural thing
to do is thus to choose some behavioural equivalence defined from syntactic operations,
use compositionality to transpose it to the model, and prove that the two coincide. More
precisely, the considered equivalence induces by quotienting two ‘extensional collapses’, one
syntactic and the other semantic, and we want to prove that the translation induces a
bijection between both extensional collapses. Following [3], we call this intensional full
abstraction for the considered equivalence. In fact, all behavioural equivalences end up
relying on some notion of observation, which we will also need to transpose to the model.
We here focus on so-called testing equivalences [20, 61, 9, 66], which are defined in two
stages. First, one chooses a ‘mode of interaction’. That is, one defines what the relevant
tests are for a given process and specifies how the two should interact. Typically, tests for
P are other processes T with the same free communication channels as P , and interaction
is just parallel composition P ∣ T . This part will be easy to transpose to the model by
compositionality. The second stage amounts to choosing when P ∣ T is successful. E.g., in
♡
may testing equivalence P ∣ T is successful just when there exists a transition (P ∣ T ) Ô
⇒ P′
(that is, a ♡ transition, possibly surrounded by silent transitions), where ♡ is some ‘tick’
action fixed in advance. In must testing equivalence, success is when all maximal (possibly
infinite) transition sequences contain at least one ♡ transition. In fair testing equivalence,
♡
one requires that all silent sequences (P ∣ T ) Ô
⇒ P ′ extend to some sequence P ′ Ô
⇒ P ′′ Ð
→ P ′′′
ending with a ♡ transition. These ideas transpose to the model by observing whether a given
trace contains a ♡ action. In this paper, we focus on fair testing equivalence, i.e., we prove
(Theorem 6.25) that our model is intensionally fully-abstract for fair testing equivalence. We
finally show (Section 7.4) that the result generalises to a wide range of testing equivalences,
obtained by varying the notion of success.
In order to fix intuitions, let us quickly motivate must and fair testing, using barbed
congruence [69] as a standard starting point. Barbed congruence equates processes P and Q,
roughly, when for all contexts C, C[P ] and C[Q] are weakly bisimilar w.r.t. reduction (i.e.,
only τ -actions are allowed), and furthermore they have the same interaction capabilities at
all stages. Barbed congruence is sometimes perceived as too discriminating w.r.t. guarded
choice. Consider, e.g., the following CCS processes.
P1

=

●

τ
τ

●
●

τ
a

●
●

τ
b

●
●

P2

=

●

τ
τ

●
●

τ
b

●
●

τ
a

●
●

Both processes may disable both actions a and b, the only difference being that P1 disables a
before disabling b. Barbed congruence distinguishes P1 from P2 (consider the trivial context
C = ◻), which some view as a deficiency.
Another possibility would be must testing equivalence [20]. Recall that P must pass a
test process R iff all maximal executions of P ∣ R perform, at some point, the ‘tick’ action ♡.
Then, P and Q are must testing equivalent iff they must pass the same tests. Must testing
equivalence does equate P1 and P2 above, but is sometimes perceived as too discriminating
w.r.t. divergence. E.g., consider Q1 = !τ ∣ a and Q2 = a. Perhaps surprisingly, Q1 and Q2 are
not must testing equivalent. Indeed, Q2 must pass the test a.♡, but Q1 does not, due to an
infinite, silent reduction sequence.
Fair testing equivalence was originally introduced (for CCS-like calculi) to rectify both
the deficiency of barbed congruence w.r.t. choice and that of must testing equivalence w.r.t.
divergence. The idea is that two processes are equivalent when they should pass the same

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

7

tests. A process P should pass the test T iff their parallel composition P ∣ T never loses the
ability of performing the special ‘tick’ action ♡, after any ♡-free reduction sequence. Fair
testing equivalence thus equates P1 and P2 above, as well as Q1 and Q2 . Cacciagrano et
al. [13] provide an excellent survey of fair testing for π.
Example 1.8 ([13]). The π-calculus features a well-known encoding of internal choice
using channel creation and parallel composition. Mixing this with replication leads to
intriguing examples of fair testing. Consider the following subtly different encodings of
!(b ⊕ c), where ⊕ denotes internal choice and ! denotes replication: let R1 =!νa.(a ∣ a.b ∣ a.c)
and R2 = νa.!(a ∣ a.b ∣ a.c). These are clearly fair testing equivalent. However, each encoding
has an execution that always makes, say, the left choice, and Cacciagrano et al. argue that
for R1 this execution is fair, as the involved channel is different each time. They use similar
examples to argue that fair testing is in fact too coarse, and instead propose alternative
notions (which lie beyond the scope of this paper).
1.5. Contributions. Since this paper follows the same approach as previous work on
CCS [40, 38, 39], we should explain in which sense extending the approach to π is more
than an easy application.
A first contribution comes from the fact that, in order to even define composition in our
category of traces, we need to show that traces form the total category of a fibration [43]
over positions. In previous work, this was done in an ad hoc way. We here introduce a more
satisfactory approach based on factorisation systems [52, 29].
A second significant contribution is prompted by the interplay between synchronisation
and private channels in π, which is notoriously subtle to handle. And indeed, our proof
method for CCS fails miserably on π. One reason for this, we think, is that our notion of
trace for π, though simple and natural, is not ‘modular’ enough, in the sense that a trace
contains strictly more information than the collection of all ‘local’ information accessible to
agents (i.e., of all of its views, in the above sense). Thus, adapting our proof technique from
CCS would have required us to define a much more complex but more modular notion of
trace. Instead, we here take a somewhat rougher route.
Finally, our proof now applies not only to fair testing equivalence, but also to a whole
class of testing equivalences.
1.6. Related work. Beyond the obviously closely related, already mentioned work of
Winskel et al., we should mention other causal models for π [11, 59, 26, 16, 7, 21, 15, 10, 18, 12],
as well as interleaving models [28, 27, 70, 15, 60, 36] and the early approach [44] based on
Girard’s Geometry of Interaction. All of these models are based on some lts for π. Instead,
ours is rather based on reduction rules. The subtleties usually showing up in ltss, related
to mixing synchronisation and private channels, do resurface in our proof of intensional full
abstraction, but not in the definition of our model. Indeed, it merely goes by describing the
‘rule of the game’ in π, and applying the general framework of playgrounds [39].
Another general framework relating operational and denotational descriptions of programs is Kleene coalgebra [6], which is mainly designed for automata theory. Playgrounds
may be viewed as adapting ideas from Kleene coalgebra to the process-algebraic setting.
We should also mention Laird’s games model of (a fragment of) π [47], which accounts
for trace (a.k.a. may testing) equivalence. Standard game models view strategies as sets
of traces (with well-formedness conditions), so, as we have seen, lend themselves better to

8

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

modelling trace equivalence. In a non-deterministic, yet not concurrent setting, Harmer and
McCusker [35] resort to an explicit action for divergence, which allows them to recover a
finer behavioural equivalence. We feel that the presheaf-based approach is more general.
Furthermore, recent work by Tsukada and Ong [71] adapts and extends some ideas
of [40, 38] to nondeterministic, simply-typed λ-calculus. In particular, they show that
innocent strategies as sheaves are compatible with the hiding operation of standard game
semantics. Eberhart and Hirschowitz further establish [22] a formal link between Tsukada
and Ong’s notion of innocence and ours: they construct a model of nondeterministic, simplytyped λ-calculus in our style, and then a morphism of Grothendieck sites, which entails that
both models are equivalent.
Let us moreover mention less closely related work: Girard’s ludics [31], Melliès’s
reworking of game semantics [56, 57], the part of it rediscovered by Levy [51] with a different
presentation, Melliès’s game semantics in string diagrams [58], Harmer et al.’s categorical
combinatorics of innocence [35], McCusker et al.’s graphical foundation for schedules [55],
and Winskel’s strategies as profunctors [73]. Finally, Hildebrandt’s work [37] also uses
sheaves, though as a tool to correctly handle infinite behaviour, as opposed to their use here
to force reactions of agents to depend only on their views.
1.7. Plan. In previous work [39], we have defined an algebraic notion called playground,
which provides a sufficient framework for sheaf-based innocence to make sense. Namely, it
organises positions, atomic actions, and traces into a pseudo double category [24, 25, 33, 34,
49, 30] with additional structure. Any playground D automatically gives rise, among other
things, to
● categories of innocent strategies SX on each position X, organised into a pseudo double
functor from Dop to small categories;
● a simple, yet complete syntax for innocent strategies, together with an lts SD for them
over an alphabet built from atomic actions.
After introducing some notation, the considered variant of π-calculus, fair testing
equivalence (Section 2), and recalling the notion of playground, we construct a playground D
for the π-calculus in Sections 3 to 5. This is a lot of work, and not all aspects of playgrounds
are used in defining the model and proving the main result. The reason we devote so
much energy to it is that playgrounds provide a really helpful setting, in fact a calculus, for
reasoning about positions, traces, views and the various notions of strategies. The underlying
pseudo double category is constructed in Section 3. The main playground axiom, asserting
that a certain functor is a Grothendieck fibration, is established in Section 4. Finally, the
remaining axioms are proved in Section 5.
We then continue in Section 6 by applying results from [39] to define our sheaf model
and semantic fair testing equivalence, as well as our translation ⟦−⟧ of π. We then state
the main result (Theorem 6.25). In Section 7, after introducing the basic notion of definite
residual, we reduce our main theorem to an analogous statement about an lts S for strategies
(derived from SD ). The advantage of the latter statement is that it lies entirely in the realm
of ltss. We then define a further, more syntactic lts M which we prove equivalent to S,
thus further reducing the main result to an analogous statement about M. We finally prove
the latter, which entails the main result.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

9

2. Notation and preliminaries
We start in this section with a few reminders. In Section 2.1, after fixing some basic
notation, we recall ltss. We use a slightly more general, graph-based notion than the
standard, relation-based one. In Section 2.2, we introduce the considered π-calculus, which
is mostly standard except that (1) we use a presentation in the style of Berry and Boudol’s
chemical abstract machine [5], and (2) we consider infinite terms, thus sparing us the need
for recursion or replication constructs. We then go on and recall fair testing equivalence
for π in Section 2.3. In fact, because we will also need to define fair testing for other ltss,
we introduce a general framework in which it makes sense, called graphs with testing. We
further provide sufficient conditions for a relation between the vertices of two graphs with
testing to preserve and reflect fair testing equivalence (Lemma 2.22 and Corollary 2.25).
Finally, in Section 2.4, we recall and briefly explain the definition of playgrounds.
2.1. Basic notation and labelled transition systems. First of all, we adopt the notation
of [39, Section 2], with the slight modification that set now denotes the category with finite
subsets of N as objects, and all maps as morphisms. (This category is equivalent to what we
used in [39], but slightly easier to work with for our purposes.) For all n ∈ N, we often abuse
̂ the category of presheaves
notation and let n denote the finite set {1, . . . , n}. We denote by C
̃
on C, and by C the category of presheaves of finite sets, i.e., of contravariant functors to set.
For any category C, let Cf denote the full subcategory of finitely presentable objects [4], or
finite objects for short. In the only case where we’ll use this, C will be a presheaf category
̂ will be
[Cop , set] and furthermore due to the special form of C, finite presentability of F ∈ C
equivalent to the category of elements of F being finite, and further equivalent to the set of
elements of F being finite, i.e., ∑c∈ob(C) F (c) is finite.
To recall some bare minimum: we often confuse objects C of a category C with the
̂ Gph denotes the category of reflexive graphs,
corresponding representable presheaves yC ∈ C.
and all our graphs are reflexive so we often omit mentioning it. We think of morphisms
p∶ G → A in Gph as ltss over the alphabet A, except that for reasons specific to playgrounds
our convention is that a transition from x to y is represented as an edge x ← y. Using graphs
as alphabets generalises the standard approach based on sets of labels: indeed, in order
to model any set of labels, take for A the graph with one vertex and one endo-edge for
each label. The extra generality is useful, e.g., to add some typing information on labels.
Finally, using graphs as alphabets provides us with standard tools for transporting ltss
across morphisms (by pullback, resp. post-composition).
For any graph G, G⋆ denotes the graph with the same vertices and all paths between
them; on the other hand, fc(G) denotes the free category on G, i.e., the category with the
same vertices and identity-free paths between them. Both (−)⋆ and fc extend to functors,
i.e., act on morphisms. We often silently coerce fc(G) into a reflexive graph, and denote by
̃
− the obvious morphism G⋆ → fc(G).
For any graph p∶ G → A over A, x, y ∈ ob(G), and edge a∶ p(y) → p(x) in A, we denote
a
by x ←
Ð y the existence of an edge e∶ y → x in G such that p(e) = a. When a = id , we just
write x ← y. We denote strong bisimilarity over A by ∼A .
For any graph p∶ G → A over A, x, y ∈ ob(G), and path ρ∶ p(y) → p(x) in A⋆ , we denote
ρ
⋆ (r) = ρ
̃. When ρ is the empty
by x ⇐
Ô y the existence of a path r∶ y → x in G⋆ such that p̃
path we just write x ⇐
Ô y. We denote weak bisimilarity over A by ≈A .

10

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

2.2. A π-calculus. We now present our variant of π, which features a chemical abstract
machine presentation and infinite terms. Also, we keep track of the channels known to the
considered process, i.e., we work with a ‘natural deduction’ presentation of terms.
Processes are infinite terms coinductively generated by the grammar
γ ⊢g P1

γ⊢P

γ ⊢g Pn

...

γ⊢Q

γ ⊢P ∣Q

γ ⊢ ∑ Pi
i∈n

γ, a ⊢ P

γ⊢P

γ⊢P

γ ⊢g νa.P

γ ⊢g ♡.P

γ ⊢g τ.P

a∈γ

γ, b ⊢ P

a, b ∈ γ

γ ⊢g a(b).P

γ⊢P

γ ⊢g ā⟨b⟩.P

,

where
● we have two judgements, ⊢ for processes and ⊢g for guarded processes;
● γ ranges over finite sets of natural numbers, and
● γ, a is defined iff a ∉ γ and then denotes γ ⊎ {a}.
Notation 2.1. Let Pi be the set of all such (non-guarded) processes. Let Pi γ denote the
set of processes γ ⊢ P .
As usual, a is bound in νa.P and b is bound in a(b).P . In the following, processes are
considered equivalent up to renaming of bound channels. Capture-avoiding substitution
extends the assignment γ ↦ Pi γ to a functor set → Set mapping σ∶ γ → γ ′ to P ↦ P [σ].
Let us now describe the dynamics of our π-calculus. They are slightly unusual, in
that they are presented in the style of the chemical abstract machine. In particular, there
are silent transitions for ‘heating’ both parallel composition and name creation. A further
slight peculiarity, which we adopt for its convenience in the chemical abstract machine
presentation, is that name creation is a guard. E.g., we have some processes of the form
(νa.P ) + b(x).Q. This is hardly significant. E.g., the previous process is strongly bisimilar to
(τ.νa.P ) + b(x).Q in more standard settings, and our results are about equivalences coarser
than weak bisimilarity anyway.
Notation 2.2. For any γ ⊢g P , γ ⊢ Q of the form ∑i∈n Qi , and injection h∶ n ↪ n + 1, we
denote by P +h Q the sum ∑j∈n+1 Pj , where Ph(i) = Qi for all i ∈ n and Pk = P , for k the
unique element of (n + 1) ∖ Im(h).
Definition 2.3. Let −⊙ denote the finite multiset monad on sets.
Definition 2.4. A configuration is an element of Conf = ∑γ∈Pf (N) Pi ⊙
γ.
Notation 2.5. Configurations (γ, S) will be denoted by ⟨γ∥S⟩, and we will use list syntax
[P1 , . . . , Pn ] for multisets, sometimes dropping brackets, e.g., as in ⟨γ∥P1 , . . . , Pn ⟩. We
sometimes resort to a hopefully clear ‘multiset comprehension’ notation [P ∣ ϕ(P )]. We use
∪ for multiset union and x ∶∶ M = [x] ∪ M .
Just as Pi , Conf extends to a functor set → Set by capture-avoiding substitution.
Let us now extend Conf to an lts over the alphabet {♡, τ }. This means that we need
to construct a graph morphism Conf → Σ, where Σ denotes
♡

●

τ ,

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

11

τ being the chosen identity edge.
This is done in Figure 1, omitting identity edges. There, we let R and R′ range over
processes of the form ∑i∈n Pi . The last rule makes sense because each transition as in the
premise implicitly comes with an inclusion h∶ γ1 ↪ γ2 , and the second occurrence of S is
implicitly S[h].
τ

τ

⟨γ∥P ∣ Q⟩ ←
Ð ⟨γ∥P, Q⟩
τ

⟨γ∥τ.P +h R⟩ ←
Ð ⟨γ∥P ⟩

⟨γ∥νa.P +h R⟩ ←
Ð ⟨γ, a∥P ⟩

⟨γ∥♡.P +h R⟩ ←
Ð ⟨γ∥P ⟩
♡

τ

⟨γ∥a(b).P +h R, ā⟨c⟩.Q +h′ R′ ⟩ ←
Ð ⟨γ∥P [b ↦ c], Q⟩
α

⟨γ1 ∥S1 ⟩ ←
Ð ⟨γ2 ∥S2 ⟩
α

⟨γ1 ∥S ∪ S1 ⟩ ←
Ð ⟨γ2 ∥S ∪ S2 ⟩

(α ∈ {τ, ♡})

Figure 1: Reduction rules for Conf

2.3. Fair testing equivalence. Let us now define fair testing equivalence for π, together
with our general framework of graphs with testing. Graphs with testing are essentially De
Nicola and Hennessy’s original framework [20], adapted to our graph-based presentation of
ltss. We derive a few results about general graphs with testing, notably sufficient conditions
for a relation between two graphs with testing to preserve and reflect fair testing equivalence.
Remark 2.6. In [39], an abstract framework was defined for studying fair testing equivalence
and its relationship with weak bisimilarity. We won’t use this here, and instead work in a
simpler setting.
We first cover π-calculus, and then generalise. The starting point is that we need to
be able to test processes against other processes, and more generally configurations against
configurations. Because configurations carry their sets of free channels, it makes sense to
consider a partial parallel composition operation:
Definition 2.7. For any ⟨γ∥S⟩, ⟨γ ′ ∥S ′ ⟩ ∈ Conf, let ⟨γ∥S⟩@⟨γ ′ ∥S ′ ⟩ denote ⟨γ∥S ∪ S ′ ⟩ if
γ = γ ′ and be undefined otherwise. Let furthermore γ = ⟨γ∥⟩.
Lemma 2.8. The domain of @, i.e., the set of pairs (C, C ′ ) such that C@C ′ , is an
equivalence relation.
Let us denote by ¨Conf this equivalence relation.
Here is the standard definition of fair testing equivalence:
Definition 2.9. Let Conf denote the set of configurations C such that for all C ⇐
Ô C ′,
♡
there exists C ′ ⇐
Ô C ′′ .
Any two configurations C and C ′ are fair testing equivalent iff C ¨Conf C ′ and for all
D ¨Conf C, (C@D) ∈ Conf iff (C ′ @D) ∈ Conf .
Let us now abstract away from this definition. For this, it would make sense to start
from a partial, parallel composition map. However, in the model, the corresponding map
will involve a pushout of positions which is only determined up to isomorphism. We thus

12

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

generalise from partial maps to relations, but we need to impose some conditions. What
matters is the use we will make of parallel composition for testing. Intuitively, we will check
that the parallel composition C@C ′ belongs to some given pole, which is closed under weak
bisimilarity over Σ. This choice is perhaps slightly arbitrary, but it encompasses all known
testing equivalences. Finally, to gain just a little more generality, we will use the fact that
weak bisimilarity over Σ coincides with strong bisimilarity over fc(Σ), and work with the
latter (Definition 7.40). For ltss over fc(Σ) obtained by applying fc to ones over Σ, this is
equivalent to the previous setting. The extra generality is useful for describing ltss which
are not free categories. E.g., in Section 7.1, we introduce the graph with testing C, whose
transitions are traces, which compose in a non-free way. We thus start from the following
notion, and then define fair testing equivalence.
Definition 2.10. A graph with testing is a graph G together with a morphism p∶ G → fc(Σ)
and a relation R∶ (ob(G))2
ob(G) whose domain is an equivalence relation and which is
partially functional up to strong bisimilarity over fc(Σ).
The domain being an equivalence relation more precisely means that the set {(x, y) ∣
∃z.(x, y) R z} forms an equivalence relation over ob(G).
Partial functionality up to strong bisimilarity means that if (x, y) R z and (x, y) R z ′ ,
then z ∼fc(Σ) z ′ .
Notation 2.11. The relation is called the testing relation, and we denote it by ∣G , i.e.,
(x, y) R z is denoted by z ∈ (x ∣G y). Furthermore, its domain is denoted by ¨G . We use ∣
and ¨ when there is no ambiguity. Since ∣ is partially functional up to strong bisimilarity,
for any (x, y) R z, as long as what we say about z is invariant under strong bisimilarity,
then it also holds for any other z ′ such that (x, y) R z ′ . In such cases, we implicitly make
some global choice of z and consider ∣ as partially functional.
Example 2.12. Figure 1 defines a morphism pConf ∶ Conf → Σ. Because, @ is a partial
map, it induces a partially functional relation ob(Conf)2
ob(Conf), whose domain is an
equivalence relation. Because partially functional implies partially functional up to strong
bisimilarity, we have:
Proposition 2.13. The morphism fc(pConf )∶ fc(Conf) → fc(Σ), with @ as testing relation,
forms a graph with testing.
We may now mimick the standard definition of fair testing equivalence in the abstract
setting:
Definition 2.14. For any graph with testing p∶ G → fc(Σ), let G denote the set of objects
♡
x such that for all x ←
Ð y, there exists y ←
Ð z.
Any two objects x and y are fair testing equivalent iff x ¨G y and for all z ¨G x,
(x ∣G z) ∈ G iff (y ∣G z) ∈ G .
Remark 2.15. Because we are working over fc(Σ), if G has the shape fc(G′ ), then single
♡
transitions like x ←
Ð y denote arbitrary paths of silent transitions. And analogously x ←
Ðy
denotes any path with all edges silent except exactly one.
Notation 2.16. We denote fair testing equivalence in G by ∼G
f . Given x, any z such that
x ¨ z is called a test for x, and x passes the test iff (x ∣G z) ∈ G .
Example 2.17. Definition 2.14 instantiates to Definition 2.9.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

13

In fact, the construction of the graph with testing fc(pConf ) from pConf is easily generalised:
ob(G) whose
Lemma 2.18. For any morphism pG ∶ G → Σ and relation R∶ (ob(G))2
domain is an equivalence relation, R equips fc(pG ) with testing structure iff it is partially
functional up to weak bisimilarity over Σ.
Proof. R is a strong bisimulation for fc(G) iff it is a weak bisimulation for G.
Definition 2.19. A graph with testing is free iff it is of the form fc(pG ).
Our fc(pConf ) is thus a free graph with testing.
Let us conclude this section with a sufficient condition for a relation between the
vertices of two graphs with testing to be adequate for fair testing equivalence, and a natural
specialisation to free graphs with testing.
Definition 2.20. A relation R∶ ob(G)
ob(H) between the vertex sets of two graphs with
testing pG ∶ G → fc(Σ) and pH ∶ H → fc(Σ) is fair iff
● x R y and x′ R y ′ implies (x ¨G x′ ) ⇔ (y ¨H y ′ );
● R is total and surjective, i.e.,
– for all x ∈ G, there exists y ∈ H such that x R y, and
– for all y ∈ H, there exists x ∈ G such that x R y;
● x R y implies x ∼fc(Σ) y;
● if x R y, x′ R y ′ , and x ¨G x′ , then there exist u ∈ (x ∣G x′ ) and v ∈ (y ∣H y ′ ) such that
u R v.
ob(H) between the vertex sets of two graphs with
Lemma 2.21. A relation R∶ ob(G)
G
H
testing p ∶ G → fc(Σ) and p ∶ H → fc(Σ) is fair iff its converse R† is, where R† is defined
by (y R† x) ⇔ (x R y).
Proof. Easy.
Lemma 2.22. For any fair relation R∶ ob(G)
′
H ′
(x ∼G
f x ) ⇔ (y ∼f y ).

ob(H), if x R y and x′ R y ′ , then

For proving this lemma, we need:
Lemma 2.23. For all graphs with testing pG ∶ G → fc(Σ) and pH ∶ H → fc(Σ), x ∈ G and
y ∈ H, if x ∼fc(Σ) y, then (x ∈ G ) ⇔ (y ∈ H ).
Proof. Assume x ∈ G and consider any transition y ← y ′ in H. By bisimilarity, x ← x′ ∼fc(Σ)
Ð x′′ , so by bisimilarity, y ′ ←
Ð y ′′ . Thus, y ∈ H , which entails
y ′ . By hypothesis, we find x′ ←
the result by symmetry.
♡

♡

Proof of Lemma 2.22. Consider any such x, y, x′ , and y ′ . By Lemma 2.21, it suffices to show
′
′
one direction of the desired equivalence. So let us assume that x ∼G
f x . Then x ¨G x , hence
also y ¨H y ′ by fairness of R. By symmetry, it again suffices to check one direction of the
desired implication. Consider thus any t ¨H y such that (y ∣ t) ∈ H . By surjectivity of R, we
find s ∈ G such that s R t. By fairness again, we find u ∈ (x ∣ s) and v ∈ (y ∣ t) such that u R v,
so (x ∣ s) ∼fc(Σ) u ∼fc(Σ) v ∼fc(Σ) (y ∣ t), and hence by the previous lemma (x ∣ s) ∈ G . Because
′
′
G
′
H
x ∼G
f x , this entails (x ∣ s) ∈  , hence by a similar argument (y ∣ t) ∈  , as desired.

14

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

ob(H) between the vertex sets of two free graphs
Definition 2.24. A relation R∶ ob(G)
with testing respectively generated by pG ∶ G → Σ and pH ∶ H → Σ is weakly fair iff it satisfies
the conditions of Definition 2.20, except for the third one, which is replaced by: x R y
implies x ≈Σ y.
Corollary 2.25. For any weakly fair relation R∶ ob(G)
fc(G) ′
fc(H) ′
then (x ∼f
x ) ⇔ (y ∼f
y ).

ob(H), if x R y and x′ R y ′ ,

Proof. Because weak bisimilarity over Σ is the same as strong bisimilarity over fc(Σ), being
weakly fair is the same as being fair for the generated graphs with testing.
2.4. Playgrounds. To conclude this preliminary section, let us recall the axioms for playgrounds [39]. Some constructions and results are developped from these axioms in op. cit.
Some of the main ideas are reviewed and reworked in Sections 6 and 7.
Let us start with a brief recap of pseudo double categories. A pseudo double category
D consists of a set ob(D) of objects, shared by a ‘horizontal’ category Dh and a ‘vertical’
bicategory Dv . Since we won’t consider strict double categories, we’ll often omit the word
‘pseudo’. Following Paré [64], Dh , being a mere category, has standard notation (normal
arrows, ○ for composition, id for identities), while the bicategory Dv earns fancier notation
(
for arrows, ● for composition, id ● for identities). D is furthermore equipped with a set
of double cells α, which have vertical, resp. horizontal, domain and codomain, denoted by
domv (α), codv (α), domh (α), and codh (α). The horizontal domain and codomain of a double
cell are vertical morphisms, while the vertical domain and codomain are horizontal morphisms.
E.g., for α in the diagram delow, we have u = domh (α), u′ = codh (α), h = domv (α), and
h′ = codv (α). D is furthermore equipped with operations for composing double cells: ○
composes them along a common vertical morphism, ● composes along horizontal morphisms.
Both vertical compositions (of morphisms and double cells) may only be associative up to
coherent isomorphism. The full axiomatisation is given by Garner [30], and we here only
mention the interchange law, which says that the two ways of parsing the above diagram
coincide: (β ′ ○ β) ● (α′ ○ α) = (β ′ ● α′ ) ○ (β ● α).
h

X
u

α

Y
v

Z

β

Y
Z

k′

′

Y

β′

v′
h′′

X ′′

α′

u′
h′

k

X′

′
k′′

Z

u′′
′′
v ′′
′′

For any (pseudo) double category D, we denote by DH the category with vertical morphisms as
objects and double cells as morphisms, and by DV the bicategory with horizontal morphisms
as objects and double cells as morphisms. Domain and codomain maps form functors
domv , codv ∶ DH → Dh and pseudofunctors domh , codh ∶ DV → Dv . We will refer to domv and
codv simply as dom and cod, reserving subscripts for domh and codh .

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

15

We then need to recall the notion of fibration (see [43]). Consider any functor p∶ E → B.
A morphism r∶ E ′ → E in E is cartesian when, as in
E ′′

t
s

E′
p(E ′′ )

E

r
p(t)

k

p(E ′ )

p(E),

p(r)

for all t∶ E ′′ → E and k∶ p(E ′′ ) → p(E ′ ), if p(r)○k = p(t) then there exists a unique s∶ E ′′ → E ′
such that p(s) = k and r ○ s = t.
Definition 2.26. A functor p∶ E → B is a fibration iff for all E ∈ E, any h∶ B ′ → p(E) has a
cartesian lifting, i.e., a cartesian antecedent by p.
Notation 2.27. We denote by E∣h the domain of the (chosen) cartesian lifting, and call it
the restriction of E along h.
We may now state the definition of playgrounds.
Remark 2.28. The following differs slightly from the original definition, mostly in presentation and terminology, but more significantly because the class B of basic moves was
mistakenly required to be replete in [39].
We provide some intuition right after the definition.
Definition 2.29. In a double category, a cell α is special when its vertical domain and
codomain cod(α) and dom(α) are identities.
Definition 2.30. A playground is a double category D such that cod is a fibration, equipped
with
● a full subcategory I ↪ Dh of objects called individuals,
● a full, replete1 subcategory M ↪ DH , whose objects are called actions, with full subcategories B and F of basic and full actions, with F replete,
● a map ∣ − ∣∶ ob(DH ) → N called the length,
satisfying the following conditions:
(P1) I is discrete. Basic actions have no non-trivial automorphisms in DH . Vertical
identities on individuals have no non-trivial endomorphisms.
(P2) (Individuality) Basic actions have individuals as both domain and codomain.
(P3) (Atomicity) For any cell α∶ v → u in DH , if ∣u∣ = 0 then also ∣v∣ = 0. Up to a special
isomorphism in DH , all plays u of length n > 0 admit decompositions into n actions.
For any u∶ X
Y of length 0, there is an isomorphism id ●X → u in DH , as in
X

X
αu

X
1Replete means closed under isomorphism.

ū

u

Y.

16

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

(P4) (Fibration, continued) Restrictions of actions (resp. full actions) to individuals either
are actions (resp. full actions), or have length 0.
X, and y∶ d → Y with d ∈ I, there exists a cell
(P5) (Views) For any action M ∶ Y
y

d

Y

αy,M

v y,M
y,M

d

M

X,

yM

where v y,M either is a basic action or has length 0, which is unique up to canonical
isomorphism, i.e., for any y ′ ∶ d′ → X, v ′ ∶ d
d′ , and α′ ∶ v ′ → M with dom(α′ ) = y
′
′
′
M
and cod(α ) = y , we have y = y and there exists a unique isomorphism β∶ v → v ′
making the diagram
y

d

αy,M ′
α
v′
yM

v y,M

dy,M

Y

β

d′

M

X
y′

commute.
(P6) (Left decomposition) Any double cell
h

A

h

A

X
α3

w1

α

decomposes as

Y

u

u

l

C

Y

α2

w2

u2

Z

k

w1

u1

w2

B

X

α1

B

Z

k

with α3 an isomorphism, in an essentially unique way.
(P7) (Right decomposition) Any double cell as in the center below, where b is a basic
action and M is an action, decomposes in exactly one of the forms on the left and
right:
A

X
α1

B

w

Y
α2

C

h

A
¢

α

B
C

A
¨

Y

B

M
k

Z

X
α1

u

b

Z

X

Y
α2

C

Z.

(P8) (Finiteness) For any object X, the comma category I/X (taken in Dh ) is finite.
(P9) (Basic vs. full) For all d ∈ I and actions M ∶ X
d, M ′ ∶ X ′
d, and b∶ d′
d with
′
′
M and M full and b basic, if there exist cells M ← b → M then M ≅ M ′ .
Intuitively, the objects of D are configurations, or positions, in the game. The considered
games are multi-party, so it makes sense to consider embeddings of positions: this is intended
to be described by the horizontal category Dh . The vertical category Dv is that of traces,

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

17

or plays: morphisms u∶ Y
X model plays from the initial position X, to the final one,
Y . Finally, cells model embeddings of plays, preserving initial and final position. E.g., this
could model embedding the part of a play involving a particular agent.
Individuals are intended to model agents in a position, with a role similar to that of
representable presheaves among general ones. Typically, the hom-set Dh (d, X), with d ∈ I,
models the set of agent slots of type d in the position X. For example, in the playground we
construct below for π, individuals bear the number of channels that an agent is connected
to, so that a morphism [n] → X amounts to an n-ary agent in X, i.e., an agent connected
to n channels. Accordingly, the object [n] models a position with just one n-ary agent.
Actions model moves in the game, and atomicity (P3) notably says that any play
decomposes into moves. The distinction between basic and full actions has to do with
innocence. The two notions are more or less dual: basic actions are as thin as possible, while
full ones are as wide as possible. Intuitively, an action is full when it cannot embed into a
larger one (unless possibly some agents are added), while it is basic when it cannot embed
any smaller one. As we will see, in our playground for π, we have an action for forking,
which describes how an agent x may fork into two, say x1 and x2 . This action is full, and it
has two basic sub-actions, which respectively model the passage from x to x1 and to x2 . For
another example, we also have an action for inputting on some given channel: it is obviously
basic, but in fact also full, because the only way to embed it into a wider action is to add an
agent and do a synchronisation. In view of this, it should be natural that basic actions have
individuals as their domain and codomain (P2). As alluded to in (P5), views will be defined
as composites of basic actions. Axiom (P5) intuitively enforces existence of one sub-action
for each agent in the final position of any action. Extending this to general plays will yield
an operation analogous to taking the view of a play in standard game semantics. Axiom (P9)
requires that these basic sub-actions may not be shared among different full actions.
Both (P6) and (P7) are decomposition axioms. The former says that a decomposition
of a play reflects essentially uniquely onto any subplay. The latter essentially says that basic
actions are strictly sequential: if any play of the form b ● w with b basic embeds into some
other play, then the image of w should occur after that of b. This is expressed in a slightly
convoluted way by saying that if the latter play decomposes as M ● u, then
● either b maps to M , in which case w should map to u,
● or b maps to U , in which case w should also map to u.
This should make most of the axioms rather intuitive: the others are technical, which
means that they emerged from our attempts to make things work out, but that we are not
yet able to explain them satisfactorily.
3. A pseudo double category of traces
In this section, we introduce our notion of trace, which is based on certain combinatorial
objects, close in spirit to string diagrams. We first define these string diagrams, and then use
them to define traces. Positions are special, hypergraph-like string diagrams whose vertices
represent agents and whose hyperedges represent channels. A perhaps surprising point is
that actions are not just a binary relation between positions, because we not only want to say
when there is an action from one position to another, but also how this action is performed.
This will be implemented by viewing actions from X to Y as cospans Y → M ← X in a
̃ f , whose objects we call higher-dimensional string diagrams for lack of a
certain category C
better term. The idea is that X and Y respectively are the initial and final positions, and

18

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

that M describes how one goes from X to Y . By combining such actions (by pushout), we
get a bicategory Dv of positions and traces. Finally, we recast Dv as the vertical bicategory
of a pseudo double category D.
̃ f will be a category of finite presheaves over a base
3.1. String diagrams. The category C
category, C. Let us motivate the definition of C by recalling that (directed, multi) graphs
may be seen as presheaves over the category with two objects ⋆ and [1], and two non-identity
morphisms s, t∶ ⋆ → [1]. Any such presheaf G represents the graph with vertices in G(⋆) and
edges in G[1], the source and target of any e ∈ G[1] being respectively G(s)(e) and G(t)(e),
or e⋅s and e⋅t for short. A way to visualise how such presheaves represent graphs is to compute
their categories of elements [54]. Recall that the category of elements el G for a presheaf G
over C has as objects pairs (c, x) with c ∈ C and x ∈ G(c), and as morphisms (c, x) → (d, y)
all morphisms f ∶ c → d in C such that y ⋅ f = x. This category admits a canonical functor πG
y
πG
̂ with the Yoneda embedding.
to C, and G is the colimit of the composite el G Ð→ C Ð
→C
s
t
E.g., the category of elements for y[1] is the poset (⋆, s) Ð
→ ([1], id [1] ) ←
Ð (⋆, t), which could
, where dots represent vertices, the triangle represents the edge, and
be pictured as
links materialise the graph of G(s) and G(t), the convention being that t connects to the
apex of the triangle. We thus recover some graphical intuition.
Let us give the formal definition of C for reference. We advise to skip it on a first
reading, as we then attempt to provide some intuition.
Definition 3.1. Let GC be the graph with, for all n, m, with a, b ∈ n and c, d ∈ m:
● vertices ⋆, [n], πnl , πnr , πn , νn , ♡n , τn , ιn,a , on,a,b , and τn,a,m,c,d ;
● edges s1 , ..., sn ∶ ⋆ → [n], plus, ∀v ∈ {πnl , πnr , ♡n , τn , on,a,b }, edges s, t ∶ [n] → v;
t

s

t

s

● edges [n] Ð
→ νn ←
Ð [n + 1] and [n] Ð
→ ιn,a ←
Ð [n + 1];
l

r

ρ



● edges πnl Ð
→ πn ←
Ð πnr and ιn,a Ð
→ τn,a,m,c,d ←
Ð om,c,d .
Let C be the free category on GC , modulo the equations
s ○ si = t ○ si

l○t=r○t

ρ ○ t ○ sa =  ○ t ○ sc

ρ ○ s ○ sn+1 =  ○ s ○ sd .

The first equation should be understood in C(⋆, v) for all n ∈ N, i ∈ n, and v ∈ ∪a,b∈n {πnl , πnr ,
♡n , τn , ιn,a , on,a,b , νn }. (This is rather elliptic: if v has the shape ιn,a or νn , s ○ si is really
si
s
⋆ Ð→ [n + 1] Ð
→ v.) The second equation should be understood in C([n], πn ) for all n, and
the last two in C(⋆, τn,a,m,c,d ), for all n, m, a ∈ n, and c, d ∈ m.
̃ f . A presheaf X
Our category of string diagrams is the category of finite presheaves C
over C is a kind of higher-dimensional graph whose components are typed by objects of C:
● X(⋆) is the set of vertices, or channels;
● X[n] is the set of agents connected to n channels (which are given by X(si ));
● X(ιn,a ) is the set of input actions by some n-ary agent on its ath channel;
● X(om,c,d ) is the set of output actions by some m-ary agent on its cth channel of its dth
channel;
● X(τn,a,m,c,d ) is the set of synchronisations between some input and some output on a
common channel;
● X(πn ) is the set of forking actions by some n-ary agent;
● and similarly for X(πnl ), X(πnr ), X(νn ), X(♡n ), and X(τn ).

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

19

(⋆, s1 ) (⋆, s2 ) (⋆, s3 )
([3], id [3] )
ls
lss1

l
s

ts1



rs
id π2

r

lss2
ρs

lt = rt
ts3

β

id τ
n,a,m,c,d

ρ

ts2
t

y′

x′

α

ρt

x

y

Figure 2: Categories of elements for [3], π2 , and τ1,1,3,2,3 , with graphical representation
To see these intuitions at work, let us compute a few categories of elements. Let us start
with an easy one, that of [3] ∈ C (recalling that we implicitly identify any c ∈ C with yc ).
An easy computation shows that it is the poset pictured in the top left part of Figure 2. We
think of it as a position with one agent ([3], id [3] ) connected to three channels, and draw it
as in the top right part, where the bullet represents the agent, and circles represent channels.
Definition 3.2. Positions are finite presheaves empty except perhaps on ⋆ and [n]s.
Let us organise positions into a category, by designing a notion of morphism. We may
equip the objects of C with a dimension: ⋆ has dimension 0, any [n] has dimension 1, all of
τn , πnl , πnr , ♡n , ιn,a , on,c,d , νn have dimension 2, πn has dimension 3, τn,i,m,j,k has dimension 4.
Definition 3.3. We accordingly define the dimension of a presheaf X on C to be the lowest
n ∈ N such that for any m ∈ C of dimension strictly greater than n, X(m) = ∅.
A position is thus equivalently a finite presheaf in [Cop , set] of dimension at most 1. An
interface is one of dimension 0.
̂ is 1-injective iff it is injective in all strictly positive dimensions.
Definition 3.4. A map in C
̂ The intuition for a morphism
A morphism of positions is a 1-injective morphism in C.
X → Y between positions is thus that X embeds into Y , possibly identifying some channels.
Definition 3.5. Positions and morphisms between them form a category Dh .
Returning to our explanation of C through categories of elements, let us consider that of
π2 . It is the poset generated by the left-hand graph in the second row of Figure 2 (omitting
base objects for conciseness). We think of it as a binary agent (lt) forking into two agents
(ls and rs), and draw it as on the right. The equation lt = rt ensures that π2l and π2r are
performed by the same agent. The graphical convention is that a black triangle stands
for the presence of id π2 , l, and r. Below, we represent just l as a white triangle with only
a left-hand branch, and symmetrically for r. Furthermore, in all our pictures, time flows
‘upwards’.
Another category of elements, characteristic of the π-calculus, is the one for synchronisation τn,a,m,c,d . The case (n, a, m, c, d) = (1, 1, 3, 2, 3) is the poset generated by the graph at

20

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

♡

♠

[p]

[p]

[m]

[n + 1]

[p]

[p]

[p + 1]

πpl

πpr

om,c,d

ιn,a

♡p

τp

νp

[p]

[p]

[m]

[n]

[p]

[p]

[p]

Figure 3: Pictures and corresponding cospans for πpl , πpr , om,c,d , ιn,a , ♡p , τp , and νp
the bottom left of Figure 2, which we will draw as on the right. The left-hand ternary agent
x outputs its 3rd channel, here β, on its 2nd channel, here α. The right-hand unary agent y
receives the sent channel on its unique channel, here α. Both agents have two occurrences,
one before and one after the action, respectively marked as x/x′ and y/y ′ . Both x and x′
are ternary here, while y is unary and y ′ , having gained knowledge of β, is binary. There are
actually three actions here, in the sense that there are three higher-dimensional elements.
The first is the output action  from x to x′ , graphically represented as the middle point of
(intended to evoke the point where β enters channel α). The second is the input
action ρ from y to y ′ , graphically represented as the middle point of
(where β
exits channel α). The third action is the synchronisation itself, which ‘glues’ the other two
together, as represented by the squiggly line.
We leave the computation of other categories of elements as an exercise to the reader.
The remaining string diagrams are depicted in the top row of Figure 3, for p = 2 and
(n, a, m, c, d) = (1, 1, 3, 2, 3). The first two are views, in the game semantical sense, of the
fork action π2 explained above. The next two, om,c,d (for ‘output’) and ιn,a (for ‘input’),
respectively are views for the sender and receiver in a synchronisation action. The τp action
is a silent, dummy action standard in π-calculus. The ♡p action is the special ‘tick’ action
used for defining fair testing equivalence. The last one, νp , is a channel creation action.
3.2. From string diagrams to actions. In the previous section, we have defined our
̃ f , and provided some intuition on its objects. The next step
category of string diagrams as C
is to construct a bicategory whose objects are positions, and whose morphisms represent
traces. We start in this section by defining in which sense higher-dimensional objects of C
represent actions, and continue in the next one by explaining how to compose actions to
form traces. Actions are defined in two stages: seeds, first, give their local form, their global
form being given by embedding into bigger positions.
To start with, until now, our string diagrams contain no information about the ‘flow of
time’, although we mentioned it informally in the previous section. To add this information,
for each string diagram M representing an action, we define its initial and final positions,
s
t
say X and Y , and view the whole action as a cospan Y Ð
→M ←
Ð X. We have taken care, in
drawing our pictures before, of placing initial positions at the bottom, and final positions at
the top. So, e.g., the initial and final positions for the example synchronisation of Figure 2
are as follows.
↝

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

21

They map into (the representable presheaf over) τ1,1,3,2,3 , yielding the cospan
s

t

Y Ð
→ τ1,1,3,2,3 ←
Ð X.
We leave it to the reader to define, based on the above pictures, the expected cospans for
forking and synchronisation
[p] ∣ [p]

[m] c,d ∣ a,n+1 [n + 1]

πp

τn,a,m,c,d

[p]

[m] c ∣ a [n]

plus the remaining ones specified in the bottom row of Figure 3. Initial positions are at the
bottom, and we use:
Notation 3.6. We denote by [m] a1 ,...,ap ∣ c1 ,...,cp [n] the position consisting of an m-ary agent
x and an n-ary agent y, quotiented by the equations x ⋅ sak = y ⋅ sck for all k ∈ p. When both
lists are empty, by convention, m = n and the agents share all channels in order.
Definition 3.7. These cospans are called seeds.
We now define actions from seeds by embedding the latter into bigger positions. E.g.,
we allow a fork action to occur in a position with more than one agent.
̂ is F (⋆) ⋅ ⋆, the F (⋆)-fold coproduct of
Definition 3.8. The interface IF of a presheaf F ∈ C
⋆ with itself, or in other words the position consisting solely of F ’s channels. The interface
s
t
of a seed Y Ð
→M ←
Ð X is IX .
Since channels occurring in the initial position remain in the final one, we have for each
seed a cone from IX to the seed. For any morphism of positions IX → Z, pushing the cone
along IX → Z using the universal property of pushout as in
Y

Y′

M

M′

IX

(3.1)

Z
X′

X
yields a new cospan, say Y ′ → M ′ ← X ′ .

Definition 3.9. Let actions be all such pushouts of seeds.
Intuitively, taking pushouts glues string diagrams together. Let us do a few examples.
[ls,rs]

lt

Example 3.10. The seed [2] ∣ [2] ÐÐÐ→ π2 ←
Ð [2] has as interface the presheaf I[2] = ⋆ + ⋆,
consisting of two channels, say a and b. Consider the position [2] + ⋆ consisting of an agent
y connected to two channels b′ and c, plus an additional channel a′ . Further consider the
map h∶ I[2] → [2] + ⋆ defined by a ↦ a′ and b ↦ b′ . The pushout
x1

I[2]

is
π2

x2

[2] + ⋆
M′

.
a=a′

b=b′
x

y

c

22

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

y ′′
c
x1

y1

x2

a=a′

y2

c

b=b′
x

y′

a

y

a

b
x

y

c
z

Figure 4: Example traces
The meaning of such an action is that x forks while y is passive.
Example 3.11. Because we push along initial channels, the interface of a seed may not
contain all involved channels. E.g., in an input action (not part of any synchronisation), the
received channel cannot be part of the initial position.
3.3. From actions to traces. Having defined actions, we now define their composition to
̃ f ), the bicategory which
yield our bicategory Dv of positions and traces. Consider Cospan(C
has as objects all finite presheaves on C, as morphisms X → Y all cospans X → U ← Y , and
obvious 2-cells. Composition is given by pushout, and hence is not strictly associative.
Notation 3.12. By convention, the initial position is the target of the morphism in
̃ f ). We denote morphisms in Cospan(C
̃ f ) with special arrows Y
Cospan(C
X; composition
●
and identities are denoted with ● and id , which matches the notation of pseudo double
categories (Section 2.4).
̃ f which is isomorphic to some finite, possibly
Definition 3.13. A trace is any cospan in C
̃ f ). Let Dv denote the subbicategory of Cospan(C
̃f )
empty composite of actions in Cospan(C
obtained by restricting to positions, traces, and 1-injective 2-cells.
Thus, arrows X → Y in Dh denote embeddings of X into Y (up to identification of
channels), whereas arrows Y
X in Dv denote traces with X initial and Y final. Intuitively,
composition in Dv glues string diagrams on top of each other, which yields a truly concurrent
notion of trace: the only information retained in a trace about the order of occurrence of
actions is their causal dependencies.
Example 3.14. Composing the action of Example 3.10 with a forking action by y yields
the first string diagram of Figure 4, which shows that the ordering between remote actions
is irrelevant. To illustrate how composition retains causal dependencies between actions,
consider the second string diagram. It is unfolded for readability: one should identify both
framed nodes, resp. both circled ones. In the initial position, there are channels a, b, and c,
and three agents x(a, b), y(b), and z(a, c) (channels known to each agent are in parentheses).
In a first action, x sends a on b, and y receives it. In a second action, z sends c on a, and
the avatar y ′ of y receives it. The second action is enabled by the first, by which y gains
knowledge of a.
Before going on to construct the base double category for our playground, let us observe
the following two basic facts about traces.
s

t

Lemma 3.15. For any trace Y Ð
→U ←
Ð X, s and t are monos.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

23

(EXPANDED VERSION)

Proof. We proceed by induction on the number of actions involved in any decomposition of
U . The base case is trivial. For the induction step, because composition of cospans is by
pushout, the result follows from the induction hypothesis, stability of monos under pushout
and composition, and the fact that the result holds for actions. The latter in turn follows
from the fact that monos are stable under pushout (again!), the pushout lemma, and the
fact that the result holds for seeds, which holds by case inspection.
s

t

Lemma 3.16. For any trace Y Ð
→U ←
Ð X, s⋆ is an isomorphism.
Proof. Similar to the previous proof.
The intuition behind the last lemma is that no channel is forgotten during the play.
3.4. The main double category. At last, we define the base double category D of our
playground for the π-calculus. It is a sub-double category of a double category of cospans
̂
in C.
Consider the double category D0 with
● positions as objects,
● horizontal morphisms X → Y given by all natural transformations h∶ X → Y ,
s
t
̂
● vertical morphisms X
Y given by cospans X Ð
→U ←
Ð Y in C,
● and double cells U → V given by commuting diagrams
X′

k

Y′

sU

U

sV
l

tU

X

(3.2)

V
tV

h

Y.

Definition 3.17. Let D denote the sub-double category of D0 obtained by restricting
● vertical morphisms to traces,
● horizontal morphisms to 1-injective maps,
● double cells to diagrams (3.2) in which k, l, and h are 1-injective.
Proposition 3.18. D indeed forms a sub-double category of D0 , i.e., is closed under all
composition operations.
Proof. The only non-obvious point is that double cells in D are closed under vertical
composition, and in particular that the middle component of the composite is 1-injective.
This follows from Lemma 3.20 and Corollary 3.22 below.
Definition 3.19. Let V0 denote the set of ‘t’-legs (i.e., lower legs) of seeds.
Lemma 3.20. For any morphism (3.2) in D0H , if U and V are traces, then the upper square
is a pullback.
s

t

Proof. For any trace Y Ð
→P ←
Ð X and n ∈ N, Y [n] consists of all elements of P [n] which
are not in the image of (the action of) any map in V0 .
Now, consider any double cell as in (3.2). Because sV is monic, U ×V Y ′ may be chosen
to be just l−1 (Y ′ ) ⊆ U . By Lemma 3.15 and standard cancellation properties of monos,

24

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

the mediating arrow X ′ → U ×V Y ′ is mono. To show that it is epi, we proceed pointwise.
Over ⋆, the result follows from sU and sV being isomorphisms (Lemma 3.16). Over [n],
if x ∈ (U ×V Y ′ )[n] then x ∈ U [n], and l(x) ∈ V [n] is not in the image of (the action of)
any t ∈ V0 . But if there existed y such that y ⋅ t = x, then by naturality we would have
l(y) ⋅ t = l(x), contradicting the latter. Any natural transformation being both epi and mono
is an isomorphism, hence the result.
Lemma 3.21. In Set, consider any cube
I

B
A

I′

C
B′

A′

f

C ′,

with the marked pushouts and pullback, and with all arrows mono except perhaps f . Then, f
is also mono and the front square is also a pullback.
Proof. Any such cube is naturally isomorphic to some cube of the shape
I +R

I
I +Y

injl

I +Y +R
injl +k

I+h

I +X

f =I+h+k

I +X +S
injl

I +X +Z

I + X + Z + S,

the only non-trivial point being that the map I + R → I + X + S has the given shape. But
this is because we know that its pullback along I + X → I + X + S is injl , so the image of R
has to lie in S.
Corollary 3.22. Consider any cube
X

B
A

X′

C
B′

A′

f

C ′,

̂ in which all arrows except perhaps f are 1-injective, and the marked squares are
in C
pushouts, resp. pullbacks. Then f is also 1-injective.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

25

Proof. We proceed pointwise. On any object C of dimension > 0, we obtain a diagram in
sets for which the lemma applies.

4. Codomain is a fibration
In this section, we prove that the double category D of traces constructed in the previous
section satisfies the primary axiom for playgrounds, namely that the codomain functor
DH → Dh is a fibration. We proceed as follows. We first define a (strong) factorisation
̂ (Section 4.1), from which we derive in Section 4.2 an intermediate sub-double
system on C
category D ↪ D1 ↪ D0 . We further show that by the properties of factorisation, the codomain
functor D1H → D1h is a fibration. Finally, we want to show that DH → Dh is a fibration by
proving that traces are stable under relevant cartesian lifting in D1 , i.e., cartesian liftings of
any trace along any morphism in Dh are again in DH . We first check this for seeds, by case
analysis, in Section 4.3. In order to generalise to actions M ∶ Y
X, the basic idea is to
(1) decompose X as a pushout of X0 , where the generating seed M0 takes place, and Z,
which is passive;
(2) decompose the morphism along which we want to restrict, say h∶ X ′ → X, accordingly,
say as h0 ∶ X0′ → X0 and hZ ∶ Z ′ → Z;
(3) restrict M0 along h0 to obtain P0′ ;
(4) recompose a trace P ′ from P0′ and Z ′ ;
(5) check that P ′ admits a cartesian morphism to M .
Step (4) is non-trivial, so we devote Section 4.4 to it. It works as a kind of formal opposite to
restriction, as we essentially lift P0′ along h0 ∶ X0′ → X ′ . We call this an oplifting of P0′ along
h0 , by analogy with lifting in opfibrations. However, opliftings do not enjoy the relevant
universal property (opcartesianness, which is dual to cartesianness). Instead, we find that
opliftings are in fact cartesian! In Section 4.5, we use opliftings to show that actions are
stable under restriction, following the above plan. Finally, we extend the result to arbitrary
traces in Section 4.6.
4.1. A factorisation system. Let us start by defining the (strong) factorisation system
̂ on which the intermediate sub-double category D1 will be based. The idea is
(V, H) on C,
that all three components of cartesian morphisms in DH are in H, while t-legs of vertical
morphisms are in V. The cartesian lifting of any V ∶ Y ′
Y as in (3.2) along any h∶ X → Y
is then given by factoring tV ○ h as l ○ tU with tU ∈ V and l ∈ H to obtain
X′

k

Y′

sU

U

sV
l

tU

X

(4.1)

V
tV

h

Y,

where the upper square is a pullback.
We recall from Definition 3.19 that V0 denotes the set of ‘t’-legs (i.e., lower legs) of
seeds. Following Bousfield’s [8] construction of ‘cofibrantly generated’ factorisation systems,
we define H = V0 to be the class of maps f such that for any t ∈ V0 and commuting square
̂ → , there exists a unique filler h making the following diagram commute:
(u, v)∶ t → f in C

26

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

X
t

Y

u

X′

h
v

f
′

Y .

In this situation, one says that f is right-orthogonal to t, and t is left-orthogonal to f , which
is denoted by t  f .
We finally define V =  H to consist of all maps which are left-orthogonal to any map in
H. Of course, we have V0 ⊆ V. The following is an application of [8, Theorem 4.1]:
Proposition 4.1. The pair (V, H) forms a factorisation system.
What does that mean? Here is a modern definition [29]:
Definition 4.2. The classes of maps V and H form a factorisation system iff V =  H,
V = H, and any arrow factors as h ○ v with h ∈ H and v ∈ V.
̂ admits a
In the case where H = V0 and V =  H, Bousfield proves that any map in C
factorisation using a transfinite construction (a so-called small object argument). But here
we will only need factorisations of particular morphisms, which we will actually be able to
calculate by hand. Bousfield’s results include:
Lemma 4.3. V is stable under pushout and composition, contains all isomorphisms, and
enjoys the right cancellation property, i.e., if v ∈ V and f v ∈ V, then f ∈ V.
H is stable under pullback and composition, contains all isomorphisms, and enjoys the
left cancellation property, i.e., if h ∈ H and hf ∈ H, then f ∈ H.
Remark 4.4. Stability under pushout is ambiguous here: we mean that for any pushout
X
v

Z

Y
v′

T,

if v ∈ V, then v ′ ∈ V. Stability under pullback is defined dually.
4.2. A first ‘fibred’ double category. We now make concrete the idea evoked in the
previous section, of using our factorisation system to obtain a codomain fibration. Consider
the sub-double category D1 of D0 obtained by restricting vertical morphisms to cospans
s
t
XÐ
→U ←
Ð Y with t ∈ V. Its vertical morphisms are stable under composition and contain
identities by Lemma 4.3, i.e.:
Lemma 4.5. D1 forms a sub-double category of D0 .
Lemma 4.6. Traces are in D1v , i.e., we have D ⊆ D1 .
Proof. By Lemma 4.3.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

27

The main interest of introducing D1 is:
Lemma 4.7. The codomain functor cod∶ D1H → D1h is a fibration in which a double cell (3.2)
is cartesian iff l ∈ H and the upper square is a pullback.
Proof. Let us show that the lifting candidate computed in (4.1) is cartesian. Indeed, consider
any double cell (4.1), and any morphism from some vertical morphism Z ′ → W ← Z to V
whose bottom component factors through h∶ X → Y . By unique lifting in (V, H), we obtain
a unique dashed arrow making
Z

X

U

Y
W

V

commute. We finally obtain the desired arrow Z ′ → X ′ by universal property of pullback.
Conversely, any cartesian double cell, being isomorphic to such a lifting, satisfies the
conditions.
As a final observation, let us record:
Lemma 4.8. Any morphism in Dh is automatically in H.
Proof. Indeed, consider any h∶ X → Y in Dh . There cannot be any commuting square
u

X0

X

t

h

U

Y

v

with t ∈ V0 , because U is a representable presheaf of dimension > 1 and Y has dimension ≤ 1,
so there cannot be any v∶ U → Y .
4.3. Restriction of seeds. We now show that restrictions of seeds (in the sense of D1 ) are
traces.
h

t

Lemma 4.9. Consider any diagram X ′ Ð
→XÐ
→ M , where t ∈ V0 and h ∈ Dh (X ′ , X). Its
t′

h′

factorisation X ′ Ð
→ M ′ Ð→ M with t′ ∈ V and h′ ∈ H is such that h′ is 1-injective and the
obtained restriction is a trace of length at most 2. If X ′ is an individual, i.e., a position of
shape [n], then it is isomorphic to some seed. If X ′ is an interface, then the restriction is
an equivalence (in Dv ).
Proof. We proceed by case analysis. In each case, one has to check that h′ is 1-injective,
that X ′ individual implies t′ seed, that X ′ interface implies that t′ is an isomorphism, and
that the upper leg of the obtained cospan is as expected: this is routine so we mention it
here once and for all.
Let us first treat the case where M = yc , for c not of the shape τn,i,m,j,k . Then, we
have X = [n] for some n. If idc ∈ Im(th), then X ′ ≅ [n] + I for some interface I (since h is
1-injective). Consider the diagram

28

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

M +I

[id,tk]

M

t+idI

t

[n] + I

[n].

h=[id,k]

The map t + idI is in V by Lemma 4.3, so we just have to prove that [id, tk] is in V0 , which
is a simple verification.
If now idc ∉ Im(h), then X ′ is an interface, and the relevant factorisation is
t○h

X′

M

X

(4.2)

t

id
′
h

[n],

because t ○ h is easily checked to be in V0 .
The case of τn,i,m,j,k is a bit more complicated. Here, t is actually t0 = [ρt, t]. First of
all, if X ′ is an interface, then we obtain a factorisation analogous to (4.2). Consider now
the case where Im(h) contains both agents of [n] i ∣ j [m]. Let x denote the n-ary one and y
denote the m-ary one (in X ′ ). If x ⋅ si = y ⋅ sj , then X ′ = ([n] i ∣ j [m]) + I for some interface
I and the required factorisation is easily seen to be
[id,t0 k]

τn,i,m,j,k + I

τn,i,m,j,k
t0

t0 +id I

([n] i ∣ j [m]) + I

h=[id,k]

[n] i ∣ j [m].

Consider now the case where X ′ still contains both agents but x ⋅ si ≠ y ⋅ sj . Then
X = [n] + [m] + I for some interface I, and the required factorisation is
′

[ρ,,t0 k]

ιn,i + om,j,k + I

τn,i,m,j,k
t0

t+t+id I

[n] + [m] + I

[x,y,k]

[n] i ∣ j [m].

The only non-trivial point here is to show that [ρ, , t0 k] is in V0 , which easily reduces
to showing that there is no commuting square
[n] i ∣ j [m]

u

t0

τn,i,m,j,k

ιn,i + om,j,k + I
[ρ,,t0 k]

v

τn,i,m,j,k ,

which is true because there is no such u.
The cases where X ′ only contains one agent of [n] i ∣ j [m] are similar to the latter case:
if it contains x then the factorisation is through ιn,i , and otherwise it is through om,j,k .

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

29

4.4. Opliftings. We now aim at extending Lemma 4.9 from seeds to actions. Consider an
arbitrary action Y → M ← X, obtained by pushing some seed Y0 → M0 ← X0 along IX0 → Z.
Consider now a morphism h∶ X ′ → X in Dh , along which we wish to restrict M . As explained
at the beginning of Section 4, our strategy is to consider the pullback
X0′

X0

X′

X.

Indeed, the part of X really concerned by M is the image of X0 , so we would like to first
restrict M0 to X0′ using Lemma 4.9, and then extend it to X ′ . The present section is devoted
to constructing the second step, the extension of (M0 )∣X0′ to X ′ , which we call an oplifting
of (M0 )∣X0′ along X0′ → X ′ .
In the general case, we want to compute the oplifting of Y → U ← X along h∶ X → X ′ .
Because h is 1-injective, we can complete the solid part of
IX

Z

⊆

⊆
′

X

X

h
′

into a pushout. Indeed, we take Z(⋆) = X (⋆), Z[n] = X ′ [n] ∖ Im(h[n] ) for all n, and
IX → Z is uniquely determined by h⋆ . In passing, we have:
Lemma 4.10. This pushout is uniquely determined up to canonical isomorphism by h alone.
Then, we observe that, because U is a trace, IX → X → U factors through Y → U .
Definition 4.11. Let the oplifting of U ∶ Y
as in (3.1) by pushing U along IX → Z.

X along h∶ X → X ′ be the cospan obtained

All horizontal maps are 1-injective by construction, and we have:
Lemma 4.12. The obtained cospan Y ′ → U ′ ← X ′ is a trace.
Proof. We start by showing that U ′ is an action if U is. So assume U is obtained by pushing
a seed Y0 → M0 ← X0 along some IX0 → Z0 . Then, Z0 → X is surjective on ⋆ because
IX0 → X0 is and epis are stable under pushout in presheaf categories. Thus, IX → X factors
through Z0 → X. Let Z ′′ denote the pushout
IX

Z0

Z

Z ′′ .

By the pushout lemma, Y ′ → U ′ ← X ′ is isomorphic to the cospan obtained by pushing
Y → U ← X along Z0 → Z ′′ . By the pushout lemma again, it is isomorphic to the cospan
obtained by pushing Y0 → M0 ← X0 along IX0 → Z0 → Z ′′ . Thus, it is indeed an action.
We now prove the general case by induction on ∣U ∣. This is trivial if U is isomorphic to
an identity. If now U is a composite Z
along h to obtain a double cell, say

V

Y

M

X, then we compute the oplifting of M

30

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Y
M

X

h′
αM
h

Y′
M′
′

X,

by pushing M along some morphism IX → Z1 making
IX
X

Z1

h

X′

into a pushout.
The crucial insight is then that by computing the following pushout Z2 and applying its
universal property, we obtain a diagram
IX

IY

Y
(4.3)

Z1

Z2

Y

′

whose exterior is a pushout by construction. So by the pushout lemma the right-hand square
is again a pushout, which by Lemma 4.10 is the unique pushout along which to push V to
compute the oplifting of V along h′ , say
Z
V

Y

h′′
αV
h′

Z′
V′
′

Y .

By induction hypothesis, V ′ is again a trace. But by the pushout lemma again, αV is also
what we obtain by pushing V along the exterior rectangle of (4.3). A bunch of applications
of the pushout lemma finally yields that αM ● αV is the oplifting of M ● V along h, so M ′ ● V ′
is a trace by construction.
Although opliftings have an opcartesian flavour, they are in fact not opcartesian in
general, and moreover opcartesian liftings do not exist in general.
Example 4.13. Consider the oplifting of the seed ι1,1 along [1] ↪ [1] 1 ∣ 1 [1], say ι1,1 1 ∣ 1 [1],
whose final position is [2] 1 ∣ 1 [1]. To see that it is not opcartesian, consider the diagram
[2] 1,2 ∣ 1,1 [1]
[2]

[2] 1 ∣ 1 [1]
τ1,1,1,1,1

ι1,1

ι1,1 1 ∣ 1 [1]
[1] 1 ∣ 1 [1]

[1]

[1] 1 ∣ 1 [1].

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

31

In this case, opcartesianness would mean finding dashed arrows rendering the diagram
commutative. There is indeed a unique arrow ι1,1 1 ∣ 1 [1] → τ1,1,1,1,1 making the corresponding
square commute, but then no arrow [2] 1 ∣ 1 [1] → [2] 1,2 ∣ 1,1 [1] fits. Indeed, there is only one
arrow of the given type, and it does not make the relevant square
[2] 1 ∣ 1 [1]

[2] 1,2 ∣ 1,1 [1]

ι1,1 1 ∣ 1 [1]

τ1,1,1,1,1

commute, because one side (down; right) of the square maps the unary player to ρ ○ t, while
the other (right; down) maps it to ρ ○ s. This shows that ι1,1 1 ∣ 1 [1] is not an opcartesian
lifting of ι1,1 . But in fact, ι1,1 1 ∣ 1 [1] and τ1,1,1,1,1 are two liftings of ι1,1 along [1] ↪ [1] 1 ∣ 1 [1].
Thus, any opcartesian lifting should have a final position mapping both to [2] 1 ∣ 1 [1] and
[2] 1,2 ∣ 1,1 [1], hence containing just one, binary player: no trace can meet this requirement.
However, even though they are not opcartesian, opliftings are in fact cartesian. Let us
now show this, starting with a few preliminary results.
Definition 4.14. Let Agents(X) = ∑n∈N X[n] denote the set of agents of any position X.
Lemma 4.15. For any seed Y → C ← X, the morphism
[x](n,x)

[n] ÐÐÐÐ→ X

∑
(n,x)∈Agents(X)

is epi.
Proof. This is trivial except in dimension 0, where it holds by case inspection.
Corollary 4.16. For all arrows as in
h

X

U

h′

t

C

U

g

f
′

̂ such that f is 1-injective, t ∈ V0 , and f h = gt = f h′ , we have h = h′ .
in C
Proof. We construct the diagram
he

∑(n,x)∈Agents(X) [n]

U
h′ e

e
h

X
t

C

U
h′

g

f

U ′,

and observe that h′ e = he by 1-injectivity of f , hence h = h′ because e is epi by Lemma 4.15.

32

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Lemma 4.17. Opliftings of traces are cartesian.
f

Proof. Consider any oplifting U Ð
→ U ′ of Y → U ← X along, say X → X ′ . By Lemma 4.7,
it is enough to show that the middle arrow U → U ′ is in H and that its upper square is a
pullback. The latter follows from Lemma 3.20. So we just have to show that any square
Z

u

U

v

U′

t

C

with t ∈ V0 admits a unique lifting C → U . By the Yoneda lemma, v amounts to an element of
U ′ (C) of dimension > 1, but by construction U and U ′ have exactly the same such elements.
This yields a candidate lifting, say k, which is unique by 1-injectivity and makes the bottom
triangle commute by construction. The top one finally commutes by Corollary 4.16 with
h = u and h′ = kt.
4.5. Restriction of actions. Let us now extend Lemma 4.9 from seeds to actions, following
the strategy sketched at the beginning of Section 4.
s

t′

t

→M ←
Ð X and h ∈ Dh (X ′ , X), the factorisation X ′ Ð
→
Lemma 4.18. For any action Y Ð
h′

P ′ Ð→ M of th with t′ ∈ V and h′ ∈ H is such that h′ is 1-injective and the obtained restriction
is a trace of length at most 2. If X ′ is an individual then it is either a seed or an equivalence;
if X ′ is an interface then it is an equivalence.
Proof. Consider any action Y → M ← X obtained by pushing the following seed-withinterface along I → Z:
I
Y0

M0

X0 .

By Lemma 4.17, the morphism M0 → M is cartesian.
Consider the pullback of the bottom square below along h∶ X ′ → X to obtain the top
square
I′

Z′
X0′

I

X′
Z

X0

f

X,

which, because presheaf categories are adhesive [46] and I → X0 is mono, is again a pushout.
Furthermore, consider the front face, which is a pullback in Dh . By Lemma 4.9, restricting
M0 along X0′ → X0 yields a trace, say Y0′ → P0′ ← X0′ with a morphism to Y0 → M0 ← X0 in

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

33

DH . Since it is a trace, I ′ ↪ X0′ ↪ M0′ factors through Y0′ ↪ M0′ . Pushing Y0′ → P0′ ← X0′
along I ′ → Z ′ , we obtain a trace Y ′ → P ′ ← X ′ (we may choose X ′ as initial position because
the top square above is a pushout) with a morphism from Y0′ → P0′ ← X0′ in DH , which is
an oplifting, hence cartesian (by Lemma 4.17). Then, by universal property of pushout we
obtain a unique morphism f ∶ P ′ → M making the following cube commute:
I′

Z′
P0′

P′

I

f

Z
M0

M.

By Corollary 3.22, f is 1-injective, which entails that the induced morphism of traces is
in DH .
We now need to show that P ′ → M is cartesian, which by Lemmas 3.20 and 4.7 amounts
to showing that its middle arrow f ∶ P ′ → M is in H. To this end, consider any morphism
̂ → . First of all, because M0 → M is identity
t∶ Z ′′ → C in V0 and morphism (u, v)∶ t → f in C
in dimensions > 1, the morphism v uniquely factors through M0 → M . Furthermore, in
all cases where f0 ∶ P0′ → M0 is identity in dimensions > 1, the Yoneda lemma entails that
C → M0 uniquely factors through P0′ . This yields a diagram
u
l

Z ′′

?
P0′

k

C

f0

M0

g

P′
f

M

v

which commutes except perhaps for the upper part marked ‘?’. But the latter also commutes
by Corollary 4.16 with h = u and h′ = gl. We thus obtain a lifting, which is unique by
1-injectivity of f .
So what happens when is f0 non-identity in dimensions > 1? By inspection of the proof
of Lemma 4.9, except for the easy case where P0′ ≅ X0′ , this is when M0 = τn,i,m,j,k for some
n, m, i, j, k, and P0′ has one of the shapes ιn,i + J, om,j,k + J, or ιn,i + om,j,k + J, for some
interface J. In the first two cases, C ≠ τn,i,m,j,k because there can be no u∶ [n] i ∣ j [m] → P ′
(one agent is missing in P ′ ), so the previous argument applies. In the third case, letting x
and y respectively denote the n- and m-ary initial agents in P0′ and a = x ⋅ si and a′ = y ⋅ sj
the corresponding channels, one easily shows that g(a) ≠ g(a′ ), so again there can be no
u∶ [n] i ∣ j [m] → P ′ . Thus, C ≠ τn,i,m,j,k and the previous argument again applies.

34

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

4.6. Restriction of traces. So far, we have shown that seeds and actions admit cartesian
liftings in DH . We now show that it is also the case for arbitrary traces. We proceed by
induction on the length of the considered trace, which requires a few preliminary results.
Lemma 4.19. In sets, for any commuting diagram
I

A

C

J

B

D

whose exterior rectangle is a pullback, with the marked pushout and monos, the right-hand
square is also a pullback.
Proof. We check the universal property of pullback for A, relative to 1, which is enough in
sets. So consider any commuting square
1

c

C

b

B

D.

First, we observe that there is at most one mediating arrow 1 → A, because A → B is mono.
If b has an antecedent in A, say a, then because C → D is mono, a makes both required
triangles commute and we are done.
Otherwise, by surjectivity of A + J → B, b admits an antecedent in J, i.e., there exists
j

j∶ 1 → B such that b is 1 Ð
→ J → B, then we have a cone to C → D ← J, so we apply the
universal property of pullback to obtain i as in
1
c

i

I

A

C

J

B

D

j
b

i

making everything commute and so 1 Ð
→ I → A suits our needs.
Corollary 4.20. In any presheaf category, in any commuting cube
I

B
A

I′

C
B′

A′

f

C ′,

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

35

with the marked pushouts, pullback, and mono, the front square is also a pullback.
Proof. It suffices to show the result in sets, as all involved properties are pointwise in presheaf
categories. First, as monos are stable under pullback and pushout, I → B, A → C, and
A′ → C ′ are also monos. Furthermore, pushouts along monos are also pullbacks, so the top
and bottom faces are also pullbacks. By the pullback lemma, the rectangle
I

I′

A′

B

B′

C′

is a pullback. The previous lemma thus entails the result.
Lemma 4.21. For any commuting diagram as the solid part of
V′

T
t

U′

h

k

C

f

V

U

with t ∈ V0 , h ∈ H, and f 1-injective, there is a unique lifting k as shown.
Proof. Because h ∈ H, there is a unique map from k ′ ∶ C → V ′ making both triangles commute.
By composing k ′ with V ′ → U ′ , we obtain a lifting k for the desired square. Uniqueness
follows from 1-injectivity of f .
Lemma 4.22. The codomain functor cod∶ DH → Dh is a subfibration of cod∶ D1H → D1h .
s

t

Proof. First of all, it is sufficient to prove that given any trace Y Ð
→ U ←
Ð X and h ∈
Dh (X ′ , X), any cartesian lifting in D1 lies in D, i.e., the obtained vertical morphism is again
a trace and the double cell to U lies in D (i.e., all its components are 1-injective). Indeed,
mediating morphisms computed in D1 are automatically in D by cancellation.
We proceed by induction on U . If U is an equivalence, then the result is obviously true.
Otherwise, U = M ● V for some action M and trace V . Let us call Z the final position of M .
By Lemma 4.18, M admits a lifting P ′ along h, with a final position Z ′ , and Z ′ → Z and
fM ∶ P ′ → M are 1-injective. By induction hypothesis, V admits a lifting V ′ along Z ′ → Z
with a double cell to V in DH . Therefore, considering the composite P ′ ● V ′ , we have a
commuting diagram as in Figure 4.6, where f is obtained by universal property of pushout.
Because pushouts along monos are also pullbacks in presheaf categories, both marked
pushouts are also pullbacks. Furthermore, by Lemma 3.20, Z ′ = P ′ ×M Z and Y ′ = (V ′ ×V Y ),
as shown. Also, by Corollary 4.20, V ′ = (P ′ ● V ′ ) ×M ●V V , as shown. Furthermore, by
Proposition 3.18, f is 1-injective.
By Lemmas 4.7 and 3.20, it suffices to show that f is in H, i.e., that it is right-orthogonal
t
to any T Ð
→ C in V0 . Consider any commuting square
T

u

f

t

C

P′ ● V ′

v

M ● V.

Since M ●V is the coproduct of M and V in dimensions greater than 1 and C is a representable
of dimension greater than 1, we have that v factors either through t2 or s2 .

36

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Y′

Y
V′
s′2

V

M ●V
Z

t′2

t2
s0

fM

P′

s2

t1

f

P′ ● V ′
Z′

s1

fV

M
t0

X′

X,
Figure 5: Diagram for induction step in Lemma 4.22

If v factors through s2 , then by universal property of pullback we find a map u′ ∶ T → V ′
making
u

T

u′

P′ ● V ′

V′

t

C

V

M ●V

s2

v

commute. Then, by Lemma 4.21, we find a unique lifting as desired.
If v factors as t2 v ′ , then by Lemma 4.21, it is sufficient to show that there is a map
u′ ∶ T → P ′ making
u

T

u′

t′2

P′

P′ ● V ′
f

t

C

M

v′

M ●V

t2

v
x

commute. To that end, it is sufficient to show that for every [n] Ð
→ T , there is a map
fx

[n] Ð→ P ′ such that
[n]

x

T

P

(4.4)

u

fx
′

P ●V
′

t′2

commutes. Indeed, if that is the case, then the square

′

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

∑(n,x)∈Agents(T ) [n]
[fx ](n,x)∈Agents(T )

P

(EXPANDED VERSION)

[x](n,x)∈Agents(T )

37

T

u′

u

P ●V′

′

′

t′2

also commutes, and since its bottom map is mono and its top map is epi by Lemma 4.15,
there is a unique lifting u′ ∶ T → P ′ making both triangles commute. The square
T

u′

P′

t

C

v′

M

also commutes because it commutes when composed with t2 , which is mono.
fx

x

So we now need to show that for every [n] Ð
→ T , there is a map [n] Ð→ P ′ making
[t′2 ,s′2 ]

the square (4.4) commute. Because P ′ + V ′ ÐÐÐ→ P ′ ● V ′ is epi and [n] is a representable
ux
presheaf, [n] Ð→ P ′ ● V ′ factors through either t′2 or s′2 .
If it factors through s′2 , say as s′2 x′ , then we have
t2 (v ′ tx) = vtx = f ux = f s′2 x′ = s2 fV x′ ,
so by universal property of the pullback Z there exists a unique x′′ ∶ [n] → Z such that
s0 x′′ = v ′ tx and t1 x′′ = fV x′ . We thus obtain a commuting diagram
[n]

x′′

Z
s0

x

T

t

C

v′

M,

which is impossible because v ′ tx, as one of the agents performing action C in M , cannot
remain in the final position of M .
Thus, ux factors through t′2 and we are done.
5. A playground for π
In the previous section, we have proved the main playground axiom, asserting that the
codomain functor DH → Dh of the double category of traces constructed in Section 3 is a
fibration. We now prove the remaining axioms. In Section 5.1, we equip D with playground
structure and prove that it satisfies all the needed axioms, except both decomposition axioms
((P6) and (P7)) which require a bit more work. In Section 5.2, we establish a correctness
̂ is a trace. We then use this criterion in
criterion detecting when a given cospan in C
Section 5.3 to prove both remaining axioms.

38

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

5.1. A candidate playground. So we start in this section by defining the needed additional
structure on D.
Definition 5.1. We recall from Lemma 4.9 that I, the set of individuals, consists of
representable positions [n]. Let B, the full subcategory of basic actions, span all seeds of
shape τn , πnr , πnl , νn , ♡n , ιn,i , or om,j,k . Full actions (notation F) are all actions obtained
from seeds of shape τn , πn , νn , ♡n , ιn,i , om,j,k , or τn,i,m,j,k . Closed-world actions are all
actions obtained from seeds of shape τn , πn , νn , ♡n , or τn,i,m,j,k . Let W denote the graph
with positions as vertices and closed-world actions between them as edges (the initial position
being the target). Finally, all decompositions of any trace U into actions have the same
length which we denote by ∣U ∣.
Here is a summary of which actions
τn πnl πnr
Basic ✓ ✓ ✓
Full ✓
Closed-world ✓

are basic, full and closed-world:
πn ιn,i om,j,k τn,i,m,j,k νn
✓
✓
✓
✓ ✓
✓
✓
✓
✓
✓
✓

♡n
✓
✓
✓ .

Remark 5.2. The definition matches the explanations following Definition 2.30. Basic
actions are as small as possible, which here means they start from one agent and only retain
one agent in the final position. Full actions are those that retain all possible agents in the
final position. So the only kind of actions which are not basic are πn and τn,i,m,j,k . They
each have one sub-action for each agent in their final positions, namely πnr and πnl for πn ,
and ιn,i and om,j,k for τn,i,m,j,k . All of these sub-actions are basic, but only ιn,i and om,j,k
are full. Finally, a new class of actions appear here, that of closed-world actions. Intuitively,
it consists of those actions that do not involve any interaction with the environment. Or,
in other words, those that cannot be extended, even by adding new agents. E.g., ιn,i may
be completed to τn,i,m,j,k by adding an agent, hence is not closed-world. But τn,i,m,j,k is.
Closed-world actions will be at the basis of our semantic notion of testing equivalence
(Definition 6.24).
Lemma 5.3.
● (P1) I, viewed as a subcategory of Dh , is discrete. Basic actions have no non-trivial automorphisms in DH . Vertical identities on individuals have no non-trivial endomorphisms.
● (P2) (Individuality) Basic actions have individuals as both domain and codomain.
● (P3) (Atomicity) For any cell α∶ U → U ′ , if ∣U ′ ∣ = 0 then also ∣U ∣ = 0. Up to a special
isomorphism in DH , all traces of length n > 0 admit decompositions into n actions. For
any U ∶ X
Y of length 0, there is an isomorphism id ●X → U in DH as in
X
X

X
αU
Ū

U

Y.

● (P4) Restrictions of actions (resp. full actions) to individuals either are actions (resp. full
actions), or have length 0.
Proof. (P1) and (P2) are direct by Yoneda. (P4) is also easy in view of Lemma 4.22 and
its proof. For (P3), any vertical X → U ← Y of length 0, being a trace, is isomorphic to an
≅
≅
identity cospan, say Z → Z ← Z. To construct αU , just take the composite id ●X Ð
→ id ●Z Ð
→ U.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

39

Let us now treat the axiom for views, which is really easy. It actually becomes stronger
because of Remark 2.28, though this does not affect the rest of the construction:
Definition 5.4. Let B0 be the full subcategory of DH having as objects basic actions and
vertical identities between individuals.
Lemma 5.5. (P5) For any action M ∶ Y
unique cell

X and y∶ d → Y in Dh with d ∈ I, there exists a
y

d
v y,M

αy,M

y,M

d

yM

Y
M

X,

with v y,M ∈ B0 .
Proof. The result holds for seeds, by case analysis. E.g., v ls,πn = πnl , v rs,πn = πnr , and so on.
Now, any action M comes with a cell from its generating seed, say β∶ M0 → M . If y is in the
image of M0 , then the required cell αy,M is β ○ αy,M0 . Otherwise, v y,M = id ●d admits a cell
to M , which suits our needs. Uniqueness follows by (P1).
Remark 5.6. The important result that Axiom (P5) entails [39, Proposition 4.24] says that
when we replace M with any trace u, we get a double cell αy,u which is only unique up to
isomorphism. Below, we still define views up to isomorphism, so our modified Axiom (P5)
does not make this any stronger.
We conclude this section with the (straightforward) verification of (P8) and (P9).
Lemma 5.7. (P8) For any X, I/X is finite.
Proof. All positions are finitely presentable presheaves.
Lemma 5.8. (P9) For all d ∈ I and actions M ∶ X
d, M ′ ∶ X ′
d, and b∶ d′
′
′
and M full and b basic, if there exist cells M ← b → M then M ≅ M ′ .

d with M

Proof. By case analysis. E.g., if b = πnl , then M ≅ πn ≅ M ′ .
Remark 5.9. While the verification of (P9) is straightforward in our case, this axiom does
impose strong constraints on playgrounds. Morally, it demands that the basic subactions of
a given full action should be disjoint from those of a different full action. To see why this is
restrictive, let, for all j ∈ n, ιn,i,j denote the quotient of ιn,i by the equation s ○ sn+1 = s ○ sj .
The equation says that the received channel was already known as channel number j. Further
let [n]/{i = j} denote [n] quotiented by si = sj . We could be tempted to decree that the
cospan
t
s
[n + 1]/{n + 1 = j} Ð
→ ιn,i,j ←
Ð [n]
is an action. An example consequence would be that, e.g., the synchronisation on [n] i,l ∣ j,k [m]
where [m] sends k on j, when restricted to the receiver, would give ιn,i,l instead of ιn,i .
But then ιn,i and ιn,i,l would be two non-isomorphic full actions sharing a common basic
subaction, ιn,i .
We now have proved all playground axioms for D, except right and left decomposition.
These require the development of more machinery, which we undertake in the next section.

40

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

5.2. Correctness criterion. In order to prove the remaining playground axioms for D,
we set up a combinatorial characterisation of traces among cospans. Before delving into
technicalities, let us briefly map out our correctness criterion. Given a trace Y ↪ U ↩ X,
we start by forgetting the cospan structure and exploring the properties of U alone.
The main idea is to construct a binary relation over the elements of U , modeling causality.
So, e.g., if an agent x ∈ U [n] forks into x1 and x2 , then we will have causal relations
x1

x2
r
x,

where r denotes the corresponding element in U (πn ). In order for U to admit a sequential
decomposition into actions, the main criterion is that the causality relation should be acyclic.
In addition to this, a few sanity checks are necessary. First of all, because actions
are merely seeds pushed along 1-injective maps from their interfaces, the neighbourhood
of each action x ∈ U (µ) should not be too degenerate. For instance, the corresponding
map ⌜x⌝∶ µ → U should be 1-injective. Moreover, for inputs and channel creations, the new
channel should really be new. This property, which is a bit tedious to define properly, is
called local 1-injectivity.
Furthermore, when we add a new action to some trace, it is played by an agent in
the final position. This entails that no two actions in U may be performed by the same
agent. We call this target-linearity below. Symmetrically, no two actions may share their
‘created’ agents, which we call source-linearity. Linearity is then the conjunction of sourceand target-linearity.
̃ f has an acyclic causal
These conditions are sufficient, in the sense that if any U ∈ C
relation, and is furthermore locally 1-injective and linear, then it is the middle object of a
trace. But in fact, it is then easy to determine the corresponding initial and final positions.
s
t
We design notions of initial and final morphisms, so that Y Ð
→U ←
Ð X is a trace iff U
satisfies the above conditions, t is initial, and s is final.
Let us first define the causal relation. A first step is to restrict attention to the cores of
U , in the following sense, which are intuitively the main elements. E.g., for a forking action
x ∈ U (πn ), keeping track of x is enough, and handling x ⋅ l and x ⋅ r tends to get in the way.
Technically, an input or output is a core iff it is not part of a synchronisation; and a left or
right fork action is a core iff it is not part of a full fork action. Here is a concise definition:
̂ is an element of dimension > 1 which is not
Definition 5.10. A core of a presheaf U ∈ C
the image of any element of higher dimension.
Our definition of the causal relation will rely on the preliminary notions of sources and
targets of a core, and that of channels created by a core. These notions will fix the direction
of the causal relation.
Definition 5.11. For any U and core µ ∈ U (c),
● the sources of µ are the agents x such that x = µ ⋅ f ⋅ s for some f ;
● the targets of µ are the agents y such that y = µ ⋅ f ⋅ t for some f ;
● a channel a ∈ U (⋆) is created by µ iff µ has the shape νn or ιn,i , and a = µ ⋅ s ⋅ sn+1 .

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

41

Example 5.12. In the representable πn , there is one target, l ○ t (or equivalently r ○ t), and
two sources, s1 = l ○ s and s2 = r ○ s. Another example is τn,i,m,j,k , which has two targets,
 ○ t and ρ ○ t, and two sources. However, ρ ○ s ○ sn+1 is not created by the input element ρ,
because it is not a core.
Definition 5.13. For any U , let its causal graph GU have:
● as vertices, all channels, agents, and cores in U ,
● for all x ∈ U [n] and i ∈ n, an edge x → x ⋅ si ,
● and, for each core µ, an edge from each of its sources and created channels, and one into
each of its targets, as in
source1

source2

created

core
target1

target2 .

Please note that edges a → µ from a channel to an input action exist only if the involved
action is not part of a synchronisation; for otherwise the synchronisation is a core, not the
input.
The obtained graph is actually a binary relation, since there is at most one edge between
any two vertices. It is also a colored graph, in the sense that it comes equipped with a
morphism to the graph L:
∞

1

0,

mapping cores to ∞, agents to 1, and channels to 0. (In particular, there are no edges from
channels to agents or from cores to channels.) For any graph G, equipped with a morphism
l∶ G → L, we call vertices of G channels, agents, or cores, according to their label.
As expected, we have:
Proposition 5.14. For any trace U , GU is acyclic (in the directed sense).
Proof. By induction on any decomposition of U .
Let us now consider local 1-injectivity, linearity, initiality and finality. First, let us
emphasise that for all seeds Y ↪ M ↩ X, M is a representable presheaf, so, e.g., it makes
sense to consider U (M ).
Definition 5.15. A presheaf U is locally 1-injective iff for any seed Y ↪ M ↩ X with
interface I and core µ ∈ U (M ), if two distinct elements of M are identified by the Yoneda
morphism µ∶ M → U , then they are in (the image of) I(⋆).
This is equivalent to requiring that all morphisms yc → U , for all c ∈ C, are 1-injective,
and that for all core inputs and channel creations x of arity n in U , for all i ∈ n, we have
x ⋅ s ⋅ sn+1 ≠ x ⋅ s ⋅ si .
Proposition 5.16. Any trace U is locally 1-injective.

42

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Proof. Choose a decomposition of U into actions; µ corresponds to precisely one such action,
say M ′ , obtained, by definition, from some seed M as a pushout (3.1). By construction
of pushouts in presheaf categories, M ′ is obtained from M by identifying some channels
according to I → Z.
Let us observe that, because local 1-injectivity is only about cores, an input which is
part of a synchronisation may receive an already known channel, even if its n + 1th channel
is not part of its interface — because it is not a core.
After local 1-injectivity, let us consider linearity.
Definition 5.17. Any G ∈ Gph/L is source-linear iff for any cores µ, µ′ , and other vertex
(necessarily an agent or a channel) x, µ ← x → µ′ in G, then µ = µ′ ; G is target-linear iff
for any cores µ, µ′ and agent x, if µ → x ← µ′ in G, then µ = µ′ ; G is linear iff it is both
source-linear and target-linear.
s

t

Proposition 5.18. For any trace Y Ð
→U ←
Ð X, GU is linear.
Proof. Straightforward, by induction on any decomposition of U into actions, observing that
we glue along agents and channels which are initial on one side and final on the other.
The last of our necessary sanity checks is about initiality and finality. The idea here is
that one may read in U alone what both legs of the cospan Y ↪ U ↩ X should be.
Definition 5.19. An agent is initial in U when it is not the source of any action, i.e., for
no action µ ∈ U , x = µ ⋅ s. A channel is initial when it is not created by any core.
An agent x in U is final iff it is not the target of any action, i.e., for no action µ ∈ U ,
x = µ ⋅ t. All channels are final.
Lemma 5.20. An agent is initial in U iff it has no edge to any core in GU .
Lemma 5.21. An agent is final in U iff it has no edge from any core in GU .
Now, here is the expected characterisation:
Theorem 5.22. A monic cospan Y s U t X of finite presheaves is a trace iff
(C1) U is locally 1-injective,
(C2) X contains exactly the initial agents and channels in U ,
(C3) Y contains exactly the final agents and channels in U ,
(C4) and GU is linear and acyclic.
Of course, we have almost proved the ‘only if’ direction, and the rest is easy, so only
the ‘if’ direction remains to prove. The rest of this section is devoted to this. So given a
cospan satisfying the above conditions, we intend to sequentialise it, i.e., decompose it into
actions. We will proceed by induction on the number of cores in U , by picking a core µ which
is maximal according to GU , removing it from U and applying the induction hypothesis
to the rest. However, it may not be obvious how we should remove µ from U . E.g., the
topos-theoretic difference U ∖ µ does not yield the expected result, as it removes all sources
of µ. Instead, we consider the following operation: for any morphism of presheaves f ∶ U → V
and set W , let U − W = ∑c∈C Im(U (c)) ∖ W ⊆ ∑c∈C V (c). This is a slight abuse of notation,
as f is implicit, but it should be easily inferred from context.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

43

Remark 5.23. We observe that U − W is generally just a set, not a presheaf; i.e., its
elements are not necessarily stable under the action of morphisms in C. Consider for
example U = [1] ∣ [1] and let W consist of the first agent and the unique channel. Then
U − W does not contain the unique channel of U , so the action of s1 on the second agent
steps outside U − W .
But there is one useful case where U − W is indeed a subpresheaf of U , as we show below
in Lemma 5.25.
Definition 5.24. For any seed Y ↪ M ↩ X, let the past past(M ) = M − Y of M be the
set of its elements not in the image of Y . For any such M , presheaf U , and core µ ∈ U (M ),
let past(µ) = Im(past(M )) consist of all images of past(M ).
To explain the statement a bit more, by Yoneda, we see µ as a map M → U , so we have
a set-function
past(M ) ↪ ob(el(M )) → ob(el(U ))
(recalling that el denotes the category of elements). We observe that past(µ) is always a set
of agents and actions only, since channels present in X always are in Y too.
Given a core µ ∈ U , the relevant way of removing µ from U will be:
U ) µ = ⋃{V ↪ U ∣ ob(el(V )) ∩ past(µ) = ∅}.

U ) µ is thus the largest subpresheaf of U not containing any element of the past of µ. The
good property of this operation is:
Lemma 5.25. If µ is a maximal core in GU (i.e., there is no path to any further core) and
GU is target-linear, then (U ) µ)(c) = U (c) ∖ past(µ) for all c.

Proof. The direction (U ) µ)(c) ⊆ U (c) ∖ past(µ) is by definition of ). Conversely, it is
enough to show that c ↦ U (c) ∖ past(µ) forms a subpresheaf of U , i.e., that for any f ∶ c → c′
in C, and x ∈ U (c′ )∖past(µ), x⋅f ∉ past(µ). Assume on the contrary that x′ = x⋅f ∈ past(µ).
Then, of course f cannot be the identity, and w.l.o.g. we may assume that x′ is an agent
and x is a core. But then, because x′ ∈ past(µ), there is an edge µ → x′ in GU , and because
x′ = x ⋅ f , there is an edge x → x′ or x′ → x in GU . The former case is impossible by
target-linearity, and the latter case would imply the existence of a path µ → x in GU , which
contradicts the maximality of µ. So x′ ∈ past(µ) is impossible altogether.
Proof of Theorem 5.22. We proceed by induction on the number of actions in U . If it is
zero, then U is a position; by (C2), t is an iso, and by (C3) so is s, hence the cospan is a
trace. For the induction step, we first decompose U into
s2

t2

s1

t1

Y Ð→ U ′ ←Ð Z Ð→ M ′ ←Ð X,
and then show that M ′ is an action and U ′ satisfies the conditions of the theorem.
First, by acyclicity, pick a maximal core µ in GU , i.e., one with no path to any other
core. Let
I0
Y0

M0

X0

44

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

be the seed with interface corresponding to µ, so we have the Yoneda morphism µ∶ M0 → U .
Let U ′ = (U ) µ), and X1 = X − Agents(X0 ). X1 is a subpresheaf of X, since it contains
all channels. The square
I0

X1

X0

X

is a pushout, since it just adds the missing agents to X1 . Define now Z, M ′ , s1 , and t1 by
the pushouts
Y0

Z
s1

M′

M0
I0

X1
X0

U

t1

X

and the induced arrows. We further obtain arrows to U by universal property of pushout.
Let us show that the arrow f ∶ M ′ → U is mono. First, it is obviously mono in dimensions
> 1. It is also mono in dimension 1, because M ′ [n] = X[n] + Y0 [n] for all n and X → U is
mono with image consisting only of initial agents, which are thus dijoint from the image of
Y0 . Finally, for dimension 0, i.e., at ⋆, the pushout defining M ′ is isomorphic to
I0 (⋆) = X0 (⋆)

X1 (⋆) = X(⋆)

injl

injl

M0 (⋆) = X0 (⋆) + I

M ′ (⋆) = X(⋆) + I

where I = M0 (⋆) ∖ X0 (⋆) is the set of channels created by the action. Consider any
a, b ∈ M ′ (⋆) such that a ≠ b. Because X → U is mono, if a, b ∈ X(⋆) then f (a) ≠ f (b). By
local 1-injectivity of U , if a, b ∈ I then f (a) ≠ f (b). Finally, if a ∈ X(⋆) and b ∈ I, then we
have an edge f (b) → µ in GU , whereas f (a) is initial by (C2), so f (a) ≠ f (b). This shows
that M ′ → U is mono, which also entails that Z → U is a mono, because s1 is a pushout of
the mono Y0 → M0 .
By (C1) and Lemma 5.25, U = M ′ ∪ U ′ , i.e., the square
Z

U′

M′

U

is a pushout, so U is indeed a composite as claimed, with Z ↪ M ′ ↩ X an action by
construction. So, it remains to prove that Y ↪ U ′ ↩ Z satisfies the conditions. First, as
a subpresheaf of U (whose inclusion preserves cores), U ′ is locally 1-injective and has a
linear and acyclic causal graph, so satisfies (C1) and (C4). U ′ furthermore satisfies (C2) by

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

45

(EXPANDED VERSION)

construction of Z and source-linearity of GU , and (C3) because removing past(µ) cannot
make any non-final agent final.
Let us conclude this section with a helpful lemma, whose proof relies on Theorem 5.22:
Lemma 5.26. There is at most one cell filling any diagram
k

Y′

Y
u

u′

X

′
h

X

in D.
In order to prove this, let us introduce:
Definition 5.27. For any action x ∈ U , let core(x), the core associated to x, be the unique
core µ ∈ U for which there exists f in C such that µ ⋅ f = x. If x is an agent or a channel,
then by definition core(x) = x.
s′

t′

s

t

Proof of Lemma 5.26. By definition, we have cospans Y ′ Ð
→ u′ ←
Ð X ′ and Y Ð
→u←
Ð X.
′ ′
′
Suppose we are given l, l ∶ u → u making (k, l, h) and (k, l , h) into cells. By naturality, l
and l′ are determined by their images on channels, agents, and cores. We show by induction
on the ordering induced by Gu′ that they have to agree on these. For the base case: they
have to agree with h on initial agents and channels by definition of cells. For the induction
step, we proceed by case analysis on the kind of element to consider. The image of any
source of or channel created by a core µ is uniquely determined by naturality, which leaves
the case of a core µ, of which we assume that there is an agent x such that µ → x in Gu′
and l(x) = l′ (x). The edge µ → x yields a morphism, say t, in C such that µ ⋅ t = x. But
then by naturality we have l(µ) ⋅ t = l(x) = l′ (x) = l′ (µ) ⋅ t. By linearity of Gu we have
core(l(µ)) = core(l′ (µ)). Now let cµ denote the object of C over which µ lies, and let c′
be the one over which core(l(µ)) lies. By inspection of C, there is exactly one morphism
f ∶ cµ → c′ , and so we have l(µ) = core(l(µ)) ⋅ f = core(l′ (µ)) ⋅ f = l(µ), as desired.
5.3. A playground. In this section, we finally prove:
Theorem 5.28. D forms a playground.
Most axioms have been proved in previous sections, and we are left with both decomposition axioms, which are proved in Lemmas 5.29 and 5.30 below, relying on the correctness
criterion of the previous section.
Lemma 5.29. (P7) Any double cell as in the center below, where B is a basic action and
M is an action, decomposes in exactly one of the forms on the left and right:
A

X
α1

C

U

Y
α2

D

h

A
C
D

A

Y

C
M

k

X
α1

V

B

Z

X

α

Z

Y
α2

D

Z.

46

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

A

h

X

U1

f1

W1

C

fm

Y
f

U
U2

f2

B

k

W
M

Z,

Figure 6: Proof of Lemma 5.30
̂ let its neighbourhood consist of
Proof. For any element a over c ∈ C of any presheaf F ∈ C,
all elements in the image of a∶ c → F .
Let b ∈ B and m ∈ M be the unique cores of B and M , respectively. Let Vm be the
neighbourhood of m in M ● V .
If α(b) ∈ Vm , let us show that the whole of U is mapped to V , and we are in the left-hand
case. It is clear for channels. If there exists an element x of U of dimension ≥ 1 mapped to y
in M − V , i.e., M − Y , then we obtain a path x → x′ to an agent x′ of C, in GB●U . Via α,
this yields a path M − Y → Y in GM ●V between elements of dimension ≥ 1, a contradiction.
If now α(b) ∉ Vm , we show similarly that the whole of B ● U is mapped to V , because
the contrary would imply the existence of a path M − Y → V − Y in GM ●V , which also is a
contradiction. Hence, we are in the right-hand case.
Lemma 5.30. (P6) Any double cell
h

A

X

α

U

f

C

k

Y

α2

W2

B

W1

U1

decomposes as

Y

X

α1

α3

W1

U

h

A

W2

U2

Z
B

k

Z

with α3 an isomorphism, in an essentially unique way.
Proof. Let α = (h, f, k). We first treat the case where W2 is an action M , recalling Definition 5.27. We construct U1 and U2 , as depicted in Figure 6. First, let U1 = U ×W W1 , where
W = W2 ● W1 , and let A → U1 denote the induced arrow. By construction, all of A → U1 → U
are monos and, by Lemma 3.20 and the pullback lemma, A = U1 ×W1 X.
Let us show that the projection f1 ∶ U1 → W1 preserves initiality of channels and agents.
We proceed by contrapositive: consider any channel or agent x ∈ U1 . If x′ = f1 (x) is not

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

47

initial in W1 , then we have an edge x′ → µ′ for some core µ′ of W1 . But, since f is a
morphism between traces, it preserves initiality, so x cannot be initial in U , hence we find
x → µ in GU . By source linearity of GW , core(f (µ)) = µ′ , so the action f (µ) ∈ W has
antecedents both in U and W1 . By universal property of pullback, there exists an action
y ∈ U1 , respectively mapped to µ and f (µ), which by naturality and injectivity of U1 → U
entails that x → y in GU1 . Therefore, x is not initial in GU1 , as required.
Let now C ↪ U1 denote the subpresheaf of U1 consisting of initial channels and agents
(a subpresheaf because if x is an initial, n-ary agent, then x ⋅ si is an initial channel for
any i ∈ n, by Theorem 5.22 and Lemma 5.21). Since f1 preserves initiality, C → U1 → W1
factors through Y → W1 , uniquely since the latter is mono, say as fm (see Figure 6). By
Theorem 5.22, A → U1 ← C is a trace and (h, f1 , fm ) defines a morphism to X → W1 ← Y .
Let then U2 ↪ U denote the subpresheaf of U consisting of elements below C in GU , i.e.,
x ∈ U2 ⇔ ∃c ∈ C.c →⋆ GU core(x).
A first observation is that all initial channels and agents of U are in U2 , so that B → U
factors through U2 . Indeed, consider any such initial x. By acyclicity of GU , each initial
element is reachable from some final element, so x is reachable from some final y. But by
source-linearity the corresponding path y →⋆ x goes through C, so we find a path c →⋆ x for
some c ∈ C, as desired.
Now, because U2 → U and M → W are monos, showing that f maps all elements x of
U2 to M will imply that U2 → U → W uniquely factors through M → W . Let us do this by
case analysis:
● If x is not a channel, then f preserves paths from agents to x, so we find some path
f (c) →⋆ GW core(f (x)) with c ∈ C hence f (c) ∈ Y , which implies that f (x) ∈ M (f (x) ∈
W1 − M would contradict initiality of Y in W1 ).
● If x is some channel initial in U , then since f preserves initiality x is mapped to Z hence
to M .
● If finally x is some non-initial channel, then x → µ for some core µ ∈ U . Now µ ∈ U2 , as
witnessed by the path c →⋆ x → µ. But then x = µ ⋅ u for some morphism u of C, so since
by the above f (µ) ∈ M , we have that f (x) = f (µ) ⋅ u is in M too, as desired.
We thus get a diagram as in Figure 6, which commutes because M → W is mono.
By Theorem 5.22, C → U2 ← B is a trace, and U = U2 ● U1 , which shows existence of the
desired decomposition.
For any decomposition as in Figure 6, we have C = U2 ×M Y by Lemma 3.20, so by
Corollary 4.20, we also have U1 = U ×W W1 . Thus, U1 is uniquely determined up to canonical
isomorphism. But by Theorem 5.22, C → U1 is so too, as the subobject of initial agents and
channels. But then U2 precisely consists of elements below C. Indeed, by finiteness of GU2
and (C3) in Theorem 5.22, all of U2 clearly lies below C. Conversely, for any x ∈ U1 − U2 , by
finiteness of GU1 and (C3) in Theorem 5.22, we have a path x →+ c to some c ∈ C, so x cannot
lie below C by (C4). Our decomposition is thus unique up to canonical isomorphism.

6. A sheaf model
In the previous sections, we have constructed a double category D and equipped it with
playground structure. We now instantiate constructions from [39] on D, which lead to the
definition of our sheaf model for π. We first recall various notions of strategy in Section 6.1:

48

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

naive strategies, innocent strategies, and behaviours. Behaviours are further studied in
Section 6.2, where we introduce a kind of calculus for them. Using this calculus, we then
define our intepretation of π in Section 6.3. Finally, in Section 6.4, we state our semantic
definition of fair testing equivalence and our main result.
6.1. Strategies and behaviours. We first recall notions of strategies. As announced in
the introduction, we define a category T(X) combining prefix ordering and isomorphism
of traces: T(X) has traces u∶ Y
X as objects, and as morphisms u → u′ all pairs (w, α)
′
with w∶ Y
Y and α an isomorphism u ● w → u′ in the hom-category Dv (Y ′ , X), as in
Y′

w
≅
α

Y
u

u′

X,

considered up to the smallest equivalence relation identifying (w, α) and (w′ , α ○ (u ● γ)),
for any w′ ∶ Y ′
Y and special γ∶ w′ → w). Thus, u′ is an extension of u by w.
̃
Definition 6.1. Let the category of (naive) strategies on X be T(X).
Strategies do not yield a satisfactory model for π:
Example 6.2. Consider the position X with three agents x, y, z sharing a channel a, and
the following traces on it: in ux,y , x sends a on a, and y receives it; in ux,z , x sends a on a,
and z receives it; in iz , z inputs on a. One may define a strategy S mapping ux,y and iz to a
singleton, and ux,z to ∅. Because ux,y is accepted, x accepts to send a on a; and because iz
is accepted, z accepts to input on a. The problem is that S rejecting ux,z roughly amounts
to x refusing to synchronise with z, or conversely.
We want to rule out this kind of strategy from our model, by adapting the idea of
innocence. We start by extending T(X) with objects representing traces on subpositions of
X. For this, we consider the following category TX . It has as objects pairs (u, h) of a trace
u∶ Z
Y and a morphism h∶ Y → X in Dh . A morphism (u, h) → (u′ , h′ ) consists of a trace
w∶ T
Z and a cell as below left with h′ r = h. Morphisms are considered up to the smallest
equivalence relation identifying (w, α) with (w′ , α ○ (u ● γ)), for any w′ and γ as below right.
s

T

Z′

T′

w
α

Z

u′

u

w′

γ

s

T

Z′

w
α

Z

u′

u
r

Y
h

X

Y′
h′

r

Y
h

X

Y′
h′

Example 6.3. Recalling the right-hand trace of Figure 4 (page 22), say u∶ Y
X, y’s first
action is an input on its unique channel b. This yields a trace ι1,1 ∶ [2]
[1]. Here is an
examlpe morphism (ι1,1 , y) → (u, id X ) in TX :

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

y ′′

[3]

(EXPANDED VERSION)

49

Y

ι2,2

[2]

u

ι1,1

y

[1]

X.

y

X.
We think of it as an occurrence of the trace ι1,1 in u. Thus, morphisms in TX account both
for prefix inclusion and for ‘spatial’ inclusion, i.e., inclusion of a trace into some other trace
on a larger position.
We now define views within TX :
Definition 6.4. A view is a trace isomorphic to some (possibly empty) composite of basic
actions (Definition 5.1). Let VX denote the full subcategory of TX spanning pairs (u, h)
where u is a view.
Intuitively, basic actions follow exactly one agent through an action. An object of VX
consists of a view, say v∶ [n′ ]
[n], plus a morphism h∶ [n] → X in Dh , which by Yoneda is
just an agent of X. So an object of VX is just an agent of X and a view from it.
Definition 6.5. The inclusion jX ∶ VX ↪ TX induces a Grothendieck topology, for which
(wi ,αi )

a sieve ((ui , hi ) ÐÐÐÐ→ (u, h))i∈I of morphisms to some trace u is covering iff it contains
all morphisms from views into u. Let the category SX ↪ T̃
X of innocent strategies be the
category of sheaves of finite sets for this topology. Let the category BX of behaviours over
̃
X be V
X.
As announced in the introduction, letting ranjop denote right Kan extension [53] along
X
op
op
the inclusion jop
X ∶ VX ↪ TX , we have:
Proposition 6.6. The embedding ranjop induces an equivalence of categories BX ≃ SX .
X

Proof. See [39, Lemma 4.34].
We thus obtain the innocent strategy SB associated to a behaviour B ∈ BX by taking
its right Kan extension as in
jop
X

Vop
X

Top
X

kop
X

T(X)op

SB
B

set.

U(SB )

Explicitly, using standard results, we obtain the end
SB (u, h) = ∫

B(v, x)TX ((v,x),(u,h)) ,
(v,x)∈VX

which is a kind of generalised product. In the boolean setting (functors to 2), this end
reduces to the conjunction ⋀{(v,x)∈VX ∣∃α∶(v,x)→(u,h)} B(v, x), demanding precisely that all
views of u are accepted by B. In the general case, the intuition is that a way of accepting u
for SB is a compatible family of ways of accepting the views of u for B. The forgetful functor
U to naive strategies is then given by restricting along the opposite of kX ∶ T(X) ↪ TX as
above. Some local information may be forgotten by U, which is hence neither injective on
objects, nor full, nor faithful. E.g., if two behaviours differ on one agent, but are both empty
on the views of another, then both are mapped to the empty naive strategy.

50

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Example 6.7. Recalling X and S from Example 6.2, let us show that for any B ∈ BX , the
̃ cannot be S. Indeed, if U(SB ) was S, then because S
associated strategy U(SB ) ∈ T(X)
accepts ux,y and iz , B has to accept the following views: (1) iz , (2) ox , in which x sends
a on a (without any matching input), (3) iy , in which y inputs on a, and (4) all identity
views on x, y, and z. But then U(SB ) has to accept both ux,y and ux,z , because B accepts
all views mapping into them.
6.2. Decomposing behaviours. In this section, we study behaviours a bit more in depth,
which yields the calculus announced at the beginning of Section 6. The starting point is that
the assignment X ↦ BX may be equipped with useful structure, describing how a behaviour
B on some given position restricts to any subposition, and also what remains of it after
a given action has been played. Otherwise said, morphisms of D act contravariantly on
behaviours:
● horizontal morphisms h∶ X → X ′ induce functors Bh ∶ BX ′ → BX , and
● vertical morphisms u∶ Y
X induce functors Bu ∶ BX → BY .
Furthermore, any cell as below left induces a natural isomorphism as below right:
k

Y
u

X

α

Y′

Bu

u′
h

X

Bk

BY

′

BX

BY ′
Bu′

≅
Bh

BX ′ ,

which notably says that B ⋅ u′ ⋅ k ≅ B ⋅ h ⋅ u for any behaviour B ∈ BX ′ . This is worked out in
detail and in full generality in [39], and extended to a pseudo double functor Dop → QCat,
where QCat denotes Ehresmann’s double category of quintets over Cat. But let us explain
how both actions look like in the present, concrete case.
The first, horizontal action is really easy: any horizontal morphism k∶ X ′ → X acts on
a given behaviour B ∈ BX by returning the behaviour B ⋅ k such that for all (v, h) ∈ VX ′ ,
(B ⋅ k)(v, h) = B(v, k ○ h).
Proposition 6.8. The functor BX → ∏n,x∶[n]→X B[n] given at (n, x) by horizontal action
of x, i.e., B ↦ B ⋅ x, is an isomorphism.
Proof. We have VX ≅ ∑n,x∶[n]→X V[n] .
Notation 6.9. If (Bx )x∶[n]→X is a family of behaviours indexed by the agents of X, we
accordingly denote its unique antecedent by [Bx ]x∶[n]→X .
Vertical action is a bit harder. Let us start by recalling the following result from [39],
which generalises Lemma 5.5:
Lemma 6.10. For any trace P ∶ Y
essentially unique cell

X and y∶ d → Y in Dh with d ∈ I, there exists an
d
v y,P

y
αy,P

y,P

d

yP

Y
P

X,

with v y,P a view.
Proof. By induction on P using Lemma 5.5. See [39] for the precise meaning of essential
uniqueness in this case.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

51

This result allows us to describe what remains of a behaviour after a trace:
Definition 6.11. Given any behaviour B ∈ BX and trace P ∶ Y
B along P is the behaviour determined (up to isomorphism) by

X, the residual B ⋅ P of

(B ⋅ P ⋅ y)(w, id [ny ] ) = B(v y,P ● w, y P )
for all agents y∶ [ny ] → Y .
So we may consider residuals of behaviours along arbitrary traces. Conversely, any
behaviour is determined by its initial states and residuals. Let us first consider the following
special kind of behaviour:
Definition 6.12. A behaviour B on [n] is definite iff B(id ● , id [n] ) ≅ 1. A behaviour B on
an arbitrary position X is definite iff for all agents x of X, B ⋅ x is definite. Let DX denote
the full subcategory of BX spanning definite behaviours.
This means that B has exactly one initial state.
Definition 6.13. For any n ∈ N and family Bb ∈ B[nb ] indexed by all basic actions b∶ [nb ]
[n], let ⟨Bb ⟩b denote the definite behaviour B determined by B ⋅ b = Bb for all b.
By construction, we have:
Proposition 6.14. For any definite behaviour D ∈ B[n] , D ≅ ⟨D ⋅ b⟩b .
This extends to arbitrary behaviours on individuals using the fact that any behaviour
on an individual is a coproduct of definite behaviours.
Notation 6.15. For any behaviour B = ∑k∈γ Dk on any [n], let ∣B∣ = γ and, for any k ∈ γ,
let the restriction B∣k of B to k be Dk .
Remark 6.16. In other words, k ∈ γ is just an element of B(id ●[n] , id [n] ) and B∣σ is
determined by
B∣σ (v, id [n] ) = {σ ′ ∈ B(v, id [n] ) ∣ σ ′ ⋅ !v = σ},
where !v denotes the unique morphism (id ●[n] , id [n] ) → (v, id [n] ) in V[n] .
We obtain:
Proposition 6.17. For any behaviour B ∈ B[n] ,
B ≅ ∑ ⟨(B∣k ) ⋅ b⟩b .
k∈∣B∣

Putting this together with spatial decomposition, we obtain:
Corollary 6.18. For any behaviour B ∈ BX ,
B ≅ [ ∑ ⟨((B ⋅ x)∣k ) ⋅ b⟩b∶[nb ]

[nx ] ]x∶[nx ]→X .

k∈∣B⋅x∣

The fact that both actions of D yield a pseudo double functor Dop → QCat essentially
boils down to:
Lemma 6.19. For any B ∈ BX and cell
Y′

α

u′

X

k

′
h

Y
u

X,

52

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

we have D ⋅ h ⋅ u′ ≅ D ⋅ u ⋅ k.
The result is stated (and proved) in full generality as [39, Proposition 4.31].
6.3. Interpretation of π. We now define our interpretation of π-calculus configurations.
We start with processes and then cover configurations. Because the notation for behaviours
introduced in the previous section only covers behaviours on representable positions, while
π-calculus syntax is name-based, we bridge the gap by keeping track, along the recursive
definition, of a bijection between the set γ of free channels of the considered process and its
cardinal ∣γ∣. So we define a family of maps in
∏

Pi ×Bij(γ,∣γ∣)

γ
D[∣γ∣]

,

γ∈Pf (N)

where Bij(A, B) denotes the set of all bijections A −∼ B. For any such γ, P , and h in
the domain, we denote the result by ⟦P ⟧h , or ⟦P ⟧γ,h when needed. Letting n = ∣γ∣, it is
coinductively defined by
⟦∑i Pi ⟧h = ⊞i ⟦Pi ⟧h
π l ↦ ⟦P ⟧h
⟦P ∣ Q⟧h = ⟨ nr
⟩
πn ↦ ⟦Q⟧h
⟦νb.P ⟧h = ⟨ νn ↦ ⟦P ⟧h′ ⟩
⟦♡.P ⟧h = ⟨ ♡n ↦ ⟦P ⟧h ⟩
⟦τ.P ⟧h = ⟨ τn ↦ ⟦P ⟧h ⟩
⟦a(b).P ⟧h = ⟨ ιn,h(a) ↦ ⟦P ⟧h′ ⟩
⟦ā⟨b⟩.P ⟧h = ⟨ on,h(a),h(b) ↦ ⟦P ⟧h ⟩
where
● in any list ⟨b1 ↦ B1 , . . . , bm ↦ Bm ⟩, all unmentioned basic actions are meant to be mapped
to the empty behaviour;
● the definite sum ⊞i Di of definite behaviours Di is the definite behaviour determined by
(⊞i Di ) ⋅ b = ∑i (Di ⋅ b), for all basic actions b∶ [n′ ]
[n];
● and h′ ∶ γ, b −∼ n + 1 maps any a ∈ γ to h(a), and b to n + 1.
Example 6.20. Let us briefly illustrate the translation. Consider any h∶ γ → ∣γ∣ and
processes γ, b ⊢ P , γ, b ⊢ Q, and γ ⊢ R, with a ∈ γ. We can form a(b).P + a(b).Q + ā⟨a⟩.R,
which is mapped to
⟨ι∣γ∣,h(a) ↦ (⟦P ⟧h′ + ⟦Q⟧h′ ), oγ,h(a),h(a) ↦ ⟦R⟧h ⟩.
To emphasise the difference, using coproduct of behaviours instead of definite sum in the
translation would yield a behaviour with three distinct initial states, closer to the internal
choice a(b).P ⊕ a(b).Q ⊕ ā⟨a⟩.R than to the original process.
Generalising this to configurations should really be intuitive: we map any ⟨γ∥P1 , . . . , Pn ⟩
to some behaviour on the position X with X(⋆) = γ and n agents of arity ∣γ∣, given for
each agent i ∈ n by ⟦Pi ⟧. In order to fully define such a position, we need to specify maps
fi ∶ ∣γ∣ → γ. We use for all of them the inverse of the canonical bijection hγ defined by:
Definition 6.21. Let hγ ∶ γ −∼ ∣γ∣ map each a ∈ γ to its position in the ordering induced by
the one on natural numbers.
We call the obtained position X(γ, n).

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

53

Definition 6.22. Let ⟦−⟧∶ ob(Conf) → ∑X BX map any configuration C = ⟨γ∥P1 , . . . , Pn ⟩
to the pair (X(γ, n), ⟦C⟧), where ⟦C⟧ is defined through Proposition 6.8 by
⟦C⟧(∣γ∣)(i) = ⟦Pi ⟧hγ ,
for all i ∈ n. We implicitly consider processes P over γ as configurations ⟨γ∥P ⟩, and hence
allow ourselves to write ⟦P ⟧ for ⟦⟨γ∥P ⟩⟧.
6.4. Semantic fair testing. In order to state our main result, it remains to define our
semantic analogue of fair testing equivalence. It rests on two main ingredients: a notion of
closed-world trace, and an analogue of parallel composition in game semantics.
The intuitive purpose of parallel composition is to let behaviours interact. If we partition
the agents of a position X into two teams, we obtain two subpositions X1 ↪ X ↩ X2 , each
agent of X belonging to X1 or X2 according to its team. The crucial fact is that the
category VX of views on X is isomorphic to the coproduct category VX1 + VX2 . Parallel
̃
̃
composition of any B1 ∈ V
X1 and B2 ∈ VX2 is then simply given by copairing [B1 , B2 ]
(following Notation 6.9), as in
Vop
X1

Vop
X
B1

[B1 ,B2 ]

Vop
X2
B2

set.
We now describe closed-world traces, which are then used as a criterion for success
of tests. Closed-world actions were defined (Definition 5.1) as those not involving any
interaction with the environment, i.e., formally, pushouts of a seed of any shape among
νn ,τn ,♡n ,πn , and τn,a,m,c,d . A trace is closed-world when it is a composite of closed-world
i

actions. Let W(X) X T(X) denote the full subcategory of T(X) consisting of closed-world
̃
traces, and let the category of closed-world strategies be W(X).
Notation 6.23. Recalling the discussion below Proposition 6.6, we denote by B ↦ B the
composite functor
op

∆kop

∆iop

ran jX
X
X
̃ ÐÐ→
̃
̃
̃ ÐÐ
V
→ T(X)
W(X),
X ÐÐÐ→ TX Ð
where ∆f denotes restriction along f .

A closed-world trace is successful when it contains a ♡ action, and unsuccessful otherwise.
̃ over a closed-world trace u∶ Z ′
A state σ ∈ S(u) of any S ∈ W(Z)
Z is successful iff u
̃ such that any unsuccessful
is. Define ⊥ Z as the set of closed-world strategies S ∈ W(Z)
closed-world state admits a successful extension, i.e. S ∈ ⊥ Z iff for all unsuccessful u ∈ W(Z)
and σ ∈ S(u), there exists a successful u′ ∈ W(Z), a morphism f ∶ u → u′ , and a state
σ ′ ∈ S(u′ ) such that σ ′ ⋅ f = σ. Finally, in order to compare behaviours for semantic fair
testing equivalence, we specify what a test is for a given behaviour B ∈ BX . A test consists
of a position Y and a behaviour T ∈ BY . Recalling Definition 3.8, we say that the pair
(X, B), with B ∈ BX , should pass the test (Y, T ) iff IX = IY and [B, T ] ∈ ⊥ Z , where Z is
the pushout X +IX Y (X and Y thus form two teams on Z). At last, we define semantic
fair testing equivalence, for any B ∈ BX and B ′ ∈ BX ′ :
Definition 6.24. Let (X, B) ∼f (X ′ , B ′ ) iff they should pass the same tests.

54

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

We may at last state:
Theorem 6.25. The translation ⟦−⟧∶ ob(Conf) → ∑X BX is intensionally fully abstract for
∼f , i.e.,
● For all configurations C1 and C2 , C1 ∼Pi
f C2 iff ⟦C1 ⟧ ∼f ⟦C2 ⟧;
● Furthermore, for all positions X and behaviours B ∈ BX , there exists C ∈ Pi X(⋆) such that
⟦C⟧ ∼f B.
The proof is the subject of the next section.
7. Intensional full abstraction
In the previous section, exploiting the playground structure of D established in Sections 4
and 5, we have defined and studied the notion of behaviour, into which we have translated
π-calculus processes and configurations. We have then defined our semantic analogue of
fair testing equivalence and stated our main result. We now work towards proving it. In
Section 7.1, we define a graph with testing S whose vertices are pairs (X, B) with B a
definite behaviour on the position X (Definition 6.12), such that fair testing equivalence
in S coincides with fair testing equivalence in the model. In order to prove that this is the
case, we introduce an intermediate graph with testing C which is in fact quite intricate. We
are then in a position where our main result is reduced to intensional full abstraction of a
translation between two graphs with testing, Conf and S, for which we may hope to apply
the results of Section 2.3. In fact, in Section 7.2, we further reduce to a translation to a
more syntactic graph with testing, M. In Section 7.3, we prove intensional full abstraction
of the translation to M, from which we deduce Theorem 6.25. Finally, we generalise to a
large class of testing equivalences in Section 7.4.
7.1. A first graph with testing for behaviours.
Definition 7.1. Let S denote the graph with vertices in ∑X DX , where we recall (Definition 6.12) that DX denotes the category of definite behaviours on X, and with non-identity
edges (X, D) ← (Y, D′ ) all closed-world actions M ∶ Y
X such that for all agents y in Y ,
there exists σy ∈ ∣D ⋅ M ⋅ y∣ such that
D′ ⋅ y ≅ (D ⋅ M ⋅ y)∣σy .
M

Moreover, let pS ∶ S → Σ denote the map sending (X, D) ←Ð (X ′ , D′ ) to the ♡ edge in Σ
if M is a tick action and to τ otherwise.
Let us now equip S with testing structure.
Definition 7.2. We define the relation ∣S by (Z, D) ∈ ((X1 , D1 ) ∣S (X2 , D2 )) iff X1 (⋆) =
X2 (⋆) and there is a pushout square
IX1

X2
injr

X1

injl

Z

such that D1 ≅ D ⋅ injl and D2 ≅ D ⋅ injr , or otherwise said D ≅ [D1 , D2 ].
Lemma 2.18 entails:

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

55

Proposition 7.3. The morphism fc(pS )∶ fc(S) → fc(Σ), with ∣S as testing relation, forms a
free graph with testing.
Proof. We exhibit a weak bisimulation relating any two such pushouts (Z, D) and (Z ′ , D′ ).
The relation containing two such pairs as soon as there exists a horizontal isomorphism
h∶ Z → Z ′ such that D ≅ D′ ⋅ h does the job.
The crucial result for proving that fair testing equivalence in S coincides with semantic
fair testing equivalence is:
Lemma 7.4. For any definite behaviour D ∈ DX , we have D ∈ ⊥ X iff (X, D) ∈ S .
Our strategy for proving this is to introduce and study an intermediate graph with
testing C, which is closer to semantic fair testing in that its transitions may comprise several
actions. However, defining C just as S with arbitrary traces instead of actions would be
wrong:
Example 7.5. Consider the trace P = (τ0 ● π0 ) consisting of a nullary agent performing
a τ action and then forking. Consider now any definite behaviour D such that D(τ0 ) =
D(τ0 ● π0l ) = D(τ0 ● π0r ) = 2, which maps both inclusions τ0 ● π0l ↩ τ0 ↪ τ0 ● π0r to the identity.
Then D(P ) = 2: it consists of pairs (σ l , σ r ) in D(τ0 ● π0l ) × D(τ0 ● π0r ) whose restrictions to
D(τ0 ) coincide, which leaves just (1, 1) and (2, 2). Using the decompositions of Section 6.2,
another way to say this is that D = ⟨τ0 ↦ D1 + D2 ⟩, with Di = ⟨π0l ↦ Dil , π0r ↦ Dir ⟩, for
i = 1, 2. In order for C to correspond to the model, assuming D1l ≇ D2l and D1r ≇ D2r ,
there should be two transitions from ([0], D), one to ([0] ∣ [0], [D1l , D1r ]) and the other to
([0] ∣ [0], [D2l , D2r ]). But if we naively generalise Definition 7.1 to arbitrary traces, we obtain
additional, ‘incoherent’ transitions, to ([0] ∣ [0], [D1l , D2r ]) and ([0] ∣ [0], [D2l , D1r ]).
Instead of relying on ∏y∈Agents(Y ) ∣D ⋅ P ⋅ y∣ as in Definition 7.1, we would like to rely on
D(P ). This may be done by constructing a map
ψPD ∶ D(P ) →

∏

∣D ⋅ P ⋅ y∣,

(7.1)

y∶[ny ]→Y

whose image will consist precisely of all ‘coherent’ elements. (From now on, we omit the
superscript D when clear from context.) Intuitively, this map associates to each global state
the corresponding family of local states. Furthermore, ψP is always injective, but Example 7.5
shows that it is not surjective in general. In order to construct ψP , recalling Definition 6.11,
we have by definition: ∏y∶[ny ]→Y ∣D ⋅ P ⋅ y∣ = ∏y∶[ny ]→Y D(v y,P , y P ). Furthermore, we also
have
D(P ) ≅ ∫
D(v, x)TX ((v,x),(P,id X )) ,
(v,x)∈VX
TX ((v,x),(P,id X ))

which is a subset of ∏(v,x)∈VX D(v, x)

. We may thus define:

ψP (σ)(y) = σ(v y,P , y P )(id ●[ny ] , αy,P ).
y,P

P

Here, σ(v y,P , y P ) is in D(v y,P , y P )TX ((v ,y ),(P,id X )) . So by applying it to αy,P viewed as
a morphism in (v y,P , y P ) → (P, id X ) in TX , we obtain an element of D(v y,P , y P ) = ∣D ⋅ P ⋅ y∣,
as desired.
We may now define the intermediate graph with testing C. We first extend the notion
of restriction:

56

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Notation 7.6. We extend Notation 6.15: if B ∈ BX and σ ∈ ∏n,x∶[n]→X ∣B ⋅ x∣, let B∣σ be
defined up to isomorphism by
B∣σ ⋅ x = (B ⋅ x)∣σ(x) .
Definition 7.7. Let C denote the graph with ob(C) = ob(S), and where C((X ′ , D′ ), (X, D))
is the set of closed-world traces W ∶ X ′ X such that there exists a state σ ∈ D(W ) satisfying
(D ⋅ W )∣ψW (σ) ≅ D′ .
Thus, C is a generalisation of S from closed-world actions to closed-world traces. Let us
turn it into a graph with testing.
Definition 7.8. Let DW
v denote the smallest locally full subbicategory of Dv containing all
closed-world traces. The graph morphism W → Σ, where we recall that W denotes the graph
of closed-world actions (Definition 5.1), extends to a pseudo functor pW ∶ DW
v → fc(Σ), which
C
W
essentially counts the number of ticks. Let p ∶ C → Dv denote the obvious projection.
pC

pW

Proposition 7.9. The composite projection C Ð→ DW
v Ð→ fc(Σ), with ∣S as testing relation,
makes C into a graph with testing.
Proof. Just as Lemma 7.3.
As announced, C is an example of a non-free graph with testing. The rest of this
section is devoted proving Lemma 7.4, and reducing Theorem 6.25 to a statement about S.
Lemma 7.4 follows from the fact that both poles are equivalent to C , as we now set out to
prove. We start with a lemma saying that C has essentially the same transitions over two
(specially) isomorphic traces.
Notation 7.10. For any morphism p∶ G → H in Gph, we denote by pA,B ∶ G(A, B) →
H(p(A), p(B)) the component of p at A and B.
Lemma 7.11. For any (X, D), (X ′ , D′ ) ∈ C, if there exists any special isomorphism W1 ≅ W2
′
in DW
v (X , X), we have
C −1
(pC )−1
(X ′ ,D′ ),(X,D) (W1 ) ≅ (p )(X ′ ,D′ ),(X,D) (W2 ).

Proof. The given special isomorphism induces by pseudo double functoriality of B an
isomorphism ϕ∶ D ⋅ W1 −∼ D ⋅ W2 , hence an isomorphism
ϕid X ′ ∶ D(W1 )

∼
−

D(W2 ).

This isomorphism is such that for any σ,
(D ⋅ W1 )∣ψW1 (σ) ≅ (D ⋅ W2 )∣ψW2 (ϕid
Thus, (D ⋅ W1 )∣ψW1 (σ) ≅ D′ iff (D ⋅ W2 )∣ψW2 (ϕid

X′

(σ))

X′

(σ)) .

≅ D′ .

In order to relate C to S, let us now show that transitions in C behave well w.r.t.
composition of traces. First, transitions compose, and second, transitions over any composite
(closed-world) trace W1 ● W2 always decompose into a transition over W1 followed by one
over W2 .
W

W′

Lemma 7.12. For all edges (X, D) ←Ð (X ′ , D′ ) ←ÐÐ (X ′′ , D′′ ) in C, there is an edge
W ●W ′

(X, D) ←ÐÐÐ (X ′′ , D′′ ).

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

57

Proof. Consider σ ∈ D(W ) such that (D ⋅ W )∣ψW (σ) ≅ D′ and σ ′ ∈ D′ (W ′ ) such that
(D′ ⋅ W ′ )∣ψW ′ (σ′ ) ≅ D′′ . We want to construct an edge W ● W ′ ∶ (X ′′ , D′′ ) → (X, D), i.e.,
find σ ′′ ∈ D(W ● W ′ ) such that (D ⋅ (W ● W ′ ))∣ψW ●W ′ (σ′′ ) ≅ D′′ . Now, the isomorphism
′
′
ϕ∶ (D ⋅ W )∣ψW (σ) −∼ D′ yields a state σ1 = ϕ−1
W ′ (σ ) ∈ (D ⋅ W )∣ψW (σ) (W ) such that
((D ⋅ W )∣ψW (σ) ⋅ W ′ )∣ψW ′ (σ1 ) ≅ (D′ ⋅ W ′ )∣ψW ′ (σ′ ) .

(7.2)

Now we have
′′
(D ⋅ W )∣ψW (σ) (W ′ ) ≅ {σ ′′ ∈ D(W ● W ′ ) ∣ σ∣W
= σ},
′′
where σ∣W
denotes restriction of σ ′′ along the prefix inclusion W ↪ W ● W ′ . So the left-hand
side in (7.2) is just (D ⋅ (W ● W ′ ))∣ψW ●W ′ (σ1 ) , which yields the desired transition.

Lemma 7.13. The projection pC ∶ C → DW
v satisfies the following weak Conduché condition:
for all X ′′

W2

X′

W1

W1 ●W2

X, if there is an edge (X ′′ , D′′ ) ÐÐÐÐ→ (X, D) in C, then there
W2

W1

exists D′ ∈ DX ′ and edges (X ′′ , D′′ ) ÐÐ→ (X ′ , D′ ) ÐÐ→ (X, D).
Proof. Consider any (X, D) ∈ C and σ ∈ D(W1 ● W2 ) witnessing the given edge. Consider
also the morphism u∶ W1 → (W1 ● W2 ) given by (W2 , id ), and let σ1 = σ ⋅ u ∈ D(W1 ). Let
D1 = (D ⋅ W1 )∣ψW1 (σ1 ) . We have σ ∈ {σ ′ ∈ D(W1 ● W2 ) ∣ σ ′ ⋅ u = σ1 }, hence σ ∈ D1 (W2 ).
Furthermore,
(D1 ⋅ W2 )∣ψW2 (σ) ≅ (D ⋅ (W1 ● W2 ))∣ψW1 ●W2 (σ) ≅ D′′ ,
so we have two edges
(W1 ,σ1 )

(W2 ,σ)

(X, D) ←ÐÐÐÐ (X ′ , D1 ) ←ÐÐÐÐ (X ′′ , D′′ )
as desired.
The previous result generalises by induction to n-ary composites:
′
′′
Notation 7.14. By default, composition in DW
v associates to the right, i.e., W ● W ● W
denotes W ● (W ′ ● W ′′ ).

Corollary 7.15. For any path p, say
X = X0

M1

X1

M2

. . . Xn = X ′ ,

(7.3)

W

in W and edge (X ′ , D′ ) Ð→ (X, D) in C over its right-associated, n-ary composition W =
(M1 ● (. . . ● Mn )), there is a path e = (e1 , . . . , en ) in C⋆ ((X ′ , D′ ), (X, D)) such that
(pC )⋆(X ′ ,D′ ),(X,D) (e) = p.
Proof. By induction on n.
Our next goal is to relate transitions in C to sequences of transitions in S. First of all, C
and S coincide on actions:
Lemma 7.16. If W ∶ X ′
X is a closed-world action (i.e., has length 1), then for all D
′
′
and D both fibres of C((X , D′ ), (X, D)) and S((X ′ , D′ ), (X, D)) over W are equal.
Proof. By [39, Proposition 5.23].

58

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Now, let us show that for any sequence of closed-world actions, sequences of transitions
in S correspond to transitions over the composite in C.
Corollary 7.17. For all closed-world paths as in (7.3), and (X, D), (X ′ , D′ ) ∈ S, we have
((pS )⋆(X ′ ,D′ ),(X,D) )−1 (p) ≠ ∅
iff
(pC(X ′ ,D′ ),(X,D) )−1 (P ) ≠ ∅,
for any special isomorphism P ≅ (M1 ● (. . . ● Mn )).
Proof. Consider any special isomorphism α∶ P
((pS )⋆(X ′ ,D′ ),(X,D) )−1 (p) ≠ ∅
iff ((pC )⋆(X ′ ,D′ ),(X,D) )−1 (p) ≠ ∅
iff (pC(X ′ ,D′ ),(X,D) )−1 (M1 ● (. . . ● Mn ))
iff (pC(X ′ ,D′ ),(X,D) )−1 (P ) ≠ ∅

∼
−

(M1 ● (. . . ● Mn )). We have

(by Lemma 7.16)
≠ ∅ (by Lemma 7.12 and Corollary 7.15)
(by Lemma 7.11).

As a corollary, we get that the identity relation on objects is a strong bisimulation
between fc(S) and C:
w

Ô (X ′ , D′ )
Corollary 7.18. For all w ∈ Σ⋆ (⋆, ⋆) and (X, D), (X ′ , D′ ) ∈ S, we have (X, D) ⇐
̃
w

in S iff (X, D) ←
Ð (X ′ , D′ ) in C.
̃
w

The last statement is slightly subtle, in that (X, D) ←
Ð (X ′ , D′ ) denotes a single edge
̃ in fc(Σ).
in C, lying over the composite w
w

̃ and
Proof. If (X, D) ⇐
Ô (X ′ , D′ ) in S, then there exists p ∈ W⋆ such that fc(pW )(p) = w
there is a path e∶ (X ′ , D′ ) → (X, D) over p in S. Let W ∶ X ′
X denote the composition of
̃
p. By Corollary 7.17, we get an edge (X ′ , D′ ) → (X, D) over W in C. So since pW (W ) = w,
this gives us the expected transition.
̃
w

Conversely, if (X, D) ←
Ð (X ′ , D′ ) in C, then let W ∶ X ′
X denote the corresponding
W
̃ Decomposing W as some path p in
edge in Dv . In particular, we have pW (W ) = w.
(pW )⋆ (p)

W, we obtain by Corollary 7.17 a transition sequence (X, D) ⇐ÔÔÔÔ (X ′ , D′ ) in S. But
W )⋆ (p) = pW (W ) = w,
̃ as desired.
(p̃
As promised, we readily obtain:
Corollary 7.19. We have S = C .
Let us also prove the analogous result with the semantic pole ⊥ .
Lemma 7.20. We have D ∈ ⊥ X iff (X, D) ∈ C .
Proof. Assume D ∈ ⊥ X , and consider any (X, D) ← (X ′ , D′ ). The latter is witnessed
by some unsuccessful, closed-world trace W ∶ X ′
X, state σ ∈ D(W ), and isomorphism
h∶ (D ⋅ W )∣ψW (σ) −∼ D′ .
By hypothesis, σ admits an extension σ ′ ∈ D(W ● W ′ ) for some successful W ′ ∶ X ′′
X ′.
′′
′
Letting D = (D ⋅ (W ● W ))∣ψW ●W ′ (σ′ ) , we have
D′′ ≅ (((D ⋅ W )∣ψW (σ) ) ⋅ W ′ )∣ψW ′ (σ′ ) ≅ (D′ ⋅ W ′ )∣ψ

W ′ (hW ′ (σ

♡n

′ ))

,

and hence (X ′ , D′ ) ←Ð (X ′′ , D′′ ) for some n > 0. This shows that (X, D) ∈ C .
Conversely, assume (X, D) ∈ C and consider any unsuccessful, closed-world trace
W ∶ X′
X and state σ ∈ D(W ). Letting D′ = (D ⋅ W )∣ψW (σ) , we have (X, D) ← (X ′ , D′ ).

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

59

By hypothesis, we find some transition (X ′ , D′ ) ←
Ð (X ′′ , D′′ ), witnessed by some successful
′
′′
′
′′
′
′
W ∶X
X . Hence, D ≅ (D ⋅ W )∣ψW ′ (σ′ ) for a certain σ ′ ∈ D′ (W ′ ). By definition of D′ ,
σ ′ is a state in D(W ● W ′ ) such that σ ′ ⋅ u = σ, where u∶ W → (W ● W ′ ) is (W ′ , id ). This
gives the desired successful extension of σ, which shows that D ∈ ⊥ X .
♡

Combining the last two results, we may now prove that the semantic pole coincides with
that of S:
Proof of Lemma 7.4. We have D ∈ ⊥ X iff (X, D) ∈ C iff (X, D) ∈ S by Corollary 7.19 and
Lemma 7.20.
As expected, this entails preservation and reflection of semantic fair testing equivalence:
Corollary 7.21. For all D ∈ DX and D′ ∈ DX ′ , we have (X, D) ∼f (X ′ , D′ ) iff (X, D) ∼Sf
(X ′ , D′ )
Proof. Let us first show that semantic fair testing equivalence may as well be defined only
with definite tests. Indeed, if IX ≠ IX ′ then the result holds trivially. So assuming IX = IX ′ ,
consider any test B ∈ BY with IX = IY , and, w.l.o.g., [D, B] ∈ ⊥ Z and [D′ , B] ∉ ⊥ Z ′ with
Z = X +IX Y and Z ′ = X ′ +IX ′ Y . Then, letting B = ∑i∈γ Di with each Di definite, there
exists i such that [D, Di ] ∈ ⊥ Z and [D′ , Di ] ∉ ⊥ Z ′ , hence Di also distinguishes D from D′ .
Returning to our main goal, for any definite test T ∈ DY with IY = IX , by Lemma 7.4,
[D, T ] ∈ ⊥ Z iff (Z, [D, T ]) = ((X, D) ∣ (Y, T )) ∈ S , which easily entails the result.
From this we may reduce our main theorem to a result on S:
Corollary 7.22. If the translation ⟦−⟧∶ ob(Conf) → ∑X DX is intensionally fully abstract
for ∼Sf , then Theorem 6.25 holds, i.e., ⟦−⟧ is also intensionally fully abstract for ∼f .
Proof. For all configurations C1 and C2 , by Corollary 7.21, ⟦C1 ⟧ ∼f ⟦C2 ⟧ iff ⟦C1 ⟧ ∼Sf ⟦C2 ⟧,
which holds iff C1 ∼Conf
C2 by hypothesis.
f
It remains to prove that surjectivity up to ∼f reduces to surjectivity up to ∼Sf . For this,
let us first show that any behaviour is ∼f -equivalent to some definite one. Indeed, consider
any B ∈ BX . Letting B ⋅ x = ∑i∈nx Dix for all agents x in X, B is fair testing equivalent to
the definite behaviour D such that
D ⋅ x = ⟨τnx ↦ ∑ Dix ⟩,
i∈nx

except if B ⋅ x = ∅ for some x. But in the latter case, B is fair testing equivalent to the
definite behaviour on one nullary player with the same interface which merely ticks.
Thus, we may restrict attention to definite behaviours. So consider any definite D ∈
DX . By hypothesis, there exists C such that ⟦C⟧ ∼Sf (X, D), hence ⟦C⟧ ∼f (X, D) by
Corollary 7.21, which concludes the proof.

60

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

7.2. A further graph with testing for behaviours. In the previous section, we have
characterised semantic fair testing equivalence using the graph with testing S, and reduced
intensional full abstraction of ⟦−⟧ w.r.t. ∼f to intensional full abstraction w.r.t. ∼Sf . We now
define a further graph with testing, M, which will help us bridge the gap between S and
π-calculus configurations. Indeed, we define a surjective morphism m∶ S → M over Σ, and we
then prove that m is intensionally fully abstract (Proposition 7.30), from which we deduce
that our main result follows from intensional full abstractness of the composite translation
T = m ○ ⟦−⟧ (Lemma 7.32).
Recall from Definition 2.3 that −⊙ denotes the finite multiset monad on sets.
Definition 7.23. Let the set M0 of mixed behaviours be
n ⊙
∑ ( ∑ D[n] × γ ) .

γ∈Pf (N) n∈N

The graph M over Σ is inductively defined by the rules in Figure 7, where S[γ1 ⊆ γ2 ] denotes
pointwise composition of the substitution component with the inclusion h∶ γ1 ⊆ γ2 , i.e., each
D[σ] is replaced by D[h ○ σ].
Let pM ∶ M → Σ denote the projection.
i ∈ ∣D ⋅ πnl ∣

j ∈ ∣D ⋅ πnr ∣

i ∈ ∣D ⋅ τn ∣

id

id

⟨γ∥D[σ]⟩ ←Ð ⟨γ∥(D ⋅ πnl )∣i [σ], (D ⋅ πnr )∣j [σ]⟩

⟨γ∥D[σ]⟩ ←Ð ⟨γ∥(D ⋅ τn )∣i [σ]⟩
i ∈ ∣D ⋅ νn ∣

i ∈ ∣D ⋅ ♡n ∣
⟨γ∥D[σ]⟩ ←
Ð ⟨γ∥(D ⋅ ♡n )∣i [σ]⟩
♡

i ∈ ∣D1 ⋅ ιn1 ,a1 ∣

a∉γ
σ+⌜a⌝

id

⟨γ∥D[σ]⟩ ←Ð ⟨γ, a∥(D ⋅ νn )∣i [n + 1 ÐÐÐ→ γ, a]⟩
j ∈ ∣D2 ⋅ on2 ,a2 ,b2 ∣

σ1 (a1 ) = σ2 (a2 )

[σ1 ,⌜σ2 (b2 )⌝]

id

⟨γ∥D1 [σ1 ], D2 [σ2 ]⟩ ←Ð ⟨γ∥(D1 ⋅ ιn1 ,a1 )∣i [n1 + 1 ÐÐÐÐÐÐÐ→ γ], (D2 ⋅ on2 ,a2 ,b2 )∣j [σ2 ]⟩
α

⟨γ1 ∥S1 ⟩ ←
Ð ⟨γ2 ∥S2 ⟩
α

⟨γ1 ∥S ∪ S1 ⟩ ←
Ð ⟨γ2 ∥S[γ1 ⊆ γ2 ] ∪ S2 ⟩

id

⟨γ∥S⟩ ←Ð ⟨γ∥S⟩

Figure 7: Transitions in M
Notation 7.24. Similarly to the notation for configurations, we denote
(γ, [(n1 , D1 , σ1 ), . . . , (np , Dp , σp )])
by
⟨γ∥D1 [σ1 ], . . . , Dp [σp ]⟩.
For the testing structure of M, we mimick Definition 2.7 and put:
Definition 7.25. For any ⟨γ∥S⟩, ⟨γ ′ ∥S ′ ⟩ ∈ M, let ⟨γ∥S⟩@⟨γ ′ ∥S ′ ⟩ denote ⟨γ∥S ∪ S ′ ⟩ if γ = γ ′
and be undefined otherwise. Let furthermore γ = ⟨γ∥⟩.
By Lemma 2.18, we have:
Proposition 7.26. The morphism fc(pM )∶ fc(M) → fc(Σ), with the graph of @ as testing
relation, forms a free graph with testing.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

61

Let us now reduce Theorem 6.25 to a statement about M. In order to do this, we will
use Lemma 2.22 and hence need to exhibit a fair relation ob(S)
M0 . We use the graph of
the following map:
Definition 7.27. Let m∶ ob(S) → M0 map any (X, D) to the mixed behaviour
⟨X(⋆)∥[(D ⋅ x)[σx ] ∣ (n, x) ∈ Agents(X)]⟩,
[⌜x⋅si ⌝]i∈n

where σx is the map n ÐÐÐÐÐ→ X(⋆).
We now need to show that m yields a fair relation. Most points are direct, like totality
or the fact that (X, D) ¨ (X ′ , D′ ) iff m(X, D) ¨ m(X ′ , D′ ). Furthermore, we have:
Proposition 7.28. The map m∶ ob(S) → M0 is surjective. Let a denote any section of m.
The point about bisimilarity is trickier:
Proposition 7.29. We have (X, D) ∼Σ m(X, D) for all (X, D) ∈ ob(S).
Proof. It is enough to prove that (the graph of) m is a strong bisimilarity up to strong
bisimilarity. For this, let us record that clearly for any isomorphism h∶ X → Y of positions
and D ∈ DY , we have (Y, D) ∼Σ (X, D ⋅ h) in S. Let us call I (for isomorphism) the relation
given by all pairs ((Y, D), (X, D ⋅ h)), so that we have I ⊆ ∼Σ . By case analysis, we can
α
show that m is a strong bisimulation up to I, i.e., for all (X, D) ←
Ð (Y, D′ ), there exists
α
(Y, D′ ) I (Z, D′′ ) such that m(X, D) ←
Ð m(Z, D′′ ), as below left. And more tightly, for all
α
α
m(X, D) ←
Ð M ′ , there exists (X, D) ←
Ð (X ′ , D′ ) such that m(X ′ , D′ ) = M ′ , as below right.
(X, D)

m

m(X, D)

α

(Y, D ) I (Z, D )
′′

m

m

α

α
′

(X, D)

m(Z, D )
′′

(Y, D )
′

m

m(X, D)
α
′

M

The right-hand diagram is a tedious yet straightforward case analysis. The left-hand one is
α
also a tedious case analysis, whose main point is that for all transitions (X, D) ←
Ð (Y, D′ ),
some renaming of elements of X may take place, which cannot happen in any transition
from m(X, D). So in each case we need to find the Z and corresponding D′′ which avoids
such renaming. In fact, this goes by indentifying the right transition from m(X, D) and
showing that the obtained M ′ is of the form m(Z, D′′ ) for (Y, D′ ) I (Z, D′′ ). Let us do one
♡
case. If (X, D) ←
Ð (Y, D′ ), then we have an iso h∶ X −∼ Y , and there is some agent (n0 , x0 )
in X and i such that D′ ⋅ h(x0 ) = (D ⋅ x0 ⋅ ♡n0 )∣i and furthermore for all (n, x) ≠ (n0 , x0 ) in
Agents(X), we have D′ ⋅ h(x) = D ⋅ x. So, letting y = h(x) for all such x, we indeed have
M = ⟨γ∥(D ⋅x0 )[σx0 ]∶∶[(D ⋅x)[σx ] ∣ x ≠ x0 ]⟩

♡

⟨γ∥(D′ ⋅y0 )[σx0 ]∶∶[(D ⋅x)[σx ] ∣ x ≠ x0 ]⟩ = M ′

with M = m(X, D), and furthermore letting D′′ be determined by D′′ ⋅ x = D′ ⋅ h(x) = D ⋅ x
for x ≠ x0 and D′′ ⋅ x = D′ ⋅ h(x0 ), we have D′′ = D′ ⋅ h and hence (Y, D′ ) I (X, D′′ ) with
m(X, D′′ ) = M ′ , as desired.

62

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

We are now ready to show:
Proposition 7.30. The map m∶ ob(S) → ob(M) is intensionally fully abstract for fair
testing equivalence.
Proof. As announced, for preservation and reflection of fair testing equivalence we apply
Lemma 2.22: we have established all necessary hypotheses, except the last one, which follows
by choosing a pushout with the same set of channels as its summands.
For surjectivity up to ∼M
f , consider any ⟨γ∥S⟩ ∈ M0 . Because a is a section of m, we have
m(a(⟨γ∥S⟩)) = ⟨γ∥S⟩, hence m(a(⟨γ∥S⟩)) ∼M
f ⟨γ∥S⟩, thus providing the desired antecedent.
Let us now reduce Theorem 6.25 to its analogue about M.
Definition 7.31. Let T∶ ob(Conf) → ob(M) denote the composite
⟦−⟧

m

ob(Conf) ÐÐ→ ob(S) Ð
→ ob(M).
Concretely, we have
−1
T⟨γ∥P1 , . . . , Pn ⟩ = ⟨γ∥⟦P1 ⟧hγ [h−1
γ ], . . . , ⟦Pn ⟧hγ [hγ ]⟩.

Lemma 7.32. The translation ⟦−⟧ from Definition 6.22 is intensionally fully abstract for
∼Sf if T is for ∼M
f .
Proof. Assuming T is intensionally fully abstract, then for all configurations C and C ′ , we
′
have that C ∼f C ′ iff T(C) ∼M
f T(C ). But by Proposition 7.30, we have
′
′
T(C) = m⟦C⟧ ∼M
f m⟦C ⟧ = T(C )

iff

⟦C⟧ ∼Sf ⟦C ′ ⟧,

hence C ∼f C ′ iff ⟦C⟧ ∼f S⟦C ′ ⟧.
Finally, for any (X, D) ∈ S, by intensional full abstractness of T, we find a configuration
C such that T(C) ∼M
f m(X, D), hence by Proposition 7.30 again ⟦C⟧ ∼f (X, D).
7.3. Intensional full abstraction. We at last prove our main result, by proving intensional
full abstractness of T. Our strategy is to define a relation &∶ Conf
M over Σ which
● relates any configuration to its image under T, and
● is surjective, i.e., relates any mixed behaviour to some configuration.
We will then show that this relation is a weak bisimulation over Σ, which will entail the
result.
Let us start with the second point, and define a map Z ∈ ob(M) → ob(Conf), which
associates a configuration to each mixed behaviour. We first coinductively define ζ for
definite behaviours on representable positions by:
⎛
⎜+
⎜
⎜+
ζ(n ⊢D D) = ⎜
⎜+
⎜
⎜
⎜+
⎝+

∑i∈∣D⋅πnl ∣,j∈∣D⋅πnr ∣ τ.(ζ(n ⊢D (D ⋅ πnl )∣i ) ∣ ζ(n ⊢D (D ⋅ πnr )∣j ))
∑i∈∣D⋅τn ∣ τ.ζ(n ⊢D (D ⋅ τn )∣i )
∑i∈∣D⋅♡n ∣ ♡.ζ(n ⊢D (D ⋅ ♡n )∣i )
∑i∈∣D⋅νn ∣ ν(n + 1).ζ(n + 1 ⊢D (D ⋅ νn )∣i )
∑a∈n,i∈∣D⋅ιn,a ∣ a(n + 1).ζ(n + 1 ⊢D (D ⋅ ιn,a )∣i )
∑a,b∈n,i∈∣D⋅on,a,b ∣ ā⟨b⟩.ζ(n ⊢D (D ⋅ on,a,b )∣i )

where n ⊢D D means D ∈ D[n] .

⎞
⎟
⎟
⎟
⎟,
⎟
⎟
⎟
⎟
⎠

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

63

Except perhaps for the first term of the sum, this should be rather natural: each definite
behaviour on a representable position corresponds to a guarded sum, with one term for each
state over each basic action – the translation is direct. The twist in the first term is due to
the fact that forking is not a guard in π, so P ∣ Q cannot appear in any guarded sum. But
τ.(P ∣ Q) can, and it is clearly weakly bisimilar to P ∣ Q, so this is precisely what ζ does.
Let us now extend ζ to arbitrary configurations:
Definition 7.33. Let Z∶ ob(M) → ob(Conf) be defined by
Z⟨γ∥D1 [σ1 ], . . . , Dn [σn ]⟩ = ⟨γ∥ζ(D1 )[σ1 ], . . . , ζ(Dn )[σn ]⟩.
Remark 7.34. Let us emphasise that brackets on the right denote proper substitutions,
while on the left Di [σi ] is just syntactic sugar for (ni , Di , σi ) by Notation 7.24.
In order for Z to return an antecedent up to ∼M
f , we immediately observe that for any
l
r
D and i ∈ ∣D ⋅ πn ∣ and j ∈ ∣D ⋅ πn ∣,
● on the one hand D has a silent transition to ∂i,j D, the behaviour on [n] ∣ [n] such that
(∂i,j D) ⋅ x1 = (D ⋅ πnl )∣i and (∂i,j D) ⋅ x2 = (D ⋅ πnr )∣j (where x1 and x2 denote the two agents
of [n] ∣ [n]);
● on the other hand ζ(D) has a silent transition to
′
ζi,j
(D) = (ζ((D ⋅ πnl )∣i ) ∣ ζ((D ⋅ πnr )∣j )),

which then has a further silent transition to the two-process configuration consisting of
ζ((D ⋅ πnl )∣i ) and ζ((D ⋅ πnr )∣j ).
id

′
Thus, when we try to relate D and ζ(D), the transition ζ(D) ←Ð ζi,j
(D) has to be matched
id

by the former transition D ←Ð ∂i,j D. So our relation & should somehow include pairs
′
(ζi,j
(D), ∂i,j D).
Definition 7.35. Let the relation &∶ Conf
in Figure 8.

M over Σ be defined inductively by the rules

(In the last rule, γ is understood in Conf on the left, and in M on the right.)
γ′ ⊢ P

h∶ γ ′

∼
−

n

n ⊢D D

σ∶ n → γ

P [σ ○ h] & ⟦P ⟧h [σ]
n ⊢D D1 , D2

σ∶ n → γ

2

1

ζ(D)[σ] & D[σ]
C&M

(ζ(D ) ∣ ζ(D ))[σ] & D [σ], D [σ]
1

2

σ∶ n → γ

D&N

C@D & M @N

γ & γ

⋅

Figure 8: The relation &
Lemma 7.36. We have C & T(C) for all C and Z(M ) & M for all M , and so & is total
and surjective.
Proof. By construction.

64

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Lemma 7.37. The relation & is a weak bisimulation over Σ.
Proof. First, we observe that & may equivalently be defined by first letting &0 be generated
by all rules except the last two, and then adding the rule
C1 &0 M1

...

Cn &0 Mn

C1 @ . . . @Cn & M1 @ . . . @Mn

(n ∈ N)⋅

The advantage of this presentation is that proofs of C & M all have depth at most 1.
The rest is then a tedious case analysis, which we defer to Appendix A. In summary, we
easily observe that the ‘forwards’ clause of weak bisimulation is satisfied, the only subtlety
being that heating (ζ(D1 ) ∣ ζ(D2 ))[σ] should be matched by the identity edge on the
corresponding behaviour. Furthermore, the ‘backwards’ clause is also easily satisfied, the
only subtlety being that if the considered behaviour performs a transition involving one or
several [D1 [σ], D2 [σ]]’s, related on the left to (ζ(D1 ) ∣ ζ(D2 ))[σ]’s, then all of the latter
first have to heat to [ζ(D1 )[σ], ζ(D2 )[σ]], and only then perform the matching transition.
This easily entails:
Lemma 7.38. For all C1 , C2 , M1 , M2 , if C1 & M1 and C2 & M2 , then C1 ∼f C2 iff M1 ∼f M2 .
Proof. The relation & is weakly fair, the only difficult points being proved by Lemmas 7.36
and 7.37 above. We thus conclude by Corollary 2.25.
Theorem 7.39. The map T∶ ob(Conf) → ob(M) is intensionally fully abstract.
Proof. Lemma 7.38 directly entails preservation and reflection of fair testing equivalence.
M
Regarding surjectivity up to ∼M
f , for any M ∈ M0 , we have M ∼f T(Z((M ))). Indeed, for
′
any M , we have
M @M ′ ∈ 
iff Z(M )@Z(M ′ ) ∈ 
(because Z(M )@Z(M ′ ) & M @M ′ and by Lemma 7.37)
iff T(Z(M ))@M ′ ∈ 
(because Z(M )@Z(M ′ ) & T(Z(M ))@M ′ and by Lemma 7.37),
as desired.
We are now able to prove our main result:
Proof of Theorem 6.25. By Theorem 7.39, T is intensionally fully abstract for ∼M
f , so by
S
Lemma 7.32 ⟦−⟧ is intensionally fully abstract for ∼f . We thus conclude by Corollary 7.22.
7.4. Generalisation. We now show that our main results generalise beyond fair testing
equivalence. Indeed, let us put:
Definition 7.40. A pole is a property of states over fc(Σ) which is stable under strong
bisimilarity.
There is a slight size issue in this definition, as it quantifies over elements of all graphs
over fc(Σ). The reader may understand this using whatever fix they prefer, e.g., using a
universe or some modal logic.
Example 7.41. Consider any x ∈ G over fc(Σ). We have

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

65

Ð x′′ ;
● x is in the pole for fair testing equivalence iff for all x ← x′ there exists x′ ←
♡ ′
● x is in the pole for may testing equivalence iff there exists x ←
Ðx.
Must testing equivalence is less easy to capture, for reasons explained in [41]. Here is an
exotic, yet perhaps relevant pole: x is in it iff for all finite, not-necessarily silent transition
♡
sequences x ←
Ð⋆ x′ , there exists x′ ←
Ð x′′ . In other words, x never loses the ability to tick.
The induced equivalence is clearly at least as fine as fair testing equivalence, but we leave
open the question of whether or not it is strictly finer.
♡

Definition 7.42. For any such pole , let ∼ denote the testing equivalence induced by
replacing G by  in the definition of fair testing equivalence (Definition 2.14).
Semantic testing equivalence may then be taken to be testing equivalence on C (Definition 7.7), and we get the exact analogue of Theorem 6.25 (without changing the model in
any way).
8. Conclusion and future work
We have described our playground for π and the induced sheaf model, which we have proved
intensionally fully abstract for a wide range of testing equivalences.
Regarding future work: our proof that traces form a playground uses a new technique
based on factorisation systems. Since submission of this paper, we have designed [22, 23] a
general setting where this technique applies, and used it to bridge the gap between our notion
of plays based on string diagrams and the standard one based on justified sequences [71].
We also consider applying our notion of trace to error diagnostics [32] or efficient machine
representation of reversible π-calculus processes [19]. Longer-term directions include applying
the approach to more complex calculi, e.g., calculi with passivation [50] or functional calculi,
and eventually consider some full-fledged functional language with concurrency primitives.
Finally, deriving the complex notion of trace evoked in Section 1.5 from the one exposed
here is akin to deriving ltss from reduction rules [48, 65]. Since the issue still seems easier
on traces than on a full operational semantics specification, this might be worthwile to
investigate further. In the same vein, the emphasis we put on traces suggests that we
might be able to deduce properties of type systems (soundness, progress, etc) or compilers
(correctness) from corresponding properties on traces.
References
[1] LICS 1996. Proc. 11th Symposium on Logic in Computer Science, 1996. IEEE.
[2] LICS 2015. Proc. 30th Symposium on Logic in Computer Science, 2015. IEEE.
[3] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for
PCF. Information and Computation, 163(2):409–470, 2000. doi:10.1006/inco.2000.2930.
[4] Jir̆ı́ Adámek and Jir̆ı́ Rosicky. Locally Presentable and Accessible Categories. Cambridge
University Press, 1994. doi:10.1017/CBO9780511600579.
[5] Gérard Berry and Gérard Boudol. The chemical abstract machine. In Proc. 17th
International Symposium on Principles of Programming Languages, pages 81–94, 1990.
doi:10.1145/96709.96717.

66

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

[6] Filippo Bonchi, Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva.
Deriving syntax and axioms for quantitative regular behaviours. In Proc. 21st International Conference on Concurrency Theory, volume 5710 of LNCS, pages 146–162.
Springer, 2009. doi:10.1007/978-3-642-04081-8 11.
[7] Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality in the
π-calculus. Acta Informatica, 35(5):353–400, 1998.
[8] A. K. Bousfield. Constructions of factorization systems in categories. Journal of Pure
and Applied Algebra, 9(2-3):287–329, 1977.
[9] Ed Brinksma, Arend Rensink, and Walter Vogler. Fair testing. In CONCUR 1995 [17],
pages 313–327. ISBN 3-540-60218-6. doi:10.1007/3-540-60218-6 23.
[10] Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari. Event structure semantics for nominal calculi. In Proc. 18th International Conference on Concurrency
Theory, volume 4137 of LNCS, pages 295–309. Springer, 2006. ISBN 3-540-37376-4.
doi:10.1007/11817949 20.
[11] Nadia Busi and Roberto Gorrieri. A Petri net semantics for π-calculus. In CONCUR
1995 [17], pages 145–159. ISBN 3-540-60218-6. doi:10.1007/3-540-60218-6 11.
[12] Nadia Busi and Roberto Gorrieri. Distributed semantics for the π-calculus based on
Petri nets with inhibitor arcs. Journal of Logic and Algebraic Programming, 78(3):
138–162, 2009. doi:10.1016/j.jlap.2008.08.002.
[13] Diletta Cacciagrano, Flavio Corradini, and Catuscia Palamidessi. Explicit fairness in
testing semantics. Logical Methods in Computer Science, 5(2), 2009. doi:10.2168/LMCS5(2:15)2009.
[14] Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally
fully abstract games model of pcf. In LICS 2015 [2].
[15] Gian Luca Cattani and Peter Sewell. Models for name-passing processes: Interleaving
and causal. In Proc. 15th Symposium on Logic in Computer Science, pages 322–333.
IEEE, 2000. ISBN 0-7695-0725-5. doi:10.1109/LICS.2000.855781.
[16] Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf models for the π-calculus.
In Category Theory and Computer Science, volume 1290 of LNCS, pages 106–126.
Springer, 1997. ISBN 3-540-63455-X. doi:10.1007/BFb0026984.
[17] CONCUR 1995. Proc. 6th International Conference on Concurrency Theory, volume
962 of LNCS, 1995. Springer. ISBN 3-540-60218-6.
[18] Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Event structure semantics of
parallel extrusion in the pi-calculus. In Proc. 15th Foundations of Software Science and
Computational Structures, volume 7213 of LNCS, pages 225–239. Springer, 2012. ISBN
978-3-642-28728-2. doi:10.1007/978-3-642-28729-9 15.
[19] Ioana Cristescu, Jean Krivine, and Daniele Varacca. A compositional semantics for the
reversible π-calculus. In Proc. 28th Symposium on Logic in Computer Science, pages
388–397. IEEE, 2013. ISBN 978-1-4799-0413-6. doi:10.1109/LICS.2013.45.
[20] Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theoretical
Computer Science, 34:83–133, 1984. doi:10.1016/0304-3975(84)90113-0.
[21] Pierpaolo Degano and Corrado Priami. Non-interleaving semantics for mobile processes. Theoretical Computer Science, 216(1-2):237–270, 1999. doi:10.1016/S03043975(99)80003-6.
[22] Clovis Eberhart and Tom Hirschowitz. Justified sequences in string diagrams: a
comparison between two approaches to concurrent game semantics. Preprint, 2016.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

67

[23] Clovis Eberhart and Tom Hirschowitz. Justified sequences in string diagrams: a
comparison between two approaches to concurrent game semantics. In Proc. 7th
International Conference on Algebra and Coalgebra in Computer Science, LIPIcs. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. To appear.
[24] Charles Ehresmann. Catégories structurées. Annales scientifiques de l’Ecole Normale
Supérieure, 80(4):349–426, 1963.
[25] Charles Ehresmann. Catégories et structures. Dunod, 1965.
[26] Joost Engelfriet. A multiset semantics for the pi-calculus with replication. Theoretical
Computer Science, 153(1&2):65–94, 1996. doi:10.1016/0304-3975(95)00118-2.
[27] Marcelo P. Fiore and Daniele Turi. Semantics of name and value passing. In Proc.
16th Symposium on Logic in Computer Science, pages 93–104. IEEE, 2001. ISBN
0-7695-1281-X. doi:10.1109/LICS.2001.932486.
A fully-abstract
[28] Marcelo P. Fiore, Eugenio Moggi, and Davide Sangiorgi.
model for the pi-calculus (extended abstract). In LICS 1996 [1], pages 43–54.
doi:10.1109/LICS.1996.561302.
[29] P. J. Freyd and G. M. Kelly. Categories of continuous functors, I. Journal of Pure and
Applied Algebra, 2:169–191, 1972. doi:10.1016/0022-4049(72)90001-1.
[30] Richard H. G. Garner. Polycategories. PhD thesis, University of Cambridge, 2006.
[31] Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical
Structures in Computer Science, 11(3):301–506, 2001. doi:10.1007/3-540-44802-0 3.
[32] Gregor Gösler, Daniel Le Métayer, and Jean-Baptiste Raclet. Causality analysis in
contract violation. In Proc. of Runtime Verification, volume 6418 of LNCS, pages
270–284. Springer, 2010. ISBN 978-3-642-16611-2. doi:10.1007/978-3-642-16612-9 21.
[33] Marco Grandis and Robert Paré. Limits in double categories. Cahiers de Topologie et
Géométrie Différentielle Catégoriques, 40(3):162–220, 1999.
[34] Marco Grandis and Robert Paré. Adjoints for double categories. Cahiers de Topologie
et Géométrie Différentielle Catégoriques, 45(3):193–240, 2004.
[35] Russell Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for
innocent strategies. In Proc. 22nd Symposium on Logic in Computer Science, pages
379–388. IEEE, 2007. doi:10.1109/LICS.2007.14.
[36] Matthew Hennessy. A fully abstract denotational semantics for the π-calculus. Theoretical Computer Science, 278(1-2):53–89, 2002. doi:10.1016/S0304-3975(00)00331-5.
[37] Thomas T. Hildebrandt. Towards categorical models for fairness: fully abstract presheaf
semantics of SCCS with finite delay. Theoretical Computer Science, 294(1/2):151–181,
2003. doi:10.1016/S0304-3975(01)00247-X.
[38] Tom Hirschowitz. Full abstraction for fair testing in CCS. In Proc. 5th International
Conference on Algebra and Coalgebra in Computer Science, volume 8089 of LNCS, pages
175–190. Springer, 2013. doi:10.1007/978-3-642-40206-7 14.
[39] Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical
Methods in Computer Science, 10(4), 2014. doi:10.2168/LMCS-10(4:2)2014.
[40] Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive
equivalences for CCS. In Proc. of Interaction and Concurrency Experience, pages 2–24.
Electronic Proceedings in Theoretical Computer Science, 2011. doi:10.4204/EPTCS.59.2.
[41] Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive
equivalences for CCS. Scientific Annals of Computer Science, 22(1):147–199, 2012.
doi:10.7561/SACS.2012.1.147. Selected papers from ICE ’11.

68

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

[42] J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II, and III. Information
and Computation, 163(2):285–408, 2000. doi:10.1006/inco.2000.2917.
[43] Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and
the Foundations of Mathematics. North Holland, Amsterdam, 1999.
[44] Lalita Jategaonkar Jagadeesan and Radha Jagadeesan. Causality and true concurrency:
A data-flow analysis of the pi-calculus (extended abstract). In Proc. of Algebraic
Methodology and Software Technology, volume 936 of LNCS, pages 277–291. Springer,
1995. doi:10.1007/3-540-60043-4 59.
[45] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps.
In Proc. 8th Symposium on Logic in Computer Science, pages 418–427. IEEE, 1993.
doi:10.1109/LICS.1993.287566.
[46] Stephen Lack and Pawel Sobociński. Adhesive categories. In Proc. 7th Foundations of
Software Science and Computational Structures, volume 2987 of LNCS, pages 273–288.
Springer, 2004. doi:10.1007/978-3-540-24727-2 20.
[47] James Laird. Game semantics for higher-order concurrency. In Proc. 26th Foundations
of Software Technology and Theoretical Computer Science, volume 4337 of LNCS, pages
417–428. Springer, 2006. doi:10.1007/11944836 38.
[48] James J. Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems.
In Proc. 11th International Conference on Concurrency Theory, volume 1877 of LNCS,
pages 243–258. Springer, 2000. ISBN 3-540-67897-2. doi:10.1007/3-540-44618-4 19.
[49] Tom Leinster. Higher Operads, Higher Categories, volume 298 of London Mathematical
Society Lecture Notes. Cambridge University Press, Cambridge, 2004.
[50] Sergueı̈ Lenglet, Alan Schmitt, and Jean-Bernard Stefani. Normal bisimulations in calculi
with passivation. In Proc. 12th Foundations of Software Science and Computational
Structures, volume 5504 of LNCS, pages 257–271. Springer, 2009. doi:10.1007/978-3642-00596-1 19.
[51] Paul Blain Levy. Morphisms between plays. GaLoP, 2013.
[52] Saunders Mac Lane. Duality for groups. Bulletin of the American Mathematical Society,
56, 1950.
[53] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate
Texts in Mathematics. Springer, 2nd edition, 1998.
[54] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First
Introduction to Topos Theory. Universitext. Springer, 1992.
[55] Guy McCusker, John Power, and Cai Wingfield. A graphical foundation for
schedules. Electronic Notes in Theoretical Computer Science, 286:273–289, 2012.
doi:10.1016/j.entcs.2012.08.018.
[56] Paul-André Melliès. Asynchronous games 2: the true concurrency of innocence. In Proc.
15th International Conference on Concurrency Theory, volume 3170 of LNCS, pages
448–465. Springer, 2004. doi:10.1007/978-3-540-28644-8 29.
[57] Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional
linear logic. In Proc. 20th Symposium on Logic in Computer Science, pages 386–395.
IEEE, 2005. ISBN 0-7695-2266-1. doi:10.1109/LICS.2005.6.
[58] Paul-André Melliès. Game semantics in string diagrams. In Proc. 27th Symposium on
Logic in Computer Science, pages 481–490. IEEE, 2012. doi:10.1109/LICS.2012.58.
[59] Ugo Montanari and Marco Pistore. Concurrent semantics for the π-calculus. Electronic Notes in Theoretical Computer Science, 1:411–429, 1995. doi:10.1016/S15710661(04)00024-6.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

69

[60] Ugo Montanari and Marco Pistore. Structured coalgebras and minimal HDautomata for the π-calculus. Theoretical Computer Science, 340(3):539–576, 2005.
doi:10.1016/j.tcs.2005.03.014.
[61] V. Natarajan and Rance Cleaveland. Divergence and fair testing. In Proc. 22nd
International Colloquium on Automata, Languages and Programming, volume 944 of
LNCS, pages 648–659. Springer, 1995. ISBN 3-540-60084-1. doi:10.1007/3-540-600841 112.
[62] Hanno Nickau. Hereditarily sequential functionals. In Proc. Logical Foundations of
Computer Science, volume 813 of LNCS, pages 253–264. Springer, 1994. doi:10.1007/3540-58140-5 25.
[63] Mogens Nielsen, Gordon Plotkin, and Glynn Winskel. Event structures and domains,
part 1. Theoretical Computer Science, 13:65–108, 1981.
[64] Robert Paré. Yoneda theory for double categories. Theory and Applications of Categories,
25(17):436–489, 2011.
[65] Julian Rathke and Pawel Sobociński. Deconstructing behavioural theories of mobility.
In IFIP TCS, volume 273 of IFIP, pages 507–520. Springer, 2008. doi:10.1007/978-0387-09680-3 34.
[66] Arend Rensink and Walter Vogler. Fair testing. Information and Computation, 205(2):
125–198, 2007. doi:10.1016/j.ic.2006.06.002.
[67] Silvain Rideau and Glynn Winskel. Concurrent strategies. In Proc. 26th Symposium on
Logic in Computer Science, pages 409–418. IEEE, 2011. doi:10.1109/LICS.2011.13.
[68] Davide Sangiorgi and Jan Rutten, editors. Advanced Topics in Bisimulation and Coinduction. Number 52 in Cambridge Tracts in Theoretical Computer Science. Cambridge
University Press, 2011.
[69] Davide Sangiorgi and David Walker. The π-calculus - a theory of mobile processes.
Cambridge University Press, 2001.
[70] Ian Stark. A fully abstract domain model for the π-calculus. In LICS 1996 [1], pages
36–42. doi:10.1109/LICS.1996.561301.
[71] Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves.
In LICS 2015 [2].
[72] Glynn Winskel. Event structure semantics for CCS and related languages. In Proc. 9th
International Colloquium on Automata, Languages and Programming, volume 140 of
LNCS, pages 561–576. Springer, 1982. ISBN 3-540-11576-5. doi:10.1007/BFb0012800.
[73] Glynn Winskel. Strategies as profunctors. In Proc. 16th Foundations of Software Science
and Computational Structures, volume 7794 of LNCS, pages 418–433. Springer, 2013.
doi:10.1007/978-3-642-37075-5 27.

70

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

Appendix A. Proof of Lemma 7.37
One wants to check two properties:
a

a

→A M with C ′ & M ′ ;
→A C with C & M , there exists M ′ Ð
(LH) for all transitions C ′ Ð
a
a
(RH) for all transitions M A ←
Ð M ′ with C & M , there exists C A ⇐
Ô C ′ with C ′ & M ′ .
The attentive reader will have noticed that (LH) imposes y to answer with a single transition.
This means we actually prove that & is an expansion [68, Chapter 6]. Any expansion being
in particular a weak bisimulation, this suffices.
Notation A.1. We sometimes cast processes P (resp. pairs D[σ]) over γ into configurations
⟨γ∥P ⟩ (resp. mixed behaviours ⟨γ∥D[σ]⟩). We proceed similarly for multisets of processes.
We start by proving (LH) for all cases, before proving that (RH) holds as well.
Synchro, (LH). We begin by the case of a synchronisation, i.e., when one has a transition
id

C = ⟨γ∥a(b).P +k1 R1 , ā⟨c⟩.Q +k2 R2 ⟩@C0 ←Ð ⟨γ∥P [b ↦ c], Q⟩@C0 = C ′ .
id

We want to show that there exists a transition M ←Ð M ′ with C ′ & M ′ .
We write P1 = a(b).P +k1 R1 and P2 = ā⟨c⟩.Q +k2 R2 . Neither of them are of the form
(⋅ ∣ ⋅) so they can only be related to mixed behaviours using the first two rules. Therefore,
four sub-cases should be considered, as detailed in Figure 9. If we are in case i1 for P1 and i2
for P2 , then we have two mixed behaviours D1 [σ1 ] and D2 [σ2 ] such that ni ⊢D Di , σi ∶ ni → γ,
and Pi & Di [σi ] for i = 1, 2, plus M = ⟨γ∥D1 [σ1 ], D2 [σ2 ]⟩@M0 with C0 & M0 .
● Case 1 for both P1 and P2 . We have M = ⟦P1′ ⟧h1 [σ1 ]@⟦P2′ ⟧h2 [σ2 ]@M0 , and there is a
transition
id
M ←Ð ⟦P ′ ⟧h′1 [σ1′ ]@⟦Q′ ⟧h2 [σ2 ]@M0 ,
[σ1 ,c]

h1 +!

where h′1 is γ1′ , b′ ÐÐ→ n1 + 1 and σ1′ is n1 + 1 ÐÐÐ→ γ.
h1 +!

σ1 +⌈b⌉

b↦c

Since σ1′ ○ h′1 equals γ1′ ÐÐ→ n1 + 1 ÐÐÐ→ (γ, b) ÐÐ→ γ, we have that P ′ [σ1′ ○ h′1 ] =
P ′ [(σ1 + ⌈b⌉) ○ (h1 +!)][b ↦ c] = P [b ↦ c], and therefore P [b ↦ c] & ⟦P ′ ⟧h′1 [σ1′ ]. Moreover,
it is clear that Q = Q′ [σ2 ○ h2 ] & ⟦Q′ ⟧h2 [σ2 ], and finally [P [b ↦ c], Q]@C0 & M ′ .
● Case 1 for P1 , Case 2 for P2 . We have a transition
id

M ←Ð ⟦P ′ ⟧h′1 [σ1′ ]@(D2 ⋅ on2 ,a2 ,c2 )∣j [σ2 ]@M0 = M ′ ,
h1 +!

[σ1 ,c]

where h′1 is γ1′ , b′ ÐÐ→ n1 + 1 and σ1′ is n1 + 1 ÐÐÐ→ γ.
As is the previous case, one can check that P [b ↦ c] & ⟦P ′ ⟧h′1 [σ1′ ]. Moreover, Q &
(D2 ⋅ on2 ,a2 ,c2 )∣j [σ2 ] and therefore [P [b ↦ c], Q]@C0 & M ′ .
● Case 2 for P1 , Case 1 for P2 . We have a transition
id

[σ1 ,⌈c⌉]

M ←Ð (D1 ⋅ ιn1 ,a1 )∣i [n1 + 1 ÐÐÐÐ→ γ]@⟦Q′ ⟧h′2 [σ2′ ]@M0 = M ′ .
As in the first case, we have Q = Q′ [σ2 ○ h2 ] & ⟦Q′ ⟧h2 [σ2 ]. Furthermore, since
[σ1 ,⌈c⌉]

ζ((D1 ⋅ ιn1 ,a1 )∣i )[n1 + 1 ÐÐÐÐ→ γ]
σ1 +⌈b⌉

= ζ((D1 ⋅ ιn1 ,a1 )∣i )[n1 + 1 ÐÐÐ→ γ, b][b ↦ c]
= P [b ↦ c],

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

P1

(EXPANDED VERSION)

71

Case 1
Case 2
′
′
′ ′
′
′
There exist γ1 ⊢ P1 = a1 (b ).P +k1 R1 There exist n1 ⊢D D1 , a1 ∈ n1 , and i ∈
and h1 ∶ γ1′ −∼ n1 such that
∣D1 ⋅ ιn1 ,a1 ∣ such that
P1 = P1′ [σ1 ○ h1 ]

σ1 (a1 ) = a

σ1 (h1 (a′1 )) = a

σ1 +⌜b⌝

σ1 +⌜b⌝

h1 +!

P = ζ((D1 ⋅ ιn1 ,a1 )∣i )[n1 + 1 ÐÐÐ→ γ, b].

P = P ′ [γ1′ , b′ ÐÐ→ n1 + 1 ÐÐÐ→ γ, b]
D1 = ⟦P1′ ⟧h1

P1 = ζ(D1 )[σ1 ]

R1 = R1′ [σ1 ○ h1 ].

P2 There exist γ2′ ⊢ P2′ = a¯′2 ⟨c′ ⟩.Q′ +k2 R2′ There exist n2 ⊢D D2 , a2 , c2 ∈ n2 , and
j ∈ ∣D2 ⋅ on2 ,a2 ,c2 ∣ such that
and h2 ∶ γ2′ −∼ n2 such that
σ2 (a2 ) = a
σ2 (c2 ) = c
P2 = P ′ [σ2 ○ h2 ]
2

P2 = ζ(D2 )[σ2 ]

σ2 +⌜b⌝

h2 +1

Q = Q′ [γ2′ , b ÐÐ→ n2 + 1 ÐÐÐ→ γ, b]
σ2 (h2 (a′2 )) = a
D2 = ⟦P2′ ⟧h2

Q = ζ((D2 ⋅ on2 ,a2 ,c2 )∣j )[σ2 ].

σ2 (h2 (c′2 )) = c
R2 = R2′ [σ2 ○ h2 ].

Figure 9: Synchro, (LH) cases
we have that [P [b ↦ c], Q]@C0 & M ′ .
● Case 2 for both P1 and P2 . We have a transition
[σ1 ,⌈c⌉]

id

M ←Ð (D1 ⋅ ιn1 ,a1 )∣i [n1 + 1 ÐÐÐÐ→ γ]@(D2 ⋅ on2 ,a2 ,c2 )∣j [σ2 ]@M0 = M ′ .
As in the previous cases, one can show that [P [b ↦ c], Q]@C0 & M ′ .
Heating, (LH). We now consider the case of heating, i.e., when one has a transition
τ

C = (P ∣ Q)@C0 ←
Ð [P, Q]@C0 = C ′ .
τ

We want to show that there exists a transition M ←
Ð M ′ with [P, Q]@C0 & M ′ .
We now have to consider a few cases, depending on which rule is applied for P ∣ Q in
the proof of (P ∣ Q)@C0 & M . Notice that P ∣ Q cannot be of the form ζ(D)[σ]. We are
therefore left with two cases, depending on whether the first or third rule is applied.
● If the first rule is applied, we find M0 , γ ′ ⊢ P ′ ∣ Q′ , h∶ γ ′ −∼ n, and σ∶ n → γ such that
P ∣ Q = (P ′ ∣ Q′ )[σ ○ h] and M = ⟦P ′ ∣ Q′ ⟧h [σ]@M0 , with C0 & M0 . Letting D = ⟦P ′ ∣ Q′ ⟧h ,
we notice that
D = ⟨πnl ↦ ⟦P ′ ⟧h , πnr ↦ ⟦Q′ ⟧h ⟩.
Thus, there is a transition
τ

M ←
Ð M ′ = [⟦P ′ ⟧h [σ], ⟦Q′ ⟧h [σ]]@M0
with [P, Q]@C0 & M ′ , as desired.
● If the third rule is applied, we find M0 , n ⊢D D1 , D2 and σ∶ n → γ such that
P ∣ Q = (ζ(D1 ) ∣ ζ(D2 ))[σ]

72

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

and M = [D1 [σ], D2 [σ]]@M0 . We notice that [P, Q] = [ζ(D1 )[σ], ζ(D2 )[σ]], so [P, Q] &
τ
[D1 [σ], D2 [σ]], hence [P, Q]@C0 & M . The identity transition M ←
Ð M thus fits our
needs.
Nu, (LH). We now consider the case of a ν rule, i.e., when one has a transition
τ

C = ⟨γ∥νa.P +k R⟩@C0 ←
Ð ⟨γ, a∥P ⟩@C0 [γ ⊂ γ, a] = C ′ .
τ

We want to show that there exists a transition M ←
Ð M ′ with ⟨γ, a∥P ⟩@C0 [γ ⊂ γ, a] & M ′ .
We notice that νa.P +k R cannot be obtained from the third rule. We thus consider two
cases corresponding to the first and second rules.
● If the first rule is applied, there exist M0 , γ ′ ⊢ νa.P ′ +k R′ , h∶ γ ′ −∼ n, and σ∶ n → γ such
that M = ⟦νa.P ′ +k R′ ⟧h [σ]@M0 and
νa.P +k R = (νa.P ′ +k R′ )[σ ○ h].
h+1

We write D = ⟦νa.P ′ +k R′ ⟧h as ⟨νn ↦ ⟦P ′ ⟧h′ ⟩ ⊞ ⟦R′ ⟧h , where h′ is γ ′ , a ÐÐ→ n + 1. Thus,
there is a transition
σ+⌜a⌝

τ

M ←
Ð M ′ = ⟨γ, a∥⟦P ′ ⟧h′ [n + 1 ÐÐÐ→ γ, a]⟩@M0 [γ ⊂ γ, a]
and, modulo the fact that C & M implies C[σ] & M [σ], we have P @C0 [γ ⊂ γ, a] &
h′

σ+1

⟦P ′ ⟧h′ [σ + ⌜a⌝]@M0 [γ ⊂ γ, a] since P = P ′ [γ ′ , a Ð→ n + 1 ÐÐ→ γ, a], as desired.
● If the second rule is applied, there exist M0 , n ⊢D D, and σ∶ n → γ such that M =
ζ(D)[σ]@M0 and
νa.P +k R = ζ(D)[σ].
σ+⌈a⌉

Thus, there exists i ∈ ∣D ⋅ νn ∣ such that ζ((D ⋅ νn )∣i )[n + 1 ÐÐÐ→ γ, a] = P . There is thus a
transition
τ
M ←
Ð M ′ = ⟨γ, a∥(D ⋅ νn )∣i [σ + ⌜a⌝]⟩@M0 [γ ⊂ γ, a]
with P @C0 [γ ⊂ γ, a] & M ′ , as desired.
Tick and Tau, (LH). We now consider the cases ♡ and τ , i.e., when one has a transition
ξ

C = (ξ.P +k R)@C0 ←
Ð P @C0 ,
ξ

where ξ ∈ {♡, τ }. We want to show that there exists a transition M ←
Ð M ′ with P @C0 & M ′ .
Once again, the third rule could not have been applied, and we are left with two cases
corresponding to the first and second rules.
● If the first rule is applied, then we find M0 , γ ′ ⊢ ξ.P ′ +k R′ , h∶ γ ′ −∼ n, and σ∶ n → γ such
that M = ⟦ξ.P ′ +k R′ ⟧h [σ]@M0 , C0 & M0 , and
ξ.P +k R = (ξ.P ′ +k R′ )[σ ○ h].
We write D = ⟦ξ.P ′ +k R′ ⟧h as ⟨ξn ↦ ⟦P ′ ⟧h ⟩ ⊞ ⟦R′ ⟧h . Thus, there is a transition
ξ

M = D[σ]@M0 ←
Ð ⟦P ′ ⟧h [σ]@M0 = M ′ ,
with P = P ′ [σ ○ h] and thus P @C0 & M ′ , as desired.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

73

● If the second rule is applied, then we find M0 , n ⊢D D, and σ∶ n → γ such that C0 & M0 ,
M = D[σ]@M0 , and
ξ.P +k R = ζ(D)[σ].
Then, there exists i ∈ ∣D ⋅ ξn ∣ such that ζ((D ⋅ ξn )∣i )[σ] = P . Hence, there is a transition
ξ

M ←
Ð (D ⋅ ξn )∣i [σ]@M0 = M ′
with P @C0 & M ′ , as desired.
We have thus proved that (LH) holds. We now proceed with the case analysis for (RH).
Synchro, (RH). We start, once again, with the case of the synchronisation, i.e., when M
has the shape ⟨γ∥D1 [σ1 ], D2 [σ2 ]⟩@M0 and we consider a silent transition to
[σ1 ,⌜σ2 (b2 )⌝]

M ′ = ⟨γ∥(D1 ⋅ ιn1 ,a1 )∣i [n1 + 1 ÐÐÐÐÐÐÐ→ γ], (D2 ⋅ on2 ,a2 ,b2 )∣j [σ2 ]⟩@M0 ,
where ni ⊢D Di and σi ∶ ni → γ for i = 1, 2, σ1 (a1 ) = a = σ2 (a2 ), and σ2 (c2 ) = c. We want to
id

show that there exists a transition C ←Ð C ′ with C ′ & M ′ . There are exactly 10 cases here.
Firstly, we have the case where the third rule is applied to D1 [σ1 ], D2 [σ2 ]. Otherwise, one
could have used each of the three rules for &0 for each of D1 and D2 , yielding nine cases.
We start with the first case, and then treat the nine others.
● If the third rule is applied on D1 [σ1 ], D2 [σ2 ] (hence n1 = n2 = n and σ1 = σ2 = σ), then we
find C0 such that C0 & M0 and C = (ζ(D1 ) ∣ ζ(D2 ))[σ]@C0 . Then, we have a transition
id

(ζ(D1 ) ∣ ζ(D2 ))[σ]@C0 ←Ð [ζ(D1 )[σ1 ], ζ(D2 )[σ2 ]]@C0 .
Since the latter configuration is again related to M , this reduces to the case where the
second rule is applied for both D1 [σ1 ] and D2 [σ2 ].
● If the third rule is applied for D1 [σ1 ] and any of the three rules is applied for D2 [σ2 ],
then we find P , M1 , M2 , C0 , and n1 ⊢D D3 such that M1 has length 1 if the third rule is
also used for D2 and 0 otherwise, M0 = D3 [σ3 ]@M1 @M2 , P & D2 [σ2 ]@M1 , C0 & M2 , and
C = (ζ(D1 ) ∣ ζ(D3 ))[σ1 ]@P @C0 .
Thus, there is a transition
id

(ζ(D1 ) ∣ ζ(D3 ))[σ1 ]@P @C0 ←Ð [ζ(D1 )[σ1 ], ζ(D3 )[σ1 ]]@P @C0
which reduces this case to the one where the second rule is applied to D1 .
● If the third rule is applied for D2 [σ2 ] and any of the first two rules is applied for D1 , then
we find M1 , P , C0 , and n2 ⊢D D3 such that M0 = D3 [σ3 ]@M1 , P & D1 [σ1 ], C0 & M1 , and
C = (ζ(D2 ) ∣ ζ(D3 ))[σ2 ]@P @C0 . Again, we are reduced to the case where the second rule
is applied for D2 , using the transition
id

(ζ(D2 ) ∣ ζ(D3 ))[σ2 ]@P @C0 ←Ð [ζ(D2 )[σ2 ], ζ(D3 )[σ2 ]]@P @C0 .
In the remaining cases, we have C = P10 @P20 @C0 with Pi0 & Di [σi ] for i = 1, 2, and
C0 & M0 . We thus have four cases, described in Figure 10 just as we did in Figure 9.
● If the second rule is applied for both D1 and D2 , then there is a transition
id

C ←Ð C ′ = ζ((D1 ⋅ ιn1 ,a1 )∣i )[[σ1 , ⌈c⌉]]@ζ((D2 ⋅ on2 ,a2 ,c2 )∣j )[σ2 ]@M0
with C ′ & M ′ as desired.

74

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

D1

Case 1
Case 2
′
′
′
There exist γ1 ⊢ P1 = a1 (b).P1 +k1 R1 P10 = ζ(D1 )[σ1 ].
and h1 ∶ γ1′ −∼ n1 such that
P10 = P1 [σ1 ○ h1 ]
D1 = ⟦P1 ⟧h1

h1 (a′1 ) = a1
i ∈ ∣D1 ⋅ ιn1 ,a1 ∣

(D1 ⋅ ιn1 ,a1 )∣i = ⟦P1′ ⟧h′1
h1 +1

P2

where h′1 is γ1′ , b ÐÐ→ n1 + 1.
There exist γ2′ ⊢ P2 = a¯′2 ⟨c′ ⟩.P2′ +k2 R2 P20 = ζ(D2 )[σ2 ].
and h2 ∶ γ2′ −∼ n2 such that
h2 (a′2 ) = a2

P20 = P2 [σ2 ○ h2 ]
h2 (c′2 ) = c2

D2 = ⟦P2 ⟧h2

j ∈ ∣D2 ⋅ on2 ,a2 ,c2 ∣
(D2 ⋅ on2 ,a2 ,c2 )∣j = ⟦P2′ ⟧h2 .
Figure 10: Synchro, (RH) cases
● If we apply the second rule for D1 and the first rule for D2 , then there is a transition
id

C ←Ð C ′ = ζ((D1 ⋅ ιn1 ,a1 )∣i )[[σ1 , ⌈c⌉]]@P2′ [σ2 ○ h2 ]@C0
with C ′ & M ′ as desired.
● If the first rule is applied for both D1 and D2 , then we have a synchronisation between
P1 [σ1 ○ h1 ] and P2 [σ2 ○ h2 ]. In order to determine the result of this synchronisation we
need to choose a representative for P1 [σ1 ○ h1 ], i.e., pick a channel for what b becomes
after substitution. A reasonable choice here is γ + 1, we choose
P1 [σ1 ○ h1 ] = a(γ + 1).(P1′ [(σ1 + 1) ○ h′1 ]) +k1 R1 [σ1 ○ h1 ].
We thus have a transition to
C ′ = P1′ [(σ1 + 1) ○ h′1 ][γ + 1 ↦ c]@P2′ [σ2 ○ h2 ]@C0 .
But the diagram
n1 + 1

σ1 +1

γ+1
[γ+1↦c]

[σ1 ,⌜c⌝]

γ

commutes, so C ′ = P1′ [[σ1 , ⌜c⌝] ○ h′1 ]@P2′ [σ2 ○ h2 ]@C0 . Finally, we also know:
M ′ = ((D1 ⋅ ιn1 ,a1 )∣i )[[σ1 , ⌜c⌝]]@(D2 ⋅ on2 ,a2 ,c2 )∣j [σ2 ]@M0
= ⟦P1′ ⟧h′1 [[σ1 , ⌜c⌝]]@⟦P2′ ⟧h2 [σ2 ]@M0 ,
which entails C ′ & M ′ as desired.

AN INTENSIONALLY FULLY-ABSTRACT SHEAF MODEL FOR π

(EXPANDED VERSION)

75

● If we apply the first rule for D1 and the second rule for D2 , then, choosing the same
representative as before for P1 [σ1 ○ h1 ], there is a transition
id

C ←Ð P1′ [(σ1 + 1) ○ h′1 ][γ + 1 ↦ c]@ζ((D2 ⋅ on2 ,a2 ,c2 )∣j )[σ2 ]@C0 = C ′
satisfying C ′ & M ′ (for the same reason as in the last case).
Fork, (RH). We consider the case of a forking action, i.e., M = ⟨γ∥D[σ]⟩@M0 with n ⊢D D
and σ∶ n → γ, and we have a transition
id

⟨γ∥D[σ]⟩@M0 ←Ð ⟨γ∥(D ⋅ πnl )∣i [σ], (D ⋅ πnr )∣j [σ]⟩@M0
id

for some i and j. We want to show that there exists a transition C ←Ð C ′ with C ′ & M ′ .
We proceed by case analysis on the rule applied for D[σ] in the proof of C & M .
● If the first rule is applied, then we find C0 & M0 , γ ′ ⊢ P = P1 ∣ P2 , and h∶ γ ′ −∼ n such that
D = ⟦P ⟧h , C = P [σ ○ h]@C0 , (D ⋅ πnl )∣i = ⟦P1 ⟧h , and (D ⋅ πnr )∣j = ⟦P2 ⟧h .
Thus, there is a transition
id

P [σ ○ h]@C0 ←Ð P1 [σ ○ h]@P2 [σ ○ h]@C0 = C ′
with C ′ & M ′ as desired.
● If the second rule is applied, then we find C0 & M0 such that C = ζ(D)[σ]@C0 . Thus,
ζ(D)[σ] has the shape
τ.(ζ((D ⋅ πnl )∣i ∣ ζ((D ⋅ πnr )∣j )))[σ] +k R

(A.1)

so we have
ζ(D)[σ]@C0

id

←Ð (ζ((D ⋅ πnl )∣i ) ∣ ζ((D ⋅ πnr )∣j ))[σ]@C0 = C ′

with C ′ & M ′ (using the third rule) as desired.
● If the third rule is applied, then we find n ⊢D D′ , M1 , and C0 such that C0 & M1 ,
C = (ζ(D) ∣ ζ(D′ ))[σ]@C0 , and M0 = D′ [σ]@M1 . But then, as in the previous case,
ζ(D)[σ] has the shape (A.1) and we have transitions:
(ζ(D) ∣ ζ(D′ ))[σ]@C0

id

←Ð

ζ(D)[σ]@ζ(D′ )[σ]@C0

←Ð
=

ζ((D ⋅ πnl )∣i )[σ]@ζ((D ⋅ πnr )∣j )[σ]@ζ(D′ )[σ]@C0
C′

id 2

with C ′ & M ′ as desired.
Nu, (RH). We consider the case of a ν rule, i.e., one has a transition
σ+⌈a⌉

id

C = ⟨γ∥D[σ]⟩@M0 ←Ð ⟨γ∥(D ⋅ νn )∣i [n + 1 ÐÐÐ→ γ, a]⟩@M0 [γ ⊂ γ, a]
id

with n ⊢D D and σ∶ n → γ. We want to show that there exists a transition C ←Ð C ′ with
C ′ & M ′ . We again proceed by case analysis on the rule applied for D[σ].
● If the first rule is applied, then we find C0 & M0 , γ ′ ⊢ P = νa.P ′ +k R, and h∶ γ ′ −∼ n such
that C = P @C0 , D = ⟦P ⟧h and (D ⋅ νn )∣i = ⟦P ′ ⟧h+1 . There are thus transitions
id

h+1

σ+⌈a⌉

C = P [σ ○ h]@C0 ←Ð P ′ [γ ′ , a ÐÐ→ n + 1 ÐÐÐ→ γ, a]@C0 [γ ⊂ γ, a] = C ′

76

C. EBERHART, T. HIRSCHOWITZ, AND T. SEILLER

with C ′ & M ′ as desired.
● If the second rule is applied, then we find C0 & M0 such that C = ζ(D)[σ]@C0 , and there
is a transition
σ+⌈a⌉

id

ζ(D)[σ]@C0 ←Ð ζ((D ⋅ νn )∣i )[n + 1 ÐÐÐ→ γ, a]@C0 [γ ⊂ γ, a] = C ′
with C ′ & M ′ as desired.
● If the third rule is applied, then we find M1 , C0 , and n ⊢D D′ such that M0 = D′ [σ]@M1 ,
C0 & M1 , and C = (ζ(D) ∣ ζ(D′ ))[σ]@C0 . But then we have
(ζ(D) ∣ ζ(D′ ))[σ]@C0
id

←Ð ζ(D)[σ]@ζ(D′ )[σ]@C0
σ+⌈a⌉

id

←Ð ζ((D ⋅ νn )∣i )[n + 1 ÐÐÐ→ γ, a]@ζ(D′ )[σ][γ ⊂ γ, a]@C0 [γ ⊂ γ, a] = C ′
and C ′ & M ′ as desired.
Tick and Tau, (RH). We now consider the cases ♡ and τ , i.e., when one has a transition
ξ

⟨γ∥D[σ]⟩@M0 ←
Ð ⟨γ∥(D ⋅ ξn )∣i [σ]⟩@M0
where ξ ∈ {♡, τ }, with n ⊢D D and σ∶ n → γ. We want to show that there exists a transition
ξ

C ←
Ð C ′ with C ′ & M ′ . Again, we proceed by case analysis on the rule applied for D[σ].
● If the first rule is applied, we find C0 & M0 , γ ′ ⊢ P = ξ.P ′ +k R, and h∶ γ ′ −∼ n such that
C = P [σ ○ h]@C0 , D = ⟦P ⟧h [σ], and (D ⋅ ξn )∣i = ⟦P ′ ⟧h . But then we have
ξ

P [σ ○ h]@C0 ←
Ð P ′ [σ ○ h]@C0 & ⟦P ′ ⟧h [σ]@M0 ,
as expected.
● If the second rule is applied, then C = ζ(D)[σ]@C0 for some C0 & M0 and we have
ξ

ζ(D)[σ]@C0 ←
Ð ζ((D ⋅ ξn )∣i )[σ]@C0 & (D ⋅ ξn )∣i [σ]@M0 ,
as desired.
● Finally, if the third rule is applied, then we find C0 , M1 , and n ⊢D D′ such that C =
(ζ(D) ∣ ζ(D′ ))[σ]@C0 , M0 = D′ [σ]@M1 , and C0 & M1 . But then, we have
id

ξ

(ζ(D) ∣ ζ(D′ ))[σ]@C0 ←Ð ζ(D)[σ]@ζ(D′ )[σ]@C0 ←
Ð ζ((D ⋅ ξn )∣i )[σ]@ζ(D′ )[σ]@C0 = C ′
with C ′ & M ′ as desired.

