Specification and correctness proof of a WAM extension with abstract type constraints

We provide a mathematical specification of an extension of Warren's Abstract Machine (WAM) for executing Prolog to type-constraint logic programming and prove its correctness. Our aim is to provide a full specification and correctness proof of a concrete system, the PROTOS Abstract Machine (PAM), an extension of the WAM by polymorphic order-sorted unification as required by the logic programming language PROTOS-L.In this paper, while leaving the details of the PAM's type constraint representation and solving facilities to a sequel to this work, we keep the notion of types and dynamic type constraints abstract to allow applications to different constraint formalisms like Prolog III or CLP(R). This generality permits us to introduce modular extensions of Börger's and Rosenzweig's formal derivation of the WAM. Since the type constraint handling is orthogonal to the compilation of predicates and clauses, we start from type-constraint Prolog algebras with compiled AND/OR structure that are derived from Börger's and Rosenzweig's corresponding compiled standard Prolog algebras. The specification of the type-constraint WAM extension is then given by a sequence of evolving algebras, each representing a refinement level, and for each refinement step a correctness proof is given. Thus, we obtain the theorem that for every such abstract type-constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct.The first author was partially funded by the German Ministry for Research and Technology (BMFT) in the framework of the WISPRO Project (Grant 01 IW 206). He would also like to thank the Scientific Center of IBM Germany where the work reported here was started.     

A prolog constraint handling rules compiler and runtime system

The most recent and advanced implementation of constraint handling rules (CHR) is introduced in a logic programming language. The Prolog implementation consists of a runtime system and a compiler. The runtime system utilizes attributed variables for the realization of the constraint store with efficient retrieval and update mechanisms. Rules describing the interactions between constraints are compiled into Prolog clauses by a compiler, the core of which comprises a small number of compact code generating templates in the form of definite clause grammar rules.     

Formal reasoning in intelligent database systems

Expert database systems were proposed to solve the difficulties encountered in traditional database systems. Prolog provides a fast prototyping tool for building such database systems. However, an intelligent database system implemented in Prolog faces a major restriction that only Horn rules are allowed in the knowledge base. We propose a theorem prover which can make inference for non-Horn intelligent database systems. Conclusions can be deduced from the facts and rules stored in a knowledge base. For a knowledge base with a finite domain, the prover can provide correct answers to queries, derive logical consequences of the database, and provide help in detecting inconsistencies or locating bugs in the database. The theorem prover is efficient in deriving conclusions from large knowledge bases which might swamp most of the other deductive systems. The theorem prover is also useful in solving heuristically the satisfiability problem related to a database with an infinite domain. A truth maintenance mechanism is provided to help eliminate repetitious work for the same goals.Supported by National Science Council under grant NSC 81-0408-E-110-9.     

Design and simulation of a sequential Prolog machine

Prolog-X is an implemented portable interactive sequential Prolog system in which clauses are incrementally compiled for a virtual machine called the ZIP Machine. At present, the ZIP Machine is emulated by software, but it has been designed to permit easy implementation in microcode or hardware. Prolog-X running on the software-based emulator provides performance comparable with existing Prolog interpreters. To demonstrate its efficiency, compatibility, and comprehensiveness of implementation, Prolog-X has been used to compile and run several large applications programs. Several novel techniques are used in the implementation, particularly in the areas of the representation of therecordx database, the selection of clauses, and the compilation of arithmetic expressions.     

Assert,retract and external processes in prolog

As Prolog becomes more widely used, it becomes important to provide clear and consistent implementations of the assert and retract primitives. This paper introduces a bit-map indexing system with a consistent semantics. It also considers the implementation of the interface between Prolog and an external source of clauses, concentrating on the storage of clauses on secondary storage, but considering also the presentation of data to Prolog programs by non-Prolog processes.     

Efficient reordering of Prolog programs

Prolog programs are often inefficient: execution corresponds to a depth-first traversal of an AND/OR graph; traversing subgraphs in another order can be less expensive. It is shown how the reordering of clauses within Prolog predicates, and especially of goals within clauses, can prevent unnecessary search. The characterization and detection of restrictions on reordering is discussed. A system of calling modes for Prolog, geared to reordering, is proposed, and ways to infer them automatically are discussed. The information needed for safe reordering is summarized, and which types can be inferred automatically and which must be provided by the user are considered. An improved method for determining a good order for the goals of Prolog clauses is presented and used as the basis for a reordering system     

Efficient database access from Prolog

In designing the interface between a relational database and a Prolog interpreter, efficiency is a major issue. The authors present a method for loading into the memory-resident database of Prolog facts permanently stored in secondary storage. The rationale of the method is to save access to the database by never repeating the same query and by storing in main memory, in a compact and efficient way, information about the past interaction with the database. The authors discuss how to reduce subsumption rests required by the method to pattern matching in many relevant cases. They also describe a simulator of the method, which validates their approach, and they discuss the results of the simulation     

Algebraic computational models of OR-parallel execution of Prolog

A specification of the OR-parallel execution of Prolog programs, using CHOCS (calculus of higher order communicating systems) [24], is presented in the paper. A translation is defined from Prolog programs and goals to CHOCS processes: the execution of the CHOCS process corresponding to a goal mimics the OR-parallel execution of the original Prolog goal. In the translation, clauses and predicate definitions of a Prolog program correspond to processes. To model OR-parallelism, the processes , corresponding to clauses (having the same head predicate ) start their execution concurrently, but, in order to respect the depth-first search rule, each is guarded by the termination of the executions of processes 's, . The computational model is proved correct with respect to the semantics of Prolog, as given in [4, 5]. Our model, because of its algebraic specification, can be easily used to prove properties of the parallel execution of Prolog programs. Moreover, the model exploits the maximum degree of parallelism, by giving the Prolog solutions in parallel, without any order among them. However, this model, being close to the Prolog semantics definition, contains sources of inefficiency which make it unpractical as a guide for the implementation. To overcome these problems, a new computational model is defined. This model is obtained by modifications of the basic one and thus its correctness can be easily proved. Finally, we show how to obtain models of different real implementations of OR-parallel Prolog by slight modification of the new model. The relations among all these models, in terms of parallelism degree, are studied by using the concepts of bisimulation and simulation, developed for concurrent calculi. Received: 5 May 1995 / 28 May 1996     

Near-Horn Prolog and beyond

Near-Horn Prolog is an extension of Prolog designed to handle disjunction and classical negation. The emphasis here is on minimal change from standard Prolog in regard to notation, derivation form, and speed of inner-loop computation. The procedure is optimized for the input program that is near-Horn; i.e., a program where almost all clauses are definite clauses. This paper goes beyond the near-Horn focus to report on the completeness of one version of nH-Prolog, along with soundness of the procedure. Completeness is important here not only for the usual reasons of guaranteed success on small problems and insight into the behavior of the procedure but also because we anticipate the introduction of negation-as-failure which requires conviction that a proof will be found if a proof exists.This research was supported in part by the U.S. Army Research Office under grants DAAG29-84-K-0072 and DAAL03-88-K-0082 and by NSF Grant IRI-8805696.     

Oracle Semantics for Prolog

This paper proposes to specify semantic definitions for logic programming languages such as Prolog in terms of an oracle which specifies the control strategy and identifies which clauses are to be applied to resolve a given goal. The approach is quite general. It can be applied to Prolog to specify both operational and declarative semantics as well as other logic programming languages. Previous semantic definitions for Prolog typically encode the sequential depth-first search of the language into various mathematical frameworks. Such semantics mimic a Prolog interpreter in the sense that following the "leftmost" infinite path in the computation tree excludes computation to the right of this path from being considered by the semantics. The basic idea in this paper is to abstract away from the sequential control of Prolog and to provide a declarative characterization of the clauses to apply to a given goal. The decision whether or not to apply a clause is viewed as a query to an oracle which is specified from within the semantics and reasoned about from outside. This approach results in simple and concise semantic definitions which are more useful for arguing the correctness of program transformations and providing the basis for abstract interpretations than previous proposals.     

Chart parsers as inference systems for fixed-mode logic programs

Logic programs resemble context-free grammars. Moreover, Prolog’s proof procedure can be viewed as a generalization of a simple top-down parser with backtracking. This simple parser has disadvantages that motivated the design of more sophisticated parsing methods. As similar disadvantages occur in Prolog’s proof procedure, it may be desirable to develop other proof procedures for logic programs than the one used by Prolog. The resemblance between definite clauses and productions suggests looking at parsing to develop such procedures. We obtain proof procedures for fixed-mode logic programs, based on “chart” parsers. Our approach concentrates on transforming (fixed-mode) logic programs rather than the parser. We first add unification to a chart parser obtaining a proof procedure for programs severely restricted in their syntax, in which the body of the clauses denotes the composition of binary relations: “chain” programs. We then show how to transform fixed-mode programs into chain form. We arrive at proof procedures that avoid some nonterminating loops as well as the recomputation of some partial results.     

P#: a concurrent Prolog for the .NET framework

We discuss P#, our implementation of a tool that allows interoperation between a concurrent superset of the Prolog programming language and C#. This enables Prolog to be used as a native implementation language for Microsoft's .NET platform. P# compiles a linear logic extension of Prolog to C# source code. We can thus create C# objects from Prolog and use C#'s graphical, networking and other libraries. We add language constructs on the Prolog side that allow concurrent Prolog code to be written. A primitive predicate is provided that evaluates a Prolog structure on a newly forked thread. Communication between threads is based on the unification of variables contained in such a structure. It is also possible for threads to communicate through a globally accessible table. All of the new features are available to the programmer through new built-in Prolog predicates. We discuss two software engineering tools implemented using P#. Copyright © 2004 John Wiley & Sons, Ltd.     

Elimination of Self-Resolving Clauses

It is shown how self-resolving clauses like symmetry or transitivity, or even clauses like condensed detachment, can faithfully be deleted from the clause set, thus eliminating or at least reducing recursiveness and circularity in clause sets. Possible applications are reducing the search space for automated theorem provers, eliminating loops in Prolog programs, parallelizing simple closure computation algorithms, and supporting automated complexity analysis.     

Regular corecursion in Prolog

Corecursion is the ability of defining a function that produces some infinite data in terms of the function and the data itself, as supported by lazy evaluation. However, in languages such as Haskell strict operations fail to terminate even on infinite regular data, that is, cyclic data.Regular corecursion is naturally supported by coinductive Prolog, an extension where predicates can be interpreted either inductively or coinductively, that has proved to be useful for formal verification, static analysis and symbolic evaluation of programs.In this paper we use the meta-programming facilities offered by Prolog to propose extensions to coinductive Prolog aiming to make regular corecursion more expressive and easier to program with.First, we propose a new interpreter to solve the problem of non-terminating failure as experienced with the standard semantics of coinduction (as supported, for instance, in SWI-Prolog). Another problem with the standard semantics is that predicates expressed in terms of existential quantification over a regular term cannot directly defined by coinduction; to this aim, we introduce finally clauses, to allow more flexibility in coinductive definitions.Then we investigate the possibility of annotating arguments of coinductive predicates, to restrict coinductive definitions to a subset of the arguments; this allows more efficient definitions, and further enhance the expressive power of coinductive Prolog.We investigate the effectiveness of such features by showing different example programs manipulating several kinds of cyclic values, ranging from automata and context free grammars to graphs and repeating decimals; the examples show how computations on cyclic values can be expressed with concise and relatively simple programs.The semantics defined by these vanilla meta-interpreters are an interesting starting point for a more mature design and implementation of coinductive Prolog.     

Finding hydrophobic microdomains using an object-oriented database

A procedure for finding clusters of adjacent residues in protein hydrophobic cores--hydrophobic microdomains--has been proposed by Plochocka et al. A program is presented that finds hydrophobic microdomains, making use of protein structure data stored in an object-oriented database and the list-processing features of Prolog. Alternative definitions for hydrophobic microdomains are explored. Results are presented for haemoglobin.     

Renaming a set of non-Horn clauses

Several extensions of the logic programming language Prolog to nonHorn clauses use case analysis to handle non-Horn clauses.In this paper,analytical and emprirical evidences are presented to show that,by making a set of clauses less “non-Horn“ using predicated renaming.the performance of these case-analysis based procedures can be improved significantly.In addition,the paper also investigated the problem of efficeiently constructing a predicate renaming that reduces the degree of “non-Hornness“ of a clause set maximally.It is shown that this problem of finding a redicate renaming to achieve minimal “non-Hornness“ is NP -complete.     

Translating a Linear Logic Programming Language into Java

There have been several proposals for logic programming language based on linear logic: Lolli [8], Lygon [7], LO [3], LinLog [2], Forum [11], HACL [10]. In these languages, it is possible to create and consume resources dynamically as logical formulas. The efficient handling of resource formulas is, therefore, an important issue in the implementation of these languages. Lolli, Lygon, and Forum are implemented as interpreter systems; Lolli is on SML and λProlog, Lygon is on Prolog, Forum is on SML, λProlog and Prolog. However, none of them have been implemented in Java.In this paper, we describe the Prolog Café ¹ system which translates a linear logic programming language called LLP to Java via the LLPAM [12] [5], an extension of the standard WAM [16] [1] for LLP. LLP is a superset of Prolog and a subset of Lolli. The main difference from the first implementation [4] is resource compilation. That is to say, resource formulas are compiled into closures which consist of a reference of compiled code and a set of bindings for free variables. Calling these resources is integrated with the ordinary predicate invocation.Prolog Café is portable to any platform supporting Java and easily expandable with increasing Java's class libraries. In performance, on average, Prolog Café generate 2.2 times faster code for a set of classical Prolog benchmarks compared with jProlog.     

Non-Horn clause logic programming without contrapositives

We present an extension of Prolog-style Horn clause logic programming to full first order logic. This extension has some advantages over other such extensions that have been proposed. We compare this method with the model elimination strategy which Stickel has recently implemented very efficiently, and with Loveland's extension of Prolog to near-Horn clauses. This new method is based on the author's simplified problem reduction format but permits a better control of the splitting rule than does the simplified problem reduction format. In contrast to model elimination, this new method does not require the use of contrapositives of clauses, permitting a better control of the search. This method has been implemented in C Prolog and has turned out to be a respectable and surprisingly compact first-order theorem prover. This implementation uses depth-first iterative deepening and caching of answers to avoid repeated solution of the same subgoal. We show that the time and space used by this method are polynomial functions of certain natural parameters of the search space, unlike other known methods. We discuss the relation of these upper bounds to Savitch's theorem relating nondeterministic time to deterministic space.This research was supported in part by the National Science Foundation under grant DCR-8516243.     

Integration of prolog and databases in both evaluational and non-evaluational approaches

DB-Prolog is an extended version of Prolog which allows users to access relational databases in both evaluational and non-evaluational approaches. Using the former approach, DB-Prolog offers some built-in predicates for retrieving relational databases. Using the latter approach, DB-Prolog enables relational databases to store facts (ground unit clauses) which may have compound terms in their arguments. As a result, DB-Prolog can execute Prolog programs which contain both a large set of facts, and conventional data (both numerical and character) efficiently. These Prolog programs are required for the construction of practical expert systems. DB-Prolog implementation techniques are described, and some of its available functions are discussed.