Danny De Schreye

LOPSTR Conference 2018 Conference Paper

Compiling Control as Offline Partial Deduction

• Vincent Nys
• Danny De Schreye

Abstract We present a new approach to a technique known as compiling control, whose aim is to compile away special mechanisms for non-standard atom selection in logic programs. It has previously been conjectured that compiling control could be implemented as an instance of the first Futamura projection, in which an interpreter is specialized for an input program. However, the exact nature of such an interpreter and of the required technique for specialization were never specified. In this work, we propose a Prolog meta-interpreter which applies the desired non-standard selection rule and which is amenable to specialization using offline partial deduction. After the initial analysis phase of compiling control, we collect annotations to specialize the interpreter using the Logen system for offline partial deduction. We also show that the result of the specialization is equivalent to the program obtained using the traditional approach to compiling control. In this way, we simplify the synthesis step.

LOPSTR Conference 2014 Conference Paper

Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction

• Danny De Schreye
• Vincent Nys
• Colin J. Nicholson

Abstract We provide an approach to formally analyze the computational behavior of coroutines in Logic Programs and to compile these computations into new programs, not requiring any support for coroutines. The problem was already studied near to 30 years ago, in an analysis and transformation technique called Compiling Control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also very ad hoc. We show how Abstract Conjunctive Partial Deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine Compiling Control. Leuschel’s framework is more general than the original formulation, it is provably correct, and it can easily be applied for simple examples. We also show that the Abstract Conjunctive Partial Deduction framework needs some further extension to be able to deal with more complex examples.

LOPSTR Conference 2011 Conference Paper

Improved Termination Analysis of CHR Using Self-sustainability Analysis

• Paolo Pilozzi
• Danny De Schreye

Abstract In the past few years, several successful approaches to termination analysis of Constraint Handling Rules (CHR) have been proposed. In parallel to these developments, for termination analysis of Logic Programs (LP), recent work has shown that a stronger focus on the analysis of the cycles in the strongly connected components (SCC) of the program is very beneficial, both for precision and efficiency of the analysis. In this paper we investigate the benefit of using the cycles of the SCCs of CHR programs for termination analysis. It is a non-trivial task to define the notion of a cycle for a CHR program. We introduce the notion of a self-sustaining set of CHR rules and show that it provides a natural counterpart for the notion of a cycle in LP. We prove that non-self-sustainability of an SCC in a CHR program entails termination for all queries to that SCC. Then, we provide an efficient way to prove that an SCC of a CHR program is non-self-sustainable, providing an additional, new way of proving termination of (part of) the program. We integrate these ideas into the CHR termination analyser CHRisTA and demonstrate by means of experiments that this extension significantly improves both the efficiency and the performance of the analyser.

LOPSTR Conference 2011 Conference Paper

Probabilistic Termination of CHRiSM Programs

• Jon Sneyers
• Danny De Schreye

Abstract Termination analysis has received considerable attention in Logic Programming for several decades. In recent years, probabilistic extensions of Logic Programming languages have become increasingly important. Languages like PRISM, CP-Logic, ProbLog, and CHRiSM have been introduced and proved very useful for addressing problems in which a combination of logical and probabilistic reasoning is required. As far as we know, the termination of probabilistic logical programs has not received any attention in the community so far. Termination of a probabilistic program is not a crisp notion. Given a query, such a program does not simply either terminate or not terminate, but it terminates with a certain probability. In this paper, we explore this problem in the context of CHRiSM, a probabilistic extension of CHR. We formally introduce the notion of probabilistic termination. We study this concept on the basis of a number of case studies. We provide some initial sufficient conditions to characterize probabilistically terminating programs and queries. We also discuss some challenging examples that reveal the complexity and interest of more general settings. The paper is intended as a first step in a challenging and important new area in the analysis of Logic Programs.

LOPSTR Conference 2010 Conference Paper

Non-termination Analysis of Logic Programs Using Types

• Dean Voets
• Danny De Schreye

Abstract In recent years techniques and systems have been developed to prove non-termination of logic programs for certain classes of queries. In previous work, we developed such a system based on mode-information and a form of loop checking performed at compile time. In the current paper we improve this technique by integrating type information in the analysis and by applying non-failure analysis and program specialization. It turns out that there are several classes of programs for which existing non-termination analyzers fail and for which our extended technique succeeds in proving non-termination.

LOPSTR Conference 2007 Conference Paper

Termination Analysis of Logic Programs Based on Dependency Graphs

• Manh Thang Nguyen
• Jürgen Giesl
• Peter Schneider-Kamp
• Danny De Schreye

Abstract This paper introduces a modular framework for termination analysis of logic programming. To this end, we adapt the notions of dependency pairs and dependency graphs (which were developed for term rewriting) to the logic programming domain. The main idea of the approach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. These conditions can then be analysed separately by possibly different well-founded orders. We propose a constraint-based approach for automating the framework. Then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.

LOPSTR Conference 2006 Conference Paper

Polytool: Proving Termination Automatically Based on Polynomial Interpretations

• Manh Thang Nguyen
• Danny De Schreye

Abstract In this system description, we present Polytool, a fully automated system for proving left-termination of definite logic programs (LPs). The aim of Polytool is to extend the power of existing termination analysers by using well-founded orders based on polynomial interpretations. This is a direct extension of the well-founded orders based on (semi-)linear level mappings and norms that are used in most of the existing LP termination analysis systems.

LOPSTR Conference 2003 Conference Paper

Proving Termination with Adornments

• Alexander Serebrenik
• Danny De Schreye

Abstract Termination is well-known to be one of the important aspects of program correctness. Logic programming provides a framework with a strong theoretical basis for tackling this problem. However, due to the declarative formulation of programs, the danger of non-termination may increase. As a result, termination analysis received considerable attention in logic programming. Recently, the study of termination of numerical programs led to the emerging of the adorning technique [7]. This technique implements the well-known “divide et impera” strategy by distinguishing between different subsets of values for variables, and deriving termination proofs based on these subsets. In this paper we generalise this technique and discuss its applicability to the domain of terms (the Herbrand domain).

LPAR Conference 2001 Conference Paper

Inference of Termination Conditions for Numerical Loops in Prolog

• Alexander Serebrenik
• Danny De Schreye

Abstract Numerical computations form an essential part of almost any real-world program. Clearly, in order for a termination analyser to be of practical use it should contain a mechanism for inferring termination of such computations. However, this topic attracted less attention of the research community. In this work we concentrate on automatic termination inference for logic programs depending on numerical computations. Dershowitz et al. [ 8 ] showed that termination of general numerical computations, for instance on floating point numbers, may be counter-intuitive, i. e. , the observed behaviour does not necessarily coincide with the theoretically expected one. Thus, we restrict ourselves to integer computations only.

LPAR Conference 2001 Conference Paper

On Termination of Meta-Programs

• Alexander Serebrenik
• Danny De Schreye

Abstract The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics [ 4 ]. The choice of logic programming as a basis for meta-programming offers a number of practical and theoretical advantages. One of them is the possibility of tackling critical foundation problems of meta-programming within a framework with a strong theoretical basis. Another is the surprising ease of programming. These reasons motivated an intensive research on meta-programming inside the logic programming community [ 4 ], [ 16 ], [ 19 ], [ 22 ], [ 23 ].

LOPSTR Conference 2000 Conference Paper

Non-tranformational termination analysis of logic programs, based on general term-orderings

• Alexander Serebrenik
• Danny De Schreye

LOPSTR Conference 1998 Conference Paper

Termination Analysis for Tabled Logic Programming

• Stefaan Decorte
• Danny De Schreye
• Michael Leuschel
• Bern Martens
• Konstantinos Sagonas

Abstract We provide a theoretical basis for studying the termination of tabled logic programs executed under SLG-resolution using a left-to-right computation rule. To this end, we study the classes of quasi-terminating and LG-terminating programs (for a set of atomic goals S ). These are tabled logic programs where execution of each call from S leads to only a finite number of different (i. e. , non-variant) calls, and a finite number of different calls and computed answer substitutions for them, respectively. We then relate these two classes through a program transformation, and present a characterisation of quasi-termination by means of the notion of quasi-acceptability of tabled programs. The latter provides us with a practical method of proving termination and the method is illustrated on non-trivial examples of tabled logic programs.

LOPSTR Conference 1997 Conference Paper

Logic Program Specialisation: How to Be More Specific (Abstract)

• Michael Leuschel
• Danny De Schreye

Abstract Standard partial deduction suffers from several drawbacks when compared to top-down abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies one of those, namely the lack of side-ways information passing. But two other problems remain: the lack of success-propagation as well as the lack of inference of global success-information. We illustrate these drawbacks and show how they can be remedied by combining conjunctive partial deduction with an abstract interpretation technique known as more specific program construction. We present a simple, as well as a more refined integration of these methods. Finally we illustrate the practical relevance of this approach for some advanced applications, where it surpasses the precision of current abstract interpretation techniques.

LPAR Conference 1994 Conference Paper

Implementing a Finite-domain CLP-language on Top of Prolog: a Transformational Approach

• Henk Vandecasteele
• Danny De Schreye

TCS Journal 1994 Journal Article

On the duality of abduction and model generation in a framework for model generation with equality

• Marc Denecker
• Danny De Schreye

We present a duality relationship between abduction for definite abductive programs and model generation on the only-if part of these programs. As was pointed out by Console et. al. (1991), abductive solutions for an abductive program correspond to models of the only-if part. We extend this observation by showing that the procedural semantics of abduction itself can be interpreted dually as a form of model generation on the only-if part. This model generation extends Satchmo with an efficient treatment of equality atoms occuring in the head of rules. It is illustrated how this duality allows to improve current procedures for both abduction and model generation by transferring technical results known for one of these computational paradigms to the other.

LOPSTR Conference 1994 Conference Paper

Some Further Issues in Finite Unfolding (Abstract)

• Bern Martens
• Danny De Schreye

TCS Journal 1994 Journal Article

Sound and complete partial deduction with unfolding based on well-founded measures

• Bern Martens
• Danny De Schreye
• Tamás Horváth

We present a procedure for partial deduction of logic programs, based on an automatic unfolding algorithm which guarantees the construction of sensibly and strongly expanded, finite SLD-trees. We prove that the partial deduction procedure terminates for all definite logic programs and queries. We show that the resulting program satisfies important soundness and completeness criteria with respect to the original program, while retaining the essentially desired amount of specialisation.

LOPSTR Conference 1993 Conference Paper

Automatic Termination Analysis

• Kristof Verschaetse
• Stefaan Decorte
• Danny De Schreye

Abstract Proving termination of programs is important in any approach to program development. In logic programming, where the logic and the control component of a program can very easily be dealt with in two separate phases of the development, the termination issue is solely addressed in the second phase. Both formal, theoretical frameworks for reasoning about termination, and automatic techniques for termination analysis have recently obtained considerable attention in the logic programming community. Unfortunately, in current work, these two types of approaches to termination have been rather orthogonal. It would be desirable if automatic techniques could rely directly on general frameworks for their correctness proofs. We recently presented a new, practical framework for termination analysis of definite logic programs with respect to call patterns. In the current paper, we describe an automated technique, which is directly based on the framework. The main advantages are: the generality of the approach (analysis can be performed for any given set of top-level goals), the clear theoretical underpinning provided by the framework and full automation. .

LOPSTR Conference 1990 Conference Paper

Bottom-Up Specialisation of Logic Programs

• Wim Vanhoof
• Danny De Schreye
• Bern Martens

Abstract Partial deduction is an important transformation technique for logic programs, capable of removing inefficiencies from programs [ 4, 5 ]. As an on-line specialisation technique, it is based on an evaluation mechanism for logic programs. The input to a typical partial deducer is a program and a partially instantiated query. The instantiated part represents the information with respect to which one would like to specialise; the uninstantiated part represents the information not yet known. Therefore, all classical partial deduction techniques use top-down evaluation (or SLD -resolution) to evaluate the program parts that depend on the known input and generate a new program that computes its result using only the remainder of the input. Since the new program has less computations to perform, in general, it will be more efficient.

IJCAI Conference 1989 Conference Paper

Explanation Based Program Transformation

• Maurice Bruynooghe
• Luc De Raedt
• Danny De Schreye

Fold-unfold is a well known program transformation technique. Its major drawback is that folding requires an Eureka step to invent new procedures. In the context of logic programming, we present a technique where the folding is driven by an example. The transformation is aimed at programs suffering from inefficiencies due to the repetition of identical subcomputations. The execution of an example is analysed to locate repeated subcomputations. Then the structure of the example is used to control a fold-unfoldtransformation of the program. The transformation can be automated. The method can be regarded as an extension of explanation based learning.

AIJ Journal 1989 Journal Article

On the existence of nonterminating queries for a restricted class of PROLOG-clauses

• Danny De Schreye
• Maurice Bruynooghe
• Kristof Verschaetse

This work studies the existence of nonterminating queries for a restricted class of recursive predicates. The class is restricted to predicates defined by a set of clauses containing only one (direct) recursive clause. Moreover, this clause must be of the form P(…): -P(…). For this restricted class of predicates, we prove a necessary and sufficient condition for the existence of a query which is nonterminating in the absence of the occur check. The condition is based upon concepts from rational trees.