A program specialiser for meta-level compositions of logic programs

Metal-level compositions of object logic programs are naturally implemented by means of meta-programming techniques. Metainterpreters defining program compositions however suffer from a computational overhead that is due partly to the interpretation layer present in all meta-programs, and partly to the specific interpretation layer needed to deal with program compositions. We show that meta-interpreters implementing compositions of object programs can be fruitfully specialised w.r.t. meta-level queries of the form Demo (E, G), where E denotes a program expression and G denotes a (partially instantiated) object level query. More precisely, we describe the design and implementation of declarative program specialiser that suitably transforms such meta-interpreters so as to sensibly reduce — if not to completely remove — the overhead due to the handling of program compositions. In many cases the specialiser succeeds in eliminating also the overhead due to meta-interpretation. Antonio Brogi, Ph.D.: He is currently assistant professor in the Department of Computer Science at the University of Pisa, Italy. He received his Laurea Degree in Computer Science (1987) and his Ph. D. in Computer Science (1993) from the University of Pisa. His research interests include programming language design and semantics, logic programming, deductive databases, and software coordination. Simone Contiero: He is currently a Ph. D. student at the Department of Computer Science, University of Pisa (Italy). He received his Laurea Degree in Computer Science from the University of Pisa in 1994. His research interests are in high-level programming languages, metaprogramming and logic-based coordination of software.     

Completeness of hyper-resolution via the semantics of disjunctive logic programs

We present a proof of completeness of hyper-resolution based on the fixpoint semantics of disjunctive logic programs. This shows that hyper-resolution can be studied from the point of view of logic programming.     

Canonical logic programs

Consider the class of programs P where the greatest fixpoint of T_P is equal to the complement of the finite failure set of P. Programs in this calss possess some important properties which others do not. The main result in this paper proves that this class is representative of all programs. Specifically, we call the programs in this class canonical and we prove that for any program P₁, there exists a semantically equivalent program P₂ which is canonical.     

Efficient and flexible access control via Jones-optimal logic program specialisation

We describe the use of a flexible meta-interpreter for performing access control checks on deductive databases. The meta-program is implemented in Prolog and takes as input a database and an access policy specification. For processing access control requests we specialise the meta-program for a given access policy and database by using the logen partial evaluation system. The resulting specialised control checking program is dependent solely upon dynamic information that can only be known at the time of actual access request evaluation. In addition to describing our approach, we give a number of performance measures for our implementation of an access control checker. In particular, we show that by using our approach we get flexible access control with virtually no overhead, satisfying the Jones optimality criterion. The paper also shows how to satisfy the Jones optimality criterion more generally for interpreters written in the non-ground representation.     

Equivalent logic programs and symmetric homogeneous forms of logic programs with equality

This article introduces the notion of CAS-equivalent logic programs: logic programs with identical correct answer substitutions. It is shown that the notions CAS-equivalence, refutational equivalence, and logical equivalence do not coincide in the case of definite clause logic programs. Least model criteria for refutational and CAS-equivalence are suggested and their correctness is proved. The least model approach is illustrated by two proofs of CAS-equivalence. It is shown that the symmetric extension of a logic program subsumes the symmetry axiom and the symmetric homogeneous form of a logic program with equality subsumes the symmetry, transitivity, and predicate substitutivity axioms of equality. These results contribute towards the goal of building equality into standard Prolog without introducing additional inference rules.     

Most specific logic programs

More specific versions of definite logic programs are introduced. These are versions of a program in which each clause is further instantiated or removed and which have an equivalent set of successful derivations to those of the original program, but a possibly increased set of finitely failed goals. They are better than the original program because failure in a non-successful derivation may be detected more quickly. Furthermore, information about allowed variable bindings which is hidden in the original program may be made explicit in a more specific version of it. This allows better static analysis of the program's properties and may reveal errors in the original program. A program may have several more specific versions but there is always a most specific version which is unique up to variable renaming. Methods to calculate more specific versions are given and it is characterized when they give the most specific version.     

Parallelism in logic programs

There is a tension between the objectives of avoiding irrelevant computation and extracting parallelism, in that a computational step used to restrict another must precede the latter. Our thesis, following [3], is that evaluation methods can be viewed as implementing a choice ofsideways information propagation graphs, or sips, which determines the set of goals and facts that must be evaluated. Two evaluation methods that implement the same sips can then be compared to see which obtains a greater degree of parallelism, and we provide a formal measure of parallelism to make this comparison.Using this measure, we prove that transforming a program using the Magic Templates algorithm and then evaluating the fixpoint bottom-up provides a most parallel implementation for a given choice of sips, without taking resource constraints into account. This result, taken in conjunction with earlier results from [3,27], which show that bottom-up evaluation performs no irrelevant computation and is sound and complete, suggests that a bottom-up approach to parallel evaluation of logic programs is very promising. A more careful analysis of the relative overheads in the top-down and bottom-up evaluation paradigms is needed, however, and we discuss some of the issues.The abstract model allows us to establish several results comparing other proposed parallel evaluation methods in the logic programming and deductive database literature, thereby showing some natural, and sometimes surprising, connections. We consider the limitations of the abstract model and of the proposed bottom-up evaluation method, including the inability of sips to describe certain evaluation methods, and the effect of resource constraints. Our results shed light on the limits of the sip paradigm of computation, which we extend in the process.     

Transformations of logic programs

This paper introduces a new concept of computation trees of logic programs that will be used in reasoning about programs. Three types of transformations improving the structure of logic programs are described. There are two natural measures of complexity suggested by computation trees, namely, the number of nodes called by recursion and the maximal number of AND/OR alternations on a branch. Both measures are shown to collapse, or more precisely, it is shown how every logic program can be transformed to a program computing the same function of which the computation tree has at most one called node and at most two alternations on every branch. Some conclusions related to this Normal Form Theorem are discussed. Theoretical results with the attempts to develop a practical methodology for the construction of logic programs are compared.     

Learning higher-order logic programs

Machine Learning - A key feature of inductive logic programming is its ability to learn first-order programs, which are intrinsically more expressive than propositional programs. In this paper, we...     

On computing logic programs

In this paper we present and compare some classical problem-solving methods for computing the stable models of logic programs with negation. Using a graph theoretic representation of logic programs and their stable models, we discuss and compare linear programming, propositional satisfiability, constraint satisfaction, and graph methods.     

Grammar-related transformations of logic programs

We investigate a simple transformation of logic programs capable of inverting the order of computation. Several examples are given which illustrate how this transformation may serve such purposes as left-recursion elimination, loop-elimination, simulation of forward reasoning, isotopic modification of programs and simulation of abductive reasoning.     

On computability by logic programs

The problem of computational completeness of Horn clause logic programs is revisited. The standard results on representability of all computable predicates by Horn clause logic programs are not related to the real universe on which logic programs operate. SLD-resolution, which is the main mechanism to execute logic programs, may give answer substitutions with variables. As the main result we prove that computability by Horn clause logic programs is equivalent to standard computability over the Herbrand universe with variables. The semantics we use isS-semantics introduced by Falaschi et al. [3]. As an application of the main result we prove the existence of a metainterpreter for a sublanguage of real Prolog, written in the language of Horn clauses with the S-semantics. We also show that the traditional semantics of Prolog do not reflect its computational behavior from the viewpoint of recursion theory.This article is a revised version of [13]. The work was essentially done during author's visit to ECRC.     

Learning hierarchical probabilistic logic programs

Machine Learning - Probabilistic logic programming (PLP) combines logic programs and probabilities. Due to its expressiveness and simplicity, it has been considered as a powerful tool for learning...     

Linearizing some recursive logic programs

We give a sufficient condition under which the least fixpoint of the equation X=a+f(X)X equals the least fixpoint of the equation X=a+f(a)X. We then apply that condition to recursive logic programs containing chain rules: we translate it into a sufficient condition under which a recursive logic program containing n⩾2 recursive calls in the bodies of the rules is equivalent to a linear program containing at most one recursive call in the bodies of the rules. We conclude with a discussion comparing our condition with the other approaches to linearization studied in the literature     

Hypothetical reasoning in logic programs

In order to express incomplete knowledge, extended logic programs have been proposed as logic programs with classical negation along with negation as failure. This paper discusses ways to deal with a broad class of common sense knowledge by using extended logic programs. For this purpose, we present a uniform approach for dealing with both incomplete and contradictory programs, as a simple framework of hypothetical reasoning in which some rules are dealt with as candidate hypotheses that can be used to augment the background theory. This theory formation framework can be used for default reasoning, contradiction removals, the closed world assumption, and abduction. We also show a translation of the theory formation framework to an extended logic program whose answer sets correspond to the consistent belief sets of augmented theories.