A Family of Unification-Oblivious Program Transformations and Their Applications.

We describe a family of program transformations that compile a Horn Clause program into equivalent programs of a simpler and more regular structure. Our transformations, seen as morphisms between term algebras, commute with unification, clause unfoldings and Prolog’s LD-resolution, thus preserving the operational semantics of the Horn Clause programs. As applications, the resulting programs have simpler execution algorithms and can be compiled to minimalist instruction sets.