Publications

Simplifying the Signature in Second-Order Unification

Publication Type:

Journal Article

Authors:

Jordi Levy; Mateu Villaret

Source:

Applicable Algebra in Engineering, Communication and Computing, Springer, Volume 20, Issue 5, p.427-445 (2009)

Keywords:

Second-Order Unification; Context Unification; Lambda Calculus

Abstract:

Second-Order Unification is undecidable even for very specialized fragments. The signature plays a crucial role in these fragments. If all symbols are monadic, then the problem is NP-complete, whereas it is enough to have just one binary constant to
lose decidability.

In this work we reduce Second-Order Unification to Second-Order Unification with a signature that contains just one binary function symbol and constants. The reduction is based on partially currying the equations by using the binary function symbol for explicit application @. Our work simplifies the study of Second-Order Unification and some of its variants, like Context Unification and Bounded Second-Order Unification.

»