hide
Free keywords:
-
Abstract:
There is a close relationship between word unification and second-order
unification. This similarity has been exploited, for instance, for proving
decidability of monadic second-order unification, and decidability of linear
second-order unification when no second-order variable occurs more than twice.
The attempt to prove the second result for (non-linear) second-order
unification failed, and lead instead to a natural reduction from simultaneous
rigid E-unification to this problem. This reduction is the first main result of
this paper, and it is the starting point for proving some novel results about
the undecidability of second-order unification presented in the rest of the
paper.
We prove that second-order unification is \emph{undecidable} in the following
three cases: 1) each second-order variable occurs at most twice and there are
only two second-order variables; 2) there is only one second-order variable and
it is unary; 3) the conditions (i--iv) hold for some fixed integer $n$: (i) the
arguments of all second-order variables are ground terms of size less than $n$,
(ii) the arity of all second-order variables is less than $n$, (iii) the
number of occurrences of second-order variables is at most 5, (iv) there is
either a single second-order variable, or there are two second-order variables
and no first-order variables.
