Decidable and undecidable second-order unification problems

There is a close relationship between word unication and second-order unication. This similarity has been exploited for instance for proving decidability of monadic second-order unication. Word uni- cation can be easily decided by transformation rules (similar to the ones applied in higher-order unication procedures) when variables are restricted to occur at most twice. Hence a well-known open question was the decidability of second-order unication under this same restric- tion. Here we answer this question negatively by reducing simultaneous rigid E-unication to second-order unication. This reduction, together with an inverse reduction found by Degtyarev and Voronkov, states an equivalence relationship between both unication problems. Our reduction is in some sense reversible, providing decidability results for cases when simultaneous rigid E-unication is decidable. This hap- pens, for example, for one-variable problems where the variable occurs at most twice (because rigid E-unication is decidable for just one equa- tion). We also prove decidability when no variable occurs more than once, hence signican tly narrowing the gap between decidable and undecidable second-order unication problems with variable occurrence restrictions.