Higher-order rigid E-unification

Higher-order E-unification, i.e. the problem of finding substitutions that make two simply typed λ-terms equal modulo Β or Βη-equivalence and a given equational theory, is undecidable. We propose to rigidifyit, to get a resource-bounded decidable unification problem (with arbitrary high bounds), providing a complete higher-order E-unification procedure. The techniques are inspired from Gallier's rigid E-unification and from Dougherty and Johann's use of combinatory logic to solve higher-order E-unification problems. We improve their results by using general equational theories, and by defining optimizations such as higher-order rigid E-preunification, where flexible terms are used, gaining much efficiency, as in the non-equational case due to Huet.