pith. sign in

arxiv: 2605.23031 · v1 · pith:IZNGAIOCnew · submitted 2026-05-21 · 💻 cs.PL

Step in Tine: Forking Processes in Functional Choreographies

Ashley Samuelson , Andrew K. Hirsch , Ethan Cecchetti This is my paper

Pith reviewed 2026-05-25 04:59 UTC · model grok-4.3

classification 💻 cs.PL
keywords choreographic programmingprocess forkingdeadlock freedomfunctional programmingconcurrent programmingprocess calculustype systems
0
0 comments X

The pith

λ⤊ is the first functional choreographic language that adds dynamic process forking while keeping deadlock freedom and a single centralized program.

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

Choreographic programming lets one program describe an entire concurrent system and then projects it into separate code for each participant. This makes deadlock freedom easier to guarantee but has made it hard to add forking, the ability to create new processes at runtime. The paper defines λ⤊ to close that gap. In λ⤊ a process can decide during execution when to spawn another process, what code that process will run, and which channels it will use. The resulting language still projects cleanly from the central program and still guarantees deadlock freedom for well-typed programs, supporting examples such as adaptive load balancers and recursive parallel divide-and-conquer.

Core claim

The paper presents λ⤊ as a functional choreographic calculus whose operational semantics and type system incorporate a fork primitive. The primitive lets one participant create a new participant whose behavior and communication partners are chosen at runtime. Projection from the global choreography to local processes remains well-defined, and the type system ensures that every well-typed program, including those that fork, is free of deadlocks.

What carries the argument

The fork primitive together with the associated typing rules that track participant identities and channel usage so that dynamic spawning preserves both projection and deadlock freedom.

If this is right

  • Load-balancer code can be written as one program that forks extra worker processes when demand rises.
  • Divide-and-conquer algorithms can spawn parallel subproblems at runtime while the deadlock guarantee still holds.
  • Communication topologies can be decided during execution rather than fixed in advance.
  • The centralized model continues to simplify reasoning about systems whose size and structure are not known statically.

Where Pith is reading between the lines

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

  • Similar forking mechanisms could be added to choreographic languages that already handle session types or multiparty protocols.
  • The same centralized-plus-forking style might simplify verification of elastic cloud services whose process count changes with load.
  • Once forking is supported, other dynamic operations such as process migration or channel passing may become expressible under the same deadlock guarantee.

Load-bearing premise

It is possible to add a forking primitive to a choreographic language without losing either the centralized single-program view or the deadlock-freedom guarantee.

What would settle it

A concrete, well-typed λ⤊ program whose projection contains a deadlock, or a useful forking pattern that cannot be expressed in λ⤊ without violating the type system.

Figures

Figures reproduced from arXiv: 2605.23031 by Andrew K. Hirsch, Ashley Samuelson, Ethan Cecchetti.

Figure 1
Figure 1. Figure 1: Example Local Language Syntax. We require that, if isSum(𝑠, 𝑡1, 𝑡2) and ⊩ 𝑣 : 𝑠 for a value 𝑣, then either getCase(𝑣) = inl(𝑣1) with ⊩ 𝑣1 : 𝑡1 or getCase(𝑣) = inr(𝑣2) with ⊩ 𝑣2 : 𝑡2. On other expressions, it may be undefined. We support first-class process names identically to 𝜆qc. Specifically, the local language has two types loc𝜌 and locset𝜌 defining first-class representations of location names and set… view at source ↗
Figure 2
Figure 2. Figure 2: Syntax of Choreographies in 𝜆⋔. computations, process polymorphism, and first-class process names—and retain the traditional deadlock-freedom guarantee of choreographic languages. 4.1 𝜆⋔ Syntax [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Selected Redices and Location Function Rules. Here [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Selected 𝜆⋔ Operational Semantics in the branches is safe when both (1) the locations involved in the step are disjoint from those computing the scrutinee (similarly to C-LetI), and (2) the step will occur regardless of the branch taken. The latter point is enforced by requiring identical redices and updates to the set of executing locations in the step in both branches. The result is the following C-Local… view at source ↗
Figure 5
Figure 5. Figure 5: Syntax of Types and Kinds. Here 𝛼 is a type variable. named locations function NL(𝜌) homomorphically collects all concrete location names appearing in the set. Its full definition can be found in Appendix D.4. The final two rules formalize how 𝜆⋔ spawns and kills new locations. To spawn a location, C-Fork selects a globally fresh location name 𝐿 ′ and binds 𝛼 to 𝐿 ′ and 𝑥 to its representation ⌈𝐿 ′ ⌋ in th… view at source ↗
Figure 6
Figure 6. Figure 6: Selected 𝜆⋔ Typing Rules Here A spawns a thread 𝛼 who then immediately dies, as the body of the fork expression—the 𝜆-abstraction—is a value. However, the returned abstraction closes over 𝛼 and, if applied, would send a message to 𝛼—which is now dead—causing deadlock. The 𝜆⋔ type system has two key features to prevent this scenario. First, it uses 𝜌 to track which locations might participate in a choreogra… view at source ↗
Figure 7
Figure 7. Figure 7: Selected Network Program Syntax. Here 𝐿 ∈ L is a concrete location name. The return expression ret(𝑒) is used to execute and yield the output of a local expression 𝑒, mirroring the choreography 𝜌.𝑒. To account for a location 𝐿 ∉ 𝜌—who should not execute 𝑒—and other scenarios where a location is not involved in part of the overall choreography, we include a unit value () which does nothing. To model message… view at source ↗
Figure 8
Figure 8. Figure 8: Selected Network Language Operational Semantics [PITH_FULL_IMAGE:figures/full_fig_p019_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: System Semantics and Labels a system Π = ∥𝐿∈Ω (𝐿 ⊲ 𝐸𝐿) as a map from each location 𝐿 in a finite set Ω ⊂ L to the network program 𝐸𝐿 it is currently executing. The operational semantics of systems are shown in [PITH_FULL_IMAGE:figures/full_fig_p020_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Selected EPP Definitions is similar, where locations involved in the function body should apply the function, while other locations can simply sequence the function and its argument, afterwards returning a unit value. The projection of functions requires an additional check compared to previous work—that the body projects for everyone—for reasons described below. Type functions project to network type fun… view at source ↗
read the original abstract

Traditional concurrent-programming techniques require programmers to painstakingly write programs for each participant in a concurrent system. Choreographic programming, in contrast, allows a programmer to write one centralized program and compile it to individual programs. This approach simplifies critical properties like deadlock freedom, but it complicates forking new processes, a core primitive in concurrent programming. This work addresses that gap with the choreographic fork calculus $\lambda{\pitchfork}$, the first functional choreographic language with process forking. $\lambda{\pitchfork}$ provides a deadlock-freedom guarantee while allowing programs to dynamically determine when to spawn new processes, what they will do, and who will communicate with them. In doing so, it supports practical applications like load balancers and parallel divide-and-conquer.

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

1 major / 0 minor

Summary. The manuscript introduces the choreographic fork calculus λ⤊ as the first functional choreographic language with a forking primitive. It claims this extension preserves the centralized programming model and provides a deadlock-freedom guarantee while supporting fully dynamic decisions on when to spawn processes, what they compute, and with whom they communicate, enabling applications such as load balancers and parallel divide-and-conquer.

Significance. If the deadlock-freedom result holds with the dynamic forking primitive, the work would address a recognized limitation in choreographic programming by enabling forking without sacrificing safety properties or the single-program model. The emphasis on fully dynamic spawn decisions strengthens its relevance to practical concurrent systems.

major comments (1)
  1. [Abstract] Abstract: the central claim of a deadlock-freedom guarantee for the forking extension is asserted without any proof outline, typing rules, or reduction semantics, leaving the soundness of the key technical result unevidenced and load-bearing for the contribution.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their feedback. The single major comment concerns the level of technical detail in the abstract. We address it point-by-point below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim of a deadlock-freedom guarantee for the forking extension is asserted without any proof outline, typing rules, or reduction semantics, leaving the soundness of the key technical result unevidenced and load-bearing for the contribution.

    Authors: Abstracts are high-level summaries by convention and do not contain typing rules, reduction semantics, or full proof outlines; those appear in the body. Section 3 presents the reduction semantics for the fork primitive, Section 4 gives the type system, and Section 5 contains the deadlock-freedom theorem together with a proof sketch that proceeds by induction on the typing derivation while handling the new dynamic spawn cases. The abstract therefore correctly states the result whose detailed justification is supplied later in the manuscript. If the referee prefers, we can append one sentence to the abstract that names the sections containing the semantics and proof. revision: partial

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The provided abstract and description introduce λ⤊ as a new functional choreographic language extending prior work with a forking primitive while preserving deadlock freedom. No equations, fitted parameters, self-definitional constructs, or load-bearing self-citations appear. The deadlock-freedom guarantee is stated as a direct technical result of the language design rather than reducing to any input by construction or prior author work. This matches the expected non-circular case for a theoretical language-design paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no free parameters, axioms, or invented entities can be identified.

pith-pipeline@v0.9.0 · 5652 in / 992 out tokens · 19991 ms · 2026-05-25T04:59:58.737737+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

42 extracted references · 42 canonical work pages

  1. [1]

    Suppose that 𝐿∈NL(𝜌 ′

    and SL(𝐶2) are disjoint. Suppose that 𝐿∈NL(𝜌 ′

    work page

  2. [2]

    By the assumption that NL(𝜌 1) and SL(𝐶2) are disjoint, we must have that 𝐿∉NL(𝜌 1)

    and 𝐿∈SL(𝐶 2). By the assumption that NL(𝜌 1) and SL(𝐶2) are disjoint, we must have that 𝐿∉NL(𝜌 1). Therefore 𝐿∈NL(𝜌 ′

    work page

  3. [3]

    But asSL(𝐶 2) ⊆NL(𝜌 2) ⊆Ω, we have a contradiction, as desired

    \NL(𝜌 1), and hence 𝐿∈Ω ′ \Ω by the inductive hypothesis. But asSL(𝐶 2) ⊆NL(𝜌 2) ⊆Ω, we have a contradiction, as desired. Now we show that NL(𝜌 2) and SL(𝐶 ′

    work page

  4. [4]

    Suppose that 𝐿∈NL(𝜌 2) and 𝐿∈SL(𝐶 ′ 1)

    are disjoint. Suppose that 𝐿∈NL(𝜌 2) and 𝐿∈SL(𝐶 ′ 1). By the assumption that NL(𝜌 2) and SL(𝐶1) are disjoint, we must have that 𝐿∉SL(𝐶 1). Therefore 𝐿∈SL(𝐶 ′

    work page

  5. [5]

    But asNL(𝜌 2) ⊆Ω, we have a contradiction, as desired

    \SL(𝐶 1), and hence 𝐿∈Ω ′ \Ω by the inductive hypothesis. But asNL(𝜌 2) ⊆Ω, we have a contradiction, as desired. Thus by the argument above and by induction,Θ⊢ + (𝐶′ 1, 𝐶2)𝜌 :𝜏 1 ×𝜏 2 ▷𝜌 ′ 1 ∪𝜌 2. (2) We show that NL(𝜌 ′

    work page

  6. [6]

    By induction NL(𝜌 ′

    ∪NL(𝜌 2) ⊆Ω ′. By induction NL(𝜌 ′

    work page

  7. [7]

    To that end, let 𝐿∈NL(𝜌 2), and suppose for contradiction that 𝐿∉Ω ′

    ⊆Ω ′, so we need only show that NL(𝜌 2) ⊆Ω ′. To that end, let 𝐿∈NL(𝜌 2), and suppose for contradiction that 𝐿∉Ω ′. Then 𝐿∈Ω because NL(𝜌 2) ⊆Ω by assumption, so 𝐿∈Ω\Ω ′. Then by the inductive hypothesis, 𝐿∈SL(𝐶 1) \SL(𝐶 ′

    work page

  8. [8]

    But by assumption SL(𝐶1) andNL(𝜌 2)are disjoint, so we have a contradiction

    ⊆SL(𝐶 1). But by assumption SL(𝐶1) andNL(𝜌 2)are disjoint, so we have a contradiction. (3) We need to show that SL((𝐶 ′ 1, 𝐶2)𝜌 ) \SL((𝐶 1, 𝐶2)𝜌 )=SL(𝐶 ′

    work page

  9. [9]

    We can see that SL(𝐶 ′

    \ (SL(𝐶 1) ∪SL(𝐶 2))= Ω′ \Ω . We can see that SL(𝐶 ′

    work page

  10. [10]

    \ (SL(𝐶 1) ∪SL(𝐶 2)) ⊆Ω ′ \Ω easily because SL(𝐶 ′

    work page

  11. [11]

    For the other direction, if 𝐿∈Ω ′ \Ω , then 𝐿∈SL(𝐶 ′

    \ SL(𝐶1) ⊆Ω ′ \Ω by the inductive hypothesis. For the other direction, if 𝐿∈Ω ′ \Ω , then 𝐿∈SL(𝐶 ′

    work page

  12. [12]

    This holds because if𝐿∈SL(𝐶 2) ⊆NL(𝐶 2), then we would have that𝐿∈Ω, a contradiction

    \SL(𝐶 1), so we need only show that 𝐿∉SL(𝐶 2). This holds because if𝐿∈SL(𝐶 2) ⊆NL(𝐶 2), then we would have that𝐿∈Ω, a contradiction. (4) We need to show that SL((𝐶 1, 𝐶2)𝜌 ) \SL((𝐶 ′ 1, 𝐶2)𝜌 )=SL(𝐶 1) \ (SL(𝐶 ′

    work page

  13. [13]

    We can see that SL(𝐶1) \ (SL(𝐶 ′

    ∪SL(𝐶 2))= Ω\Ω ′. We can see that SL(𝐶1) \ (SL(𝐶 ′

    work page

  14. [14]

    ∪SL(𝐶 2)) ⊆Ω\Ω ′ easily because SL(𝐶1) \ SL(𝐶 ′

    work page

  15. [15]

    For the other direction, if 𝐿∈Ω\Ω ′, then 𝐿∈SL(𝐶 1) \SL(𝐶 ′ 1), so we need only show that 𝐿∉SL(𝐶 2)

    ⊆Ω\Ω ′ by the inductive hypothesis. For the other direction, if 𝐿∈Ω\Ω ′, then 𝐿∈SL(𝐶 1) \SL(𝐶 ′ 1), so we need only show that 𝐿∉SL(𝐶 2). This holds because 54 Ashley Samuelson, Andrew K. Hirsch, and Ethan Cecchetti 𝐿∈NL(𝐶 1) \NL(𝜌 ′

    work page

  16. [16]

    But then as NL(𝐶1) and SL(𝐶 ′ 2)are disjoint,𝐿∉SL(𝐶 2)as desired

    by (6) of the induction, so 𝐿∈NL(𝐶 1). But then as NL(𝐶1) and SL(𝐶 ′ 2)are disjoint,𝐿∉SL(𝐶 2)as desired. (5) We need to show that (NL(𝜌 ′

    work page

  17. [17]

    ∪NL(𝜌 2)) \ (NL(𝜌 1) ∪NL(𝜌 2))=NL(𝜌 ′

    work page

  18. [18]

    However,NL(𝜌 ′ 1)\NL(𝜌 1) ⊆Ω ′\Ω by (5) of the inductive hypothesis, which is satisfactory

    \ (NL(𝜌 1) ∪ NL(𝜌 2)) ⊆Ω ′\Ω. However,NL(𝜌 ′ 1)\NL(𝜌 1) ⊆Ω ′\Ω by (5) of the inductive hypothesis, which is satisfactory. (6) We need to show that Ω\Ω ′ ⊆ (NL(𝜌 1) ∪NL(𝜌 2)) \ (NL(𝜌 ′

    work page

  19. [19]

    ∪NL(𝜌 2))=NL(𝜌 1) \ (NL(𝜌 ′

    work page

  20. [20]

    To that end, let 𝐿∈Ω\Ω ′

    ∪NL(𝜌 2)). To that end, let 𝐿∈Ω\Ω ′. Clearly 𝐿∈NL(𝜌 1) as NL(𝜌 1) ⊆Ω , so we must show that 𝐿∉NL(𝜌 ′

    work page

  21. [21]

    But by (6) of the inductive hypothesis, 𝐿∉NL(𝜌 ′ 1), so we must simply show that𝐿∉NL(𝜌 2)

    ∪NL(𝐶 2). But by (6) of the inductive hypothesis, 𝐿∉NL(𝜌 ′ 1), so we must simply show that𝐿∉NL(𝜌 2). By (4) of the inductive hypothesis, 𝐿∈SL(𝜌 1) \SL(𝜌 ′ 1), and hence𝐿∉NL(𝜌 2)becauseSL(𝜌 1)andNL(𝜌 2)are disjoint. The argument for reductions on the right-hand side of the pair is symmetric. For inl𝜌 𝐶, the assumptions are that Θ⊢ + 𝐶1 :𝜏 1 ▷𝜌 1, tloc(Θ; 𝜏...

    work page

  22. [22]

    Suppose that 𝐿∈SL(𝐶 ′

    are disjoint. Suppose that 𝐿∈SL(𝐶 ′

    work page

  23. [23]

    We must have that 𝐿∉SL(𝐶 1), as NL(𝜌) and SL(𝐶1) are disjoint by assumption

    and 𝐿∈NL(𝜌) . We must have that 𝐿∉SL(𝐶 1), as NL(𝜌) and SL(𝐶1) are disjoint by assumption. But then 𝐿∈SL(𝐶 ′

    work page

  24. [24]

    Therefore by the argument above and by induction,Θ⊢ + inl𝜌 𝐶 ′ 1 :𝜏 1 +𝜌 𝜏2 ▷𝜌 ′ 1

    \SL(𝐶 1)=Ω ′ \Ω , and hence 𝐿∉NL(𝜌) ⊆Ω , a contradiction as desired. Therefore by the argument above and by induction,Θ⊢ + inl𝜌 𝐶 ′ 1 :𝜏 1 +𝜌 𝜏2 ▷𝜌 ′ 1. (2) We need to show that NL(𝜌 ′

    work page

  25. [25]

    (3) We need to show that SL(inl 𝜌 𝐶 ′

    ⊆Ω ′, which is precisely (2) of the inductive hypothesis. (3) We need to show that SL(inl 𝜌 𝐶 ′

    work page

  26. [26]

    \SL(inl 𝜌 𝐶1)=SL(𝐶 ′

    work page

  27. [27]

    (4) Symmetrically, SL(inl 𝜌 𝐶1) \SL(inl 𝜌 𝐶 ′ 1)=SL(𝐶 1) \SL(𝐶 ′ 1)=Ω\Ω ′ by (4) of the inductive hypothesis

    \SL(𝐶 1)=Ω ′ \Ω , but this is precisely (3) of the inductive hypothesis. (4) Symmetrically, SL(inl 𝜌 𝐶1) \SL(inl 𝜌 𝐶 ′ 1)=SL(𝐶 1) \SL(𝐶 ′ 1)=Ω\Ω ′ by (4) of the inductive hypothesis. (5) We need to show thatNL(𝜌 ′

    work page

  28. [28]

    (6) Finally, we need to show that NL(𝜌 1) \NL(𝜌 ′

    \NL(𝜌 1) ⊆Ω ′ \Ω, which is given directly by the inductive hypothesis. (6) Finally, we need to show that NL(𝜌 1) \NL(𝜌 ′

    work page

  29. [29]

    •(C-Done) Follows by local type preservation, and as no locations are spawned or killed

    ⊆Ω\Ω ′, which is also provided by (6) of the inductive hypothesis. •(C-Done) Follows by local type preservation, and as no locations are spawned or killed. • (C-App) The assumptions are that Θ, 𝐹:𝜏 1 𝜌 − →𝜏2, 𝑋:𝜏 1 ⊢+ 𝐶:𝜏 2 ▷𝜌 , Θ⊢ + 𝑉:𝜏 1 ▷∅ , and tloc(Θ;𝜏 1) ∪tloc(Θ;𝜏 2) ∪𝜌=𝜌 ′. (1) By Lemma 23,Θ⊢ + 𝐶[𝐹↦→𝑓 , 𝑋↦→𝑉]:𝜏 2 ▷𝜌, where𝑓=fun 𝜌 𝐹(𝑋) :=𝐶. (2) By a...

    work page

  30. [30]

    By induction on the definition of ≾

    That is, the following diagram holds: 𝐸2 𝐸1 𝐸′ 2 𝐸′ 1 𝑅 𝑅 ≿ ⪰ Proof. By induction on the definition of ≾. Each case follows by either applying the inductive hypothesis, or by recalling that substitution (of each sort) preserves the relation, or produces terms which are related by⪯.□ E.4 Endpoint Projection The following lemmas relate EPP to the substituti...

    work page

  31. [31]

    The second equality holds because 𝑋∉fv(J𝐶 ′ 1K𝐿) and 𝑌∉fv(J𝐶 ′ 2K𝐿) by Lemma 39 and the assumption that the original choreography projects

    (inr𝑌⇒𝐶 ′ 2) y 𝐿 , where the inequality holds because of Lemmas 48 and 66. The second equality holds because 𝑋∉fv(J𝐶 ′ 1K𝐿) and 𝑌∉fv(J𝐶 ′ 2K𝐿) by Lemma 39 and the assumption that the original choreography projects. In the alternate case that𝐿∈𝜌the logic is straightforward: q case𝜌 𝐶of(inl𝑋⇒𝐶 1) (inr𝑌⇒𝐶 2) y 𝐿 =case J𝐶K𝐿 of(inl𝑋⇒𝐶 1) (inr𝑌⇒𝐶 2) ⪰case J𝐶K𝐿 ...

    work page

  32. [32]

    (inr𝑌⇒𝐶 ′ 2) = q case𝜌 𝐶of(inl𝑋⇒𝐶 ′

    work page

  33. [33]

    The other out-of-order steps follow similar logic

    (inr𝑌⇒𝐶 ′ 2) y 𝐿 . The other out-of-order steps follow similar logic. □ 68 Ashley Samuelson, Andrew K. Hirsch, and Ethan Cecchetti Corollary 11.If Θ⊢ + 𝐶:𝜏▷𝜌 , ⟨𝐶,Ω⟩ 𝑅 =⇒𝑐 ⟨𝐶′,Ω ′⟩, 𝐿∈Ω\rloc(𝑅) , and J𝐶K⋔ 𝐿 =𝐸 , then there is some𝐸 ′ ⪯𝐸such thatJ𝐶 ′K⋔ 𝐿 =𝐸 ′. Proof. If 𝐿∉SL(𝐶) , then this follows immediately by Lemma 75. Otherwise if 𝐿∈SL(𝐶) , then it eit...

    work page

  34. [34]

    𝐶 𝐶 ′ 𝐸 𝐸′ ⪰ J𝐶′K𝐿 𝐿∈𝑅 𝑐 J·K𝐿 J·K𝐿 J𝑅K𝐿 + Proof.By induction on the step⟨𝐶,Ω⟩ 𝑅 =⇒𝑐 ⟨𝐶′,Ω ′⟩

    That is, the following diagram holds. 𝐶 𝐶 ′ 𝐸 𝐸′ ⪰ J𝐶′K𝐿 𝐿∈𝑅 𝑐 J·K𝐿 J·K𝐿 J𝑅K𝐿 + Proof.By induction on the step⟨𝐶,Ω⟩ 𝑅 =⇒𝑐 ⟨𝐶′,Ω ′⟩. •(C-Ctx) Straightforward by induction. •(C-Done) ApplyN-Ret. •(C-App) The left side of the step projects to q 𝑓$ 𝜌 𝑉 y 𝐿 =(fun𝐹(𝑋) := J𝐶K𝐿) J𝑉 K𝐿 . We can applyN-Appto step to J𝐶K𝐿 [𝐹↦→J𝑓K 𝐿, 𝑋↦→J𝑉K 𝐿], which is satisfactory ...

    work page

  35. [35]

    𝐶 𝐶 ′ Π Π′ ⪰ J𝐶′K⋔ Ω′ 𝑅 𝑐 J·K⋔ Ω J·K⋔ Ω′ J𝑅K L + Proof

    That is, the following diagram holds. 𝐶 𝐶 ′ Π Π′ ⪰ J𝐶′K⋔ Ω′ 𝑅 𝑐 J·K⋔ Ω J·K⋔ Ω′ J𝑅K L + Proof. First the case for steps which are not fork or kill. By Lemma 79 and Lemma 80, it suffices to prove that 𝐿⊲ J𝐶K⋔ 𝐿 J𝑅K𝐿 = = = =⇒∗ Π′ 2(𝐿) and J𝐶′K⋔ 𝐿 ⪯Π ′ 2(𝐿) for each location 𝐿∈Ω . If 𝐿∉rloc(𝑅) , this holds by Corollary 11, noting that J𝑅K𝐿 is empty. Otherwise...

    work page

  36. [36]

    By Lemma 83, we can take a step Π′′ 2 =⇒𝑆 Π′′′ 2 to some Π′′′ 2 where Π′′ 1 ⪯Π ′′′ 2

    By Corollary 13, we can step Π′ 2 =⇒∗ 𝑆 Π′′ 2 where Π′ 1 ≾Π ′′ 2 . By Lemma 83, we can take a step Π′′ 2 =⇒𝑆 Π′′′ 2 to some Π′′′ 2 where Π′′ 1 ⪯Π ′′′ 2 . Then the reduction sequence Π2 =⇒𝑘 𝑆 Π′ 2 =⇒∗ 𝑆 Π′′ 2 =⇒𝑆 Π′′′ 2 is precisely as is required. □ Theorem 10(Completeness).If Θ⊢ + 𝐶:𝜏▷𝜌 , NL(𝜌) ⊆Ω , ⟨𝐶,Ω⟩=⇒ 𝑛 𝑐 ⟨𝐶′,Ω ′⟩, and J𝐶K⋔ Ω =Π , then there is som...

    work page

  37. [37]

    Then Π′ 3 is satisfactory, as J𝐶1K⋔ Ω1 =⇒𝑘 𝑆 Π2 =⇒+ 𝑆 Π′ 3 andJ𝐶 3K⋔ Ω3 ⪯Π 3 ⪯Π ′

    work page

  38. [38]

    The argument is summarized by the following diagram. J𝐶1K⋔ Ω1 Π2 J𝐶2K⋔ Ω2 Π′ 3 Π3 J𝐶3K⋔ Ω3 𝑘 + + ⪰ ⪰⪰ □ Step in Tine: Forking Processes in Functional Choreographies 73 Theorem 5(Completeness).If Θ⊢𝐶:𝜏▷𝜌 and NL(𝜌) ⊆Ω , then whenever ⟨𝐶,Ω⟩=⇒ ∗ 𝑐 ⟨𝐶′,Ω ′⟩, there is someΠ ′ such thatJ𝐶K ⋔ Ω =⇒∗ 𝑆 Π′ andJ𝐶 ′K⋔ Ω′ ⪯Π ′. Proof.Follows directly from Theorem 10 an...

    work page

  39. [39]

    Then it must be the case thatloc(𝑙 1) ∩loc(𝑙𝑠 ′ 2)≠∅ , so we may apply induction to𝑙𝑠 ′ 2 to yield 𝑙𝑠𝑎, 𝑙𝑠𝑏, and 𝑙 ′

    First suppose that loc(𝑙 1) ∩loc(𝑙 2)=∅ . Then it must be the case thatloc(𝑙 1) ∩loc(𝑙𝑠 ′ 2)≠∅ , so we may apply induction to𝑙𝑠 ′ 2 to yield 𝑙𝑠𝑎, 𝑙𝑠𝑏, and 𝑙 ′

    work page

  40. [40]

    catch-up

    Then 𝑙𝑠 ′ 𝑎 =𝑙 2 + +𝑙𝑠𝑎, 𝑙𝑠 ′ 𝑏 =𝑙𝑠 𝑏, and 𝑙 ′′ 1 =𝑙 ′ 1 suffice. Otherwise suppose that there is some location 𝐿∈loc(𝑙 1) ∩loc(𝑙 2). Then by Lemma 91, ⌊𝑙1⌋𝐿 and ⌊𝑙2⌋𝐿 are either equal, receives of two different values, or local programs stepping to two different values. We claim that 𝐿 cannot receive two different values. Indeed, the message sent by the ...

    work page

  41. [41]

    catch up

    The we apply induction on 𝑙𝑠 ′ 2 and Π2 𝑙𝑠 1 = =⇒∗ 𝑆 Π′ 1 to find some 𝑙𝑠 ′ 1 ⊆𝑙𝑠 1 and Π′′ 1 where Π′ 1 𝑙𝑠 ′ 1 = =⇒∗ 𝑆 Π′′ 1 and ∀𝐿,⌊𝑙𝑠 ′ 2⌋𝐿 ≤ ⌊𝑙𝑠1 + +𝑙𝑠′ 1⌋𝐿. ThenΠ ′′ 1 and𝑙+ +𝑙𝑠 ′ 1 suffices because –𝑙𝑠 ′ 1 ⊆𝑙𝑠 ′ 2, so𝑙+ +𝑙𝑠 ′ 1 ⊆𝑙+ +𝑙𝑠 ′ 2 =𝑙𝑠 2, and –for each𝐿 ⌊𝑙𝑠2⌋𝐿 =⌊𝑙⌋ 𝐿 + + ⌊𝑙𝑠′ 2⌋𝐿 ≤ ⌊𝑙⌋ 𝐿 + + ⌊𝑙𝑠1 + +𝑙𝑠′ 1⌋𝐿 =⌊𝑙+ +𝑙𝑠 1 + +𝑙𝑠′ 1⌋𝐿 76 Ashley Sa...

    work page

  42. [42]

    Thus by Lemma 92, there is some 𝑙𝑠𝑎, 𝑙𝑠𝑏, and 𝑙 ′ such that 𝑙𝑠 1 =𝑙𝑠 𝑎 + +𝑙′ + +𝑙𝑠𝑏, loc(𝑙) ∩loc(𝑙𝑠 𝑎)=∅ , and either 𝑙 ′ =𝑙 , or 𝑙=𝐿.ret(𝑒⇒𝑒 1) and 𝑙 ′ =𝐿.ret(𝑒⇒𝑒 2) where 𝑒1 ≠𝑒 2

    Because there is some𝐿∈loc(𝑙) , and as ⌊𝑙+ +𝑙𝑠 2⌋𝐿 ≤ ⌊𝑙𝑠 1⌋𝐿, we must have that 𝐿∈loc(𝑙𝑠 1), and so loc(𝑙) ∩loc(𝑙𝑠 1)≠∅ . Thus by Lemma 92, there is some 𝑙𝑠𝑎, 𝑙𝑠𝑏, and 𝑙 ′ such that 𝑙𝑠 1 =𝑙𝑠 𝑎 + +𝑙′ + +𝑙𝑠𝑏, loc(𝑙) ∩loc(𝑙𝑠 𝑎)=∅ , and either 𝑙 ′ =𝑙 , or 𝑙=𝐿.ret(𝑒⇒𝑒 1) and 𝑙 ′ =𝐿.ret(𝑒⇒𝑒 2) where 𝑒1 ≠𝑒 2. However, the latter case is impossible because ⌊𝑙+ +𝑙...

    work page