Naïve Reverse Can be Linear.

Abstract

We propose a new implementation of logic programming with higher-order terms. In order to illustrate the properties of our implementation, we apply the coding of lists as functions to the context of logic programming. As a side-effect, we show that higher-order unification is a good tool for manipulating the function-lists. It appears that the efficiency of the program thus obtained relies critically upon the implementation of higher-order operations (unification and reduction). In particular, we show that a good choice for data-structures and reduction strategy yields a linear naive reverse. 1 Introduction The extension of Prolog to higher-order terms has been proposed by Miller and Nadathur[6]. The prototypal system is Prolog, of which we know two implementations: a Prolog based implementation and a Lisp based one. The first one was intended for experimental use and is very inefficient. We shall only refer to the Lisp based implementation. We propose another implementation in which ...