pith. sign in

arxiv: 2404.10616 · v10 · submitted 2024-04-16 · 💻 cs.LO

One is all you need: Second-order Unification without First-order Variables

David M. Cerna , Julian Parsert This is my paper

Pith reviewed 2026-05-24 02:23 UTC · model grok-4.3

classification 💻 cs.LO
keywords second-order unificationassociativityundecidabilityHilbert's tenth problempower associativityground termsDiophantine equations
0
0 comments X

The pith

Hilbert's tenth problem reduces to second-order unification with one variable and no first-order terms.

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

The paper shows that deciding whether two terms have a unifier is undecidable even in a minimal fragment of second-order unification that allows only one second-order variable and bans first-order variables entirely. This is proved by reducing the solvability of Diophantine equations directly to the existence of such unifiers when an associative binary symbol is present. The same reduction works when associativity is weakened to the power-associative law and only a single constant symbol is used. A reader would care because the result removes several requirements that all earlier undecidability proofs for second-order unification needed.

Core claim

The authors prove that the unifiability problem for second-order ground terms under associativity, called ASOGU, is undecidable by exhibiting a many-one reduction from Hilbert's tenth problem. The construction uses exactly one second-order variable and one constant symbol. The same undecidability result holds when the equational theory is restricted to power associativity, that is, the identity f(f(x,x),x)=f(x,f(x,x)).

What carries the argument

The explicit reduction from integer Diophantine equations to ASOGU unifiability instances that uses only one second-order variable and one constant under the power-associative law.

Load-bearing premise

The mapping from Diophantine equations to unification problems preserves solvability in both directions.

What would settle it

An explicit Diophantine equation that has an integer solution yet whose image under the reduction has no unifier, or vice versa.

Figures

Figures reproduced from arXiv: 2404.10616 by David M. Cerna, Julian Parsert.

Figure 1
Figure 1. Figure 1: Construction of terms from a polynomial. The red circles denote the start of terms representing the encircled polynomial. We leave it as an exercise to verify the other solution, as it yields a term containing 21 occurrences of a. To illustrate how the number of unknowns influences the function variable, let us consider the polynomial p(x, y) = xy − 3x − 2y + 6 or (x − 2)(y − 3) when factored. The result u… view at source ↗
Figure 2
Figure 2. Figure 2: Computation of mul[F, h1, t] (See Example 1). mul[F, h1, g(F(a), F(F(F(b))))] mul[F, h1, F(g(a, F(s(a))))] = 1 + h1 · mul[F, h1, g(a, F(s(a)))] mul[F, h1, g(F(a), F(F(F(b))))] = mul[F, h1, F(a)] + mul[F, h1, F(F(F(b)))] mul[F, h1, g(a, F(s(a)))] = 1 mul[F, h1, F(a)] = 1 mul[F, h1, F(F(F(b)))] = 1 + h1 · mul[F, h1, F(F(b))] mul[F, h1, F(F(b)))] = 1 + h1 Thus, when h1 = 2 we get mul[F, h1, t] = 11. Observe o… view at source ↗
Figure 3
Figure 3. Figure 3: Computation of cnt[F, h1, a, t] (See Example 2). • cnt[F, hn, a, b] = 0 • cnt[F, hn, a, a] = 1 • cnt[F, hn, f, g(tl)] = Pl j=1 cnt[F, hn, f, tj ] • cnt[F, hn, f, f(tl)] = 1 + Pl j=1 cnt[F, hn, f, tj ] • cnt[F, hn, f, F(tn)] = Pn i=1 hi · cnt[F, hn, f, ti ] Furthermore, let (U, F) be an SOGU problem. Then cnt[F, hn, g, U] l = X u ?=F v∈U cnt[F, hn, g, u] cnt[F, hn, g, U] r = X u ?=F v∈U cnt[F, hn, g, v]. Th… view at source ↗
Figure 4
Figure 4. Figure 4: We recursively apply reduction and monomial grouping decomposition (Defini￾tion 4) to the polynomial at the root of the tree. In each box, the lower polynomial is the reduction of the upper polynomial by the unknown labeling the edge to the parent box. By 0, we denote the monomial grouping 0, and x,y, and z denote the groupings associated with unknowns. 4. Undecidability of ASOGU Unification We now use the… view at source ↗
Figure 5
Figure 5. Figure 5: Applying Definition 5 to the polynomial of Example 6, we derive cvt[F, p(x, y)] − and cvt[F, p(x, y)] + . The boxed section of the polynomial tree results in the boxed sections of the two term trees. The precise construction is described in Example 6. cvt[F, 3 · x 3 + xy − 2 · y 2 − 2]+ = F(cvt[F, 3 · x 2 + y] + , cvt[F, −2 · y] + ) cvt[F, 3 · x 2 + y] + = F(cvt[F, 3 · x] + , cvt[F, 1]+ ) cvt[F, 3 · x] + =… view at source ↗
read the original abstract

We introduce a fragment of second-order unification, referred to as \emph{Second-Order Ground Unification (SOGU)}, with the following properties: (i) only one second-order variable is allowed, and (ii) first-order variables do not occur. We study an equational variant of SOGU where the signature contains \textit{associative} binary function symbols (ASOGU) and show that Hilbert's 10$^{th}$ problem is reducible to ASOGU unifiability, thus proving undecidability. Our reduction provides a new lower bound for the undecidability of second-order unification, as previous results required first-order variable occurrences, multiple second-order variables, and/or equational theories involving \textit{length-reducing} rewrite systems. Furthermore, our reduction holds even in the case when associativity of the binary function symbol is restricted to \emph{power associative}, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a single constant.

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 introduces Second-Order Ground Unification (SOGU), a fragment of second-order unification restricted to a single second-order variable and no first-order variables. It studies the equational variant ASOGU over associative binary symbols and claims to prove undecidability of ASOGU unifiability by an explicit reduction from Hilbert's tenth problem; the reduction is asserted to hold even when associativity is weakened to power-associativity (f(f(x,x),x)=f(x,f(x,x))) using only a single constant.

Significance. If the reduction is correct, the result supplies a new lower bound on the undecidability of second-order unification, using strictly fewer variables and a weaker equational theory than prior proofs that required first-order variables, multiple second-order variables, or length-reducing rewrite systems.

major comments (1)
  1. [Reduction (main theorem)] The central claim rests on an explicit reduction showing Diophantine solvability iff the constructed ASOGU instance is unifiable. No derivation steps, term encodings for addition/multiplication, or verification that the mapping preserves unifiability (without extraneous solutions) under the power-associative axiom are supplied; this is load-bearing for the undecidability result.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review and for highlighting the need for greater explicitness in the reduction. We address the major comment below and will revise the manuscript to incorporate additional details.

read point-by-point responses

  1. Referee: [Reduction (main theorem)] The central claim rests on an explicit reduction showing Diophantine solvability iff the constructed ASOGU instance is unifiable. No derivation steps, term encodings for addition/multiplication, or verification that the mapping preserves unifiability (without extraneous solutions) under the power-associative axiom are supplied; this is load-bearing for the undecidability result.

    Authors: We agree that the manuscript as submitted does not supply sufficient derivation steps, explicit term encodings for addition and multiplication, or a full verification that the mapping is equivalence-preserving under power-associativity without extraneous solutions. The construction encodes natural numbers via iterated applications of the single binary symbol (with one constant) and uses the second-order variable to witness solutions; the power-associativity axiom is used only to ensure the necessary equalities hold. In the revised version we will add the missing encodings, the step-by-step correspondence between Diophantine equations and unification problems, and the argument that no spurious unifiers arise. This material will be placed in a dedicated section or appendix. revision: yes

Circularity Check

0 steps flagged

Explicit reduction from Hilbert's 10th problem establishes undecidability without circularity

full rationale

The paper's central result is an explicit many-one reduction from the independently known undecidable Hilbert's tenth problem (Diophantine solvability) to unifiability in ASOGU (and its power-associative restriction). The construction encodes integer equations into ground terms using one second-order variable and a single constant, with the equivalence between solvability and unifiability shown directly by the term constructions. No step defines a quantity in terms of itself, renames a fitted parameter as a prediction, or relies on a self-citation chain for a load-bearing uniqueness or ansatz claim. The derivation is therefore self-contained against the external benchmark of Matiyasevich's theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the known undecidability of Hilbert's tenth problem together with the correctness of an encoding that maps Diophantine equations into unification problems under the stated signature restrictions; no free parameters or new entities are introduced.

axioms (1)
  • standard math Hilbert's tenth problem is undecidable
    Standard result in computability theory invoked as the source problem for the reduction.

pith-pipeline@v0.9.0 · 5708 in / 1287 out tokens · 24663 ms · 2026-05-24T02:23:16.323251+00:00 · methodology

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

18 extracted references · 18 canonical work pages

  1. [1]

    Counterexample guided inductive synthesis modulo theories

    Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. Counterexample guided inductive synthesis modulo theories. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 20...

    work page 2018

  2. [2]

    Iteration methods for finding all zeros of a polynomial simultaneously

    Oliver Aberth. Iteration methods for finding all zeros of a polynomial simultaneously. Mathematics of Computation , 27:339--344, 1973

    work page 1973

  3. [3]

    Madhusudan, Milo M

    Rajeev Alur, Rastislav Bod \' k, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress - Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar - Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Maximilian Irlbeck, Doron A. Peled, and Alexander Pretsc...

    work page 2015

  4. [4]

    Haniel Barbosa, Andrew Reynolds, Daniel El Ouraoui, Cesare Tinelli, and Clark W. Barrett. Extending SMT solvers to higher-order logic. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings , volume 11716 of Lecture Notes in Computer Science , pages 3...

    work page 2019

  5. [5]

    William M. Farmer. A unification algorithm for second-order monadic terms. Ann. Pure Appl. Log. , 39(2):131--174, 1988

    work page 1988

  6. [6]

    Rigid reachability

    Harald Ganzinger, Florent Jacquemard, and Margus Veanes. Rigid reachability. In Jieh Hsiang and Atsushi Ohori, editors, Advances in Computing Science - ASIAN '98, 4th Asian Computing Science Conference, Manila, The Philippines, December 8-10, 1998, Proceedings , volume 1538 of Lecture Notes in Computer Science , pages 4--21. Springer, 1998

    work page 1998

  7. [7]

    Goldfarb

    Warren D. Goldfarb. The undecidability of the second-order unification problem. Theor. Comput. Sci. , 13:225--230, 1981

    work page 1981

  8. [8]

    Program synthesis

    Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program synthesis. Found. Trends Program. Lang. , 4(1-2):1--119, 2017

    work page 2017

  9. [9]

    G \' e rard P. Huet. The undecidability of unification in third order logic. Inf. Control. , 22(3):257--267, 1973

    work page 1973

  10. [10]

    Context unification is in PSPACE

    Artur Jez. Context unification is in PSPACE . In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II , volume 8573 of Lecture Notes in Computer Science , pages 244--255. Springer, 2014

    work page 2014

  11. [11]

    Linear second-order unification

    Jordi Levy. Linear second-order unification. In Harald Ganzinger, editor, Rewriting Techniques and Applications, 7th International Conference, RTA-96, New Brunswick, NJ, USA, July 27-30, 1996, Proceedings , volume 1103 of Lecture Notes in Computer Science , pages 332--346. Springer, 1996

    work page 1996

  12. [12]

    On the limits of second-order unification

    Jordi Levy. On the limits of second-order unification. In Temur Kutsia and Christophe Ringeissen, editors, Proceedings of the 28th International Workshop on Unification, UNIF 2014, Vienna, Austria, July 13, 2014 , pages 5--14, 2014

    work page 2014

  13. [13]

    The complexity of monadic second-order unification

    Jordi Levy, Manfred Schmidt - Schau , and Mateu Villaret. The complexity of monadic second-order unification. SIAM J. Comput. , 38(3):1113--1140, 2008

    work page 2008

  14. [14]

    On the undecidability of second-order unification

    Jordi Levy and Margus Veanes. On the undecidability of second-order unification. Inf. Comput. , 159(1-2):125--150, 2000

    work page 2000

  15. [15]

    The undecidability of the unification problem for third order languages

    Claudio L Lucchesi. The undecidability of the unification problem for third order languages. Report CSRR , 2059:129--198, 1972

    work page 2059

  16. [16]

    Matiyasevich

    Yuri V. Matiyasevich. Hilbert's tenth problem . MIT Press, Cambridge, MA, USA, 1993

    work page 1993

  17. [17]

    Brown, Mikolas Janota, and Cezary Kaliszyk

    Julian Parsert, Chad E. Brown, Mikolas Janota, and Cezary Kaliszyk. Experiments on infinite model finding in SMT solving. In Ruzica Piskac and Andrei Voronkov, editors, LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023 , volume 94 of EPiC Series in ...

    work page 2023

  18. [18]

    Decidability of bounded second order unification

    Manfred Schmidt - Schau . Decidability of bounded second order unification. Inf. Comput. , 188(2):143--178, 2004

    work page 2004