Implementational Issues in GCLA: A-Sufficiency and the Definiens Operation

Abstract

We present algorithms for computing A-sufficient substitutions and constraint sets together with the definiens operation. These operations are primitive operations in the language GCLA. The paper first defines those primitives, which together form a dual rule to SLD resolution, and then describes the different algorithms and some of their properties together with examples. One of the algorithms shows how a definition can be compiled into a representation holding all possible A-sufficient substitutions/constraint sets together with their corresponding definiens. This representation makes the computation at runtime of a definiens and an A-sufficient substitution/constraint set have the same complexity as the table lookup operation clause/2 in Prolog. The paper also describes the generalisation from unification (sets of equalities) to constraint sets and satisfiability of systems of equalities and inequalities.