Pith. sign in

REVIEW 2 major objections 4 minor 64 references

A General Completeness Theorem for Skip-free Star Algebras

T0 review · 2 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that for any equational theory with a support and a malleability property, bisimilarity of skip-free star expressions is completely axiomatized by a fixed set of rules, unifying four known or new process-algebra…

desk verdict A promising unification with a real gap: the entry/body rules in Proposition 5.7 are unsound for star terms that don't use the loop variable, so Theorem 5.15 is unproven as stated. read the letter →

arxiv 2501.15325 v1 pith:ESS3EUOF submitted 2025-01-25 cs.LO

Tobias Kappé , Todd Schmid This is my paper · ORCID
classification cs.LO MSC 68Q8503B70
keywords completenesstheorembisimilarityprocessalgebraequationaltheoryskip-freestarexpressionscoalgebraguardedKleenewithtestsprobabilisticregular
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper proves a single completeness theorem for a whole family of process algebras at once. Fix an equational theory T that describes how processes branch — nondeterministically, probabilistically, or under tests; if T has a support (each term has a well-defined set of essential variables) and is malleable (any term can be split along a partition of its variables into s(t1, t2)), then one fixed set of axioms completely axiomatizes bisimilarity for skip-free star expressions over T. The theorem recovers the known completeness results for 1-free regular expressions and skip-free guarded Kleene algebra with tests, and it yields new completeness theorems for probabilistic regular expressions and for guarded convex algebra. The payoff is that five axiom schemes replace a collection of bespoke, hard-won completeness arguments.

What carries the argument

The carrying object is an M-system, a coalgebra for the functor M(Act × (✓ + (−))) where M is the free-algebra construction of the branching theory T; the syntactic M-system (Exp, γ) gives every skip-free unified-star expression a transition structure. A support is a natural transformation supp : M ⇒ P that assigns each term its set of essential variables, and malleability says that any term can be rewritten, along any partition of its variables, as s(t1, t2) with t1 and t2 on the two parts. These two conditions allow the well-layered chart technology — entry/body labellings, loop-around reachability, and the canonical solution formula of Definition 5.13 — to be lifted from ordinary charts to arbitrary M-systems.

What would settle it

Find a supported, malleable equational theory T and two skip-free unified-star expressions that are bisimilar in (Exp, γ) yet not provably equal in T*; the easiest place to look is the convex-semilattice theory CS, where malleability fails, or a weighted-transition (semimodule) theory where the canonical solution might not be unique. Alternatively, exhibit a well-layered chart whose homomorphic image is not well-layered, which would refute the imported closure theorem.

Watch

Extended reading notes

Core claim

The central claim is Theorem 5.15: for every supported, malleable equational theory T, if two skip-free unified-star expressions are bisimilar in the syntactic M-system (Exp, γ), then the equational theory T* proves them equal. The axioms of T* state that provable T-equivalence is respected (T), that sequential composition is associative (A) and right-distributive (D), that the s-star unfolds as a recursion equation (U), and that this recursion equation has a unique solution (RSP). The proof follows the strategy of the earlier 1-free completeness argument: every expression generates a finite, well-layered subsystem; well-layered systems are closed under homomorphic images (by an imported theorem); and every well-layered M-system has a unique solution, computed by a canonical formula. Therefore two bisimilar expressions share a common bisimulation quotient, whose unique solution witnesses their provable equality.

Load-bearing premise

The proof imports, without reproving, the theorem that well-layered charts are closed under homomorphic images; if that theorem fails, the completeness argument collapses at Theorem 5.9.

Editorial extensions

If this is right

  • Bisimilarity and provable equivalence coincide for every supported, malleable theory T, so bisimilarity is automatically a congruence for the skip-free expressions of that theory.
  • The completeness of CA* gives a finitary axiomatization for bisimilarity of 1-free probabilistic regular expressions, and the completeness of GC* does the same for a skip-free variant of probabilistic guarded Kleene algebra with tests.
  • The two existing completeness results, for SL* and GA*, are not merely analogous but instantiations of one theorem, which explains why their proofs share the same structure.
  • The framework reduces the open problem of full GKAT completeness to bringing the 'skip' constant into the supported-malleable world, likely by adding a right-annihilation axiom for 0.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The two conditions are plausibly close to necessary, not just sufficient: without support there is no underlying chart to layer, and without malleability the unique-solution formula cannot be built; a characterization of all supported, malleable theories would delimit exactly which branching effects admit such finite axiomatizations.
  • The semimodule instantiation generalizes to any semiring-valued transition system, suggesting a template for proving completeness of weighted process algebras beyond the three concrete examples.
  • A concrete stress test is the convex semilattice theory CS: if a counterexample to completeness of CS* exists, it would confirm that the malleability boundary is real, and it might be found by looking at bisimilar pairs whose common quotient needs a non-malleable mixture of convex and semilattice structure.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper develops a unifying framework for axiomatizing bisimilarity in process algebras with branching parametrized by an equational theory T. It introduces skip-free unified-star expressions Exp over an arbitrary equational theory, defines a syntactic M-system (Exp, γ), and proposes an inference system T∗ (Figure 4). The main theorem (Theorem 5.15) states that for every supported, malleable equational theory T, bisimilarity of expressions coincides with provable equivalence in T∗. The proof adapts the Grabmayer--Fokkink completeness argument: it establishes expressivity (the syntactic system is well-layered), closure under homomorphic images (via the imported Theorem 2.13), and solvability (unique canonical solutions to well-layered M-systems). The framework is claimed to recover completeness for the semilattice theory SL∗ and guarded algebra GA∗, and to yield new completeness theorems for convex algebra CA∗ and guarded convex algebra GC∗.

Significance. If the main theorem is correct, this is a valuable and genuinely abstract contribution: it isolates two structural conditions (support and malleability) under which a uniform completeness proof works, recovers two known results, and produces new completeness theorems for probabilistic and guarded-probabilistic process algebras. The paper is also careful to give nontrivial nonexamples, such as convex semilattices, and to state the reliance on the external closure theorem of Grabmayer and Fokkink. The proof is mostly in the appendix and follows the expected architecture, but the validity of Proposition 5.7 is essential and, as detailed below, needs repair before the main theorem is established.

major comments (2)
  1. [Section 5, Proposition 5.7] The entry/body rules in (10) do not respect the actual transition structure for star terms whose term s does not depend on the loop variable u. For T = SL, take e1 = a, e2 = b and s(u,v) = v. Then by Fig. 3, γ(a(v)b) = vρ(γ(a(a(v)b)), γ(b)) = γ(b) = {(b, ✓)}, so there is no transition a(v)b → a(v)b. Rule (10) nevertheless derives a(v)b →e a(v)b via the first or second premise, since a → ✓. Because Definition 2.11 requires →e to be a partition of the actual transition relation →δ, this is not an entry/body labelling of (Exp, γ). Example 4.3 explicitly allows s = v, so the issue is not an excluded case. Since Proposition 5.7 is the only source of (Expressivity) for the class of well-layered M-systems, the proof of Theorem 5.15 is incomplete for the syntax as defined. The rules need to be restricted to star terms that actually use u (or the syntax of Exp needs to be changed accordingly), and the proof of Lemma C.2 must be reworked under that restriction.
  2. [Definition 2.11 and rules (2)/(10)] The well-layeredness conditions as written are inconsistent with self-loop entry transitions, which the rules generate for genuinely looping terms such as a(u)b with T = SL and s(u,v) = u. The actual chart has a(u)b →a a(u)b, and rule (10) labels this self-loop as →e. Property 2 then requires a(u)b →b+ a(u)b, contradicting property 1. The proof of Proposition 5.7 in the appendix avoids the contradiction by proving property 2 only for transitions with e′ ≠ e. If the intended definition of well-layered is meant to exclude the case x = y in property 2, that exclusion must be stated explicitly; otherwise the definition and the rules are in direct conflict.
minor comments (4)
  1. [Section 2, Example 4.3] In Example 4.3, the line 'γ(a ∗ b) = ...' should presumably read 'γ((a + b) ∗ c) = ...', since the surrounding text is discussing (a + b) ∗ c.
  2. [Section 2, Definition 2.11] Please clarify whether property 2 of well-layeredness applies to self-loop entry transitions; the proof in the appendix silently uses it only for transitions with distinct source and target.
  3. [Appendix C, Lemma C.2] The statement of Lemma C.2 uses the notation f1(e(s)1 e2) with f1 ranging over expressions, but in the case e1 → ✓ the apparent form would require f1 to be the success marker, which is not an expression. This case needs to be separated out or stated more carefully.
  4. [Section 5, Theorem 5.15] The statement of the main theorem should explicitly note that it depends on the imported closure result Theorem 2.13 (Grabmayer--Fokkink), which is not reproved in this paper.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the completeness theorem follows from a standard unique-solution argument whose only heavy external import (Theorem 2.13) is independent prior work, not the target result.

full rationale

Theorem 5.15 is proved by the classical Milner/Grabmayer-Fokkink strategy: choose the class of well-layered M-systems; establish (Expressivity) via Proposition 5.7 (verified directly from the transition structure with the support assumption), (Closure) via Lemma 5.8 combined with the external Theorem 2.13, and (Solvability) via Proposition 5.14 (a proof within the fixed axiom system T* using rules (U), (D), (RSP)). None of these steps assumes bisimilarity implies provable equality. The canonical solution in Definition 5.13 is constructed from the syntax and proof rules, not from the target equivalence. The conditions 'supported' and 'malleable' are structural properties of the equational theory T, verified independently for SL, GA, CA, and GC, and are not defined in terms of T*-provability or bisimilarity. The only load-bearing import is Theorem 2.13, which is explicitly attributed to Grabmayer and Fokkink (LICS'20) and Schmid, Rot, and Silva (CALCO'21); it is an external theorem about charts, not a disguised version of the present completeness result, and the paper transparently flags it as a reliance rather than reproving it. No equation in the paper is defined in terms of the claimed conclusion, and no fitted parameter is renamed as a prediction. The derivation is therefore self-contained relative to its stated external premise.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

The paper introduces no fitted constants or ad hoc numerical parameters; its conditions are structural. The central claim rests on standard universal algebra and coalgebra background, on the imported closure theorem, and on the explicit support/malleability hypotheses, all of which are verified for the concrete instantiations.

assumptions (4)
  • standard math Equational logic and the free-algebra construction for an equational theory T
    Preliminaries in Section 3; standard universal algebra and monad theory.
  • domain assumption Theorem 2.13: the class of well-layered charts is closed under homomorphic images
    Imported from Grabmayer-Fokkink [6] and Schmid-Rot-Silva [27]; used as a black box in Theorem 5.9 to establish (Closure).
  • domain assumption T admits a support and is malleable
    Explicit hypotheses of Theorem 5.15; verified for SL, GA, CA, GC, SMod in Section 6.
  • standard math Coalgebraic facts: bisimilarity via span of homomorphisms, subcoalgebra intersection (Gumm-Schroeder)
    Used in Lemma 2.4, Proposition 2.9, Proposition 4.4.
invented entities (2)
  • Skip-free unified-star expressions (Exp)
    purpose: A uniform syntax for process algebras with T-branching, subsuming 1-free star expressions and skip-free GKAT programs.
    New formal language defined in Section 4; no empirical handle, internal to the framework.
  • Support and malleability conditions on equational theories
    purpose: Abstract conditions that make the Grabmayer-Fokkink completeness strategy go through; delimiting the scope of the theorem.
    New conditions defined in Section 5; used to state Theorem 5.15 and to identify examples and a nonexample.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A General Completeness Theorem for Skip-free Star Algebras." pith.science (2026). https://pith.science/paper/ESS3EUOF

@misc{pith2026250115325,
  author       = {Pith},
  title        = {Pith review of: A General Completeness Theorem for Skip-free Star Algebras},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ESS3EUOF}},
  note         = {Machine review of arXiv:2501.15325}
}
read the original abstract

We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS'20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results.

Figures

Figures reproduced from arXiv: 2501.15325 by the authors.

Figure 1
Figure 1. Rules defining the transition structure of the syntactic chart (StExp, δ). In the above, a ∈ Act, r1, r2, s ∈ StExp, and ξ ∈ ✓ + StExp. In the absence of parentheses, ∗ takes precedence over ·, which is evaluated before +. So, a+b · c ∗ d should be read as a+ (b ·(c ∗ d)). We typically write r1r2 instead of r1 · r2. The process semantics for 1-free star expressions can be phrased in terms of a variant of labelled tr… view at source ↗
Figure 2
Figure 2. The axioms proposed by Grabmayer and Fokkink in [6]. The theory SL∗ consists of the axioms above and equational logic (not pictured above). It is straightforward to show that charts and chart homomorphisms form a category, i.e., identity maps id: (X, δ) → (X, δ) are homomorphisms and any composition of homomorphisms is a homomorphism. Furthermore, bisimilarity can be characterized using chart homomorphisms, via the … view at source ↗
Figure 3
Figure 3. The definition of (Exp, γ) w.r.t. the free-algebra construction (M, η, ρ). Above, ei ∈ Exp, a ∈ Act, and s = s(u, v) ∈ S ∗Var . In the formulas for e1e2 and e (s) 1 e2 above, γ(e1) = t ρ = t ρ ((⃗b, ✓),(⃗a, ⃗f)). In the last formula, we have used red to indicate the portion of the formula that corresponds to the s in e (s) 1 e2. construction — suggests a syntax for behaviour expressed by well-layered charts, as well… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: The theory T ∗ that axiomatizes bisimilarity of star expressions. Above, e1, . . . , en ∈ Exp, e, f, g ∈ Exp, t = t(⃗v) ∈ S ∗Var , and s(u, v) ∈ S ∗Var is a binary term with free variables u, v. Recall that the notation ⃗ef means e1f, . . . , enf. The process denoted e…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 45 canonical work pages

  1. [1]

    London Mathematical Society Lecture Note Series, Cambridge University Press (1994)

    Adamek, J., Rosicky, J.: Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series, Cambridge University Press (1994)

    work page 1994

  2. [2]

    In: STACS

    Antimirov, V.M.: Partial derivates of regular expressions and finite automata constructions. In: STACS. pp. 455–466 (1995). https://doi.org/10.1007/ 3-540-59042-0_96

    work page 1995

  3. [3]

    In: CONCUR

    Baeten, J.C.M., Bergstra, J.A.: Process algebra with a zero object. In: CONCUR. pp. 83–98 (1990).https://doi.org/10.1007/BFB0039053

    work page doi:10.1007/bfb0039053 1990

  4. [4]

    In: CALCO

    Bonchi, F., Sokolova, A., Vignudelli, V.: Presenting convex sets of probability distributions by convex semilattices and unique bases ((co)algebraic pearls). In: CALCO. pp. 11:1–11:18 (2021).https://doi.org/10.4230/LIPICS.CALCO.2021. 11

    doi:10.4230/lipics.calco.2021 2021

  5. [5]

    In: LICS

    Grabmayer, C.: Milner’s proof system for regular expressions modulo bisimilarity is complete: Crystallization: Near-collapsing process graph interpretations of regular expressions. In: LICS. pp. 34:1–34:13 (2022).https://doi.org/10.1145/3531130. 3532430

    doi:10.1145/3531130 2022

  6. [6]

    In: LICS

    Grabmayer, C., Fokkink, W.J.: A complete proof system for 1-free regular ex- pressions modulo bisimilarity. In: LICS. pp. 465–478 (2020).https://doi.org/10. 1145/3373718.3394744

    arXiv 2020

  7. [7]

    Gumm, H.P., Schröder, T.: Coalgebras of bounded type. Math. Struct. Comput. Sci. 12(5), 565–578 (2002).https://doi.org/10.1017/S0960129501003590

    doi:10.1017/s0960129501003590 2002

  8. [8]

    Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Ob- servation, Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press (2016).https://doi.org/10.1017/CBO9781316823187

    doi:10.1017/cbo9781316823187 2016

Show all 64 references
  1. [9]

    In: ESOP

    Kappé, T., Schmid, T., Silva, A.: A complete inference system for skip-free guarded Kleene algebra with tests. In: ESOP. pp. 309–336 (2023).https://doi.org/10. 1007/978-3-031-30044-8_12

    2023

  2. [10]

    Keimel, K., Plotkin, G.D.: Mixed powerdomains for probability and nondeterminism. Log. Methods Comput. Sci.13(1) (2017). https://doi.org/10.23638/LMCS-13(1: 2)2017

    2017 doi

  3. [11]

    Automata studies 34, 3–41 (1956)

    Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata studies 34, 3–41 (1956)

    1956

  4. [12]

    ACM Trans

    Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.19(3), 427–443 (1997). https://doi.org/10.1145/256167.256195

    1997

  5. [13]

    Kozen, D., Tseng, W.D.: The Böhm-Jacopini theorem is false, propositionally. In: MPC. pp. 177–192 (2008).https://doi.org/10.1007/978-3-540-70594-9_11

    2008 doi

  6. [14]

    Liell-Cock, J., Staton, S.: Compositional imprecise probability: A solution from graded monads and markov categories. Proc. ACM Program. Lang.9(POPL) (Jan 2025). https://doi.org/10.1145/3704890

    2025 doi

  7. [15]

    Milner, R.: A complete inference system for a class of regular behaviours. J. Com- put. Syst. Sci.28(3), 439–466 (1984).https://doi.org/10.1016/0022-0000(84) 90023-0

    1984 doi

  8. [16]

    In: EXPRESS

    Mislove, M.W., Ouaknine, J., Worrell, J.: Axioms for probability and nondetermin- ism. In: EXPRESS. pp. 7–28 (2003).https://doi.org/10.1016/J.ENTCS.2004. 04.019

    2003 doi

  9. [17]

    Piróg, M., Staton, S.: Backtracking with cut via a distributive law and left- zero monoids. J. Funct. Program.27, e17 (2017). https://doi.org/10.1017/ S0956796817000077 A General Completeness Theorem for Skip-free Star Algebras 21

    2017

  10. [18]

    In: MFCS

    Plotkin, G.D., Power, J.: Semantics for algebraic operations. In: MFCS. pp. 332–345 (2001). https://doi.org/10.1016/S1571-0661(04)80970-8

    2001 doi

  11. [19]

    In: FOSSACS

    Plotkin, G.D., Power, J.: Notions of computation determine monads. In: FOSSACS. pp. 342–356 (2002).https://doi.org/10.1007/3-540-45931-6_24

    2002 doi

  12. [20]

    Aurora Dover Modern Math Originals, Dover Publications, Inc., Mineola, NY (2016)

    Riehl, E.: Category theory in context. Aurora Dover Modern Math Originals, Dover Publications, Inc., Mineola, NY (2016)

    2016

  13. [21]

    In: ICALP

    Rozowski, W., Kappé, T., Kozen, D., Schmid, T., Silva, A.: Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In: ICALP. vol. 261, pp. 136:1–136:20 (2023). https://doi.org/10.4230/LIPICS.ICALP.2023.136

    2023 doi

  14. [22]

    In: LICS

    Rozowski, W., Silva, A.: A completeness theorem for probabilistic regular expres- sions. In: LICS. pp. 66:1–66:14. ACM (2024).https://doi.org/10.1145/3661814. 3662084

    2024 doi

  15. [23]

    Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000).https://doi.org/10.1016/S0304-3975(00)00056-6

    2000 doi

  16. [24]

    Salomaa, A.: Two complete axiom systems for the algebra of regular events. J. ACM 13(1), 158–169 (1966).https://doi.org/10.1145/321312.321326

    1966

  17. [25]

    Schmid, T.: Coalgebraic Completeness Theorems for Effectful Process Algebras. Ph.D. thesis, University College London (2024)

    2024

  18. [26]

    In: ICALP

    Schmid, T., Kappé, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. In: ICALP. pp. 142:1–142:14 (2021). https://doi.org/10.4230/LIPIcs.ICALP.2021.142

    2021 doi

  19. [27]

    In: CALCO

    Schmid, T., Rot, J., Silva, A.: On star expressions and coalgebraic completeness theorems. In: CALCO. pp. 242–259 (2021).https://doi.org/10.4204/EPTCS.351. 15

    2021 doi

  20. [28]

    In: ICALP

    Schmid, T., Rozowski, W., Silva, A., Rot, J.: Processes parametrised by an algebraic theory. In: ICALP. pp. 132:1–132:20 (2022).https://doi.org/10.4230/LIPICS. ICALP.2022.132

    2022 doi

  21. [29]

    Smolka, S., Foster, N., Hsu, J., Kappé, T., Kozen, D., Silva, A.: Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang.4(POPL), 61:1–61:28 (2020). https://doi.org/10. 1145/3371129

    2020

  22. [30]

    Journal of Pure and Applied Algebra 219(8), 3110–3148 (2015)

    Sokolova, A., Woracek, H.: Congruences of convex algebras. Journal of Pure and Applied Algebra 219(8), 3110–3148 (2015). https://doi.org/j.jpaa.2014.10. 005

    2015

  23. [31]

    In: Proof, Language, and Interaction, Essays in Honour of Robin Milner

    Stark, E.W., Smolka, S.A.: A complete axiom system for finite-state probabilistic processes. In: Proof, Language, and Interaction, Essays in Honour of Robin Milner. pp. 571–596. MIT Press (2000)

    2000

  24. [32]

    Institute of Mathe- matics, Polish Academy of Sciences (1974)

    Świrszcz, T.: Monadic functors and categories of convex sets. Institute of Mathe- matics, Polish Academy of Sciences (1974)

    1974

  25. [33]

    In: LICS

    Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: LICS. pp. 280–291 (1997).https://doi.org/10.1109/LICS.1997.614955

    1997

  26. [34]

    Mathe- matical Structures in Computer Science16(1), 87–113 (2006).https://doi.org/ 10.1017/S0960129505005074 22 T

    Varacca, D., Winskel, G.: Distributing probability over non-determinism. Mathe- matical Structures in Computer Science16(1), 87–113 (2006).https://doi.org/ 10.1017/S0960129505005074 22 T. Kappé and T. Schmid A Proof of Proposition 4.4 and Soundness (Theorem 4.6) Proposition 4....

    2006 doi

  27. [35]

    – Let e = e(s) 1 e2

    Then γ(e1e2) = t1((⃗b, e2), (⃗ a,⃗f e2)) ∈ S∗(Act × (✓ + U (e))) because fie2 ∈ U (e1e2) for each i. – Let e = e(s) 1 e2. By induction, we findtk = tk((⃗b, ✓), (⃗ a,⃗f )) ∈ S∗(Act × (✓ + U (ek))) such that γ(ek) = tρ k for k ∈ {1, 2}. Then s t1((⃗b, e(s) 1 e2), (⃗ a,⃗f (e(s) 1...

  28. [36]

    , xn) ∈ S∗X, then suppX (tρ) ⊆ {x1,

    If t = t(x1, . . . , xn) ∈ S∗X, then suppX (tρ) ⊆ {x1, . . . , xn}

  29. [37]

    If x ∈ supp(tρ 1), then for any t2 such that T |= t1 = t2, x appears in t2 as a variable

    Let t1 ∈ S∗X. If x ∈ supp(tρ 1), then for any t2 such that T |= t1 = t2, x appears in t2 as a variable. Proof. Let us start with the first claim. By induction ont. If t = x ∈ X, then by definition of supp, suppX (xρ) = suppX ◦ η(x) = {x}. If t = σ(t1(⃗ x), . . . , tn(⃗ x)), th...

  30. [38]

    ⊆ {x1, . . . xn}. Hence, ifx ∈ suppX (tρ

  31. [39]

    A path of the formx1 → x2 → · · · →xn → x1 is called acycle

    = suppX (tρ 2), then x = xi for some i, which means thatx appears in t2. A path of the formx1 → x2 → · · · →xn → x1 is called acycle. Asimple cycle is a path of the same form withxi ̸= xj for i ̸= j. It is worth noting that (in an arbitrary directed graph), every cycle is the ...

  32. [40]

    Without loss of generality, we can assume that we haveh′ 1 = (e(s) 1 e2)g1 · · ·gk, ki = fi(e(s) 1 e2)g1 · · ·gk for e1 → f1 → · · · →✓

    By the induction hypothesis, sinceh1 →∗ h′ 1, this simple cycle is of the form(11). Without loss of generality, we can assume that we haveh′ 1 = (e(s) 1 e2)g1 · · ·gk, ki = fi(e(s) 1 e2)g1 · · ·gk for e1 → f1 → · · · →✓. Then we haveh →∗ h′ 1h2 = (e(s) 1 e2)g1 · · ·gkh2 → f1(e...

  33. [41]

    In this case,e is contained in a simple cycle of the form(11) by taking k = 0, e1 = h1, s = r, and e2 = h2

    We could havee = h′ 1(h(r) 1 h2) → · · · →h(s) 1 h2 → · · · →h′ 1(h(r) 1 h2) where h′ 1 →+ ✓. In this case,e is contained in a simple cycle of the form(11) by taking k = 0, e1 = h1, s = r, and e2 = h2

  34. [42]

    In this case, we must haveh′ 1 → k1 → · · · →km → h′

    Or, we could havee = h′ 1(h(r) 1 h2) → · · · →h′ 1(h(r) 1 h2) avoid h(r) 1 h2 alto- gether. In this case, we must haveh′ 1 → k1 → · · · →km → h′

  35. [43]

    gk and ki = fi(e(s) 1 e2)g1

    By the induction hypothesis applied toh1 →∗ h′ 1, without loss of generality we can assume that this cycle is of the formh′ 1 = (e(s) 1 e2)g1 . . . gk and ki = fi(e(s) 1 e2)g1 . . . gk for f1 → f2 → · · · →✓. In this case,e = h′ 1(h(r) 1 h2) = (e(s) 1 e2)g1 . . . gk(h(r) 1 h2)...

  36. [44]

    We do not havee →b+ e for any e ∈ Exp

  37. [45]

    For anye, f∈ Exp, if e →e f, then f →b+ e

  38. [46]

    The directed graph(Exp, ↷) is acyclic

  39. [47]

    For anye, f∈ Exp, if e ↷ f, then we do not havef → ✓. Proof. We already saw that(Exp, γ) is locally finite in Proposition 4.4. Let us check that it satisfies the other properties. Suppose e → · · · →e. We can assume without loss of generality that this is a simple cycle, since...

  40. [48]

    T∗ ⊢ ϕβ(y) = τβ(y, x)ϕβ(x), and

  41. [49]

    for any solutionφ to (X, β), T∗ ⊢ φ(y) = τβ(y, x)φ(x). Proof. We prove the first claim by induction on|y|bo. Suppose x ↷ y, and let β(y) = sρ tρ 1((⃗ a, y), (⃗b, ⃗ x)), tρ 2((⃗ c, x), ( ⃗d, ⃗ z)) (13) where ⃗ xis a vector such thaty ̸= xi and y →e xi for each i, and ⃗ zis a ve...

  42. [50]

    Define suppX (θ) = {x ∈ X | θ(x) > 0}

    ∪ suppX (tρ 2) ⊆ {⃗ x} ∪ {⃗ y} (IH) The free-algebra construction forCA is given by(D, η, ρ) [32], where D is the finitely supported probability distribution functor,ηX (x) = δx, (θ1 ⊕ρ p θ2)(α) = pθ1(α) + (1 − p)θ2, and 0ρ = δ⊥. Define suppX (θ) = {x ∈ X | θ(x) > 0}. This is ...

  43. [51]

    Define suppX (χ) = S α∈At{x ∈ X | χ(α)(x) > 0}

    ∪ suppX (tρ 2) ⊆ {⃗ x} ∪ {⃗ y} (IH) The free-algebra construction forGC is given by(D(⊥ + (−))At, η, ρ), where ηX (x)(α) = δx, (χ1 ⊕ρ p χ2)(α) = pχ1(α) + (1 − p)χ2, and 0ρ(α) = δ⊥. Define suppX (χ) = S α∈At{x ∈ X | χ(α)(x) > 0}. Again, it is straightforward to check that supp ...

  44. [52]

    ∪ suppX (tρ 2) ⊆ {⃗ x} ∪ {⃗ y} (IH) – If t = t1(⃗ x) +b t2(⃗ y), then suppX (tρ) = [ α∈At {x ∈ X | tρ(α)(x) > 0} = [ α≤b {x ∈ X | tρ 1(α)(x) > 0} ∪ [ α≤¯b {x ∈ X | tρ 2(α)(x) > 0} ⊆ [ α∈At {x ∈ X | tρ 1(α)(x) > 0} ∪ [ α∈At {x ∈ X | tρ 2(α)(x) > 0} = suppX (tρ

  45. [53]

    Define suppX (U ) = S θ∈U {x ∈ X | θ(x) > 0}

    ∪ suppX (tρ 2) ⊆ {⃗ x} ∪ {⃗ y} (IH) The free-algebra construction forCS is given by(C, η, ρ), where CX is the set of convex subsets ofD(⊥ + X) containing ⊥, ηX (x) = {pδ⊥ + (1 − p)δx | p ∈ [0, 1]}, (U ⊕ρ p V ) = {pθ1 + (1 − p)θ2 | p ∈ [0, 1], θ1 ∈ U, θ2 ∈ V }, and U +ρ V = con...

  46. [54]

    Skew commutativity.For any binary operationσ ∈ S, there is a binary operation τ ∈ S such that T ⊢ σ(x, y) = τ (y, x)

  47. [55]

    Skew associativity.For any binary operationsσ1, σ2 ∈ S, there are binary operations τ1, τ2 ∈ S such that T ⊢ σ1(x, σ2(y, z)) = τ1(τ2(x, y), z). Note that in a skew commutative skew associative theory, the reverse direction for skew associativity holds as well, since there must...

  48. [56]

    to obtain a term T ⊢ t′′ = τ ′(t1, t′

  49. [57]

    , xi+1, xi,

    such that the appearance sequence of t′′ is (x1, . . . , xi+1, xi, . . . , xm). • Suppose t1 = τ (t′ 1, t′′ 1 ) for some τ ∈ S, and the appearance sequences of t′ 1, t′′ 1 are (x1, . . . , xm) and (xm+1, . . . , xi) respectively. Then there are σ′, τ′, τ′′ ∈ S such that T ⊢ σ(...

  50. [58]

    if i + 1 < n, there is a termt′ = σ′(t′ 1, t′

  51. [59]

    , xn), T ⊢ t = t′, and the index ofσ′ in t′ is i + 1; and 40 T

    such that the appearance sequence of t′ is (x1, . . . , xn), T ⊢ t = t′, and the index ofσ′ in t′ is i + 1; and 40 T. Kappé and T. Schmid

  52. [60]

    if 1 < i, there is a termt′ = σ′(t′ 1, t′

  53. [61]

    , xn), T ⊢ t = t′, and the index ofσ′ in t′ is i − 1

    such that the appearance sequence of t′ is (x1, . . . , xn), T ⊢ t = t′, and the index ofσ′ in t′ is i − 1. Proof of claim 2.We will argue for these two items simultaneously by induction on t. There are two base cases, because of the restrictions oni in either situation (in pa...

  54. [62]

    Then we can manipulate terms T ⊢ t = σ(t1, τ(t2, t3)) = σ(t1, τ′(xi+1, t′ 3)) = σ′(τ ′′(t1, xi+1), t′

    and the conditions of item 2 are satisfied. Then we can manipulate terms T ⊢ t = σ(t1, τ(t2, t3)) = σ(t1, τ′(xi+1, t′ 3)) = σ′(τ ′′(t1, xi+1), t′

  55. [63]

    (skew associativity) Thus, the index ofσ′ in t′ = σ′(τ ′′(t1, xi+1), t′

  56. [64]

    – If the index ofσ in t is 1 < i, then there existt1, t2, t3 and τ ∈ S such that t = σ(τ (t1, t2), t3)

    is i + 1. – If the index ofσ in t is 1 < i, then there existt1, t2, t3 and τ ∈ S such that t = σ(τ (t1, t2), t3). By repeatedly applying the induction hypothesis, item 1, to τ (t1, t2), we can find aτ ′ and t′ 1 such that T ⊢ τ (t1, t2) = τ ′(t′ 1, xi) and the conditions of it...

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.