一句话：将 EUF 扩展为支持参数化复合深度的 EUFⁿ，并用条件同余图给出可判定性与复杂度上界。
标准未解释函数等式理论（EUF）只允许固定有限深度的函数复合，难以表达 f^n(x) 这类复合深度由自然数变量决定的项。本文提出 EUF^n，将一元函数复合深度参数化；EUF^n 公式可视为无限多个 EUF 公式的析取，其可满足性定义为存在某个自然数实例化后的 EUF 公式可满足。作者设计条件同余图（CCG）算法，将判定问题归约到带整除的 Presburger 算术存在句，从而给出无量词 EUF^n 片段的判定过程，并证明复杂度上界为 2NEXPTIME。该扩展还可编码一类可判定的交错 Dyck 可达性问题和一类新的可判定未解释程序验证问题。
The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations, enabling generalization and simplification of theorems and proofs. However, standard EUF restricts function composition to fixed finite depths ( e.g. , f k ( x ) where k is constant). This work extends EUF to EUF n , supporting parametric composition depth for unary functions ( e.g. , f n ( x ) where n is a natural number variable). An EUF n formula can be viewed as a disjunction of infinitely many EUF formulas, each instantiated by an assignment of natural numbers. Its satisfiability is defined by the satisfiability of at least one such instantiated EUF formula. We establish the decidability of the EUF n satisfiability problem via a conditional congruence graph (CCG) algorithm. This approach generalizes the standard congruence closure procedure by maintaining conditional equivalence relations between terms. The algorithm reduces the satisfiability problem to deciding existential sentences in Presburger arithmetic with divisibility, which is a decidable problem, thereby yielding a decision procedure for the quantifier-free fragment of EUF n with a 2NEXPTIME complexity upper bound. The enhanced expressiveness of EUF n enables new applications: (1) Encoding a decidable subclass of interleaved Dyck reachability problems where existing over/under-approximations produce false positives/negatives, and (2) Encoding a new decidable subclass of uninterpreted program verification problems.
@article{paperbot12126,
title = {EUFⁿ: A Decidable Extension to the Theory of Equality with Uninterpreted Functions},
author = {Yide Du and Zhenbang Chen and Weijiang Hong and Wei Dong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839461}
}