A Comparison of Three Occur-Check Analysers.pdf

A Comparison of ThreeOccur-Check AnalysersLobel Crnogorac, Andrew D. Kellyand Harald SndergaardTechnical Report 96/20 Dept. of Computer ScienceThe University of MelbourneParkville Vic. 3052Australia A Comparison of Three Occur-Check AnalysersLobel Crnogorac, Andrew D. Kellyy and Harald Sndergaard Department of Computer Science y Department of Computer ScienceUniversity of Melbourne Monash UniversityParkville Vic. 3052, Australia Clayton Vic. 3168, Australiaflobel,haraldg@cs.mu.oz.au kelly@cs.monash.edu.auAbstractA well known problem of most Prolog interpreters and compilers is the lack of occur-check in theimplementation of the unication algorithm. This means that such systems are unsound with respectto rst-order predicate logic. Static analysis oers an appealing approach to the problem of occur-checkreduction, that is, how to safely omit occur-checks in unication. We compare, for the rst time, threestatic methods that have been suggested for occur-check reduction, two based on assigning \modes toprograms and one which uses abstract interpretation. In each case, the analysis or some essential partof it had not been implemented so far. Of the mode-based methods, one is due to Chadha and Plaistedand the other is due to Apt and Pellegrini. The method using abstract interpretation is based on earlierwork by Plaisted, Sndergaard and others who have developed \groundness and \sharing analysesfor logic programs. The conclusion is that a truly global analysis based on abstract interpretation leadsto markedly higher precision and hence fewer occur-checks at run-time. The analysis is a compile-timeinvestment, and given the potential run-time speedups, a precise analysis would be well worth theextra time. 1 1 IntroductionUnication is the central operation in the execution of logic programs. For reasons of eciency, it iscommon for Prolog systems to omit the so-called occur-check when performing unication, with the resultthat soundness can no longer be guaranteed.