SearcharxivSearch

arXiv subjects

David S. Warren

Publications and source records attributed to David S. Warren.

14 recordsLinked to original sources

A Prolog Program for Bottom-up Evaluation

This short paper describes a simple and intuitive Prolog program, a metainterpreter, that computes the bottom up meaning of a simple positive Horn clause definition. It involves a simple transformation of the object program rules into metarules, which are then used by a metainterpreter to compute bottom up the model of the original program. The resulting algorithm is a form of semi-naive bottom-up evaluation. We discuss various reasons why this Prolog program is particularly interesting. In particular, this is perhaps the only Prolog program for which I find the use of Prolog's assert/1 to be intrinsic, easily understood, and the best, most perspicuous, way to program an algorithm. This short paper might be best characterized as a Prolog programming pearl.

cs.PL

The Semantics of Metapropramming in Prolog

This paper describes a semantics for pure Prolog programs with negation that provides meaning to metaprograms. Metaprograms are programs that construct and use data structures as programs. In Prolog a primary mataprogramming construct is the use of a variable as a literal in the body of a clause. The traditional Prolog 3-line metainterpreter is another example of a metaprogram. The account given here also supplies a meaning for clauses that have a variable as head, even though most Prolog systems do not support such clauses. This semantics naturally includes such programs, giving them their intuitive meaning. Ideas from M. Denecker and his colleagues form the basis of this approach. The key idea is to notice that if we give meanings to all propositional programs and treat Prolog rules with variables as the set of their ground instances, then we can give meanings to all programs. We must treat Prolog rules (which may be metarules) as templates for generating ground propositional rules, and not as first-order formulas, which they may not be. We use parameterized inductive definitions to give propositional models to Prolog programs, in which the propositions are expressions. Then the set of expressions of a propositional model determine a first-order Herbrand Model, providing a first-order logical semantics for all (pure) Prolog programs, including metaprograms. We give examples to show the applicability of this theory. We also demonstrate how this theory makes proofs of some important properties of metaprograms very straightforward.

cs.PL

The Logic of Logic Programming

Our position is that logic programming is not programming in the Horn clause sublogic of classical logic, but programming in a logic of (inductive) definitions. Thus, the similarity between prototypical Prolog programs (e.g., member, append, ...) and how inductive definitions are expressed in mathematical text, is not coincidental but essential. We argue here that this provides a natural solution to the main lingering semantic questions of Logic Programming and its extensions.

cs.LO

Proceedings of the 2nd Workshop on Logic and Practice of Programming (LPOP)

This proceedings contains abstracts and position papers for the work presented at the second Logic and Practice of Programming (LPOP) Workshop. The workshop was held online, virtually in place of Chicago, USA, on November 15, 2010, in conjunction with the ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) 2020. The purpose of this workshop is to be a bridge between different areas of computer science that use logic as a practical tool. We take advantage of the common language of formal logic to exchange ideas between these different areas.

cs.PL

LPOP: Challenges and Advances in Logic and Practice of Programming

This article describes the work presented at the first Logic and Practice of Programming (LPOP) Workshop, which was held in Oxford, UK, on July 18, 2018, in conjunction with the Federated Logic Conference (FLoC) 2018. Its focus is challenges and advances in logic and practice of programming. The workshop was organized around a challenge problem that specifies issues in role-based access control (RBAC), with many participants proposing combined imperative and declarative solutions expressed in the languages of their choice.

cs.PL

Top-down and Bottom-up Evaluation Procedurally Integrated

This paper describes how XSB combines top-down and bottom-up computation through the mechanisms of variant tabling and subsumptive tabling with abstraction, respectively. It is well known that top-down evaluation of logical rules in Prolog has a procedural interpretation as recursive procedure invocation (Kowalski 1986). Tabling adds the intuition of short-circuiting redundant computations (Warren 1992) .This paper shows how to introduce into tabled logic program evaluation a bottom-up component, whose procedural intuition is the initialization of a data structure, in which a relation is initially computed and filled, on first demand, and then used throughout the remainder of a larger computation for efficient lookup. This allows many Prolog programs to be expressed fully declaratively, programs which formerly required procedural features, such as assert, to be made efficient. This paper is under consideration for acceptance in "Theory and Practice of Logic Programming (TPLP)".

cs.LO

AppLP: A Dialogue on Applications of Logic Programming

This document describes the contributions of the 2016 Applications of Logic Programming Workshop (AppLP), which was held on October 17 and associated with the International Conference on Logic Programming (ICLP) in Flushing, New York City.

cs.PL

Efficiently Retrieving Function Dependencies in the Linux Kernel Using XSB

In this paper we investigate XSB-Prolog as a static analysis engine for data represented by medium-sized graphs. We use XSB-Prolog to automatically identify function dependencies in the Linux Kernel---queries that are difficult to implement efficiently in a commodity database and that developers often have to identify manually. This project illustrates that Prolog systems are ideal for building tools for use in other disciplines that require sophisticated inferences, because Prolog is both declarative and can efficiently implement complex problem specifications through tabling and indexing.

cs.PL

Interning Ground Terms in XSB

This paper presents an implementation of interning of ground terms in the XSB Tabled Prolog system. This is related to the idea of hash-consing. I describe the concept of interning atoms and discuss the issues around interning ground structured terms, motivating why tabling Prolog systems may change the cost-benefit tradeoffs from those of traditional Prolog systems. I describe the details of the implementation of interning ground terms in the XSB Tabled Prolog System and show some of its performance properties. This implementation achieves the effects of that of Zhou and Have but is tuned for XSB's representations and is arguably simpler.

cs.PL

XSB: Extending Prolog with Tabled Logic Programming

The paradigm of Tabled Logic Programming (TLP) is now supported by a number of Prolog systems, including XSB, YAP Prolog, B-Prolog, Mercury, ALS, and Ciao. The reasons for this are partly theoretical: tabling ensures termination and optimal known complexity for queries to a large class of programs. However the overriding reasons are practical. TLP allows sophisticated programs to be written concisely and efficiently, especially when mechanisms such as tabled negation and call and answer subsumption are supported. As a result TLP has now been used in a variety of applications from program analysis to querying over the semantic web. This paper provides a survey of TLP and its applications as implemented in XSB Prolog, along with discussion of how XSB supports tabling with dynamically changing code, and in a multi-threaded environment.

cs.PL

Swapping Evaluation: A Memory-Scalable Solution for Answer-On-Demand Tabling

One of the differences among the various approaches to suspension-based tabled evaluation is the scheduling strategy. The two most popular strategies are local and batched evaluation. The former collects all the solutions to a tabled predicate before making any one of them available outside the tabled computation. The latter returns answers one by one before computing them all, which in principle is better if only one answer (or a subset of the answers) is desired. Batched evaluation is closer to SLD evaluation in that it computes solutions lazily as they are demanded, but it may need arbitrarily more memory than local evaluation, which is able to reclaim memory sooner. Some programs which in practice can be executed under the local strategy quickly run out of memory under batched evaluation. This has led to the general adoption of local evaluation at the expense of the more depth-first batched strategy. In this paper we study the reasons for the high memory consumption of batched evaluation and propose a new scheduling strategy which we have termed swapping evaluation. Swapping evaluation also returns answers one by one before completing a tabled call, but its memory usage can be orders of magnitude less than batched evaluation. An experimental implementation in the XSB system shows that swapping evaluation is a feasible memory-scalable strategy that need not compromise execution speed.

cs.PL

TCHR: a framework for tabled CLP

Tabled Constraint Logic Programming is a powerful execution mechanism for dealing with Constraint Logic Programming without worrying about fixpoint computation. Various applications, e.g in the fields of program analysis and model checking, have been proposed. Unfortunately, a high-level system for developing new applications is lacking, and programmers are forced to resort to complicated ad hoc solutions. This papers presents TCHR, a high-level framework for tabled Constraint Logic Programming. It integrates in a light-weight manner Constraint Handling Rules (CHR), a high-level language for constraint solvers, with tabled Logic Programming. The framework is easily instantiated with new application-specific constraint domains. Various high-level operations can be instantiated to control performance. In particular, we propose a novel, generalized technique for compacting answer sets.

cs.PL

An Environment for the Exploration of Non Monotonic Logic Programs

Stable Model Semantics and Well Founded Semantics have been shown to be very useful in several applications of non-monotonic reasoning. However, Stable Models presents a high computational complexity, whereas Well Founded Semantics is easy to compute and provides an approximation of Stable Models. Efficient engines exist for both semantics of logic programs. This work presents a computational integration of two of such systems, namely XSB and SMODELS. The resulting system is called XNMR, and provides an interactive system for the exploration of both semantics. Aspects such as modularity can be exploited in order to ease debugging of large knowledge bases with the usual Prolog debugging techniques and an interactive environment. Besides, the use of a full Prolog system as a front-end to a Stable Models engine augments the language usually accepted by such systems.

cs.PL