Crossing the syntactic barrier: Hom-disequalities for H ₁-clauses

We extend H ₁-clauses with disequalities between images of terms under a tree homomorphism (hom-disequalities). This extension allows to test whether two terms are distinct modulo a semantic interpretation, allowing, e.g., to neglect information that is not considered relevant for the intended comparison. We prove that H ₁-clauses with hom-disequalities are more expressive than H ₁-clauses with ordinary term disequalities, and that they are incomparable with H ₁-clauses with disequalities between paths. Our main result is that H ₁-clauses with this new type of constraints can be normalized into an equivalent tree automaton with hom-disequalities. Since emptiness for that class of automata turns out to be decidable, we conclude that satisfiability is decidable for positive Boolean combinations of queries to predicates defined by H ₁-clauses with hom-disequalities.