Simplifying the signature in second-order unification (Q843951): Difference between revisions

The difficulty of a second-order unification problem is related to the signature of the involved language. It is well known that, in general, second-order unification is undecidable when non-unary function symbols are considered. Conversely, second-order unification becomes decidable (more precisely NP-complete) when only unary function symbols (i.e. monadic symbols) are considered. This work presents a method that NP-reduces the signature of a general second-order unification to an equivalent one containing only constants and one binary function symbol. The reduction uses partial Currying of terms by introducing a binary symbol \(\@\) for function application. In particular, the proposed reduction transforms function symbols applications, leaving variable applications unchanged. This is in order to preserve the solvability of second-order equations. The reduction presented in this paper applies to a broad class of second-order unification variants. It preserves the order and the solvability of the second-order unification equations, hence it does not make a significative difference in terms of decidability. However, the reduction can be used to simplify practical implementations and to simplify the study of decidable fragments.