Abstract Matching can improve on Abstract Unification
University of Kent at Canterbury,
Canterbury, CT2 7NF, UK.
Dept. of Electronics and Computer Science,
University of Southampton,
Southampton, S09 5NH, UK.
March 3, 1995
Analyses for sharing and freeness are important in the optimisation and the parallelisation of logic programs. By using a standard fixed-point framework, sharing and freeness analysis can be constructed by defining suitable abstract analogs for concrete operations like renaming, restriction, unification and extension. Extension is required in the clause exit mechanisms and is typically formulated in terms of restriction and matching. Matching also arises as goal-head unification in normalised programs in which the (formal) arguments of each clause head are distinct variables. Abstract matching, however, is rarely given special attention and is usually implemented by abstract unification. This paper remedies this, contributing a series of useful, practical and formally-justified abstract matching algorithms for the popular domains Share, Share ? Free and Share ? Free ? Lin. The matching algorithms are useful and important because they can outperform their corresponding unification algorithms in both precision and speed.
Analyses for sharing and freeness are important topics of logic programming with applications which include: the sound removal of the occur-check ; optimisation of backtracking ; the specialisation of unification ; and the identification [13, 35] and efficient exploitation [14, 28, 29] of independent and-parallelism .
Following the approach of abstract interpretation , sharing and freeness analyses are usually constructed by tracing possible program executions with descriptions of the data values (the abstract data) rather than using actual data values (the concrete data). The construction usually divides into domain and framework related issues. For the domain, suitable abstract analogs for concrete operations like renaming, unification, composition and restriction are specified and proven safe for a particular description of substitutions. For example, unification would be mimicked by an abstract unification algorithm in which substitutions are finitely represented by sharing and freeness abstractions, the abstract substitutions. The framework traces the control-flow of Prolog, the concrete semantics, calculating abstract substitutions at various points of a program thereby characterising the actual substitutions which can possibly arise at those program points. Frameworks [1, 11, 16, 17, 23, 26, 29, 30, 34] are usually parameterised by the domain operations and basically solve a set of fixed-point equations.
1.1 Abstract matching in standard frameworks
Although the concrete semantics of logic programs are formulated in terms of unification, both matching and unification usually require to be abstracted in a framework. Frameworks typically trace the values of substitutions which, for finiteness, are restricted to sets of program variables. To