A Kleene theorem for free many-sorted algebras

Enric Cosme Ll\'opez; L\"u Gong; Nofre Sanmart\'in Vich; Ra\'ul Ruiz Mora

arxiv: 2606.29939 · v1 · pith:XBT4CARQnew · submitted 2026-06-29 · 💻 cs.LO · cs.FL

A Kleene theorem for free many-sorted algebras

L\"u Gong , Ra\'ul Ruiz Mora , Nofre Sanmart\'in Vich , Enric Cosme Ll\'opez This is my paper

Pith reviewed 2026-06-30 04:27 UTC · model grok-4.3

classification 💻 cs.LO cs.FL

keywords many-sorted algebrasKleene theoremrecognizable languagesregular languagesfree algebrasautomata theoryformal language theory

0 comments

The pith

In free many-sorted algebras, a language of a given sort is recognizable if and only if it is regular under finitary assumptions.

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

This paper generalizes Kleene's theorem from single-sorted to many-sorted free algebras. It shows that recognizability by finite automata matches regularity via expressions for any language over one fixed sort, once finitary assumptions are in place. The result lets the same decision procedures and closure properties known for ordinary regular languages carry over to structures that distinguish multiple sorts, such as typed terms or multi-category algebraic data.

Core claim

The paper proves that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra is recognizable if and only if it is regular.

What carries the argument

The equivalence between recognizability by many-sorted automata and regularity by many-sorted expressions over the free algebra.

If this is right

Regular expressions denote exactly the sets recognizable by finite many-sorted automata.
Standard conversions between automata and expressions extend directly to the multi-sorted case.
Closure properties of regular languages hold for languages of each individual sort.
Decision procedures for emptiness, membership and equivalence transfer to the many-sorted setting.

Where Pith is reading between the lines

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

The same automata constructions could be applied to term rewriting systems over multi-sorted signatures.
Typed query languages or database schemas might inherit regular-language algorithms via this equivalence.
One could test the boundary by relaxing the finitary assumptions in small concrete algebras.

Load-bearing premise

The algebra must be free and the finitary assumptions must hold so the usual automata-to-expression constructions remain valid.

What would settle it

Exhibit a free many-sorted algebra obeying the finitary assumptions together with a set of elements of one sort that is accepted by a finite automaton yet not denoted by any regular expression.

read the original abstract

In this work, we generalize Kleene's theorem from free single-sorted algebras to free many-sorted algebras. Our main result establishes that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra is recognizable if and only if it is regular.

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.

Desk Editor's Note private letter to a colleague

The paper lifts Kleene's theorem to many-sorted free algebras under finitary conditions; the lift looks plausible but the abstract supplies no proof details.

read the letter

The core claim is that in free many-sorted algebras, under suitable finitary assumptions, a language of a given sort is recognizable exactly when it is regular. This is the natural many-sorted version of the classical single-sorted result.

The new element is the handling of multiple sorts while preserving the equivalence. The authors correctly flag that the result is conditional on finitary assumptions, which matches how these theorems are usually stated. If the proof adapts the standard constructions without extra machinery, that is useful incremental work for people who already use many-sorted algebras in logic or typed automata.

The main limitation visible from the abstract is the absence of any proof sketch or explicit statement of the finitary conditions. Without seeing how the sorting discipline interacts with the automata or the regularity definition, it is impossible to judge whether the generalization is routine or requires new technical steps. The claim itself does not look circular or over-stated, but the lack of even a high-level argument leaves the technical substance untested.

This is a paper for specialists already working in automata theory or algebraic language theory who need the many-sorted case for their own models. A reader outside that niche will not gain much. The result is narrow enough that it does not need to be read by everyone, but it is the sort of targeted extension that can be cited when someone needs the typed version.

If the full manuscript contains a complete, self-contained proof that checks out, it is worth sending to referees. The topic is established enough that a careful verification of the details would be the main service a review provides.

Referee Report

0 major / 1 minor

Summary. The manuscript generalizes Kleene's theorem from free single-sorted algebras to free many-sorted algebras. The central claim is that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra is recognizable if and only if it is regular.

Significance. If the result holds with the stated assumptions, it extends a foundational theorem in automata theory to the many-sorted setting. This could support further work on recognizability in typed or multi-sorted algebraic structures. The explicit conditioning on finitary assumptions is a strength, as it avoids overclaiming generality.

minor comments (1)

[Abstract] Abstract: the claim is stated without a proof sketch, without an explicit list of the finitary assumptions, and without indication of how the sorting discipline is preserved in the equivalence. This makes it difficult to assess the central claim from the provided text alone.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the summary and for noting the potential significance of extending Kleene's theorem under finitary assumptions. The recommendation is listed as uncertain, but the report contains no major comments. We therefore provide no point-by-point responses. If the referee can supply specific concerns, we will address them directly in a revision.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper states a conditional equivalence theorem generalizing Kleene's result to free many-sorted algebras under finitary assumptions. No equations, parameters, or self-citations appear in the provided abstract or reader's extraction that reduce the claim to its inputs by construction. The result is presented as a theorem rather than a renaming, fit, or self-referential definition, making the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no explicit free parameters, axioms, or invented entities; the finitary assumptions are mentioned but not enumerated.

pith-pipeline@v0.9.1-grok · 5576 in / 1016 out tokens · 41339 ms · 2026-06-30T04:27:27.612542+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

13 extracted references · 11 canonical work pages

[1]

[Ber15] G. M. Bergman.An Invitation to General Algebra and Universal Constructions. Universitext. Springer, Cham, 2 edition, 2015.doi:10.1007/978-3-319-11478-1. [Bou70] N. Bourbaki.Th´ eorie des Ensembles. Hermann, Paris,

work page doi:10.1007/978-3-319-11478-1 2015
[2]

Bonsangue, J

[BRS09] M. Bonsangue, J. Rutten, and A. Silva. A Kleene theorem for polynomial coalgebras. In L. de Alfaro, editor,Foundations of Software Science and Computational Structures (FOSSACS 2009), volume 5504 ofLecture Notes in Computer Science, pages 122–136, Berlin, Heidelberg,

2009
[3]

doi:10.1007/978-3-642-00596-1_10

Springer. doi:10.1007/978-3-642-00596-1_10. [BS81] S. Burris and H. P. Sankappanavar.A Course in Universal Algebra. Springer, New York, Berlin,

work page doi:10.1007/978-3-642-00596-1_10
[4]

Cruchten

[Cru25] M. Cruchten. Kleene theorems for lasso languages and ω-languages.Theory of Computing Systems, 2025.doi:10.1007/s00224-025-10231-0. [CVCL20] J. Climent Vidal and E. Cosme Ll´ opez. Congruence-based proofs of the recognizability theorems for free many-sorted algebras.Journal of Logic and Computation, 30(2):561–633,

work page doi:10.1007/s00224-025-10231-0 2025
[5]

[Die66] K.-H

doi: 10.1093/logcom/exz032. [Die66] K.-H. Diener. Order in absolutely free and related algebras.Colloquium Mathematicum, 14:63–72, 1966.doi:10.4064/cm-14-1-63-72. A KLEENE THEOREM FOR FREE MANY-SORTED ALGEBRAS 35 [Eil74] S. Eilenberg.Automata, Languages, and Machines. Vol. A, volume 58 ofPure and Applied Mathematics. Academic Press, New York,

work page doi:10.1093/logcom/exz032 1966
[6]

10 Uli Fahrenberg and Krzysztof Ziemianski

doi: 10.46298/lmcs-20(4:22)2024. [Gr¨ a08] G. Gr¨ atzer.Universal Algebra. Springer, New York, 2 edition,

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

With appendices by the author, Bjarni J´ onsson, Walter Taylor, Robert W

Revised reprint of the 1979 second edition. With appendices by the author, Bjarni J´ onsson, Walter Taylor, Robert W. Quack- enbush, G¨ unter H. Wenzel, and the author and W. A. Lampe.doi:10.1007/978-0-387-77487-9 . [GS84] F. G´ ecseg and M. Steinby.Tree Automata. Akad´ emiai Kiad´ o, Budapest,

work page doi:10.1007/978-0-387-77487-9 1979
[8]

[GTW78] J

doi:10.1007/978-3-642-59126-6_1. [GTW78] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor,Current Trends in Programming Methodology, IV, chapter 5, pages 80–149. Prentice Hall, New Jersey,

work page doi:10.1007/978-3-642-59126-6_1
[9]

[Kle56] S. C. Kleene. Representation of events in nerve nets and finite automata. In C. E. Shannon and J. McCarthy, editors,Automata Studies, number 34 in Annals of Mathematics Studies, pages 3–42. Princeton University Press, Princeton, NJ, 1956.doi:10.1515/9781400882618-002. [Mat76] G. Matthiessen.Theorie der Heterogenen Algebren. Mathematik-Arbeitspapie...

work page doi:10.1515/9781400882618-002 1956
[10]

Matthiessen

[Mat79] G. Matthiessen. A heterogeneous algebraic approach to some problems in automata theory, many valued logic and other topics. InContributions to General Algebra (Proc. Klagenfurt Conf., Klagenfurt, 1978), pages 193–211. Heyn, Klagenfurt,

1978
[11]

Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathe- matics

[ML98] S. Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathe- matics. Springer, New York, 2 edition, 1998.doi:10.1007/978-1-4757-4721-8. [MW67] J. Mezei and J. B. Wright. Algebraic automata and context-free sets.Information and Control, 11:3–29, 1967.doi:10.1016/S0019-9958(67)90353-1. [MY60] R. McNaughton and H. Yamada. ...

work page doi:10.1007/978-1-4757-4721-8 1998
[12]

[Ner58] A. Nerode. Linear automaton transformations.Proceedings of the American Mathematical Society, 9:541–544, 1958.doi:10.1090/S0002-9939-1958-0135681-9. [Rie16] E. Riehl.Category Theory in Context. Dover Publications, Inc., Mineola, New York,

work page doi:10.1090/s0002-9939-1958-0135681-9 1958
[13]

[RS59] M. O. Rabin and D. Scott. Finite automata and their decision problems.IBM Journal of Research and Development, 3:114–125, 1959.doi:10.1147/rd.32.0114. [Sch61] M. P. Sch¨ utzenberger. On the definition of a family of automata.Information and Control, 4:245–270, 1961.doi:10.1016/S0019-9958(61)80020-X. [Wec92] W. Wechler.Universal Algebra for Computer...

work page doi:10.1147/rd.32.0114 1959

[1] [1]

[Ber15] G. M. Bergman.An Invitation to General Algebra and Universal Constructions. Universitext. Springer, Cham, 2 edition, 2015.doi:10.1007/978-3-319-11478-1. [Bou70] N. Bourbaki.Th´ eorie des Ensembles. Hermann, Paris,

work page doi:10.1007/978-3-319-11478-1 2015

[2] [2]

Bonsangue, J

[BRS09] M. Bonsangue, J. Rutten, and A. Silva. A Kleene theorem for polynomial coalgebras. In L. de Alfaro, editor,Foundations of Software Science and Computational Structures (FOSSACS 2009), volume 5504 ofLecture Notes in Computer Science, pages 122–136, Berlin, Heidelberg,

2009

[3] [3]

doi:10.1007/978-3-642-00596-1_10

Springer. doi:10.1007/978-3-642-00596-1_10. [BS81] S. Burris and H. P. Sankappanavar.A Course in Universal Algebra. Springer, New York, Berlin,

work page doi:10.1007/978-3-642-00596-1_10

[4] [4]

Cruchten

[Cru25] M. Cruchten. Kleene theorems for lasso languages and ω-languages.Theory of Computing Systems, 2025.doi:10.1007/s00224-025-10231-0. [CVCL20] J. Climent Vidal and E. Cosme Ll´ opez. Congruence-based proofs of the recognizability theorems for free many-sorted algebras.Journal of Logic and Computation, 30(2):561–633,

work page doi:10.1007/s00224-025-10231-0 2025

[5] [5]

[Die66] K.-H

doi: 10.1093/logcom/exz032. [Die66] K.-H. Diener. Order in absolutely free and related algebras.Colloquium Mathematicum, 14:63–72, 1966.doi:10.4064/cm-14-1-63-72. A KLEENE THEOREM FOR FREE MANY-SORTED ALGEBRAS 35 [Eil74] S. Eilenberg.Automata, Languages, and Machines. Vol. A, volume 58 ofPure and Applied Mathematics. Academic Press, New York,

work page doi:10.1093/logcom/exz032 1966

[6] [6]

10 Uli Fahrenberg and Krzysztof Ziemianski

doi: 10.46298/lmcs-20(4:22)2024. [Gr¨ a08] G. Gr¨ atzer.Universal Algebra. Springer, New York, 2 edition,

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

[7] [7]

With appendices by the author, Bjarni J´ onsson, Walter Taylor, Robert W

Revised reprint of the 1979 second edition. With appendices by the author, Bjarni J´ onsson, Walter Taylor, Robert W. Quack- enbush, G¨ unter H. Wenzel, and the author and W. A. Lampe.doi:10.1007/978-0-387-77487-9 . [GS84] F. G´ ecseg and M. Steinby.Tree Automata. Akad´ emiai Kiad´ o, Budapest,

work page doi:10.1007/978-0-387-77487-9 1979

[8] [8]

[GTW78] J

doi:10.1007/978-3-642-59126-6_1. [GTW78] J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the specification, correctness, and implementation of abstract data types. In R. T. Yeh, editor,Current Trends in Programming Methodology, IV, chapter 5, pages 80–149. Prentice Hall, New Jersey,

work page doi:10.1007/978-3-642-59126-6_1

[9] [9]

[Kle56] S. C. Kleene. Representation of events in nerve nets and finite automata. In C. E. Shannon and J. McCarthy, editors,Automata Studies, number 34 in Annals of Mathematics Studies, pages 3–42. Princeton University Press, Princeton, NJ, 1956.doi:10.1515/9781400882618-002. [Mat76] G. Matthiessen.Theorie der Heterogenen Algebren. Mathematik-Arbeitspapie...

work page doi:10.1515/9781400882618-002 1956

[10] [10]

Matthiessen

[Mat79] G. Matthiessen. A heterogeneous algebraic approach to some problems in automata theory, many valued logic and other topics. InContributions to General Algebra (Proc. Klagenfurt Conf., Klagenfurt, 1978), pages 193–211. Heyn, Klagenfurt,

1978

[11] [11]

Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathe- matics

[ML98] S. Mac Lane.Categories for the Working Mathematician, volume 5 ofGraduate Texts in Mathe- matics. Springer, New York, 2 edition, 1998.doi:10.1007/978-1-4757-4721-8. [MW67] J. Mezei and J. B. Wright. Algebraic automata and context-free sets.Information and Control, 11:3–29, 1967.doi:10.1016/S0019-9958(67)90353-1. [MY60] R. McNaughton and H. Yamada. ...

work page doi:10.1007/978-1-4757-4721-8 1998

[12] [12]

[Ner58] A. Nerode. Linear automaton transformations.Proceedings of the American Mathematical Society, 9:541–544, 1958.doi:10.1090/S0002-9939-1958-0135681-9. [Rie16] E. Riehl.Category Theory in Context. Dover Publications, Inc., Mineola, New York,

work page doi:10.1090/s0002-9939-1958-0135681-9 1958

[13] [13]

[RS59] M. O. Rabin and D. Scott. Finite automata and their decision problems.IBM Journal of Research and Development, 3:114–125, 1959.doi:10.1147/rd.32.0114. [Sch61] M. P. Sch¨ utzenberger. On the definition of a family of automata.Information and Control, 4:245–270, 1961.doi:10.1016/S0019-9958(61)80020-X. [Wec92] W. Wechler.Universal Algebra for Computer...

work page doi:10.1147/rd.32.0114 1959