Title | Stratified Context Unification is NP-complete |

Publication Type | Conference Paper |

Year of Publication | 2006 |

Authors | Levy J, Schmidt-Schauss M, Villaret M |

Conference Name | Lecture Notes in Computer Science |

Volume | 4130 |

Publisher | Springer-Verlag |

Pagination | 82-96 |

Abstract | Context Unification is the problem to decide for a given set of second-order equations $E$ where all second-order variables are unary, whether there exists a unifier, such that for every second-order variable X, the abstraction lambda x. r instantiated for X has exactly one occurrence of the bound variable x in r. Stratified Context Unification is a specialization where the nesting of second-order variables in E is restricted. It is already known that Stratified Context Unification is decidable, NP-hard, and in PSPACE, whereas the decidability and the complexity of Context Unification is unknown. We prove that Stratified Context Unification is in NP by proving that a size-minimal solution can be represented in a singleton tree grammar of polynomial size, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time. This also demonstrates the high potential of singleton tree grammars for optimizing programs maintaining large terms. A corollary of our result is that solvability of rewrite constraints is NP-complete. |