Stratified Context Unification Is NP-Complete

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 bstraction 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, NPhard, 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 corolla...

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Jordi Levy, Manfred Schmidt-Schauß, Mateu Villaret
• Keywords: Automated Reasoning, CADE 2006, Second-order Variable Bstraction, Second-order Variables, Stratified Context Unification