pith. sign in

arxiv: 2605.18496 · v1 · pith:FRGRQXJ6new · submitted 2026-05-18 · 💻 cs.LO · cs.PL

Wiring the Pi-calculus to Denotational Semantics

Ken Sakayori (UTokyo) , Davide Sangiorgi (OLAS , DISI) , Simon Castellan (EPICURE) , Pierre Clairambault (LIS , CNRS) This is my paper

Pith reviewed 2026-05-20 08:14 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords asynchronous pi-calculusdenotational semanticsbarbed congruenceSeely categorygame semanticsprocess calculicategorical modelswires
0
0 comments X

The pith

AWpi restricts input ownership and capabilities so wires behave as substitutions, forming a category for denotational semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents AWpi, a dialect of the asynchronous pi-calculus with single input ownership and unidirectional capabilities. These restrictions cause wire processes to act as substitutions when composed with AWpi processes. This turns the processes, up to barbed congruence, into morphisms of a category with types as objects and wires as identities. The construction further yields a relative Seely category to support higher-order features. The dialect maintains the expressiveness and operational theory of standard pi-calculus while linking to denotational semantics.

Core claim

The restrictions of single input ownership and unidirectional capabilities make every wire process behave as a substitution when composed with any AWpi process, thereby turning the processes (modulo barbed congruence) into the morphisms of a category whose objects are types, and further allowing the construction of a relative Seely category.

What carries the argument

Wire processes that forward messages between names, which act as substitutions under the single-ownership and unidirectional restrictions.

If this is right

  • AWpi processes can be interpreted as morphisms in a category with types as objects.
  • Common higher-order language features can be given denotational interpretations using the relative Seely category.
  • The operational semantics and barbed congruence can be developed similarly to ordinary pi-calculus.
  • Expressiveness is preserved, making AWpi a faithful extension.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Insights from game semantics can be directly applied to process calculi through this categorical structure.
  • This may enable new models for concurrent programming languages that combine operational and denotational views.
  • Similar restrictions could be explored in other process calculi to achieve categorical interpretations.

Load-bearing premise

The two syntactic restrictions preserve enough of the expressive power and algebraic properties of the ordinary asynchronous pi-calculus to justify it as a faithful extension.

What would settle it

An example of a computation or equivalence in the standard asynchronous pi-calculus that cannot be reproduced in AWpi, or a counterexample where a wire does not behave as a substitution under barbed congruence.

read the original abstract

We introduce a dialect of the Asynchronous pi-calculus, called AWpi, in which (1) an input name may be owned, at any time, by at most one process; (2) each name has either only the input or only the output capability. As a result, special processes called wires (aka forwarders, that is, processes that receive values at one name and re-transmit) behave as substitutions when composed with any AWpi process. Thus AWpi naturally yields a category, whose morphisms are AWpi processes (modulo the reference behavioural equivalence, barbed congruence) and whose objects are types; and where wires act as identity morphisms. We show that the category of processes can be further organised into (sub)categories with the structures needed for the interpretation of common higher-order language features in the literature by drawing on insights from game semantics; notably, we construct a relative Seely category, the categorical structure that concurrent game semantics has. At the same time, AWpi follows the tradition of ordinary pi-calculi in that expressiveness is preserved and the operational and algebraic theory are developed in a similar manner, notwithstanding substantial technical differences in their development and proofs. In short, the goal of AWpi is to remain faithful to the operational and algebraic tradition of the pi-calculi while connecting to the tradition of denotational models for programming languages.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces AWpi, a dialect of the asynchronous π-calculus enforcing at most one owner per input name and strictly unidirectional capabilities. It claims that these restrictions ensure wire processes (forwarders) behave as substitutions when composed with any AWpi process, so that processes modulo barbed congruence form the morphisms of a category whose objects are types, with wires as identities; the construction is then extended to a relative Seely category using insights from game semantics. The work asserts that expressiveness is preserved and that operational and algebraic theory can be developed analogously to standard π-calculi despite technical differences.

Significance. If the substitution property and category construction are rigorously established, the result would usefully link the operational tradition of the π-calculus to denotational models, in particular supplying the relative Seely structure employed in concurrent game semantics for higher-order features. The explicit syntactic restrictions that turn wires into identities constitute a concrete strength, as does the attempt to retain the standard development of barbed congruence and operational theory.

major comments (2)
  1. [wire-substitution lemma (§4 or §5)] The central claim that (x↔y) | P ≃ P{y/x} (barbed congruence) for every AWpi process P rests on the single-ownership rule never blocking a reduction or adding an observable that would occur in unrestricted Aπ. The manuscript must supply the full induction for the wire-substitution lemma (presumably §4 or §5) and show that any process excluded by the ownership restriction is already inexpressible under the unidirectional-capability discipline alone; otherwise the argument risks assuming uniqueness of owners before the wire is introduced.
  2. [expressiveness preservation (abstract and §3)] The claim that the two restrictions preserve enough expressiveness to justify calling AWpi a faithful extension (rather than a severe fragment) is load-bearing for the categorical interpretation. The paper must exhibit a concrete argument or counter-example showing that standard encodings relying on multiple parallel inputs on the same name (e.g., choice or replication) remain expressible under the uni-directional discipline, or else retract the faithfulness assertion.
minor comments (2)
  1. [Introduction] The abstract refers to 'substantial technical differences in their development and proofs' without enumerating them; a short paragraph in the introduction contrasting the barbed-congruence proof with the standard Aπ case would improve readability.
  2. [relative Seely category construction] Notation for the relative Seely structure (objects, morphisms, tensor, etc.) should be introduced with explicit reference to the corresponding AWpi processes or types before the construction is invoked.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The comments highlight important points for strengthening the rigor and clarity of our arguments. We address each major comment below and indicate the revisions planned for the next version of the manuscript.

read point-by-point responses

  1. Referee: [wire-substitution lemma (§4 or §5)] The central claim that (x↔y) | P ≃ P{y/x} (barbed congruence) for every AWpi process P rests on the single-ownership rule never blocking a reduction or adding an observable that would occur in unrestricted Aπ. The manuscript must supply the full induction for the wire-substitution lemma (presumably §4 or §5) and show that any process excluded by the ownership restriction is already inexpressible under the unidirectional-capability discipline alone; otherwise the argument risks assuming uniqueness of owners before the wire is introduced.

    Authors: We agree that the full inductive argument for the wire-substitution lemma must be presented explicitly. In the revised manuscript we will expand the proof in §4 to include the complete induction on process structure, with separate cases for the interaction between single ownership and reductions under the barbed congruence relation. We will also add a short subsection demonstrating that any configuration requiring multiple simultaneous owners on an input name is already ruled out by the unidirectional-capability discipline alone, because such a configuration would require an input capability to be duplicated in a way forbidden by the uni-directional rule. This shows the ownership restriction is not an independent assumption but a consequence of the capability discipline. revision: yes

  2. Referee: [expressiveness preservation (abstract and §3)] The claim that the two restrictions preserve enough expressiveness to justify calling AWpi a faithful extension (rather than a severe fragment) is load-bearing for the categorical interpretation. The paper must exhibit a concrete argument or counter-example showing that standard encodings relying on multiple parallel inputs on the same name (e.g., choice or replication) remain expressible under the uni-directional discipline, or else retract the faithfulness assertion.

    Authors: We accept that a concrete illustration is required to substantiate the expressiveness claim. The revised §3 will contain explicit encodings of standard choice and replication operators that avoid multiple parallel inputs on the same name. These encodings assign distinct owned input names to each branch and route values via wires, preserving the observable behaviour under barbed congruence. With this addition we maintain the assertion that AWpi remains a faithful extension; we do not retract it. revision: yes

Circularity Check

0 steps flagged

No significant circularity; construction rests on explicit syntactic restrictions and direct proofs

full rationale

The paper defines AWpi by two explicit syntactic restrictions (at most one owner per input name; strictly uni-directional capabilities) and then proves that wires behave as substitutions under barbed congruence for all processes in this fragment. This substitution property is established by induction over the restricted syntax rather than by re-using a fitted parameter or prior self-citation as a premise. The subsequent category whose morphisms are processes (modulo barbed congruence) and whose identities are wires follows directly from the proven substitution lemma; the relative Seely category is obtained by standard categorical constructions drawing on game-semantics insights. No load-bearing step reduces the claimed structures to a definition by construction or to an unverified self-citation chain. The preservation of expressiveness is argued via operational and algebraic development that parallels ordinary pi-calculi, keeping the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on the two syntactic restrictions being sufficient to make wires behave as substitutions and on the existence of a barbed congruence that respects the category structure; these are introduced by the paper rather than derived from prior literature.

axioms (2)
  • domain assumption Barbed congruence is a congruence on AWpi processes that respects the wire-substitution property.
    Invoked when the paper states that morphisms are processes modulo barbed congruence.
  • ad hoc to paper The two restrictions preserve enough expressiveness for typical concurrent programs.
    Stated as part of the goal to remain faithful to the pi-calculus tradition.
invented entities (1)
  • AWpi dialect no independent evidence
    purpose: Restricted pi-calculus in which wires act as substitutions
    New syntactic rules introduced to obtain the category structure.

pith-pipeline@v0.9.0 · 5799 in / 1577 out tokens · 37649 ms · 2026-05-20T08:14:58.241772+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    5 Roberto M

    doi:10.1007/3-540-63383-9\_92. 5 Roberto M. Amadio, Gérard Boudol, and Cédric Lhoussaine. The receptive distributed pi-calculus. ACM Trans. Program. Lang. Syst., 25(5):549–577, 2003.doi:10.1145/937563. 937564. K. Sakayori, D. Sangiorgi, S. Castellan and P. Clairambault 25 6 Nathanael Arkor and Dylan McDermott. The formal theory of relative monads.Journal ...

    work page doi:10.1007/3-540-63383-9 2003

  2. [2]

    Types for dyadic interaction

    doi:10.1007/3-540-57208-2\_10. 57 Davide Sangiorgi. Locality and interleaving semantics in calculi for mobile processes.Theor. Comput. Sci., 155(1):39–83, 1996.doi:10.1016/0304-3975(95)00020-8. 58 Davide Sangiorgi. 𝜋-Calculus, internal mobility, and agent-passing calculi.Theor. Comput. Sci., 167(1&2):235–274, 1996.doi:10.1016/0304-3975(96)00075-8. 59 Davi...

    work page doi:10.1007/3-540-57208-2 1996

  3. [3]

    A Additional material for Section 3 ▶ Definition 37(Structural congruence)

    doi:10.1016/S0304-3975(00)00310-8. A Additional material for Section 3 ▶ Definition 37(Structural congruence). Structural congruenceis the smallest congruence on processes induced by the following rules: 𝑃 | 0 ≡ 𝑃 𝑃 | 𝑄 ≡ 𝑄 | 𝑃 𝑃 | ( 𝑄 | 𝑅) ≡ ( 𝑃 | 𝑄) | 𝑅 𝑃 | 𝝂˘𝑎 𝑄 ≡ 𝝂˘𝑎 (𝑃 | 𝑄) if 𝑎, 𝑎c ∉ fn(𝑃) 𝝂˘𝑎 𝝂˘𝑐 𝑃 ≡ 𝝂˘𝑐 𝝂˘𝑎 𝑃 𝝂˘𝑎 0 ≡ 0 There is no unfolding of rep...

    work page doi:10.1016/s0304-3975(00)00310-8

  4. [4]

    𝑃 𝜇 − →𝑃′ implies that there is𝑄′ with 𝑄 b𝜇 − → 𝑄′ and 𝑃′ R 𝑄′

    work page

  5. [5]

    𝑃 expands 𝑄, written 𝑄 ≼s 𝑃, if 𝑃 R 𝑄, for some expansionR

    𝑄 𝜇 − →𝑄′ implies that there is𝑃′ with 𝑃 𝜇 = =⇒ 𝑃′ and 𝑃′ R 𝑄′. 𝑃 expands 𝑄, written 𝑄 ≼s 𝑃, if 𝑃 R 𝑄, for some expansionR. The definition of weak bisimulation up-to ≈s and ≼s is obtained from that of weak bisimulation by replacing the requirement𝑃′ R 𝑄′ (on the derivatives the challenge and response transitions), with𝑃′ ≈s R ≼s 𝑄′. ▶ Theorem 43(Soundness...

    work page

  6. [6]

    (𝑃; 𝛿) 𝑏⟨𝑐⟩ − − − → 𝑎 ( 𝑥 ) − − − − → (𝑃′′; 𝛿), for some𝑐, 𝑃′ with (𝑃′; 𝛿) ≡ ( 𝑃′′ {𝑐/𝑥}; 𝛿), or

    work page

  7. [7]

    Lemma 49 is a standard result for asynchronous calculi, relating visible and silent transitions

    (𝑃; 𝛿) 𝑏 (𝑐) − − − → 𝑎 ( 𝑥 ) − − − − → (𝑃′′; 𝛿′), for some˘𝑐, 𝑃′′, 𝛿′ with (𝑃′; 𝛿) ≡ ( 𝝂˘𝑐 𝑃 ′′ {𝑐/𝑥}; 𝛿′). Lemma 49 is a standard result for asynchronous calculi, relating visible and silent transitions. ▶ Lemma 49. Suppose 𝑎∗𝑏 ∈ 𝛿

    work page

  8. [8]

    If (𝑃; 𝛿) 𝑏⟨𝑐⟩ − − − → 𝑎 ( 𝑥 ) − − − − → (𝑃′; 𝛿), then also (𝑃; 𝛿) 𝜏 − → ≡ (𝑃′{𝑐/𝑥}; 𝛿)

    work page

  9. [9]

    Application of a substitution to a process does not diminish its capabilities for action

    If (𝑃; 𝛿) 𝑏 (𝑐) − − − → 𝑎 ( 𝑥 ) − − − − → (𝑃′; 𝛿′), then also (𝑃; 𝛿) 𝜏 − → ≡ (𝝂˘𝑐 𝑃 ′{𝑐/𝑥}; 𝛿). Application of a substitution to a process does not diminish its capabilities for action. A substitution 𝜎 agrees witha connection set𝛿 if 𝑎∗𝑏 ∈ 𝛿 implies that also𝜎(𝑎)∗𝜎(𝑏) ∈ 𝛿 holds. (We recall that a substitution acts on names of the same type.) ▶ Lemma 50. ...

    work page

  10. [10]

    If (𝑃; 𝛿) 𝑏⟨𝑐⟩ = = = =⇒ 𝑎 ( 𝑥 ) = = = = =⇒ ( 𝑃′; 𝛿) then also (𝑃; 𝛿) 𝜏 = =⇒≡ ( 𝑃′{𝑐/𝑥}; 𝛿)

    work page

  11. [11]

    If (𝑃; 𝛿) 𝑏 (𝑐) = = = =⇒ 𝑎 ( 𝑥 ) = = = = =⇒ ( 𝑃′; 𝛿′) then also (𝑃; 𝛿) 𝜏 = =⇒≡ ( 𝝂˘𝑐 (𝑃′{𝑐/𝑥}); 𝛿). As a final example of transfer of results concerning transitions, we mention the Harmony Lemma, relating reductions in the reduction semantics and𝜏-transitions in the LTS of a process calculus [60]. Indeed, the correspondence between transitions in the LTS ...

    work page

  12. [12]

    𝑃 | ( 𝑄1 | 𝑄2)) Δ 𝝂˘𝑎 (!𝑎(𝑥)

    𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | ( 𝑄1 | 𝑄2)) Δ 𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | 𝑄1) | 𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | 𝑄2)

    work page

  13. [13]

    𝑃 | 𝑏(𝑦)

    𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | 𝑏(𝑦). 𝑄) Δ 𝑏(𝑦). 𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | 𝑄)

    work page

  14. [14]

    𝑃 | !𝑏(𝑦)

    𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | !𝑏(𝑦). 𝑄) Δ !𝑏(𝑦). 𝝂˘𝑎 (!𝑎(𝑥). 𝑃 | 𝑄)

    work page

  15. [15]

    𝑃 | 𝑎c⟨𝑣⟩) Δ 𝝂˘𝑎 (𝑃{𝑣/𝑥})

    𝝂˘𝑎 (𝑎(𝑥). 𝑃 | 𝑎c⟨𝑣⟩) Δ 𝝂˘𝑎 (𝑃{𝑣/𝑥}). The first three laws are often called ‘replication theorems’. To derive law (1) in the corollary from 𝜋-calculus laws, we have however first to apply Lemma 7 (for O-names) so to make sure that name𝑎c is never exported within𝑃, 𝑄1 and 𝑄2. 34 Wiring the 𝜋-calculus to Denotational Semantics C Internal processes C.1 Trans...

    work page

  16. [16]

    𝑃 ≡ 𝝂e𝑧 (𝝂˘𝑐 (𝑎⟨𝑐⟩ | 𝑐c ⋄ 𝑏) | 𝑃2), and 𝑃1 ≡ ( 𝝂e𝑧) ( 𝑐c ⋄ 𝑏) | 𝑃2), for some e𝑧, 𝑏, 𝑃2 with {𝑎, 𝑐, 𝑐 c} ∩ e𝑧 = ∅and 𝑐, 𝑐c ∉ fn(𝑃2)

    work page

  17. [17]

    Sakayori, D

    𝑃 ≈s 𝝂˘𝑐 ( [[𝑎⟨𝑐⟩] ] | 𝑃1) K. Sakayori, D. Sangiorgi, S. Castellan and P. Clairambault 35 The other relevant lemma about bound outputs for internal processes is Lemma 14 in the main text. Its proof is a straightforward transition induction. The lemma is important for defining proof techniques about process behaviours. One of the reasons is that, as hinted...

    work page

  18. [18]

    𝛿 ⊢ 𝝂e𝑎∗e𝑎′ 𝑃 =⇒ 𝝂e𝑎∗e𝑎′ 𝑃′

    work page

  19. [19]

    The following lemma transport Lemma 52 to the LTS for plain (as opposed to composite) internal processes

    𝛿, e𝑎∗e𝑎′ ⊢ 𝝂e𝑧 𝑃 =⇒ 𝝂e𝑧 𝑃 ′, fore𝑧 ∩n(𝛿, e𝑎∗e𝑎′) = ∅. The following lemma transport Lemma 52 to the LTS for plain (as opposed to composite) internal processes. ▶ Lemma 65. Suppose 𝑎∗𝑏 ∈ 𝛿

    work page

  20. [20]

    If 𝛿 ⊢ 𝑃 𝑏⟨𝑐⟩ = = = =⇒ 𝑃1 and 𝛿 ⊢ 𝑃1 𝑎 ( 𝑥 ) = = = = =⇒ 𝑃′ then also 𝛿 ⊢ 𝑃 𝜏 = =⇒ 𝑃′{𝑐/𝑥}

    work page

  21. [21]

    C.3 Some results on internal bisimulation ▶ Lemma 66

    If 𝛿 ⊢ 𝑃 𝑏 (𝑐) = = = =⇒ 𝑃1 and 𝛿 ⊢ 𝑃1 𝑎 ( 𝑥 ) = = = = =⇒ 𝑃′ then also 𝛿 ⊢ 𝑃 𝜏 = =⇒ 𝝂˘𝑐 (𝑃′{𝑐/𝑥}). C.3 Some results on internal bisimulation ▶ Lemma 66. If 𝑎 ∉ n(𝛿) and 𝑐 is fresh, and𝑃 ≈ 𝛿 𝑄, then also𝑃{𝑐/𝑎} ≈ 𝛿 𝑄{𝑐/𝑎}. We will need some ‘up-to’ proof of technique for internal bisimulation: 36 Wiring the 𝜋-calculus to Denotational Semantics internal bisim...

    work page

  22. [22]

    Then 𝛿 ⊢ 𝑄 =⇒ 𝑄′ with 𝝂˘𝑐 (𝑃2{𝑐/𝑥}) ≈ 𝛿,e𝑎∗e𝑎′ 𝑄′ It also holds𝛿 ⊢ 𝝂e𝑥 𝑄𝜎 =⇒ 𝝂e𝑥 𝑄 ′𝜎 and we are done, as 𝑃★ = 𝝂e𝑥 (( 𝝂˘𝑐 𝑃2{𝑐/𝑥})𝜎) R 𝛿 𝝂e𝑥 (𝑄′𝜎) K

    If 𝑃 𝑎′ (𝑐) − − − − →𝑃1 𝑎 ( 𝑥 ) − − − − →𝑃2, since 𝑎∗𝑎′ ∈ 𝛿, we also have𝛿 ⊢ 𝑃 𝜏 − →𝝂˘𝑐 (𝑃2{𝑐/𝑥}). Then 𝛿 ⊢ 𝑄 =⇒ 𝑄′ with 𝝂˘𝑐 (𝑃2{𝑐/𝑥}) ≈ 𝛿,e𝑎∗e𝑎′ 𝑄′ It also holds𝛿 ⊢ 𝝂e𝑥 𝑄𝜎 =⇒ 𝝂e𝑥 𝑄 ′𝜎 and we are done, as 𝑃★ = 𝝂e𝑥 (( 𝝂˘𝑐 𝑃2{𝑐/𝑥})𝜎) R 𝛿 𝝂e𝑥 (𝑄′𝜎) K. Sakayori, D. Sangiorgi, S. Castellan and P. Clairambault 37

    work page

  23. [23]

    From Corollary 63, We also have 𝛿, e𝑎∗e𝑏 ⊢ 𝑄𝜎 𝑏 (𝑐) = = = =⇒ 𝑄1𝜎

    If 𝑃 𝑏 (𝑐) − − − →𝑃1 𝑎 ( 𝑥 ) − − − − →𝑃2, since 𝑃 ≈ 𝛿,e𝑎∗e𝑎′ 𝑄, and 𝑏 ∉ n(𝛿, e𝑎∗e𝑎′), there is 𝛿, e𝑎∗e𝑎′ ⊢ 𝑄 𝑏 (𝑐) = = = =⇒ 𝑄1 with 𝑃1 ≈ 𝛿,e𝑎∗e𝑎′ 𝑄1. From Corollary 63, We also have 𝛿, e𝑎∗e𝑏 ⊢ 𝑄𝜎 𝑏 (𝑐) = = = =⇒ 𝑄1𝜎. (4) Given the challenge𝛿, e𝑎∗e𝑎′ ⊢ 𝑃1 𝑎 ( 𝑥 ) − − − − →𝑃2, we have two subcases for𝑄1: a. 𝛿, e𝑎∗e𝑎′ ⊢ 𝑄1 𝑎 ( 𝑥 ) = = = = =⇒ 𝑄2 and 𝑃2 ≈ 𝛿,e𝑎∗...

    work page

  24. [24]

    Then, since𝑐 is fresh for𝑃1, 𝑄1 (Lemma 14), by Lemma 66 also𝑃2{𝑐/𝑥} ≈ 𝛿,e𝑎∗e𝑎′ 𝑄2{𝑐/𝑥}

    𝛿, e𝑎∗e𝑎′ ⊢ 𝑄1 𝑎 ( 𝑥 ) = = = = =⇒ 𝑄2 and 𝑃2 ≈ 𝛿,e𝑎∗e𝑎′ 𝑄2. Then, since𝑐 is fresh for𝑃1, 𝑄1 (Lemma 14), by Lemma 66 also𝑃2{𝑐/𝑥} ≈ 𝛿,e𝑎∗e𝑎′ 𝑄2{𝑐/𝑥}. Moreover, reasoning as in the previous case, 𝛿, e𝑎∗e𝑏 ⊢ 𝑄1𝜎 𝑎 ( 𝑥 ) = = = = =⇒ 𝑄2𝜎, and also 𝛿 ⊢ 𝝂e𝑥 (𝑄𝜎) =⇒ 𝝂e𝑥 𝝂˘𝑐 (𝑄2𝜎{𝑐/𝑥}). We can thus conclude (𝛿, 𝝂e𝑥 𝝂˘𝑐 (𝑃2{𝑐/𝑥}𝜎), 𝝂e𝑥 𝝂˘𝑐 (𝑄2{𝑐/𝑥}𝜎) ∈ R

    work page

  25. [25]

    We recall that we have𝑎 ∉ e𝑎

    The answer from𝑄1 does not involve an input action. We recall that we have𝑎 ∉ e𝑎. We have 𝛿, e𝑎∗e𝑎′ ⊢ 𝑄1 =⇒ 𝑄2 and 𝑃2 ≈ 𝛿,e𝑎∗e𝑎′ ,𝑎∗𝑎′′ [[𝑎′′ ⟨𝑥⟩] ] | 𝑄2, where 𝑎′′ is fresh. Again, we can apply an injective substitution and derive 𝑃2{𝑐/𝑥} ≈ 𝛿,e𝑎∗e𝑎′ ,𝑎∗𝑎′′ ( [[𝑎′′ ⟨𝑥⟩] ] | 𝑄2){ 𝑐/𝑥}. = [[𝑎′′ ⟨𝑐⟩] ] | 𝑄2 (6) Since 𝛿, e𝑎∗e𝑎′ ⊢ 𝑄 𝑏 (𝑐) = = = =⇒ 𝑄1, employin...

    work page

  26. [26]

    The most interesting case is a𝜏 action from 𝑃 stemming from an interaction along names in e𝑥

    Action from 𝑅 or 𝑃 alone: this case is easy. The most interesting case is a𝜏 action from 𝑃 stemming from an interaction along names in e𝑥. We can then infer an answer from𝑄 using the fact thate𝑥 appears in 𝛿′

    work page

  27. [27]

    In this case the input must originate from𝑃 (as 𝑃 owns the input end)

    Interaction between 𝑃 and 𝑅 along names ine𝑥. In this case the input must originate from𝑃 (as 𝑃 owns the input end). Thus let𝑎, 𝑎c be the names involved, and suppose𝑃 𝑎 (𝑐) − − − →𝑃′, and 𝑅 𝑎c (𝑐) − − − − →𝑅′, and 𝛿 ⊢ 𝝂e𝑧 (𝑃 | 𝑅) 𝜏 − → 𝝂e𝑧 𝝂˘𝑐 (𝑃′ | 𝑅′) ≡ 𝝂˘𝑐 𝝂e𝑧 (𝑃′ | 𝑅′). Since 𝑃 ≈ 𝛿′ 𝑄, we have two cases. a. 𝛿′ ⊢ 𝑄 𝑎 (𝑐) = = = =⇒ 𝑄′ with 𝑃′ ≈ 𝛿′ 𝑄′. We...

    work page

  28. [28]

    Let𝑎, 𝑎c the names involved, and suppose𝑃 𝑎 (𝑐) − − − →𝑃′, and 𝑅 𝑎c (𝑐) − − − − →𝑅′, and 𝛿 ⊢ 𝝂e𝑧 (𝑃 | 𝑅) 𝜏 − →𝝂e𝑧 𝝂˘𝑐 (𝑃′ | 𝑅′)

    Interaction between 𝑃 and 𝑅 along names ine𝑦 in which 𝑃 makes the input. Let𝑎, 𝑎c the names involved, and suppose𝑃 𝑎 (𝑐) − − − →𝑃′, and 𝑅 𝑎c (𝑐) − − − − →𝑅′, and 𝛿 ⊢ 𝝂e𝑧 (𝑃 | 𝑅) 𝜏 − →𝝂e𝑧 𝝂˘𝑐 (𝑃′ | 𝑅′). We know that𝑎c does not appear in𝑃, 𝑄. Again, as 𝑃 ≈ 𝛿′ 𝑄, we have two cases. a. 𝛿′ ⊢ 𝑄 𝑎 (𝑐) = = = =⇒ 𝑄′ with 𝑃′ ≈ 𝛿′ 𝑄′. We have𝛿 ⊢ 𝝂e𝑧 (𝑄 | 𝑅) 𝜏 =⇒≡ 𝝂˘𝑐...

    work page

  29. [29]

    Let𝑎, 𝑎c the names involved; we have𝑃 𝑎c (𝑐) − − − − →𝑃′, and 𝑅 𝑎 (𝑐) − − − →𝑅′, and 𝛿 ⊢ 𝝂e𝑧 (𝑃 | 𝑅) 𝜏 − →𝝂e𝑧 𝝂˘𝑐 (𝑃′ | 𝑅′) ≡ 𝝂˘𝑐 𝝂e𝑧 (𝑃′ | 𝑅′)

    Interaction between 𝑃 and 𝑅 along names ine𝑦 in which 𝑃 makes the output. Let𝑎, 𝑎c the names involved; we have𝑃 𝑎c (𝑐) − − − − →𝑃′, and 𝑅 𝑎 (𝑐) − − − →𝑅′, and 𝛿 ⊢ 𝝂e𝑧 (𝑃 | 𝑅) 𝜏 − →𝝂e𝑧 𝝂˘𝑐 (𝑃′ | 𝑅′) ≡ 𝝂˘𝑐 𝝂e𝑧 (𝑃′ | 𝑅′). Since 𝑃 ≈ 𝛿′ 𝑄 and 𝑎∗𝑎c ∉ 𝛿′, it holds that𝛿′ ⊢ 𝑄 𝑎c (𝑐) = = = = =⇒ 𝑄′ with 𝑃′ ≈ 𝛿′ 𝑄′. Hence also 𝛿 ⊢ 𝝂e𝑧 (𝑄 | 𝑅) 𝜏 =⇒ 𝝂e𝑧 𝝂˘𝑐 (𝑄′ | 𝑅′) ...

    work page

  30. [30]

    If 𝛿 ⊢ 𝑃 𝜏 − →𝑃′, then there is𝑄′ such that 𝛿 ⊢ 𝑄 =⇒ 𝑄′ and 𝑃′ ≈Δ 𝛿,𝑛 −1 𝑄′

    work page

  31. [31]

    if 𝛿 ⊢ 𝑃 𝑏 (𝑐) − − − →𝑃′ and 𝑏 ∉ n(𝛿), then there is 𝑄′ such that 𝛿 ⊢ 𝑄 𝑏 (𝑐) = = = =⇒ 𝑄′ and 𝑃′ ≈Δ′ 𝛿,𝑛 −1 𝑄′, where Δ′ is the extension ofΔ in which the appropriate type for𝑐c is added

    work page

  32. [32]

    either 𝛿 ⊢ 𝑄 𝑎 (𝑐) = = = =⇒ 𝑄′ and 𝑃′ ≈Δ′ 𝛿,𝑛 −1 𝑄′, b

    If 𝛿 ⊢ 𝑃 𝑎 (𝑐) − − − →𝑃′, and Δ′ is the extension ofΔ in which the appropriate type for𝑐 is added, then there is𝑄′ such that: a. either 𝛿 ⊢ 𝑄 𝑎 (𝑐) = = = =⇒ 𝑄′ and 𝑃′ ≈Δ′ 𝛿,𝑛 −1 𝑄′, b. or 𝛿 ⊢ 𝑄 =⇒ 𝑄′ and, either i. 𝑎∗𝑎′ ∈ 𝛿, for some𝑎′, and 𝑃′ ≈Δ′ 𝛿,𝑛 −1 (𝑄′ | [[ 𝑎′ ⟨𝑐⟩] ]), or ii. 𝑎 ∉ n(𝛿) and 𝑃′ ≈Δ′′ 𝛿,𝑎 ∗𝑎′ ,𝑛 −1 (𝑄′ | [[ 𝑎′ ⟨𝑐⟩] ]), for 𝑎′ fresh, and ...

    work page

  33. [33]

    𝜇 = 𝜏. Then ∅ ⊢ 𝝂e𝑥 (𝑃 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ ∼ s 𝝂e𝑥 (𝑃 | ( 𝑐 𝜏𝑛 ⊕ 𝑅(𝑛 − 1, 𝐴))) To match this reduction (up to barbed bisimulation) we must have: ∅ ⊢ 𝝂e𝑥 (𝑄 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ s≽ 𝝂e𝑥 (𝑄1 | ( 𝑐 𝜏𝑛 ⊕ 𝑅(𝑛 − 1, 𝐴))) with e𝑥 ⊢ 𝑄 =⇒ 𝑄1, and hence also 𝛿 ⊢ 𝑄 =⇒ 𝑄1 (Lemma 73). We make a further reduction: 𝝂e𝑥 (𝑃 | ( 𝑐 𝜏𝑛 ⊕ 𝑅(𝑛 − 1, 𝐴)) 𝜏 =⇒ ∼ s 𝝂e𝑥 (𝑃′ | 𝑅(𝑛 − 1, 𝐴)) Aga...

    work page

  34. [34]

    Moreover we assume that 𝑐 is an O-name

    𝜇 = 𝑏(𝑐), and there is 𝑎 with 𝑎∗𝑏 ∈ e𝑥 and 𝑎 ∈ 𝐴. Moreover we assume that 𝑐 is an O-name. We may also suppose𝑐 ∉ fn(𝑄). Then ∅ ⊢ 𝝂e𝑥 (𝑃 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ ∼ s 𝝂e𝑥 (𝑃 | 𝑐𝑎𝑛 ⊕ 𝑎(𝑥). 𝑅(𝑛 − 1, 𝐴 ∪ {𝑥}))) This has to be matched by: ∅ ⊢ 𝝂e𝑥 (𝑄 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ s≽ 𝝂e𝑥 (𝑄1 | ( 𝑐𝑎𝑛 ⊕ 𝑎(𝑥). 𝑅(𝑛 − 1, 𝐴 ∪ {𝑥}))) with 𝛿 ⊢ 𝑄 =⇒ 𝑄1. We take some further steps: ∅ ⊢ 𝝂e𝑥 (𝑃 | ...

    work page

  35. [35]

    We reason as in the previous case

    The same case as before, that is,𝜇 = 𝑏(𝑐), but 𝑐 is an I-name. We reason as in the previous case

    work page

  36. [36]

    We let 𝐵 = {𝑎′ c}

    𝜇 = 𝑎c (𝑎′), and there is 𝑎 with 𝑎c∗𝑎 ∈ e𝑥 and 𝑎 ∈ 𝐴; we assume 𝑎′, 𝑎′ c fresh. We let 𝐵 = {𝑎′ c} . We have ∅ ⊢ 𝝂e𝑥 (𝑃 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ ∼ s 𝝂e𝑥 (𝑃 | ( 𝑐𝑎𝑛 ⊕ 𝑎(𝑎′) : 𝑅(𝑛 − 1, 𝐴 ∪ 𝐵))) This has to be matched by ∅ ⊢ 𝝂e𝑥 (𝑄 | 𝑅(𝑛, 𝐴)) 𝜏 =⇒ s≽ 𝝂e𝑥 (𝑄1 | ( 𝑐𝑎𝑛 ⊕ 𝑎(𝑎′) : 𝑅(𝑛 − 1, 𝐴 ∪ 𝐵))) K. Sakayori, D. Sangiorgi, S. Castellan and P. Clairambault 43 (as before, ...

    work page

  37. [38]

    It is worth emphasizing that interaction between𝐶 and the process inside the context using the names 𝑏, 𝑏 c does not happen due to the 1-input property

    The interaction happens between𝐶 and the process inside the context using the name𝑎. It is worth emphasizing that interaction between𝐶 and the process inside the context using the names 𝑏, 𝑏 c does not happen due to the 1-input property. The proof for the first case is trivial since we can simply match the transition with𝐶 − →𝐶′; note that𝐶′ is a context ...

    work page

  38. [39]

    That is,𝐶 − →𝐶′

    The interaction occurs in𝐶. That is,𝐶 − →𝐶′

    work page

  39. [40]

    The interaction happens between𝐶 and the process inside the context using the name𝑎

    work page

  40. [41]

    The proof for the first two cases is essentially identical to what we have done above

    The interaction happens between𝐶 and the process inside the context using the name𝑏. The proof for the first two cases is essentially identical to what we have done above. Therefore we only consider the third case. In this case, the context must be of the form 𝝂˘𝑏 (𝝂e𝑧) ( 𝑄 | 𝑏c⟨𝑥𝑛+1⟩ | [·]) and the reduction must be of the form 𝝂˘𝑏 (𝝂e𝑧) ( 𝑄 | 𝑏c⟨𝑥𝑛+1⟩ |...

    work page

  41. [42]

    Input at 𝑎 from 𝑄2

    In this case, 𝑄2 need not move, using clause 3.b.i of Definition 15, as𝑄′′ 1 R 𝛿 ( [[𝑏c⟨𝑐⟩] ] | 𝑃){ 𝑎, 𝑎c/𝑏, 𝑏c}. Input at 𝑎 from 𝑄2. For this case, we split the base and the inductive case. The base case is where the input action is simply𝑎. It must be the case that 𝑃 ≡ 𝝂e𝑧 (𝑏. 𝑃1 | 𝑃2), and the derivative for𝑄2 is 𝝂e𝑧 (𝑃1 | 𝑃2){ 𝑎, 𝑎c/𝑏, 𝑏c}. We have an...

    work page

  42. [43]

    derℓi (𝑇 ) † = id i 𝑇

    work page

  43. [44]

    We already proved 1 in the body of the paper

    (𝑃†; 𝑄)† = 𝑃†; 𝑄† Proof. We already proved 1 in the body of the paper. The law 2 holds because !𝑐(𝑥). 𝝂˘𝑏 (𝑏(𝑥). 𝑎⟨𝑥⟩ | 𝑏c⟨𝑥⟩) s≽ !𝑐(𝑥). 𝑎⟨𝑥⟩. Now we prove the law 3. Let𝑃: 𝑎 : i 𝑆 → 𝑏 : ℓi (𝑇) and 𝑄 : 𝑐 : i 𝑇 → 𝑑 : ℓi (𝑈). Observe that (𝑃†; 𝑄) † : 𝑎 : i 𝑆 → 𝑒 : i 𝑈 = !𝑒(𝑥). 𝝂𝑑, 𝑑 ′ (𝝂𝑐′, 𝑐 (!𝑐′ (𝑥). 𝝂𝑏, 𝑏 ′ (𝑃 | 𝑏′ ⟨𝑥⟩) | 𝑄) | 𝑑′ ⟨𝑥⟩) s≽ !𝑒(𝑥). 𝝂𝑑, 𝑑 ′ (...

    work page