TitleThe Complexity of Monadic Second-Order Unification
Publication TypeJournal Article
Year of Publication2008
AuthorsLevy J, Schmidt-Schauss M, Villaret M
JournalSIAM Journal on Computing
Volume38
Number3
Pagination1113-1140
KeywordsLambda Calculus, second-order unification
Abstract

Monadic Second-Order Unification is Second-Order Unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context free grammars. We prove that Monadic Second-Order Matching is also NP-complete.