@article {3415,
title = {On the Relation Between Context and Sequence Unification},
journal = {Journal of Symbolic Computation},
volume = {45},
year = {2010},
pages = {74-95},
abstract = {Both Sequence and Context Unification generalize the same problem: Word Unification. Besides that, Sequence Unification solves equations between unranked terms involving sequence variables, and seems to be appealing for information extraction in XML documents, program transformation, knowledge representation, and rule-based programming. It is decidable. Context Unification deals with the same problem for ranked terms involving context variables, and has applications in computational linguistics and program transformation. Its decidability is a long-standing open question. In this work we study a relation between these two problems. We introduce a variant (restriction) of Context Unification, called Left-Hole Context Unification (LHCU), to which Sequence Unification is P-reduced: We define a partial currying procedure to translate sequence unification problems into left-hole context unification problems, and prove soundness of the translation. Furthermore, a precise characterization of the shape of the unifiers allows us to easily reduce Left-Hole Context Unification to (the decidable problem of) Word Unification with Regular Constraints, obtaining then a new decidability proof for Sequence Unification. Finally, we define an extension of Sequence Unification (ESU) and, closing the circle, prove the inter P-reducibility of LHCU and ESU.},
keywords = {context unification, second-order unification, sequence unification},
author = {Temur Kutsia and Jordi Levy and Mateu Villaret}
}
@article {3453,
title = {Simplifying the Signature in Second-Order Unification},
journal = {Applicable Algebra in Engineering, Communication and Computing},
volume = {20},
year = {2009},
pages = {427-445},
publisher = {Springer},
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.},
keywords = {context unification, Lambda Calculus, second-order unification},
author = {Jordi Levy and Mateu Villaret}
}