Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

David M. Cerna, Julian Parsert

TL;DR

The paper investigates the decidability of second-order ground unification under an associative theory, showing that even a restricted fragment with a single second-order variable and no first-order variables is undecidable. It introduces two conceptual tools, the $n$-multiplier and $n$-counter, to count symbol occurrences under substitutions and to relate unifiability to Diophantine equations. Through a careful polynomial-to-unification encoding using monomial groupings and an $n$-converter, the authors reduce Hilbert's $10^{\text{th}}$ problem to ASOGU, establishing undecidability and deriving a lower bound on the arity required (at least $9$). Notably, the undecidability persists even when the associative operator is restricted to power associativity, and the decidability of the non-associative second-order ground unification remains open. The work suggests future directions toward identifying decidable fragments and exploring alternative encodings.

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.

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

TL;DR

The paper investigates the decidability of second-order ground unification under an associative theory, showing that even a restricted fragment with a single second-order variable and no first-order variables is undecidable. It introduces two conceptual tools, the -multiplier and -counter, to count symbol occurrences under substitutions and to relate unifiability to Diophantine equations. Through a careful polynomial-to-unification encoding using monomial groupings and an -converter, the authors reduce Hilbert's problem to ASOGU, establishing undecidability and deriving a lower bound on the arity required (at least ). Notably, the undecidability persists even when the associative operator is restricted to power associativity, and the decidability of the non-associative second-order ground unification remains open. The work suggests future directions toward identifying decidable fragments and exploring alternative encodings.

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 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.
Paper Structure (5 sections, 7 theorems, 48 equations, 5 figures)

This paper contains 5 sections, 7 theorems, 48 equations, 5 figures.

Table of Contents

  1. Introduction
  2. preliminaries
  3. n-Multipliers and n-Counters
  4. Undecidability of ASOGU Unification
  5. Conclusion and Future Work

Key Result

Theorem 1

Let $p(\overline{x})$ be a polynomial with integer coefficients. Then whether $p(\overline{x}) = 0$ has an integer solution is undecidable.

Figures (5)

  • Figure 1: Construction of terms from a polynomial. The red circles denote the start of terms representing the encircled polynomial.
  • Figure 2: Computation of $\mathtt{mul}\mathtt{[} F,h_1,t\mathtt{]}$ (See Example \ref{['ex:n-mult']}).
  • Figure 3: Computation of $\mathtt{cnt}\mathtt{[} F,h_1,a,t\mathtt{]}$ (See Example \ref{['ex:n-counter']}).
  • Figure 4: We recursively apply reduction and monomial grouping decomposition (Definition \ref{['def:monogrp']}) 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.
  • Figure 5: Applying Definition \ref{['def:convert']} to the polynomial of Example \ref{['ex:monomial']}, we derive $\mathtt{cvt}\mathtt{[} F,p(x,y)\mathtt{]}^-$ and $\mathtt{cvt}\mathtt{[} F,p(x,y)\mathtt{]}^+$. The boxed section of the polynomial tree results in the boxed sections of the two term trees. The precise construction is described in Example \ref{['ex:monomial']}.

Theorems & Definitions (30)

  • Definition 1: Equational theory DBLP:books/daglib/0092409
  • Theorem 1: Matiyasevich–Robinson–Davis–Putnam theorem or Hilbert's 10$^{th}$ problem 10.5555/164759
  • proof
  • Definition 2: $n$-Mutiplier
  • Example 1
  • Definition 3: $n$-Counter
  • Example 2
  • Lemma 1
  • proof
  • Example 3
  • ...and 20 more