An Abstract Machine for SLG Resolution: Definite Programs

This paper addresses the correctness of the SLG-WAM for definite programs, and describes its architecture for executing these programs. We argue its correctness through a restriction of SLGO, an operational semantics for SLG, which models the actions of the SLG-WAM. We then offer a detailed description of the algorithms, data structures and instructions of the SLGWAM, and a performance analysis of engine overhead due to the extensions. 1 Introduction The lack of finiteness of SLD, even on datalog programs, is a well-known problem. Despite much research, there is no general agreement on the best solution to this problem. Some papers advocate a set-at-a-time solution, usually based on a variant of magic sets [1] (but see also [13]); others prefer a tuple-at-a-time approach based on tabling, such as OLDT [11], or Extension Tables [5]; mixtures are also possible as in SLD-AL [12]