2024/04/16 by Cerna, David M., Parsert, Julian
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2404.10616
We introduce a fragment of second-order unification, referred to as 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 associative binary function symbols (ASOGU) and show that Hilbert's 10th 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 length-reducing rewrite systems. Furthermore, our reduction holds even in the case when associativity of the binary function symbol is restricted to power associative, i.e. f(f(x,x),x)= f(x,f(x,x)), as our construction requires a single constant.