Unification modulo ACUI plus Homomorphisms/Distributivity

Siva Anantharaman (1) , Paliath Narendran (1, 2) , Michaël Rusinowitch (1, 3)

1 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
2 CS - Department of Computer Science [Albany]
3 CASSIS - Combination of approaches to the security of infinite states systems

We consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol `*' that distributes over the ACUI-symbol denoted `+'. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUID_l-unification problem, i.e., unification modulo ACUI plus left-distributivity of `*' over `+', and prove it is NEXPTIME-decidable. When we assume the symbol `*' to be 2-sided distributive over `+', we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativity-commutativity, or just of associativity, on `$*$' are added on to ACUID, the unification problem becomes undecidable.

Mots clés: E-Unification; complexity; rewrite reachability; Minsky machine; Post correspondence problem; set constraints

Domaines: Informatique et langage [cs.CL]

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch. Unification modulo ACUI plus Homomorphisms/Distributivity. 2003, pp.442--457. ⟨hal-00080670⟩