PaperlayerView exact revision on arXiv

Source-linked AI summary

Two Sides of the Same Proof: Extraction and Projection in Choreographic Programming

Matteo Acclavio, Giulia Manara, Fabrizio Montesi, Marco Peressotti

arXiv:2610.29736v1cs.LO

TL;DR

Extraction from networks is difficult because it must reconstruct global behavior from local programs, and the relationship between extraction and projection has lacked a direct correspondence. The paper connects choreographies, network execution trees, and proofs to extend the framework to infinite behaviors and characterize lock-free networks. It also develops proof-based extraction and endpoint projection results.

  • Problem

    Extraction must reconstruct global behavior from distributed local programs, and earlier procedures lacked a direct correspondence with projection.

    Source: §1 · p. 2

  • Method

    The paper relates network execution trees and choreographies to proofs in a linear-logic framework extended to cyclic proofs for infinite behaviors.

    Source: §8 · p. 25

  • Results

    Lock-free networks are characterized by provability of their encoded sequents, and the proof framework establishes correspondence with network execution trees.

    Source: §6.2 · p. 18, §8 · p. 25

  • Takeaways & Limitations

    The proposed endpoint projection supports a strictly larger class of choreographies than alternative approaches without runtime auxiliary communications, merge, or amendment.

    Source: §8 · p. 26

    The network calculus is restricted to tail-recursive processes and networks, for which the set of reachable states is finite.

    Source: §3 · p. 5

Abstract

from arXiv · show

A new approach to the theory of choreographic languages has recently been proposed, based on the interpretation of choreographies with finite behaviors as proofs in an extension of linear logic. This paper further develops this approach to cyclic proofs to be capable of representing infinite behaviors, and prove a completeness result for choreographies with respect to the class of lock-free networks. We show that in a choreographies-as-proofs correspondence, the proof equivalence induced by rule permutations corresponds to bisimilarity, and that, under adequate assumption on the procedure definitions, the proof search procedure has a finite search space, and can be used to extract a choreography from a network.

1 Introduction

Choreographic programming studies both which global choreographies networks can implement and which networks can be described choreographically; extraction is difficult because it reconstructs global behavior from local programs. The paper extends choreographies-as-proofs to infinite behaviors and uses the framework for extraction and endpoint projection.

1 Introduction

  • Extraction must reconstruct global behavior from local programs, while choreographies make intended communications and recursive structure explicit.Earlier extraction procedures lacked a direct correspondence with projection, leaving the relationship between realisability and expressivity open.Source: §1 · p. 2

1.1 Contribution of the paper

  • The paper extends choreographies-as-proofs to infinite behaviors using cyclic proofs and rules for greatest fixpoints.The approach builds on multiplicative additive linear logic with fixpoints.Source: §1.1 · p. 3
  • Fair proofs in ChorL𝔉 are in bijection with choreographies, and restricted proof search can extract choreographies from lock-free tail-recursive networks.The synthetic rules restrict the proof-search space while preserving completeness.Source: §1.1 · p. 3
  • Proof search extracts a choreography bisimilar to the illustrated initial network.The example demonstrates extraction from a network through the structure of a proof.Source: §1.1 · p. 3
  • The framework also gives a new endpoint projection proof, with proof conclusions encoding networks bisimilar to the choreography.It projects more choreographies than existing endpoint-projection algorithms and avoids the merge operator.Source: §1.1 · pp. 3–4

1.2 Structure of the paper

  • The paper proceeds from LTS and network semantics through choreographies and fixpoint proof systems to extraction and projection results.Its final section discusses related and future work.Source: §1.2 · p. 4

2 Background

The paper uses labeled transition systems to define behavioral equivalence between networks and choreographies. Strong bisimulation relates states by matching their labeled transitions.

2 Background

  • The paper uses strong bisimulation as a shared behavioral equivalence for choreographies and networks.This common notion is used to relate their LTSs.Source: §2 · p. 4
  • A labeled transition system consists of states, labels, and a transition relation; a reduction sequence is a sequence of labeled steps between states.The paper defines both networks and choreographies with LTSs induced by their operational semantics.Source: §2 · p. 4
  • A bisimulation relates state pairs so that transitions from either state can be matched by the other while preserving the relation.States are bisimilar when some bisimulation contains their pair.Source: §2 · p. 5

3 Network Calculus and Reduction Trees

The network calculus is the target language for endpoint projection, with synchronous direct communication and tail-recursive processes. Reduction trees represent network executions and characterize lock-freedom through fair progress.

3 Network Calculus and Reduction Trees

  • The calculus assumes synchronous direct communication over unique private channels and restricts networks to tail-recursive processes, yielding finitely many reachable states.The synchronous model provides race freedom by design, a property used in proving extraction completeness.Source: §3 · p. 5

3.1 Processes

  • Process terms include communication, choices, and procedure variables, with finite closed guarded procedure definitions fixed for each process.Active process names are those appearing before any procedure call; process names also include names in reachable procedure bodies.Source: §3.1 · p. 5

3.2 Networks

  • A network maps process names to process terms with finite support, and disjoint networks compose by union.Network operational semantics uses communication, label communication, and selection steps.Source: §3.2 · pp. 5–6
  • A reduction tree represents possible network executions; at a branching node, successors correspond to the available choices of one process.The tree is maximal, and its paths are maximal executions.Source: §3.2 · pp. 6–7
  • A network is lock-free exactly when it admits a fairly lock-free reduction tree.Tail recursion ensures such a tree can be represented finitely because the reachable-state set is finite.Source: §3.2 · p. 7

4 Choreographies...now with tensor!

The choreography language adds tensor composition to represent independent behaviors in parallel, alongside communication, choice, and recursion. Its semantics permits independent reductions, and every well-formed choreography is lock-free.

4 Choreographies...now with tensor!

  • Tensor composition lets choreographies represent independent behaviors over disjoint process sets, needed when one component continues independently of another's choice.Without tensor, recursion could force independent components to share a recursive variable and terminate together, unlike the corresponding network.Source: §4 · p. 8

4.1 Syntax

  • The syntax includes termination, variables, communication, choice, and tensor composition; well-formed tensor components must have disjoint process-name sets.Recursive variables cannot occur in both components of a well-formed parallel composition.Source: §4.1 · pp. 8–9
  • Communication sends an expression and substitutes it at the receiver, while choice communicates the selected label before continuing along that branch.A choice receiver may offer more labels than the sender can select.Source: §4.1 · pp. 8–9

4.2 Semantics

  • The operational semantics unfolds procedure variables, executes communication and two-step choices, and lets either tensor component reduce independently.Delay rules allow continuation steps before a prefix when the step does not involve its controlling processes and, for choices, is enabled in every branch.Source: §4.2 · pp. 9–10
  • Bisimilarity treats tensor composition as commutative and associative, with 0 as its unit.These equivalences are stated for the choreography semantics.Source: §4.2 · p. 10
  • Every well-formed choreography is lock-free.Lock-freedom requires each process appearing in a reachable choreography to eventually participate in a step.Source: §4.2 · p. 10

5 Cyclic proofs in PiL

This section extends PiL with procedural variables to represent procedure calls and develops cyclic proofs for reasoning about process formulas and networks.

5 Cyclic proofs in PiL

  • Procedural variables model procedure calls without full fixpoint operators, with an interpretation as fixed-body existential witnesses or greatest-fixpoint formulas.The greatest-fixpoint reading captures the possibility of infinite unfolding.Source: §5 · p. 11

5.1 Formulas

  • Process terms are encoded inductively as PiL formulas, with variables mapped identically and prefixes and choices represented using logical connectives.Output and input prefixes use ◀; input binding uses existential quantification, while selections and branchings use additive choices.Source: §5.1 · p. 12

5.2 Sequent calculi

  • Networks are encoded as sequents containing the formulas for their component processes, with a process name identifying each formula's location.The encoding removes unit occurrences except when the whole network encodes to the unit.Source: §5.2 · pp. 12–13
  • PiL extends standard multiplicative-additive linear-logic rules with a non-commutative ◀ rule, and satisfies initial and final coherence.The ◀ rule generalizes tensor to multiple pairs of formulas; its n=0 case corresponds to mix.Source: §5.2 · p. 13, Figure 4 · p. 13

5.3 Cyclic Proofs

  • Cyclic proofs allow infinite derivations subject to correctness conditions, including regularity and progress along infinite branches.Regularity requires only finitely many distinct non-isomorphic subderivations; progress requires infinitely many progress points on every infinite branch.Source: §5.3 · pp. 14–15
  • The proof-theoretic fairness condition adds a requirement for choices enabled infinitely often, beyond the justness-like condition on non-principal formulas.In PiL_F, progress points are occurrences of procedural variables principal for unfold.Source: §5.3 · pp. 14–15

6 Proofs as Execution Trees

The paper relates ChorL proofs to network execution trees, then characterizes lock-freedom through provability. Its cyclic proof system supports infinite behaviors and yields a proof for every lock-free network.

6 Proofs as Execution Trees

  • ChorL_F uses synthetic rules derivable in PiL_F, designed to correspond to individual network transitions and extend the approach to infinite behaviors.The rules include communication, choice, mix, and unfolding rules.Source: §6 · p. 16, §6.2 · p. 17
  • C-unfold defines progress points in ChorL_F; the resulting progressing proofs are regular and fair.Niceness also constrains mix-rule placement and requires choice actions to be resolved by matching label rules.Source: §6 · pp. 16–17
  • For finite, closed procedure definitions, a progressing proof has only finitely many possible sequents and is regular.The argument relies on finitely many subformulas and on rules other than unfold and C-unfold not introducing new formulas.Source: §6 · p. 17

6.2 Proofs as Execution Trees, and Lock-freedom as provability

  • Network reduction trees correspond one-to-one with proofs of their network encodings in ChorL_F.The translation extends the network-to-sequent encoding from networks to reduction trees.Source: §6.2 · p. 18
  • A network is lock-free if and only if its encoding admits a progressing proof in ChorL_F.The proof system's cyclic proofs are sound and complete with respect to encodings of lock-free networks.Source: §6 · p. 16, §6.2 · p. 18
  • Every lock-free network has a proof in ChorLnice, providing a proof-theoretic basis for the extraction procedure.This result is stated as a corollary for the network encoding JNK.Source: §6.2 · p. 18

7 Proofs as Choreographies

Section 7 develops a correspondence between choreographies and proofs, with translation and proof search connecting bisimilar choreographies and networks. It establishes the existence of a bisimilar choreography for every lock-free network and describes how, under the nice-proof condition, extraction separates independent components into disjoint choreographies composed with ⊗.

7.1 Endpoint Projection, Logically

  • A total pre-derivation translation uses a relaxed limbo rule, and a choreography is projectable when each limbo occurrence can be replaced by the sound choice rule; recursive variables track processes involved in infinite behavior.Processes occurring only in finite sub-choreographies are represented by finite formulas instead of procedure calls.Source: §7.1 · pp. 19–20
  • The endpoint-projection translation handles a choice example that standard techniques cannot project because process r lacks knowledge of the choice, while its proof conclusion is bisimilar to the resulting network.The paper attributes this to the proof’s handling of knowledge of choice.Source: §7.1 · p. 20
  • For projectable choreographies, equivalent translated proofs—under rule permutations—imply bisimilar choreographies.Each permutation preserves bisimilarity of the corresponding choreographies.Source: §7.1 · p. 21
  • If Pr(C) is a well-defined proof with conclusion Γ, there is a lock-free network N such that C is bisimilar to N and Γ = JNK.The result ties the proof’s conclusion to the network encoding.Source: §7.1 · p. 22

7.2 Extraction, logically

  • The extraction algorithm maps a proof of a sequent encoding a lock-free network to a choreography bisimilar to that network.Proof equivalence also induces a bisimulation between the choreographies extracted from equivalent derivations.Source: §7.2 · pp. 23–24
  • Every lock-free network N has a choreography C with the same participants, pn(C) = pn(N), and C ∼ N.The completeness proof obtains C by extracting it from a proof of the network.Source: §7.2 · p. 25
  • The nice-proof condition makes extraction separate independent components with C-mix, yielding disjoint choreographies composed by ⊗.This mirrors the network’s independent structure.Source: §7.2 · p. 25
  • For the example network, extraction produces the parallel choreography C⊗ rather than the sequential C1, better reflecting the network’s disjoint structure.Both choreographies are bisimilar to the network.Source: §7.2 · p. 25

8 Conclusions and Future Work

The paper presents a linear-logic framework that treats projection and extraction uniformly through a correspondence between proofs and network execution trees. It uses this framework to characterize lock-freedom and develop projection without merge, while identifying restricted conditions for finite proof search.

8 Conclusions and Future Work

  • Projection and extraction are studied uniformly through a correspondence between sequent-calculus proofs and trees of network executions.This provides a proof-theoretic framework for studying choreographies and their relation to process calculi.Source: §8 · p. 25
  • Lock-freedom is characterized by the existence of proofs in the logic, whose successful execution can be viewed as logic-program execution.The proof-theoretic endpoint projection also dispenses with merge and permits recursive choices that previous projection procedures had not handled, to the authors’ knowledge.Source: §8 · p. 25
  • Without merge, the proof-theoretic projection extends the projectable class to choreographies with recursive choices.The paper also suggests compilers based on this projection that support a strictly larger class of choreographies than comparable approaches, without runtime costs for auxiliary communications or complex merge or amendment procedures.Source: §8 · pp. 25–26
  • For lock-free networks with only tail-recursive calls, extraction is guaranteed to terminate because proof search has finitely many formulas modulo first-order substitutions.The authors state that polynomial-space proof search should be possible under this restriction; the captured fragment is restricted, including no least fixpoints, tail-recursive networks, and race-freedom.Source: §8 · p. 25

A Details of Proofs

The appendix details proof arguments connecting choreographies, networks, and derivations. The arguments use constructed bisimulation relations and case analysis over transition rules.

A Details of Proofs

  • The proof of the projection result proceeds by induction over proof derivations and considers cases for communication, choice, labels, and procedure transitions.The case arguments relate choreography transitions to corresponding network steps.Source: A Details of Proofs · p. 29
  • A fair proof with conclusion Γ yields a lock-free network N such that N is bisimilar to choreography C.The proof uses the network encoded by Γ and establishes bisimilarity by showing a relation is a bisimulation.Source: A Details of Proofs · p. 29
  • For extraction, the argument defines a relation between choreographies and networks and shows it is a bisimulation containing (Extr(D), N).The proof checks transition cases in both directions to establish the correspondence.Source: A Details of Proofs · pp. 30–31
Loading 2610.29736v1…