The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #455

Title:The Improvement of Prolog Program Efficiency by Compiling Control: a Proof-Theoretic View
Date:Mar 1990
Presented:Submitted to META-90 Workshop, Leuven, Belgium, April 1990.
Abstract:In this paper, I report on progress in applying Proof Planning techniques developed by Bundy et al at Edinburgh to the ideas of Compiling Control proposed by Bruynooghe de Schreye et al at Leuven. The overall theme of the paper is the application of a proof-theoretic view of Prolog program execution to the issues involved in performing Compiling Control. In particular, I show how the use of strict data-typing can help to guide an inductive proof, analogous to the execution of a recursive Prolog program for some given computational rule, to produce an execution tree equivalent (in many cases) to that required for the compilation of control under the Leuven regime. I conclude that this is a worthwhile direction to follow, though there are some cases not covered by the proof-theoretic approach which are dealt with by the techniques of abstract interpretation involved in Compiling Control.

[Search These Pages] [DAI Home Page] [Comment]