pith. sign in

arxiv: 2605.25253 · v2 · pith:FDN3NEN2new · submitted 2026-05-24 · 💻 cs.FL

Algebraic Characterization of FO-definable Languages of Higher-Dimensional Automata

Enzo Erlich , J\'er\'emy Ledent , Krzysztof Ziemia\'nski This is my paper

Pith reviewed 2026-06-30 11:45 UTC · model grok-4.3

classification 💻 cs.FL
keywords higher-dimensional automatapomset languagesregular languagesfirst-order definabilityalgebraic characterizationaperiodic categoriesMcNaughton-Papert theorem
0
0 comments X

The pith

A pomset language is regular exactly when it is the inverse image of a functor from the pomset category to a finite category.

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

Higher-dimensional automata recognize languages consisting of pomsets, which generalize words to allow partial ordering of events for modeling concurrency. The paper proves that such a language is regular if and only if it equals the inverse image of a functor mapping the category of all pomsets into some finite category. It is definable in first-order logic precisely when the target category is aperiodic. This extends the McNaughton-Papert theorem from sequential words to concurrent pomset languages, so that algebraic properties of categories can determine logical definability of concurrent behaviors.

Core claim

We prove that a language of pomsets is regular if and only if it is the inverse image of a functor from the category of pomsets into a finite category. Furthermore, the language is definable in first-order logic exactly when it is recognized by an aperiodic category. This generalizes the McNaughton-Papert theorem to HDA languages. We also show that if a language is accepted by a counter-free HDA, it must be definable in first-order logic, though the converse is open.

What carries the argument

The inverse image of a functor from the category of pomsets to a finite or aperiodic category, which recognizes the language.

If this is right

  • Regular HDA languages are exactly those obtained as inverse images under functors to finite categories.
  • First-order definable HDA languages are exactly those obtained as inverse images under functors to aperiodic categories.
  • Counter-free higher-dimensional automata accept only first-order definable languages.
  • The algebraic characterization allows using category theory to classify definable languages of concurrent systems.

Where Pith is reading between the lines

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

  • If the characterization holds, one could develop algorithms to check first-order definability by constructing or verifying the target category's properties.
  • The open converse for counter-free HDA suggests a direction for future work to find if every FO-definable language has a counter-free automaton.
  • Similar functor-based characterizations might apply to other concurrency models beyond HDA.
  • Testing the result on small pomset languages from specific concurrent protocols could validate or refine the equivalence.

Load-bearing premise

That acceptance by a higher-dimensional automaton is equivalent to the language being the inverse image of some functor from the pomset category to a finite category.

What would settle it

Finding a specific pomset language that can be obtained as the inverse image of a functor to a finite category but is not accepted by any higher-dimensional automaton.

read the original abstract

Higher-dimensional automata (HDA) are a model of concurrency that models simultaneous execution of events using higher dimensional cells. HDA recognize languages of pomsets, a generalization of finite words whose letters are partially ordered. We prove a new algebraic characterization of HDA languages: a language of pomsets is regular if and only if it is the inverse image of a functor from the category of pomsets into a finite category. Furthermore, the language is definable in first-order logic exactly when it is recognized by an aperiodic category, generalizing the McNaughton-Papert theorem to HDA languages. We also investigate a notion of counter-free HDA, and show that if a language is accepted by a counter-free HDA, it must be definable in first-order logic. The converse, however, is still open.

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 paper claims an algebraic characterization of languages recognized by higher-dimensional automata (HDA) over pomsets: a pomset language is regular iff it is the inverse image of a functor from the category of pomsets to a finite category, and it is first-order definable exactly when recognized by an aperiodic category (generalizing McNaughton-Papert). It further shows that acceptance by counter-free HDA implies FO definability, but leaves the converse open.

Significance. If the central equivalences hold, the work extends classical word-language results to concurrent models via HDA and pomsets, supplying algebraic and categorical tools for regularity and logic definability in higher-dimensional settings. The explicit one-direction result for counter-free HDA is a useful partial contribution.

major comments (1)
  1. [Main theorems (statements and proofs of the regularity and FO characterizations)] The load-bearing claim is the equivalence between HDA recognition and inverse images under functors to finite (resp. aperiodic) categories. Both directions of the stated iff must be shown to preserve acceptance on pomsets whose partial order is not a total order (i.e., on higher-dimensional cells). The manuscript must supply explicit constructions of the finite/aperiodic category and functor from an arbitrary HDA, and of an HDA from an arbitrary such functor, together with verification that the acceptance condition agrees on non-linear pomsets; otherwise the characterizations do not extend beyond the linear case.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful review and for emphasizing the need to confirm that the algebraic characterizations extend to non-linear pomsets. We address the major comment below.

read point-by-point responses

  1. Referee: [Main theorems (statements and proofs of the regularity and FO characterizations)] The load-bearing claim is the equivalence between HDA recognition and inverse images under functors to finite (resp. aperiodic) categories. Both directions of the stated iff must be shown to preserve acceptance on pomsets whose partial order is not a total order (i.e., on higher-dimensional cells). The manuscript must supply explicit constructions of the finite/aperiodic category and functor from an arbitrary HDA, and of an HDA from an arbitrary such functor, together with verification that the acceptance condition agrees on non-linear pomsets; otherwise the characterizations do not extend beyond the linear case.

    Authors: We agree that explicit verification on non-linear pomsets is essential for the claims to hold in full generality. The constructions of the finite (resp. aperiodic) category from an HDA and the reverse HDA from a functor are defined using the full category of pomsets, whose objects and morphisms incorporate arbitrary partial orders; the acceptance condition is likewise defined via functor application to the entire pomset. Nevertheless, the current proofs do not isolate a separate argument or example confirming agreement specifically when events are incomparable. In the revision we will add an explicit lemma (with proof) verifying both directions on a representative non-linear pomset, together with a short subsection containing the constructions restated for the higher-dimensional case. This will be a clarifying addition rather than a change to the theorems themselves. revision: yes

Circularity Check

0 steps flagged

No circularity; equivalence is the independent theorem being proved

full rationale

The paper states and proves the iff characterizations as its central results, generalizing the external McNaughton-Papert theorem to HDA/pomset languages. No self-definitional steps, fitted inputs renamed as predictions, load-bearing self-citations, uniqueness theorems imported from the authors, or ansatzes smuggled via citation appear in the provided text. The load-bearing equivalence between HDA recognition and inverse images under functors is the content of the new proof, not an input that reduces to itself by construction. The derivation is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard mathematical structures from category theory and the established definitions of HDA and pomsets from prior literature; no free parameters, ad-hoc axioms, or new entities are indicated in the abstract.

axioms (1)
  • standard math Standard axioms of category theory (existence of categories, functors, and finite categories)
    The characterizations are stated in terms of functors from the category of pomsets to finite or aperiodic categories.

pith-pipeline@v0.9.1-grok · 5676 in / 1331 out tokens · 47336 ms · 2026-06-30T11:45:39.203941+00:00 · methodology

Review history (2 revisions) →

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

10 extracted references · 9 canonical work pages

  1. [1]

    Presenting interval pomsets with interfaces

    1 Amazigh Amrane, Hugo Bazille, Emily Clement, Uli Fahrenberg, and Krzysztof Ziemianski. Presenting interval pomsets with interfaces. In Uli Fahrenberg, Wesley Fussner, and Roland Glück, editors,Relational and Algebraic Methods in Computer Science - 21st International Conference, RAMiCS 2024, Prague, Czech Republic, August 19-22, 2024, Proceedings, volume...

    2024

  2. [2]

    2 Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, and Marie Fortin

    doi:10.1007/ 978-3-031-68279-7\_3. 2 Amazigh Amrane, Hugo Bazille, Uli Fahrenberg, and Marie Fortin. Logic and languages of higher-dimensional automata. In Joel D. Day and Florin Manea, editors,Developments in Language Theory - 28th International Conference, DLT 2024, Göttingen, Germany, August 12-16, 2024, Proceedings, volume 14791 ofLecture Notes in Com...

    work page doi:10.1007/978-3-031-66159-4 2024

  3. [3]

    4 Thomas Baronner, Henning Basold, and Márton Hablicsek

    URL:https://doi.org/10.1016/j.tcs.2025.115156,doi:10.1016/J.TCS.2025.115156. 4 Thomas Baronner, Henning Basold, and Márton Hablicsek. Irrationality of process rep- lication for higher-dimensional automata. In Uli Fahrenberg, Wesley Fussner, and Ro- land Glück, editors,Relational and Algebraic Methods in Computer Science - 21st Inter- national Conference, ...

    work page doi:10.1016/j.tcs.2025.115156 2025

  4. [4]

    5 Emily Clement, Enzo Erlich, and Jérémy Ledent

    doi:10.1007/978-3-031-68279-7\_4. 5 Emily Clement, Enzo Erlich, and Jérémy Ledent. Kamp theorem for pomset languages of higher dimensional automata.CoRR, abs/2410.12493,

    work page doi:10.1007/978-3-031-68279-7

  5. [5]

    48550/arXiv.2410.12493,arXiv:2410.12493,doi:10.48550/ARXIV.2410.12493

    URL: https://doi.org/10. 48550/arXiv.2410.12493,arXiv:2410.12493,doi:10.48550/ARXIV.2410.12493. 6 Volker Diekert and Paul Gastin. First-order definable languages. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors,Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 ofTexts in Logic and Games, pages 261–306. Ams- terdam ...

    work page doi:10.48550/arxiv.2410.12493

  6. [6]

    9 Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemianski

    doi: 10.1017/S0960129521000293. 9 Uli Fahrenberg, Christian Johansen, Georg Struth, and Krzysztof Ziemianski. Kleene theorem for higher-dimensional automata.Log. Methods Comput. Sci., 20(4),

    work page doi:10.1017/s0960129521000293

  7. [7]

    10 Uli Fahrenberg and Krzysztof Ziemianski

    URL: https: //doi.org/10.46298/lmcs-20(4:22)2024,doi:10.46298/LMCS-20(4:22)2024. 10 Uli Fahrenberg and Krzysztof Ziemianski. Myhill-Nerode theorem for higher-dimensional automata.Fundam. Informaticae, 192(3-4):219–259, 2024.doi:10.3233/FI-242194. 11 Johan Anthony Willem Kamp.Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Departme...

    work page doi:10.46298/lmcs-20(4:22)2024 2024

  8. [8]

    On interprocess communication

    12 Leslie Lamport. On interprocess communication. part I: basic formalism.Distributed Comput., 1(2):77–85, 1986.doi:10.1007/BF01786227. 13 Robert McNaughton and Seymour Papert.Counter-Free Automata, volume Research Mono- graph,

    work page doi:10.1007/bf01786227 1986

  9. [9]

    14 Vaughan R. Pratt. Modeling concurrency with geometry. In David S. Wise, editor,Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, pages 311–322. ACM Press, 1991.doi:10.1145/ 99583.99625. E. Erlich, J. Ledent, K. Ziemiański 17 15 Marcel Paul Schützenberger. On fini...

    work page arXiv 1991

  10. [10]

    URL:https://www.sciencedirect.com/science/article/ pii/S0019995865901087,doi:10.1016/S0019-9958(65)90108-7

    work page doi:10.1016/s0019-9958(65)90108-7