Extending the Ginsburg-Spanier Theorem to Functions and Mixed Arithmetic

Alain Finkel; J\'er\^ome Leroux

Extending the Ginsburg-Spanier Theorem to Functions and Mixed Arithmetic

T0 review · 0 major / 4 minor · reviewed 2026-07-11 · grok-4.5

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

Pith's one-line read Definable functions in the three classical additive theories are exactly the piecewise-linear and piecewise-simple functions, characterized purely algebraically.

desk verdict Clean algebraic normal forms for functions in three additive theories, plus a real correction of Weispfenning; short, elementary, and worth citing. read the letter →

arxiv 2607.05701 v2 pith:AVTLBR7Z submitted 2026-07-06 cs.LO cs.FL

Alain Finkel , Jérôme Leroux This is my paper · ORCID

classification cs.LOcs.FL MSC 03B2503C1068Q60

keywords Presburgerarithmeticsemi-linearsetspiecewiselinearfunctionsmixedreal-integersemi-polinearpiecewise-simpleadditivetheoriesGinsburg–Spaniertheorem

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 gives a single geometric picture of the sets and functions that can be defined using only addition and order, over the integers, over the reals, and over both at once. It starts from the classical Ginsburg–Spanier theorem (definable integer sets are the semi-linear sets) and extends it in two directions. First, the functions definable over the integers or over the reals are exactly the piecewise-linear functions on a definable partition of the domain. Second, for the mixed theory that talks about both reals and integers, the definable sets are exactly the new semi-polinear sets (a polyhedral fractional piece plus a semi-linear integer piece), and the definable functions are exactly the piecewise-simple functions that treat the integer and fractional parts of each argument with independent linear coefficients. The proofs use only linear algebra and a short stability lemma, with no automata or quantifier-elimination machinery, and they also correct an earlier incomplete description of the mixed sets. A sympathetic reader cares because the three theories now sit in one clean algebraic framework that can be used directly in verification, constraint solving, and synthesis.

What carries the argument

Semi-polinear sets (a polyhedral convex piece in the unit cube plus a finitely generated monoid of integer vectors) together with the stability lemma that any additive function whose graph lies in rational vectors is linear; these objects turn the classical Ginsburg–Spanier theorem into function and mixed-arithmetic characterisations.

What would settle it

Exhibit a function whose graph is definable by a first-order formula using only addition and order over Z (or R, or R and Z) but that fails to be piecewise linear (or piecewise-simple) on any finite definable partition of its domain, or exhibit a mixed-definable set that is not a finite union of polinear sets.

Watch

Extended reading notes

Core claim

The paper proves that FO(Z,+,≤)-definable functions are exactly the FO(Z,+,≤)-piecewise linear functions, that FO(R,+,≤)-definable functions are exactly the FO(R,+,≤)-piecewise linear functions, that FO(R,Z,+,≤)-definable sets are exactly the semi-polinear sets, and that FO(R,Z,+,≤)-definable functions are exactly the piecewise-simple functions.

Load-bearing premise

The whole argument treats the classical Ginsburg–Spanier theorem (integer-definable sets are semi-linear) as a black box; any gap there would immediately break the function and mixed characterisations.

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.

Desk Editor's Note

read the letter

The punchline is simple: Finkel and Leroux give explicit geometric normal forms for the functions (not just the sets) of FO(Z,+,≤), FO(R,+,≤) and FO(R,Z,+,≤). Presburger and real-additive functions are exactly the piecewise-linear ones; mixed functions are the new “piecewise-simple” class (linear separately on fractional and integer parts, possibly with different slopes). They also introduce semi-polinear sets and prove they coincide with the mixed-definable sets, correcting Weispfenning’s monoid-versus-group slip on R.

What is actually new is the packaging and the mixed case. Applying Ginsburg–Spanier to the graph of a Presburger function and reading off linearity was always available; nobody wrote the theorem with a direct algebraic proof. The real case is similar once you have density of rational points in polyhedra. The mixed material is the real contribution: the semi-polinear definition, the structural-induction proof that mixed sets are exactly those, the extraction of simple pieces for functions, and the explicit fix of Weispfenning. All of it is done with linear algebra, Fourier–Motzkin and Ginsburg–Spanier; no automata, no QE black boxes beyond the classical ones.

The proofs are short and look solid. The stability lemma (stable rational graph implies linear) is elementary and correctly applied; the mixed-function argument that the integer part cannot have a non-trivial kernel in the last coordinate is clean. Soft spots are minor: the paper is candid that the integer and real function results were “implicit,” the significance is inside the subfield rather than a new decision procedure, and the open problem on Büchi arithmetic is left open. None of that undercuts the claims.

This is for people who work with Presburger, real or mixed linear arithmetic in verification, synthesis or constraint solving and want geometric normal forms they can actually use. It deserves a serious referee; I would accept it for peer review and I would cite the mixed characterisations and the Weispfenning correction. Bring it to reading group if the group cares about additive theories or geometric model theory of arithmetic.

Referee Report

0 major / 4 minor

Summary. The paper extends the Ginsburg–Spanier theorem from sets to functions and from pure integer/real additive theories to the mixed theory FO(R,Z,+,≤). It proves that FO(Z,+,≤)- and FO(R,+,≤)-definable functions are exactly the piecewise-linear functions (Theorems 4.2 and 3.4), introduces semi-polinear sets and shows they coincide with mixed-linear sets (Theorem 5.4), and characterises FO(R,Z,+,≤)-definable functions as the piecewise-simple functions (Theorem 5.9). All arguments are purely algebraic, relying on a stability lemma (Proposition 3.1), density of rationals in polyhedra, Fourier–Motzkin elimination, and the classical Ginsburg–Spanier theorem; an error in Weispfenning’s description of mixed-linear sets of R is corrected (Remark 5.5).

Significance. If correct, the results supply the missing algebraic row of the comparison table for the three classical additive theories and give clean, logic-free normal forms (piecewise linear / piecewise-simple) that are immediately usable in verification, synthesis and constraint solving. The proofs are short, self-contained and free of automata or quantifier-elimination machinery; the correction of the monoid-versus-group error in Weispfenning is a genuine service to the literature. The notions of semi-polinear set and piecewise-simple function are new and natural. The work therefore unifies three well-studied decidable theories under a single geometric framework and fills a surprising gap that had remained open despite decades of related automata-theoretic and logical characterisations.

minor comments (4)

In the proof of Theorem 5.9 the extraction of the integer-part function h relies on a short linear-algebra argument that P⊥ cannot lie inside Q^n × {0}. A one-sentence remark that the same conclusion follows from the fact that the projection of a monoid graph that is a function must itself be a monoid would make the argument even more transparent.
Table 1 lists “semi-polinear” and “piecewise-simple” in bold as contributions of the paper; it would be helpful to add a footnote or parenthetical citation to the corresponding theorems so that a reader scanning the table can jump directly to the statements.
The open problem on FO(Z,+,Vp)-definable functions is interesting; a one-line pointer to the known automata or logical characterisations of Büchi arithmetic would orient the reader.
A few minor typographical inconsistencies appear (e.g., “polinear” vs. “polylinear” in informal prose, spacing around “FO(R,Z,+,≤)”). They do not affect readability but should be cleaned in the final version.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: characterizations are derived from classical Ginsburg–Spanier plus elementary linear algebra, not from self-defined or fitted quantities.

full rationale

The paper’s load-bearing steps are (i) the classical Ginsburg–Spanier theorem (Thm 4.1 / [GS66]) that FO(Z,+,≤)-definable sets are semi-linear, (ii) the elementary stability lemma (Prop 3.1) that a stable map with rational graph is linear, proved from first principles via bases of Q-vector spaces, and (iii) for the mixed theory a structural induction on FO(R,Z,R≥0,G+) that exhibits an explicit finite polinear decomposition of the addition relation (Thm 5.4). Piecewise-linear and piecewise-simple characterizations of functions then follow by restricting the graph to one linear/polinear piece (Lemma 2.1) and applying stability or a short orthogonal-complement argument (P⊥ cannot lie in Q^n×{0}). None of these steps defines the target notion in terms of itself, fits a parameter and renames it a prediction, or rests on a self-citation that already contains the claimed result. The 2008 unpublished manuscript is acknowledged only as historical origin; every proof is written out in full. The correction of Weispfenning’s monoid-versus-group error is independent of the authors’ own prior work. Consequently the derivation chain is non-circular.

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

The paper works entirely inside classical first-order arithmetic and linear algebra. The only non-trivial external theorem is Ginsburg–Spanier; all other ingredients are standard. The two new geometric notions (semi-polinear sets, piecewise-simple functions) are definitional and receive independent characterisations, so they do not function as free parameters or ungrounded entities.

assumptions (3)

domain assumption Ginsburg–Spanier theorem: FO(Z,+,≤)-definable sets are exactly the semi-linear sets
Invoked as a black box in the proofs of Theorems 4.2 and 5.4; any incompleteness would propagate.
standard math Fourier–Motzkin elimination preserves polyhedral convexity
Used for quantifier elimination over the reals and for component removal of semi-polinear sets.
ad hoc to paper A stable function f:R^n o R^q whose graph lies in Q^n imes Q^q is linear (Proposition 3.1)
Proved in the paper from the definition of a Q-vector-space basis; serves as the key algebraic engine for all three function characterisations.

invented entities (2)

semi-polinear set independent evidence
purpose: Geometric normal form for FO(R,Z,+,≤)-definable sets: finite union of C+b+M where C is polyhedral in [0,1)^n and M is a finitely generated monoid
Definitional; shown equivalent to mixed-linear sets by structural induction on formulas, so it has an independent characterisation inside the paper.
piecewise-simple function independent evidence
purpose: Normal form for FO(R,Z,+,≤)-definable functions: linear separately on fractional and integer parts, possibly with different coefficients
Definitional; proved equivalent to mixed-definable functions by decomposing the graph into polinear pieces and analysing each piece.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Extending the Ginsburg-Spanier Theorem to Functions and Mixed Arithmetic." pith.science (2026). https://pith.science/paper/AVTLBR7Z

@misc{pith2026260705701,
  author       = {Pith},
  title        = {Pith review of: Extending the Ginsburg-Spanier Theorem to Functions and Mixed Arithmetic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/AVTLBR7Z}},
  note         = {Machine review of arXiv:2607.05701}
}

abstract

We study sets and functions definable in the three additive theories $\FO(\Z,+,\leq)$, $\FO(\R,+,\leq)$, and $\FO(\R,\Z,+,\leq)$. The Ginsburg--Spanier theorem~\cite{GS66} characterizes $\FO(\Z,+,\leq)$-definable sets as exactly the semi-linear sets. We extend this characterization in two directions. First, we show that $\FO(\Z,+,\leq)$-definable \emph{functions} are exactly the piecewise linear functions (Theorem~\ref{thm:integer}), and that $\FO(\R,+,\leq)$-definable functions are also exactly the piecewise linear functions (Theorem~\ref{thm:real}). The proofs are direct algebraic arguments using only a stability lemma and the Ginsburg--Spanier theorem. Second, we introduce \emph{semi-polinear sets} as the $\FO(\R,\Z,+,\leq)$ analogue of semi-linear sets, and prove that the class of mixed-linear sets and the class of semi-polinear sets coincide (Theorem~\ref{thm:mixed-sets}). We further show that $\FO(\R,\Z,+,\leq)$-definable functions are exactly the \emph{piecewise-simple} functions (Theorem~\ref{thm:mixed-functions}), a new class of functions that are linear in the integer part and in the fractional part of the argument, but with potentially different linear coefficients for each. These algebraic characterizations unify the three theories in a single framework, and the proofs are purely algebraic, without reference to automata or machines.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages

[1]

A. L. Semenov , title =. Siberian Mathematical Journal , volume =

work page
[2]

Parikh , title =

Rohit J. Parikh , title =. Journal of the ACM , volume =

work page
[3]

Parikh automata and monadic theories of -words , booktitle =

Felix Klaedtke and Harald Rue. Parikh automata and monadic theories of -words , booktitle =

work page
[4]

Micha. Bounded. Proceedings of CIAA 2012 , series =

work page 2012
[5]

Spanier , title =

Seymour Ginsburg and Edwin H. Spanier , title =. Pacific J. Math. , volume =

work page
[6]

Moj. C. R. 1er congr\`es des Math\'ematiciens des pays slaves , address =

work page
[7]

Logic and p -recognizable sets of integers , journal =

V\'eronique Bruy. Logic and p -recognizable sets of integers , journal =

work page
[8]

Pierre Wolper and Bernard Boigelot , title =. Proc. 6th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (

work page

Show all 52 references

[9]

Bernard Boigelot , title =
[10]

J\'er\^ome Leroux , title =. 20th
[11]

Gurari , title =

Eitan M. Gurari , title =. Journal of the
[12]

Cherniavsky , title =

John C. Cherniavsky , title =. SIAM Journal on Computing , volume =
[13]

Ibarra , title =

Tat Hung Chan and Oscar H. Ibarra , title =. SIAM Journal on Computing , volume =
[14]

Gurari and Oscar H

Eitan M. Gurari and Oscar H. Ibarra , title =. Conference Record of the Eleventh Annual
[15]

Ibarra and Brian S

Oscar H. Ibarra and Brian S. Leininger , title =. SIAM Journal on Computing , volume =
[16]

Meyer and Dennis M

Albert R. Meyer and Dennis M. Ritchie , title =. Proceedings of the 1967 22nd National Conference , pages =

1967
[17]

Volker Weispfenning , title =
[18]

ACM Transactions on Computational Logic , volume =

Bernard Boigelot and S\'ebastien Jodogne and Pierre Wolper , title =. ACM Transactions on Computational Logic , volume =
[19]

Alexander Schrijver , title =
[20]

Christoph Haase and Shankara Narayanan Krishna and Khushraj Madnani and Om Swostik Mishra and Georg Zetzsche , title =. Proc. 51st International Colloquium on Automata, Languages, and Programming (. 2024 , doi =

2024
[21]

Journal of Symbolic Computation , volume =

Volker Weispfenning , title =. Journal of Symbolic Computation , volume =. 1988 , doi =

1988
[22]

Christoph Haase , title =
[23]

Dmitry Chistikov , title =. Proc. 44th. doi:10.4230/LIPIcs.FSTTCS.2024.1 , year =

2024 doi
[24]

Dmitry Chistikov and Christoph Haase , title =. Proc. 43rd International Colloquium on Automata, Languages, and Programming (. doi:10.4230/LIPIcs.ICALP.2016.128 , year =

2016 doi
[25]

Michael Benedikt and Dmitry Chistikov and Alessio Mansutti , title =. Proc. 50th International Colloquium on Automata, Languages, and Programming (. 2023 , doi =

2023
[26]

Starchak , title =

Alessio Mansutti and Mikhail R. Starchak , title =. Proc. 50th International Symposium on Mathematical Foundations of Computer Science (. doi:10.4230/LIPIcs.MFCS.2025.72 , year =

2025 doi
[27]

Dmitry Chistikov and Christoph Haase and Alessio Mansutti , title =. Proc. 31st EACSL Annual Conference on Computer Science Logic (
[28]

Dietrich Kuske and Markus Schwarz , title =. Proc. 32nd EACSL Annual Conference on Computer Science Logic (
[29]

Loris D'Antoni and Christof L\"oding and Joel Ouaknine , title =. Proc. ACM Program. Lang. , volume =. 2024 , doi =

2024
[30]

Emmanuel Filiot and Sarah Winter , title =. Proc. 39th
[31]

The Complexity of Separability for Semilinear Sets and

Lorenzo Clemente and S. The Complexity of Separability for Semilinear Sets and. Proc. 50th International Symposium on Mathematical Foundations of Computer Science (
[32]

J\'er\^ome Leroux and Sylvain Schmitz , title =. Proc. 30th Annual
[33]

J\'er\^ome Leroux and Sylvain Schmitz , title =. Proc. 34th Annual
[34]

J\'er\^ome Leroux , title =. Proc. 36th Annual
[35]

Wojciech Czerwi\'nski and Lukasz Orlikowski , title =. Proc. 62nd
[36]

On Flatness for 2-Dimensional Vector Addition Systems with States , booktitle =

J. On Flatness for 2-Dimensional Vector Addition Systems with States , booktitle =. 2004 , doi =

2004
[37]

Reachability in Two-Dimensional Vector Addition Systems with States Is

Michael Blondin and Alain Finkel and Stefan G. Reachability in Two-Dimensional Vector Addition Systems with States Is. 30th Annual. 2015 , doi =

2015
[38]

Flat Acceleration in Symbolic Model Checking , booktitle =

S. Flat Acceleration in Symbolic Model Checking , booktitle =. 2005 , doi =

2005
[39]

Complexity Analysis of Continuous

Est. Complexity Analysis of Continuous. Fundam. Informaticae , volume =. 2015 , url =

2015
[40]

Alain Finkel and J\'er\^ome Leroux , title =. Proc. 22nd Annual Conference on Foundations of Software Technology and Theoretical Computer Science (
[41]

Alain Finkel and Mathieu Praveen , title =. Proc. 30th International Conference on Concurrency Theory (
[42]

Local Search for

Bing. Local Search for. Proc. 34th International Conference on Computer Aided Verification (
[43]

An Automata-Based Decision Procedure for

Vojtěch Havlena and Luk\'a. An Automata-Based Decision Procedure for. Proc. 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (
[44]

Florent Madelaine and Manon Stipulanti , title =. Proc. 27th International Conference on Theory and Applications of Satisfiability Testing (
[45]

Fischer and Michael O

Michael J. Fischer and Michael O. Rabin , title =. Proc. 1974 , note =

1974
[46]

Theoretical Computer Science , volume =

Leonard Berman , title =. Theoretical Computer Science , volume =
[47]

Akshay and A

S. Akshay and A. R. Balasubramanian and Supratik Chakraborty and Georg Zetzsche , title =. Proc. 22nd International Conference on Principles of Knowledge Representation and Reasoning (
[48]

Definable Groups in Models of

Annalisa Conversano and Fran. Definable Groups in Models of. Annals of Pure and Applied Logic , volume =
[49]

Groups Definable in

Annalisa Conversano and Fran. Groups Definable in. Annals of Pure and Applied Logic , year =
[50]

arXiv preprint arXiv:2209.11598 , year =

Philipp Hieronymi and Rahim Nazari , title =. arXiv preprint arXiv:2209.11598 , year =

arXiv
[51]

SMT Workshop 2022 , year =

Alberto Griggio and Roberto Sebastiani , title =. SMT Workshop 2022 , year =

2022
[52]

Educational Times , volume =

James Joseph Sylvester , title =. Educational Times , volume =. 1884 , note =

Pith tools

Reviewed July 11, 2026 · model on record in the stance chip above.

[1] [1]

A. L. Semenov , title =. Siberian Mathematical Journal , volume =

work page

[2] [2]

Parikh , title =

Rohit J. Parikh , title =. Journal of the ACM , volume =

work page

[3] [3]

Parikh automata and monadic theories of -words , booktitle =

Felix Klaedtke and Harald Rue. Parikh automata and monadic theories of -words , booktitle =

work page

[4] [4]

Micha. Bounded. Proceedings of CIAA 2012 , series =

work page 2012

[5] [5]

Spanier , title =

Seymour Ginsburg and Edwin H. Spanier , title =. Pacific J. Math. , volume =

work page

[6] [6]

Moj. C. R. 1er congr\`es des Math\'ematiciens des pays slaves , address =

work page

[7] [7]

Logic and p -recognizable sets of integers , journal =

V\'eronique Bruy. Logic and p -recognizable sets of integers , journal =

work page

[8] [8]

Pierre Wolper and Bernard Boigelot , title =. Proc. 6th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (

work page