Equation, sets, and reduction semantica for functional and logic programming

We present a framework for first-order functional and Horn-logic programming using rewrite rules and equations. A program in this framework is a set of rewrite rules followed by a set of equations that need to be solved. These rewrite rules are an extension of the rewrite rules found in non-canonical term-writing systems in that they permit conditions, expressed as a set of equations having logical variables, on the right-hand side of a rule. The reduction semantics of equations is given in terms of complete sets of solutions. An operational strategy which computes these solutions is given in terms of a new technique called object refinement. This semantics is also called the refinement semantics. Object refinement is a generalisation of the outermost reduction rule of functional languages and the unification rule of logic languages. Consistency and completeness theorems are presented in order to establish the equivalence of the reduction and refinement semantics. Since an equation may possess multiple solutions, a set construct is provided to collect these solutions. The resulting language, called EqL, is currently being implemented. Examples are used to illustrate the language constructs and their semantics. The relationship of these ideas to other closely related ideas, notably narrowing, is also discussed.