Although Warren's method for the evaluation in Prolog of expressions with higherorder functions appears to have been neglected, it is of great value. Warren's paper needs to be supplemented in two respects. He showed examples of a translation from expressions to clauses, but did not present a general method. Here we present a general translation program and prove it correct with respect to the axioms of equality and those of the -calculus. Warren's paper only argues in general terms that a structure-sharing Prolog implementation can be expected to efficiently evaluate the result of his translation. We show a comparison of timings between lisp and a structure-copying implementation of Prolog. The result suggests that Warren's method is about as efficient as the Lisp method for the evaluation of expressions involving higher-order functions.
Mantis H. M. Cheng, Maarten H. van Emden, B. E. Ri