A Model for Mathematical Analysis of Functional Logic Programs and Their Implementations.
Egon Börger, Francisco J. López-Fraguas, Mario Rodríguez-Artalejo · 1994
Introduction We extend the core Prolog model of [2] to a model for the functional logic programming language BABEL [8] by adding, to Prolog's backtracking structure, rules for the reduction of functional expressions to normal form. Then we define six typical provably correct refinements which are directed towards implementation of functional logic programs: structure sharing for expressions, explicit computation of the normal form condition, embedding of the backtracking tree into a stack, localization of the normal form computation for expressions (introducing local environments for computation of subexpressions) together with some optimizations in IBAM [6], a (graph---) narrowing machine actually implementing innermost BABEL. Thus the machinery of [2,3] for mathematical description and analysis of logic programs, is linked to functional logic programs and their implementation on machines which typically combine the WAM [9] with features from reduction machines [4] for functi