Search

Properties of programs can be formulated using various techniques: dataflow analysis, abstract interpretation and type-like inference systems. This paper reconstructs strictness analysis (establishing when function parameters are evaluated in a lazy language) as a dataflow analysis by expressing the dataflow properties as an effect system. Strictness properties so expressed give a clearer operational understanding and enable a range of additional optimisations including implicational strictness. At first order strictness effects have the expected principality properties (best-property inference) and can be computed simply. [ABSTRACT FROM AUTHOR]

Proving termination of, or generating efficient control for Constraint Handling Rules (CHR) programs requires information about the kinds of constraints that can show up in the CHR constraint store. In contrast to Logic Programming (LP), there are not many tools available for deriving such information for CHR. Hence, instead of building analyses for CHR from scratch, we define a transformation from CHR to Prolog and reuse existing analysis tools for Prolog. The proposed transformation has been implemented and combined with PolyTypes 1.3, a type analyser for Prolog, resulting in an accurate description of the types of CHR programs. Moreover, the transformation is not limited to type analysis. It can also be used to prove other properties of the constraints showing up in constraint stores, using tools for Prolog. [ABSTRACT FROM AUTHOR]

In this paper, we propose an approach for automated test case generation based on techniques from constraint programming (CP). We advocate the use of standard CP search strategies in order to express preferences on the generated test cases and to obtain the desired degree of coverage. We develop our framework in the concrete context of an imperative language and show that the technique is sufficiently powerful to deal with arbitrary pointer-based data-structures allocated on the heap. [ABSTRACT FROM AUTHOR]

Type information has many applications; it can e.g. be used in optimized compilation, termination analysis and error detection. However, logic programs are typically untyped. A well-typed program has the property that it behaves identically on well-typed goals with or without type checking. Hence the automatic inference of a well-typing is worthwhile. Existing inferences are either cheap and inaccurate, or accurate and expensive. By giving up the requirement that all calls to a predicate have types that are instances of a unique polymorphic type but instead allowing multiple polymorphic typings for the same predicate, we obtain a novel strongly-connected-component-based analysis that provides a good compromise between accuracy and computational cost. [ABSTRACT FROM AUTHOR]

In this work, we consider the automatic generation of test inputs for Mercury programs. We use an abstract representation of a program that allows to reason about program executions as paths in a control-flow graph. Next, we define how such a path corresponds to a set of constraints whose solution defines input values for the predicate under test such that when the predicate is called with respect to these input values, the execution is guaranteed to follow the given path. The approach is similar to existing work for imperative languages, but has been considerably adapted to deal with the specificities of Mercury, such as symbolic data representation, predicate failure and non-determinism. [ABSTRACT FROM AUTHOR]

The overhead of matching CHR rules is alleviated by constraint store indexing. Attributed variables provide an efficient means of indexing on logical variables. Existing indexing strategies for ground terms, based on hash tables, incur considerable performance overhead, especially when frequently computing hash values for large terms. In this paper we (1) propose attributed data, a new data representation for ground terms inspired by attributed variables, that avoids the overhead of hash-table indexing, (2) describe program analysis and transformation techniques that make attributed data more effective, and (3) provide experimental results that establish the usefulness of our approach. [ABSTRACT FROM AUTHOR]

This paper introduces a framework for the specification of tree search strategies in CHR with disjunction (CHR ⌄ ). We support the specification of common search strategies such as depth-first, breadth-first and best-first, as well as constrained optimization by means of branch & bound search. The framework is given as an extension of CHR with rule priorities (CHRrp) in which each branch of the search tree is assigned a branch priority. This approach leads to a uniform solution to execution control in CHR. [ABSTRACT FROM AUTHOR]

In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude. [ABSTRACT FROM AUTHOR]

Constraint Handling Rules (CHR) is a high-level programming language based on multi-headed guarded rules. The original high-level operational semantics of CHR is very nondeterministic. Recently, instantiations of the high-level operational semantics have been proposed and implemented, removing sources of nondeterminism and hence allowing better execution control. Rule guards may be redundant under a more instantiated semantics while being necessary in the general high-level semantics. Expert CHR programmers tend to remove such redundant guards. Although this tends to improve the performance, it also destroys the local logical reading of CHR rules: in order to understand the meaning of a rule, the entire program and the details of the instantiated operational semantics have to be taken into account. As a solution, we propose compiler optimizations that automatically detect and remove redundant guards. [ABSTRACT FROM AUTHOR]

This paper investigates the relationship between the Logical Algorithms language (LA) of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation scheme from LA to CHR$^{\textrm{rp}}$: CHR with rule priorities and show that the meta-complexity theorem for LA can be applied to a subset of CHR$^{\textrm{rp}}$ via inverse translation. This result is compared with previous work. Inspired by the high-level implementation proposal of Ganzinger and McAllester, we demonstrate how LA programs can be compiled into CHR rules that interact with a scheduler written in CHR. This forms the first actual implementation of LA. Our implementation achieves the complexity required for the meta-complexity theorem to hold and can execute a subset of CHR$^{\textrm{rp}}$ with strong complexity bounds. [ABSTRACT FROM AUTHOR]

We observe that the combination of multi-parameter type classes with existential types and type annotations leads to a loss of principal types and undecidability of type inference. This may be a surprising fact for users of these popular features. We conduct a concise investigation of the problem and are able to give a type inference procedure which, if successful, computes principal types under the conditions imposed by the Glasgow Haskell Compiler (GHC). Our results provide new insights on how to perform type inference for advanced type extensions. [ABSTRACT FROM AUTHOR]

Two Constraint Handling Rules compiler optimizations that drastically reduce the memory footprint of CHR programs are introduced. The reduction is the result of reusing suspension terms, the internal CHR constraint representation, and avoiding the overhead of constraint removal followed by insertion. The optimizations are defined formally and their correctness is proved. Both optimizations were implemented in the K.U.Leuven CHR system. Significant memory savings and speedups were measured on classical and well-known benchmarks. [ABSTRACT FROM AUTHOR]

Constraint Handling Rules (CHR) is a high-level rule-based language extension, commonly embedded in Prolog. We introduce a new occurrence representation of CHR programs, and a new operational semantics for occurrence representations, equivalent to the widely implemented refined operational semantics. The occurrence representation allows in a natural way to express guard and continuation optimizations, which remove redundant guards and eliminate redundant code for subsumed occurrences. These optimizations allow CHR programmers to write self-documented rules with a clear logical reading. We show correctness of both optimizations, present an implementation in the K.U.Leuven CHR compiler, and discuss speedup measurements. [ABSTRACT FROM AUTHOR]

Constraint Handling Rules (CHR) [2,3,4] is a general-purpose programming language based on committed-choice, multi-headed, guarded multiset rewrite rules. As the head of each CHR rule only considers a fixed number of constraints, any form of aggregation over unbounded parts of the constraint store necessarily requires explicit encoding, using auxiliary constraints and rules. [ABSTRACT FROM AUTHOR]

In his article A Wake-Up Call for the Logic Programming Community, published in the December 2007 issue of the ALP Newsletter, the first author raised concerns about the viability of the Prolog programming language in the near future. The article had a pessimistic undertone, but expressed the hope that the current evolution can be reversed by uniting the Prolog community. Now, almost a year later, it is time for more optimistic news and we are happy that the ALP –through the ICLP 2008 program chairs–has given us the opportunity to re-iterate the arguments, present the recent positive developments and involve the whole community. [ABSTRACT FROM AUTHOR]

Constraint Handling Rules (CHR) [2,5] is a high-level programming language based on multi-headed, committed-choice, guarded multiset rewrite rules. Originally designed in 1991 by Frühwirth for the particular purpose of adding user-defined constraint solvers to a host-language, CHR has matured over the last decade to a powerful and elegant general-purpose language with a wide spectrum of application domains. Different semantics have been proposed for the language, based on various logics (first-order logic, linear logic, ...). These logics, in combination with rewriting techniques, have been used to study program properties such as soundness and completeness, confluence, termination, ...While that line of work treats CHR as a calculus, this tutorial teaches CHR as a proper programming language. As a programming language, CHR seems simple enough: The programmer specifies a number of rewrite rules, and the CHR engine applies these rules exhaustively to an initial (multi-)set of constraints. Yet, this simplicity hides great power: e.g., the power to quickly prototype new constraint solvers, the power to implement Prolog΄s co-routining predicates freeze/2 and when/2 in a single CHR rule each, and the power to subsume Guarded Horn Clauses while still not exploiting CHR΄s full potential. Moreover, CHR is the only declarative language known in which every algorithm can be implemented with optimal space and time complexity [4]. Unfortunately, few Prolog programmers are aware of the CHR language or that it is available in their Prolog system. These programmers are unable to tap into CHR΄s power, so they have to go to great length to accomplish even simple tasks. Or they simply give up. This tutorial shows how to use CHR for solving their problems quickly and elegantly. Simple examples teach interactively how to write and reason about CHR programs, and what problems one can solve effectively with CHR. This tutorial starts with ground CHR, the three types of rules, and the refined semantics [1] which is based on the notion of the active constraint and its occurrences. Other topics covered are triggering of rules, the propagation history, the use of data structures and the host language, declarations and impure features, and the common pitfalls of CHR. This tutorial intends to make the attendants aware of CHR΄s strengths as a programming language, and teaches them when and how to apply CHR for small to medium sized problems. The full set of tutorial slides is available at http://www.cs.kuleuven.be/~dtai/projects/CHR/ . About the Speaker. Tom Schrijvers is a post-doctoral researcher at the K.U.Leuven in Belgium, who has defended his Ph.D. thesis on Analyses, Optimizations and Extensions of Constraint Handling Rules in 2005 [3]. His CHR implementation, the K.U.Leuven CHR system, is the most advanced in its kind and is in wide-spread use in many Prolog systems. Tom uses CHR on a daily basis, for implementing his compiler, for supporting his type checking and test generation research, or simply for gaining an edge in the Prolog Programming Contest. [ABSTRACT FROM AUTHOR]

This is a summary of the Ph.D. thesis of Tom Schrijvers [4]. Constraint Handling Rules (CHR) [3] is a rule-based language commonly embedded in a host language. It combines elements of Constraint Logic Programming and term rewriting. Several implementations of CHR exist: in Prolog, Haskell, Java and HAL. Typical applications of CHR are in the area of constraint solving, but currently CHR is also used in a wider range of applications, such as type checking, natural language processing and multi-agent systems. In this work we contribute program analyses, program optimizations and extensions of the CHR language. For the optimized compilation of CHR we present several new optimizations: code specialization for ground constraints, anti-monotonic delay avoidance, hashtable constraint stores and a new late storage optimization. These and other optimizations have been implemented in a new state-of-the-art CHR system: the K.U.Leuven CHR system [5] which is currently available in SWI-Prolog [10], XSB [9] and hProlog [2]. Abstract interpretation is a general technique for program analysis [1]. We propose a framework of abstract interpretation for the CHR language [7], in particular for the formulation of analyses that drive program optimization. This frameworks allows for the uniform formulation of program analyses as well as easier improvements and combinations of existing analyses. We also evaluate analyses for theoretical properties, confluence and time complexity, on a practical case study to investigate their relevance. We contribute two extensions to the expressivity of CHR. The first extension comprises the integration of CHR with tabled execution [8]. Tabled execution avoids many forms of non-termination and is useful for automatic program optimization through the dynamic reuse of previous computations. The second extension automatically provides implication checking functionality to constraint solvers written in CHR [6]. Implication checking is an essential building block for formulating complex constraints in terms of basic constraints and for composing constraint solvers. [ABSTRACT FROM AUTHOR]