Publications

The Complexity of Monadic Second-Order Unification

Publication Type:

Journal Article

Authors:

Jordi Levy; Manfred Schmidt-Schauss; Mateu Villaret

Source:

SIAM Journal on Computing, Volume 38, Number 3, p.1113-1140 (2008)

Keywords:

Second-Order Unification; Lambda Calculus

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.

Projects: 
MULOG 2
»