In this and the next chapter, algorithms for reasoning in constraint systems, i.e. for solving, simplification, and propagation of constraints, will be presented as logical inference rules that are directly executable in CHR. Unless otherwise noted, these constraint solvers are well-behaved (terminating and confluent). For most solvers, we will contrast the worst-case time complexity given by the meta-complexity Theorem 5.35 with empirical results from a preliminary set of test runs. Typically, the observed time complexity has lower exponents than those predicted by the meta-complexity theorem.

There are two main approaches for constraint-solving algorithms, variable elimination and local consistency (local propagation) techniques. A clear distinction between the two approaches is not always possible. Variable elimination substitutes terms for variables. This typically results in solvers defined by rules with recursive calls to the given constraints that contain fewer variables. In the local propagation approach, we derive simple constraints from the given constraints at hand and let the given constraints react to them. Local consistency techniques typically have to be interleaved with search to achieve global consistency, i.e. satisfaction-completeness. (Satisfaction-) completeness means that the solver can always detect unsatisfiability of allowed constraints.

In this chapter, we deal with constraint solvers for problems where the variables can only take values from a finite domain. Here the solvers try to reduce the set of possible values for a variable, i.e. to remove values from its domain that do not occur in any solution. So finite domain constraint solving proceeds by making domains smaller and smaller. The smallest useful finite domain contains the two truth values of Boolean algebra.

We present the essentials of the Constraint Handling Rules (CHR) programming language by the use of examples in this Tutorial part.

The first chapter Getting started is a step-by-step introduction to CHR based on simple examples.

The second chapter My first CHR programs introduces some simple, but concise and effective, CHR programs. We discuss basic properties of CHR programs in an informal way: anytime and online algorithm property, correctness, confluence, concurrency, and complexity. The formal analysis of these programs is deferred to Part III.

Exercises and selected solutions are given for the practical programming chapters in Parts I and III. More exercises can be found online.

CHR has taken off. After five dedicated workshops, two special journal issues, and hundreds of related research articles, it was time to write this book about CHR.

About this book

This book is about programming with rules. It presents a rule-based constraint programming language called CHR (short for Constraint Handling Rules). While conceptually simple, CHR embeds the essential aspects of many rule-based and logic-based formalisms and can implement algorithms in a declarative yet highly effective way. The combination of information propagation and multiset transformation of relations in a concurrent, constraint-based language makes CHR a powerful declarative tool for knowledge representation and reasoning. Over the last decade CHR has not only cut its niche as a special-purpose language for writing constraint solvers, but has matured into a general-purpose language for computational logic and beyond.

This intermediate-level book with a gentle introduction and more advanced chapters gives an overview of CHR for readers of various levels of experience. The book is addressed to researchers, lecturers, graduate students, and professional programmers interested in languages for innovative applications. The book supports both self-study and teaching. It is accompanied by a website at chr.informatik.uni-ulm.de.

In short, this book concentrates on the basics of CHR while keeping in mind dozens of research papers. In 2009, there will be a companion book on recent advances in CHR and a survey article in a journal. A book on implementation of CHR and a collection of classical CHR papers is also planned.

We analyze the programs from the CHR tutorial and then a number of larger programs in more detail and more formally. The programs solve problems over finite and infinite domains of values: propositional satisfaction problems (Boolean algebra), syntactic equations over rational trees and linear polynomial equations, implementing the graph-based constraint algorithms of arc and path consistency, and the global lexicographic order constraint. We also directly implement description logic (extended with rules), which is the formal basis of ontology languages of the semantic web. We give a program for the classical union-find algorithm with optimal time and space complexity. We parallelize the algorithm and generalize it for efficient equation solving. We use it in an efficient syntactic equation solver.

In this chapter, we present constraint solvers for constraints over variables that have infinite domains. The first domain is the numbers, and we solve linear polynomial equations. The second domain is some ordered set of values that we extend to a lexicographic order, which we consider as a constraint on a sequence of variables. The third domain is the objects that occur in knowledge representation with description logics. Reasoning in these logics is reducible to consistency checking. The fourth domain is the universal data structure of logical terms where we consider the unification problem as equation solving.

Linear polynomial equation solving

Typically, in arithmetic constraint solvers, incremental variants of classical variable elimination algorithms like Gaussian elimination for equations and Dantzig's Simplex algorithm for equations are implemented. Gaussian elimination has cubic complexity in the number of different variables in a problem. The Simplex algorithm has exponential worst-case time complexity but is polynomial on average.

Similar to Gaussian elimination, we solve linear polynomial equations by eliminating variables, one at a time. For solving inequations, the rules for Fourier's algorithm turn out to be very similar to those for equation solving.

Variable elimination

We define the syntax of the equations and show the principle of eliminating a variable.

We are interested in the relationship of other rule-based formalisms and programming languages to CHR. In particular, we want to know about the principles of embedding essential aspects of them in CHR. We will informally discuss the following formalisms, systems, and language paradigms:

• Rule-based systems such as Production Rules (e.g. OPS5), Event{ Condition{Action (ECA) Rules, Business Rules, and the Logical Algorithms (LA) formalism in Section 6.1.

• Rewriting-based and graph-based formalisms such as Term Rewriting Systems (TRS) with a remark on Functional Programming (FP) and on Graph Rewriting Systems (GTS), the General Abstract Model for Multiset Manipulation (GAMMA), and standard and Colored Petri Nets (CPN) in Section 6.2.

• Prolog, a remark on deductive databases, the Constraint Logic Programming (CLP), and the Concurrent Constraint Programming (CC) language framework in Section 6.3.

We cannot give a full account of all these approaches, after all this is a book about CHR. We have to assume some basic knowledge of the approach discussed. The approaches range from theoretically well-researched formalisms like term rewriting and programming language schemes like constraint logic programming to concrete rule-based systems like OPS5. Readers may find the presentation of the formalisms overly simplistic, but this has been done for space reasons and to emphasize the relationship with CHR. We will take the viewpoint of CHR, and this should not be taken as a critique on the other approaches. We also cannot go into the details of the embeddings. When available, we refer to research papers. If not, we present the main idea behind a possible answer to an otherwise unexplored open research question.

The classical union-find (also: disjoint set union) (UF) algorithm was introduced by Tarjan in the 1970s. This essential algorithm efficiently solves the problem of maintaining a collection of disjoint sets under the operation of union. It is the basis for many graph algorithms (e.g. efficient computation of spanning trees). By definition of set operations, a union operator working on representatives of sets is an equivalence relation, i.e. we can view sets as equivalence classes and deal with equality.

We give concise CHR programs for the union-find algorithm and some variants that have best-known time and space complexity. This is believed impossible in other pure declarative programming languages due to their lack of destructive assignment which is needed for efficient update of graph data structures. Our program benefits from the guaranteed properties of wellbehaved CHR programs such as the anytime and online algorithm property. This makes our implementation particularly well-suited for use in constraint solvers.

Using CHR analysis techniques we study logical correctness and confluence of these programs. We observe the essential update of the algorithm which makes it nonconfluent and nonmonotonic but efficient. Based on the confluence analysis, we are able to parallelize the UF algorithm. This is considered to be hard in the literature. When the UF algorithm is extended to deal with function terms (rational trees), the algorithm can be used for optimal complexity unification. Last but not least, we discuss a generalization of UF that yields novel algorithms for simple Boolean and linear equations that are well-suited for constraint solving.

This chapter is a basic introduction to CHR using simple examples. They introduce the types of rules used in CHR, their behavior and basic ingredients of the language such as logical variables and built-in constraints. Last but not least, we define the concrete syntax of CHR and we informally describe how CHR executes its rules.

In this book, we will use the concrete syntax of CHR with Prolog as the host language in the practical programming parts and mathematical abstract syntax in the formal Part II.

How CHR works

For programming, we recommend using a CHR implementation from K.U. Leuven, since they are currently the most recent and advanced. The CHR rules themselves will also be executable in other Prolog implementations of CHR and with minor modifications in K.U. Leuven JCHR, an implementation of CHR in Java and in the K.U. Leuven CHR library for C.

When we write a CHR program, we can mix host language statements and CHR code. The CHR-specific part of the program consists of declarations and rules.

Propositional rules

We start programming in CHR with rules that only involve propositions, i.e. constraints without arguments. Syntactically, constraints are similar to procedure calls.

Example 1.1.1 (Weather) Everybody talks about the weather, and we do as well.

Declarations. They introduce the CHR constraints we are going to define by the rules. They are specific to the implementation and the host language. Later in this book, we will usually skip the declarations and concentrate on the rules.

In this chapter, we introduce some simple, but concise and effective CHR programs. Often these programs consist just of one rule. We discuss basic properties of CHR programs which we introduce in an informal way. These properties are the anytime and online algorithm property, logical correctness, rule confluence, declarative concurrency, and worst-case time complexity. The programs in this section will be formally analyzed for these properties in Part III.

We will sometimes give longer examples of computations as a sequence of goals, one per line. We may underline the constraints involved in a rule application if it helps to understand the computation.

CHR as a database language

We can use CHR as an information store, as a simple deductive database, where database relations are modeled as CHR constraints which are maintained in the constraint store. Each database tuple corresponds to an instance of the constraint. The query contains (or generates) the tuples of the database as CHR constraints. Database queries, views, integrity constraints, and deductive database rules can be formulated as CHR propagation rules. This leads to the deduction of new and additional data constraints, i.e. tuples.

In this formal part of the book, we define the syntax and semantics of the CHR programming language. We will actually define several operational and several declarative semantics. We introduce guaranteed properties of CHR programs such as incrementality and concurrency. We then analyze CHR programs for desired properties such as termination and confluence.

Last but not least we show how to embed essential aspects of other rulebased and graph-based formalisms such as term rewriting, Petri nets, and constraint programming in CHR.

When we present theorems and the like, we will only give the proof idea, detailed proofs can be found in the respective research papers.

One advantage of a declarative programming language is the ease of formally sound program analysis. Properties like confluence and program equivalence have been investigated for CHR. These properties are decidable for terminating programs.

Since CHR is Turing-complete, termination is undecidable. Still, establishing termination for CHR programs can be straight forward, if simplification and propagation rules occur by themselves mainly.

Confluence means that it does not matter for the result which of the applicable rules are applied in a computation. The result will always be the same. Even if the computation itself is nondeterministic, in confluent programs, the relation between initial and final state, between query and answer, is a function and thus deterministic. For terminating CHR programs, there is a decidable, sufficient, and necessary test for confluence. Confluence implies consistency of the logical reading of the program. It improves the soundness and completeness results between the operational and declarative semantics. We have already discussed that confluent programs enjoy declarative concurrency and logical parallelism. So confluent programs can be run in parallel without change (cf. Section 4.3).

There is also a decidable, sufficient, and necessary test for operational equivalence of CHR programs. We do not know of any other programming language in practical use that admits such a test.

Unless otherwise noted, we use the very abstract semantics in this chapter to avoid clutter and technicalities of the abstract semantics. Not all results carry over to the refined semantics.

Real-world applications have to interact with their environment and be sufficiently fast for real-time computation, and thus concurrent, anytime, online algorithms are an asset.

A CHR program will automatically implement algorithms with these desirable properties due to the properties of its operational semantics. The anytime (approximation) algorithm property means that we can interrupt the execution of a program at any time, observe an approximation to the result and restart from that intermediate result. The online (incremental) algorithm property means that we can add additional constraints while the program is running without the need to recompute from scratch. Concurrency means that rules can be applied in parallel to separate (even certain overlapping) parts of a goal.

Unless otherwise noted, we use the very abstract semantics in this chapter to avoid clutter and technicalities of the abstract semantics.

The results in this chapter carry over to the refined operational semantics with some limitations only. In particular, programs written with the refined semantics in mind may give wrong results when executed in parallel. However, if a program has the confluence property (cf. Section 5.2), programs executing under the refined semantics basically also have the three properties (anytime, online, concurrent) discussed in this chapter.

Anytime approximation algorithm property

In an anytime algorithm we can interrupt the execution of a program at any time, observe an approximation to the result and continue from that intermediate result without the need to recompute from scratch. The intermediate results from successive interrupts better and better approximate the final result.