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

Document detail

ID

oai:arXiv.org:2404.10616

Topic

Computer Science - Logic in Comput...

Author

Cerna, David M. Parsert, Julian

Year

2024

listing date

9/18/2024

Keywords

second-order

Metrics

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.

;Comment: Under review

Cerna, David M.,Parsert, Julian, 2024, One is all you need: Second-order Unification without First-order Variables