Regular approximation of computation paths in logic and functional languages

Abstract

The aim of this work is to compute descriptions of successful computation paths in logic or functional program ex ecutions. Computation paths are represented as terms, built from special constructor symbols, each constructor symbol corresponding to a specific clause or equation in a program. Such terms, called trace-terms, are abstractions of computation trees, which capture information about the control flow of the program. A method of approximating trace-terms is described, based on well-established methods for computing regular approximations of terms. The special function symbols are first introduced into programs as extra arguments in predicates or functions. Then a regular approximation of the program is computed, describing the terms occurring in some set of program executions. The approximation of the extra arguments (the trace-terms) can then be examined to see what computation paths were followed during the computation. This information can then be used to control both off-line or on-fine specialisation systems. A key aspect of the analysis is the use of suitable widening operations during the regular approximation, in order to preserve information on determinacy and branching structure of the computation. This method is applicable to both logic and functional languages, and appears to offer appropriate control information in both formalisms.