On the complexity of bounded second-order unification and stratified context unification (Q2889573)

Bounded second-order unification is a decidable variant of second-order unification. It requires that in the unifier, the arguments of terms that instantiate second-order variables can use their arguments bounded number of times. This paper considers a special case of bounded second-order unification where the unifiers map second-order variables to linear or constant term functions. That means, each of the arguments is used at most once. Earlier, in [the second author, Decidability of bounded second order unification. Inf. Comput. 188, No. 2, 143--178 (2004; Zbl 1078.68139)], it was shown that the general case of bounded second-order unification can be NP-reduced to this restricted case.NEWLINENEWLINEContext unification, considered from the perspective of second-order unification, can be seen as a variant of its fragment, obtained by restricting the second-order variables to be unary (such variables are called context variables), and unifiers to map those variables to terms that use their argument exactly once (such terms are called contexts). Decidability of context unification is a long-standing open problem. Stratified context unification is a decidable fragment of context unification where the nesting of context variables is required to be the same for all occurrences of the same variable.NEWLINENEWLINEThe main result of the paper is the proof that bounded second-order unification and stratified context unification are in NP. It implies that these problems are NP-complete, because their NP-hardness has been proved earlier in [loc. cit.] and [the second author, J. Log. Comput. 12, No. 6, 929--953 (2002; Zbl 1019.03002)]. In the proof, the authors show that given a bounded second-order or a stratified context unification problem, they can represent its size-minimal unifiers in a compressed form by means of a polynomially sized singleton tree grammar.NEWLINENEWLINEAs the corollaries of the main result, the authors prove the NP-completeness of one-step rewrite constraints and generalized bounded second-order unification problems, and the NEXPTIME-membership of generalized stratified context unification problems.