Cross-reference glossary for README.adoc, EXPLAINME.adoc, and the choreographic-types wiki. Terms are classified as standard (existing concept used without modification), rephrased (standard concept with project-specific vocabulary), or project-specific (originating in this project).
- Global type (G)
-
A choreographic specification of a multiparty interaction, read here as a partial causal order of communication events. Classification: rephrased. Global types are standard in multiparty session types (Honda–Yoshida–Carbone). Reading them explicitly as partial causal orders with antichain cuts is the project-specific emphasis. See also: [cut], [endpoint-projection]
- Endpoint projection
-
The mapping from a global type
Gto the local type at each participant. Standard in choreographic programming. Classification: standard. See also: [k-cut]
- Cut (consistent frontier)
-
An antichain across the partial causal order of a global type: a set of events such that no two are causally related. Represents a consistent snapshot of the distributed interaction. Classification: rephrased. Antichains and consistent cuts are standard in event structures and distributed systems. Applying them as the cut structure for session-type grading is project-specific. See also: [k-cut]
- Echo loss-grade
-
The grade attached to a choreographic edge, measuring the structured information loss at that interaction. Drawn from the
ℕ ∪ {∞}loss-dioid inecho-types. Classification: project-specific (composition of echo-types vocabulary with choreographic types).
- Epistemic standpoint-warrant
-
The grade attached to a choreographic edge, measuring the evidence required to authorise that interaction. Drawn from
epistemic-types. Classification: project-specific (composition of epistemic-types vocabulary with choreographic types).
- Loss modality (∇ / △)
-
∇ contingent: loss may occur at this cut. △ non-contingent: loss is impossible. Indexed by an ordinal loss value. Classification: project-specific.
- K-CUT
-
The conjecture that grading and transport commute with endpoint projection across a consistent frontier (cut). Splits into [k-cut-loss] and [k-cut-warrant]. Classification: project-specific (conjecture). Status: OPEN.
- K-CUT-LOSS
-
The fragment of K-CUT concerning echo loss-grades. Holds as an equality: the grade of the global cut equals the grade computed locally at the endpoint, because loss is type-determined. Classification: project-specific (conjecture). Status: OPEN (base case proved in
echo-types).
- K-CUT-WARRANT
-
The fragment of K-CUT concerning epistemic warrants. Holds only as a bound under a
SoundWarrantside-condition: the type upper-bounds discoverability but cannot determine it. Classification: project-specific (conjecture). Status: OPEN.
- RapidNJ reduction
-
In this repository’s application note, one already-selected RapidNJ-style neighbour-joining update over a global state. The note does not claim that upstream RapidNJ has the same two-thread batch interface. Classification: application-specific. See also: [two-thread-diamond], [independent-frontier]
- Independent frontier (
Independent₂) -
A two-event frontier that is an antichain and additionally satisfies the implementation’s read/write disjointness, phase-safety, and deterministic tie-policy conditions. Antichain membership alone is not enough to justify concurrent mutation of a RapidNJ state. Classification: project-specific application predicate. Status: OPEN until instantiated and proved for a concrete reduction representation. See also: [cut], [rapidnj-reduction]
- Two-thread state diamond
-
The algorithmic equality, up to canonical state equivalence, that applying two independent reductions in either serialisation gives the same observed RapidNJ state:
step e2 (step e1 s) ~= step e1 (step e2 s). It is a prerequisite for the K-CUT application, not K-CUT itself. Classification: application-specific proof target. Status: OPEN. See also: [k-cut-loss]
- Two-thread K-CUT-LOSS
-
The first non-degenerate K-CUT-LOSS target in the RapidNJ application. For every endpoint
pand witnessed independent two-event frontier, the local grade after the two projected steps equals the transported global loss grade after the two global steps. The conclusion is an equality of loss grades; it is not the warrant bound. Classification: project-specific application conjecture. Status: OPEN. See also: [k-cut], [k-cut-warrant]
- Port-and-reprove pattern
-
Re-proving a result in-site rather than importing across kernels or language boundaries. Ensures self-containment at the cost of manual synchronisation. Classification: project-specific (estate pattern). Precedent:
typed-wasm/…/Tropical.idr.