paperbot · PL 论文追踪

RSS

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

LMCS vol.Volume 22, Issue 22026
David M. Cerna, Julian Parsert

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(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.

链接与引用

DOI 原文 ·

BibTeX
@article{paperbot4005,
  title = {One is all you need: Second-order Unification without First-order Variables},
  author = {David M. Cerna and Julian Parsert},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 22, Issue 2},
  year = {2026},
  doi = {10.46298/lmcs-22(2:3)2026}
}