一句话：提出仅含一个二阶变量且无一阶变量的 SOGU 片段，并证明其结合变体 ASOGU 不可判定。
本文研究二阶合一的判定性，定义了一个新的片段 SOGU：只允许一个二阶变量，并且不允许一阶变量出现。作者进一步考察该片段的等式变体 ASOGU，其签名包含结合性二元函数符号。通过将希尔伯特第十问题归约到 ASOGU 的可合一性，论文证明 ASOGU 是不可判定的。该归约给出的不可判定下界比以往结果更强：此前需要一阶变量出现、多个二阶变量，或涉及长度递减重写系统的等式理论。此外，该归约在结合性被弱化为幂结合性（f(f(x,x),x)=f(x,f(x,x))）时仍然成立，因为构造只需一个常量。
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 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2404-10616,
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}
}