An Equational Extension

Abstract

It has been recognized for some time that Prolog will need to be extended in order for it to realize the vision of declarative programming. One example is the so-called problem of equality and functions. The underlying deduction mechanism for Prolog, SLD-resolution, is defined only for languages without equality. As mentioned in chapter 1, current Prolog systems include a collection of interpretations of the equality symbol which are basically inherited from LISP, and that it is even possible for the “equality” predicate to cause the side-effect of binding an uninstantiated variable to an instantiated variable. The absence of equality also means that value-returning functions cannot be defined equationally. Instead, an n-ary function f(x ₁,..., x, _n ) is defined by an n+1-ary predicate p(x ₁,..., x _n , x _n+l) which “collects” the value in the n + 1^st argument. In order for Prolog to reason equationally, rules for rewriting one term to another must be expressed via a distinguished predicate (say rewrite).