Constraint Handling Rules - What Else?

TL;DR

Constraint Handling Rules (CHR) is a versatile, declarative programming language with a strong theoretical foundation, efficient execution, and powerful analysis tools, extensively applied since 2000.

Contribution

This paper provides an overview of CHR research and applications focusing on developments since 2000, highlighting its features and practical relevance.

Findings

CHR has a solid semantic foundation in logic.

It supports efficient sequential and parallel execution.

CHR offers powerful analysis methods for program properties.

Abstract

Constraint Handling Rules (CHR) is both an effective concurrent declarative constraint-based programming language and a versatile computational formalism. While conceptually simple, CHR is distinguished by a remarkable combination of desirable features: - semantic foundation in classical and linear logic, - effective and efficient sequential and parallel execution model - guaranteed properties like the anytime online algorithm properties - powerful analysis methods for deciding essential program properties. This overview of CHR research and applications is by no complete. It concentrates on the years since 2000. Up-to-date information on CHR can be found at the CHR web-site www.constraint-handling-rules.org, including the slides of the keynote talk associated with this article, an extensive bibliography, online demo versions and free downloads of the language.

Equations

$$H_1\backslash H_2\iff C|B$$

$$H_1\wedge H_2\wedge C\leftrightarrow H_1\wedge C\wedge B.$$

$$(H_1\wedge H_2\wedge C)⟼(H_1\wedge C\wedge B).$$

Full text

• •

a semantic foundation in classical and linear logic,

• •

an effective and efficient sequential and parallel execution model

• •

guaranteed properties like the anytime online algorithm properties

• •

powerful analysis methods for deciding essential program properties.

This overview of CHR research and applications is by no complete. It concentrates on the years since 2000. Up-to-date information on CHR can be found at the CHR web-site www.constraint-handling-rules.org, including the slides of the keynote talk associated with this article, online demo versions and free downloads of the language.

The final publication [56] is available at Springer via http://dx.doi.org/10.1007/978-3-319-21542-6_2.

1 Introduction

Constraint Handling Rules (CHR) [55] tries to bridge the gap between theory and practice, between logical specification and executable program by abstraction through constraints and the concepts of computational logic. CHR has its roots in constraint logic programming and concurrent constraint programming, but also integrates ideas from multiset transformation and rewriting systems as well as automated reasoning and theorem proving. It seamlessly blends multi-headed rewriting and concurrent constraint logic programming into a compact user-friendly rule-based programming language. CHR consists of guarded reactive rules that transform multisets of relations called constraints until no more change occurs. By the notion of constraint, CHR does not need to distinguish between data and operations, and its rules are both descriptive and executable.

In CHR, one distinguishes two main kinds of rules: Simplification rules replace constraints by simpler constraints while preserving logical equivalence, e.g., X$\leq$Y$\land$Y$\leq$X ${\;\Leftrightarrow\;}$ X$=$Y. Propagation rules add new constraints that are logically redundant but may cause further simplification, e.g., X$\leq$Y$\land$Y$\leq$Z ${\;\Rightarrow\;}$ X$\leq$Z. Together with X$\leq$X $\Leftrightarrow$ true, these rules encode the axioms of a partial order relation. The rules compute its transitive closure and replace inequalities $\leq$ by equalities $=$ whenever possible. For example, A$\leq$B$\land$B$\leq$C$\land$C$\leq$A becomes A$=$B$\land$B$=$C. More program examples can be found in Section 2. Semantics of CHR are discussed in Section 3.

1.1 Powerful Program Analysis

One advantage of a declarative programming language is the ease of program analysis. CHR programs have a number of desirable properties guaranteed and can be analyzed for others. They will be discussed in Section 4.

Since CHR (and many of its fragments) are Turing-complete, termination is undecidable, but often a ranking in the form a a well-founded termination order can be found to prove termination. From the ranking, a crude upper bound for the time complexity can automatically be derived. More precise bounds on the complexity can also be found by inspecting the rules.

Confluence of a program guarantees that any computation starting from the same initial state results in the same final state no matter which of the applicable rules are applied. There is a decidable, sufficient and necessary condition for confluence of terminating programs.

Any terminating and confluent CHR program has a consistent logical reading. It will automatically implement a concurrent any-time (approximation) and on-line (incremental) algorithm, where constraints can arrive during the computation that can be stopped and restarted at any time. It ensures that rules can be applied in parallel to different parts of a state without any modification and without harming correctness. This property is called declarative concurrency or logical parallelism.

Surprisingly, there is also a decidable, sufficient and necessary syntactic condition for operational equivalence of terminating and confluent programs (we do not know of any other programming language in practical use with this property). So one can check if two programs behave in the same way and if a program has redundant parts.

1.2 Implementations and Applications

CHR is often used as a language extension to other programming languages, its syntax can be easily adapted to that of the host language. In the host language, CHR constraints can be posted and inspected; in the CHR rules, host language statements can be included. CHR libraries are now available in almost all Prolog implementations, but also in Haskell, Curry, Java and C as well as in hardware.

It has been proven that every algorithm can be implemented in CHR with best known time and space complexity, something that is not known to be possible in other pure declarative programming languages. The efficiency of the language is empirically demonstrated by optimizing CHR compilers that compete well with both academic and commercial rule-based systems and even classical programming languages. The fastest implementations of CHR, e.g. in C, allow to apply up to millions of rules per second.

Other rule- and logic-based approaches have been successfully and rather straightforwardly embedded in CHR. For this reason, CHR is considered a candidate for a lingua franca of such approaches with the potential for cross-fertilization of research in computational systems and languages. Implementations and embeddings are discussed in Section 5.

CHR has been used for such diverse applications as type system design for Haskell, time tabling, optimal sender placement, computational linguistics, spatio-temporal reasoning, verification, semantic web reasoning, data mining and computational linguistics. Successful commercial application include financial services, network design, mould design, robot vehicle control, enterprise applications and software verification. Applications of CHR and research using CHR are discussed in Section 6.

CHR is also available online for demos and experimentation at chrjs.net at an introductory level and as WebCHR at chr.informatik.uni-ulm.de/~webchr/ with more than 50 example programs. More than 200 academic and industrial projects worldwide use CHR, and about 200 scientific books and 2000 research papers reference it. The CHR community and other interested researchers and practitioners gather at the yearly CHR workshops and the biannual CHR summer schools.

2 A Taste of CHR Programs

The following programs can be run with little modification in the online versions of CHR just mentioned. Note that all programs have the anytime online algorithm properties. So they can be stopped at any time for intermediate results, constraints can be added while they already run (incrementality), and they can be directly executed in parallel. These program examples are explained more in [54] and discussed in detail in [55].

Some examples use a third kind of rule, a hybrid rule called simpagation rule. It has the form $H_{1}\backslash H_{2}\Leftrightarrow C|B$. Basically, if $H_{1}$ and $H_{2}$ match constraints and the guard $C$ holds, then the constraints matching $H_{1}$ are kept, the constraints matching $H_{2}$ are removed and the body $C$ is added. For logical conjunction $\land$ we will simply write a comma between constraints.

Multiset Transformation - One-Rule Algorithms

Compute minimum of a set of min candidates min(I) \ min(J) $\Leftrightarrow$ J>I | true. Compare two numbers, keep smaller one.

Compute greatest common divisor of a set of numbers gcd(I) \ gcd(J) $\Leftrightarrow$ J>=I | gcd(J mod I). Replace I and J by I and (J mod I) until all numbers are the same.

Compute primes, given prime(2),...,prime(MaxN) prime(I) \ prime(J) $\Leftrightarrow$ J mod I = 0 | true. Keep removing multiples until only primes are left.

Sort array with elements a(Index,Value) a(I,V), a(J,W) $\Leftrightarrow$ I>J, V<W | a(I,W), a(J,V). Keep swapping numbers that are out of order until sorted.

Merge Sort, given values as next(start,Value) next(A,B) \ next(A,C) $\Leftrightarrow$ A<B,B<C | next(B,C). Turn common successors into direct successors until sorted chain results.

Newton’s Method for Square Root Approximation for N>1 eps(E) \ sqrt(X,R) $\Leftrightarrow$ R*R/X-1>E | sqrt(X,(R+X/R)/2). Start with sqrt(N,N). E is the required precision factor.

Fibonacci Variations

• M is the Nth Fibonacci number

Top-down Evaluation fib(0,M) $\Leftrightarrow$ M=1. fib(1,M) $\Leftrightarrow$ M=1. fib(N,M) $\Leftrightarrow$ N>=2 | fib(N-1,M1), fib(N-2,M2), M=M1+M2. Matching is used on left hand sides of rules.

Top-down Evaluation with Memorization (in first rule) fib(N,M1) \ fib(N,M2) $\Leftrightarrow$ M1=M2. fib(0,M) $\Rightarrow$ M=1. fib(1,M) $\Rightarrow$ M=1. fib(N,M) $\Rightarrow$ N>=2 | fib(N-1,M1), fib(N-2,M2), M=M1+M2. Turned simplification into propagation rules.

Bottom-up Evaluation without Termination fibstart $\Leftrightarrow$ fib(0,1), fib(1,1). fib(N1,M1), fib(N2,M2) $\Rightarrow$ N2=N1+1 | fib(N2+1,M1+M2). Basically, original simplification rules have been reversed.

Bottom-up Evaluation with Termination at Max fib(Max) $\Rightarrow$ fib(0,1), fib(1,1). fib(Max), fib(N1,M1), fib(N2,M2) $\Rightarrow$ Max>N1, N1=N2+1 | fib(N2+1,M1+M2). The auxiliary constraint fib(Max) is added. Computation stops when Max=N1.

All-Pair Shortest Paths

The distance from X to Y is D path(X,Y,D1) \ path(X,Y,D2) $\Leftrightarrow$ D1=<D2 | true. arc(X,Y,D) $\Rightarrow$ path(X,Y,D). arc(X,Y,D), path(Y,Z,Dn) $\Rightarrow$ path(X,Z,D+Dn). Compute all paths with propagation rules, keep smaller ones.

Dynamic Programming

• Bottom-up Parsing with CYK Algorithm

Grammar rules are in Chomsky normal form A->T or A->BC. A sequence of terminal symbols is encoded as a chain of arcs. parse(X,Y,A) \ parse(X,Y,A) $\Leftrightarrow$ true. terminal @ A->T, arc(X,Y,T) $\Rightarrow$ parse(X,Y,A). non-term @ A->BC, parse(X,Y,B), parse(Y,Z,C) $\Rightarrow$ parse(X,Z,A). Note the similarity with All-Pair Shortest Paths.

Boolean Conjunction as Constraint

The result of X$\land$Y is Z and(X,Y,Z) $\Leftrightarrow$ X=0 | Z=0. and(X,Y,Z) $\Leftrightarrow$ Y=0 | Z=0. and(X,Y,Z) $\Leftrightarrow$ X=1 | Z=Y. and(X,Y,Z) $\Leftrightarrow$ Y=1 | Z=X. and(X,Y,Z) $\Leftrightarrow$ X=Y | Y=Z. and(X,Y,Z) $\Leftrightarrow$ Z=1 | X=1,Y=1. Also computes with unknown input values and backwards. Such rules can be automatically generated from specifications [8].

3 CHR Semantics

In this section we give an overview of the main semantics for CHR. More detailed overviews can be found in [63, 19]. As a declarative programming language and formalism, CHR features both operational semantics that describe the execution of a program and declarative semantics that interpret a program as a logical theory. These semantics exist at various levels of refinement. They are related by soundness and completeness results, showing their correspondence.

3.1 CHR Rules and their Declarative Semantics

To simplify the presentation, we use a generic notation for all three kinds of CHR rules. Built-in constraints are host language statements that can be used as tests in the guard or auxiliary computations in the body of a rule. A generalized simpagation rule is of the form

[TABLE]

where in the rule head (left-hand-side), $H_{1}$ and $H_{2}$ are conjunctions of user-defined constraints, the optional guard $C$ is a conjunction of built-in constraints from the host language and the body (right-hand-side) $B$ is a conjunction of arbitrary constraints. If $H_{1}$ and $H_{2}$ are non-empty, the rule corresponds to a simpagation rule. If $H_{1}$ is empty, the rule corresponds to a simplification rule, if $H_{2}$ is empty, the rule corresponds to a propagation rule.

The declarative semantics is based on first-order predicate logic, where constraints are viewed as predicates and rules as logical implications and equivalences. A generalized simpagation rule basically corresponds to a logical equivalence

[TABLE]

An interesting refinement is the linear-logic semantics [19, 20]. It is closer to the operational semantics in that it captures the meaning of constraints as resources, where multiplicities matter.

3.2 Operational Semantics for CHR

The execution of CHR can be described by structural operational semantics, which are given as state transition systems. Basically, states are conjunctions of constraints. These semantics exist in various formulations and at various levels of refinement, going from the abstract (analytical) to the concrete (pragmatic):

• •

The very abstract semantics [55] is close to modus ponens of predicate logic.

• •

The abstract (or theoretical) semantics [5] is often used as a basis for program analysis.

• •

The refined semantics [43] describes the behavior of CHR implementations.

Several alternative operational semantics for CHR have also been proposed, among them [67, 79, 107, 21].

The essential aspect of the operational semantics is the application of a rule: Take a generalized simpagation rule from the program. If there are constraints in the current state that match the head of the rule and if the guard holds under this matching, then the constraints matching second part of the head $H_{2}$ (if any) are removed and the guard and body of the rule are added to the state.

There are alternative formulations for the above semantics. Chapter 8 in the book [63] and [102, 19] develop an axiomatic notion of state equivalence. The equivalence relation $\equiv$ on states treats built-in constraints semantically and user-defined constraints syntactically. Basically, two states are equivalent if they are logically equivalent while taking into account that - forming multisets - multiplicities of user-defined constraints matter. For example, $X{=<}Y\land Y{=<}X\land c(X,Y)\ \equiv\ X{=}Y\land c(X,X)$ which is different to $X{=}Y\land c(X,X)\land c(X,X)$.

Using state equivalence, the presentation of the abstract semantics can be simplified. It basically boils down to

$\underline{S\equiv(H_{1}\land H_{2}\land C\land G)\ \ \ \ (H_{1}\backslash H_{2}\Leftrightarrow C|B)\ \ \ \ (H_{1}\land C\land B\land G)\equiv T}$

$S\longmapsto T$

where all upper-case letters stand for conjunctions of constraints. $G$ is called the context of the rule application, $G$ is not affected by it. Note that the transition $S\longmapsto T$ is only allowed if the built-in constraints in state $S$ are consistent and if the rule has not been applied before to the same constraints under the same matching.

3.3 Operational Semantics for Parallel CHR

One of the main features of CHR is its inherent concurrency. Intuitively, in a parallel execution of CHR we can apply rules simultaneously to different parts of a state. But we can do more than that: We can also apply rules to overlapping parts of a state as long as the overlap is only removed by at most one rule. In Chapter 4 of [55], this parallelism in CHR is defined by an interleaving semantics as

$\underline{A\land G\longmapsto C\land G\ \ \ \ \ \ B\land G\longmapsto D\land G}$

$A\land B\land G\longmapsto C\land D\land G$

This inference rule is justified by the monotonicity property of CHR (explained below). If a program executed under the refined semantics makes use of the order of constraints in a state and the order of rules in a program, this kind of automatic parallelization may not work. Such programs are not confluent. On the other hand, confluent programs can be executed in parallel without modification. As we will see, we can check CHR programs for confluence, and we can even semi-automatically complete them to make them confluent. Thus, using completion, we can turn non-confluent programs into parallel programs. This method has been applied to the classical Union-Find algorithm which is very hard to parallelize [51] (with [129] showing the effectiveness of the resulting program) and to the Preflow-Push algorithm [93]. Alternative and more refined semantics for parallel CHR are e.g. [86, 114, 87, 104, 63].

4 Properties of CHR and Their Analysis

We first introduce three essential types of monotonicity and the anytime online algorithm properties that all come for free in CHR. We then discuss the analysis of termination and time complexity as well as of confluence, completion and operational equivalence of CHR programs.

4.1 CHR Monotonicity Properties

In the abstract operational semantics we can observe three essential types of monotonicity.

First, adding rules to a program cannot inhibit the applicability of any rules that were applicable. This aids incremental program development and rapid prototyping. Already a program with a few first rules is executable, and we can add rules to cover more and more cases, enabling more and more desired computations. The confluence test (see next Section) can be used to discover situations where old and new rules lead to different results.

Second, built-in constraints (that occur in the guard and body of a rule) can only be added to a state, they are never removed. Hence they accumulate monotonically. On the other hand, user-defined constraints are non-monotonic in that they can be added and removed from a state. This means that an applicable rule will remain applicable as long as the user-defined constraints it matches are present in the state and as long as the state is consistent.

Third, during a rule application, the context $G$ stays unchanged. We can actually change it without influencing the rule application itself. So if a rule is applicable in a state, it is also applicable in any larger state where constraints have been added (as long as the state is consistent) [5]. This is an important modularity property of CHR, it is usually called CHR’s monotonicity property. Clearly such context-independence does not hold in traditional programming languages, where the context may update as well, resulting in write conflicts.

On the other hand, if we have an empty context $G$, we get the minimal transition for to the given rule:

[TABLE]

The state $(H_{1}\land H_{2}\land C)$ is called minimal state of the rule. Removing any constraint from it would make its rule inapplicable. Adding constraints to it cannot inhibit the applicability due to monotonicity. Since minimal states and transitions capture the essence of a rule application, they will come handy later when analyzing CHR programs for confluence and operational equivalence.

4.2 Anytime Online Algorithm Properties

Any algorithm expressed properly as a CHR program will enjoy several important properties: It will be an anytime algorithm and it will be an online algorithm and it can be run in parallel without modification.

The anytime (approximation) algorithm property means that we can interrupt the execution of a program at any time, observe the current state as an approximation to the result and restart from that intermediate result. This is obvious from the operational semantics and the notion of states and transitions used there.

The online (incremental) algorithm property means that we can add additional constraints while the program is running without the need to recompute from scratch. This is an immediate consequence of the monotonicity property of CHR. The program will behave as if the newly added constraints were present from the beginning but had been ignored so far. Therefore only a minimal amount of computation is performed to accommodate the new constraint. Incrementality is useful for interactive, reactive and control systems, in particular for agent and constraint programming.

In the refined semantics, the order of constraints in a state and the order of rules in a program can be made to matter, and this may weaken the above properties.

4.3 Termination and Time Complexity Analysis

One way to show termination is to prove that in each rule, if the guard holds, the rule head is strictly larger than the rule body using some well-founded termination order called a ranking. For CHR programs that mainly use simplification rules, simple rankings are often sufficient to prove termination [48, 49]. More sophisticated methods are needed in the presence of propagation rules [97, 98, 57]. An approximation of CHR programs by constraint logic programs (CLP) has also been used to analyse the termination behavior of CHR [81].

The run-time of a CHR program not only depends on the number of rule applications (derivation lengths), but also on the number of rule application attempts. The meta-complexity theorem in [50] basically states that the complexity is bounded by the derivation length taken to the power of the number of heads in a rule. This only gives crude upper-bounds.

Actual CHR systems achieve much better complexity results since they implement the refined semantics and feature compiler optimizations such as indexing. For CHR with and without priorities, there is a more realistic sophisticated meta-complexity result derived from the Logical Algorithms (LA) formalism [33].

4.4 Confluence and Completion

Confluence means that it does not matter for the result which of the applicable rules are applied in which order in a computation. The resulting states will always be equivalent to each other. For terminating CHR programs, there is a decidable, sufficient and necessary condition for confluence [5]. These papers also have shown the many benefits of confluent programs:

• •

Confluent programs are always implement anytime online algorithms.

• •

Confluent programs can be run in parallel without modification.

• •

Confluence implies consistency of the logical reading of the program.

• •

Confluence improves the soundness and completeness results between the operational and declarative semantics. These theorems are stronger than those for other (concurrent) constraint programming languages.

• •

The least models of confluent CHR programs and its CLP approximation coincide [81].

The idea of the confluence test is to construct a finite number of so-called critical states by overlapping minimal states of rules in the program. An overlap equates some user-defined constraints and removes the resulting duplicate occurrences. If these constraints are to be removed by more than one rule, we have generated a conflict. One now checks if these conflicting rule applications on its own can be continued with computations that lead to equivalent states. If this holds for all critical states in the program, we have proven confluence.

In practice, this notion of confluence can be too strict. In [44] the notion of observable confluence is introduced, where the states considered must satisfy a user-defined invariant. Other related notions of confluence are considered in [80, 31]. Confluence for non-terminating programs is in general undecidable, it is discussed in [105].

Completion is the process of adding rules to a non-confluent program until it becomes confluent [2]. These rules are generated between the successor states of critical states. In contrast to completion for term rewriting, in CHR we generally need more than one rule to make a critical pair joinable: a simplification rule and a propagation rule. Unfortunately, completion may not terminate. Completion can be also used for program specialisation [4, 2].

4.5 Operational equivalence

Operational equivalence means that given two programs, for any given state, its computations in both programs lead to the same final state. There is a decidable, sufficient and necessary condition for operational equivalence of terminating and confluent CHR programs [3]. We do not know of any other programming language in practical use that admits such a test.

The test is straightforward: The minimal states of the rules in both programs are each executed in both programs, and for each minimal state, the computations must reach equivalent states in both programs. This test can also be used to discover redundant rules in a program.

5 CHR Implementations and Embeddings in CHR

We discuss efficient implementations, variants and extensions of CHR and embeddings of other rule- and graph-based approaches in CHR.

5.1 CHR Implementations and Their Efficiency

The first wide-spread implementations of CHR were based on [83]. Most available CHR implementations today - be it in Prolog, Java or C - are based on the expertise of the CHR team at Katholieke Universiteit Leuven [137, 134, 130].

State-of-the-art CHR libraries with mode and type declarations in Prolog and C allow to implement any algorithm in a natural and high-level way, with time and space consumption that is typically within an order of magnitude from the best-known implementations in any other language [121, 131]. Indeed, [121] has proven that every algorithm can be implemented in CHR with the best known time and space complexity. This has been exemplified by providing elegant implementations with optimal time-complexity of the classical union-find algorithm [112] and Fibonacci heaps [120]. CHR is the only known declarative language where this results holds, it is unlikely to hold for other declarative languages like Prolog or Haskell [121]. Actually, CHR cannot be embedded in pure Prolog [65]. The fastest CHR implementations in CCHR [137] and hProlog allow to up to apply millions of rules per second.

One reason for the effectiveness of CHR is that it uses a compiler and run-time system that is a significant advancement over existing algorithms (such as RETE, TREAT, LEAPS) for executing rule-based languages as has been impressingly demonstrated in [131]. In addition to a superior rule-application mechanism, CHR compilers use sophisticated optimizations (besides indexing on constraint arguments taking into account mode and type information), such as memory reuse, late storage, guard optimization and join ordering optimization [84, 131, 63].

CLIPS (in C) and JESS (in Java)) are considered by many to be the most efficient rule-based systems available. The benchmarks of [131] show that his novel Java implementation of CHR as well as CHR in C (CCHR) [137] are faster than CLIPS and JESS, sometimes by several orders of magnitude. In benchmarks of [121], CHR with mode declarations achieves the optimal time and space complexity (as do imperative languages). Prolog and strict Haskell have a time complexity which is a polylogarithmic factor from optimal, and their space complexity is not optimal. Lazy Haskell quickly gets into memory problems.

As for concurrency, prototype parallel CHR implementations exist in software using Haskell [86] and in hardware using Nvidia CUDA by transforming a subset of CHR to C++ [138] and using FPGA’s [129]. These papers feature experiments that show a potential for optimal linear speedup by parallelization of CHR programs (and super-linear speed-up e.g. in the case of the greatest-common-divisor program).

5.2 CHR Language Variants and Extensions

We start with a remark on fragments of CHR, indicating the adequacy of the overall language. We then discuss language extensions for CHR, program transformation and new programming languages based on CHR.

While there are many Turing-complete language subsets of CHR [116, 66, 92] (a single multi-headed simplification rule suffices), it has also been shown in [37, 65] that each of the following features of CHR can be considered essential, since they increase the expressive power of CHR: constraints with arguments, built-in constraints, function symbols to build complex terms, multi-headed rules, introduction of new variables in the body of a rule.

Since CHR libraries in Prolog naturally allow to use backtracking search by Prolog’s disjunction, most operational semantics can be extended to the resulting language CHR∨ [10]. In [34] the authors extend the refined operational semantics of CHR to support the implementation of different search strategies.

In adaptive CHR, constraints can be declaratively removed together with the consequences they produced by getting involved in rule applications. This means that any properly written algorithm becomes adaptive. An adaptive semantics is defined in [136]. Adaptive CHR is used for realizing intelligent search strategies in [135, 136].

In [35] the authors extend CHR with user-defined rule priorities that can be static or dynamic. This language extension reduces the level of non-determinism that is inherent to the abstract operational semantics of CHR, and gives a more high-level form of execution control compared to the refined operational semantics. Priorities make CHR more expressive.

Other notable extensions of CHR include non-monotonic negation-as-absence [133], aggregates such as sum, count, findall, and min [122], rules with probabilities [61, 29, 119], Except for search, all above CHR extensions have been implemented by simple effective source-to-source program transformation in CHR itself, also see Chapter 6 in [55] and the online transformation tool at http://pmx.informatik.uni-ulm.de/chr/stssemantics/. Program transformation in itself has been studied in [62, 1]. Partial evaluation is covered by [52], discussing specialisation of CHR rules, and by [68], which is concerned with unfolding of CHR rules. Confluence completion can be used to great effect for program specialisation [4, 2].

Notable new programming languages that are based on CHR are:

• •

HYPROLOG [30] as an extension of Prolog with assumptions and abduction.

• •

DatalogLB adds features of CHR to Datalog [78].

• •

CHRISM is CHR with probabilistic reasoning and statistical learning [119].

• •

CADMIUM is an implementation of ACD Term Rewriting, a generalization of CHR and Term Rewriting (TRS) [42].

• •

SMCHR is an implementation of Satisfiability Modulo Theories (SMT) [39], where the theory part can be implemented in CHR.

• •

Linear Meld (LM) is a linear logic language closely related to CHR [32].

• •

CoMingle is CHR for distributed logic programming (on Android) [88].

5.3 Embedding Other Formalisms and Languages in CHR

The expressiveness, effectiveness and efficiency of CHR enables the embedding of the characteristic features of other rule-based and graph-based formalisms, systems and languages in CHR by simple source-to-source transformations:

• •

Prolog and Constraint Logic Programming (CLP) programs are translated into CHR∨ in [10] using Clark’s completion.

• •

Logical Algorithms (LA) are mapped into CHR with and without rule priorities in [85]. This are the only known implementations of LA. They achieve the tight time complexity required for the LA meta-complexity theorem to hold.

• •

Term Rewriting Systems (TRS) are translated to rules with equational constraints in CHR in [103].

• •

Graph Transformation Systems (GTS) are encoded in CHR in [100]. Soundness and completeness of the encoding is proven. GTS joinability of critical pairs can be mapped onto joinability of specific critical pairs in CHR.

• •

Petri Nets are translated to CHR in [18]. It is proven that there is a one-to-one correspondence between Colored Petri Nets and positive ground range-restricted CHR simplification rules over finite domains.

Chapter 6 and 9.3 of [55] and the CHR web-page also describe these embeddings:

• •

Production Rules and Business Rules,

• •

Event-Condition-Action (ECA) Rules,

• •

Functional Programming,

• •

General Abstract Model for Multiset Manipulation (GAMMA),

• •

Deductive databases languages like DATALOG,

• •

Description logic (DL) with OWL- and SWRL-style rules,

• •

Concurrent Constraint Programming (CC) language framework.

The online tool http://pmx.informatik.uni-ulm.de/chr/translator supports the basic translation for some of these embeddings: term rewriting systems, functional programming, multiset transformation, production rules with negation-as-absence.

The embeddings are quite useful for comparing and for cross-fertilization between different approaches. For example, in the CHR embedding, the close relationship between colored Petri Nets and the GAMMA chemical abstract machine (CHAM) can be immediately seen. On the other hand, it seems difficult to come up with an embedding of full CHR in one of the afore-mentioned formalisms. Basically, other approaches either lack the notion of constraints and logical variables or they lack multi-headed rules and propagation rules. Given these embeddings and its power in general, CHR can be considered a candidate for a lingua franca for computational systems with the potential for cross-fertilization of research.

6 CHR in Research and Applications

Typical research applications of CHR can be found in areas of computational linguistics, constraint solving, cognitive systems, spatio-temporal reasoning, agent-based systems, bio-informatics, semantic web, type systems, verification and testing and many more.

Commercial applications include financial services in stockbroking (SecuritEase, New Zealand), vehicle control by robotic brains (Cognitive Systems, Spain), injection mould design (Cornerstone Intelligent Software Corp, Canada), optical network design (Mitre, USA), enterprise applications (LogicBlox, USA), and software verification (BSSE, Germany). See Section 7 in [123] for details.

6.1 Language Design and Algorithm Design

One of the most successful research applications of CHR is in the design, prototyping and analysis of advanced type systems for the functional programming language Haskell [126, 125, 40]. Type reconstruction with CHR is performed for functional and logic programs in [110]. A flow-based approach for a variant of parametric polymorphism in Java is based on CHR in [27].

The union-find algorithm can be seen as solving simple equations between variables or constants. By choosing the appropriate equational relations, one can derive fast incremental algorithms for solving certain propositional logic (SAT) problems and polynomial equations in two variables [53]. Almost-linear tree equation solving algorithms are reconstructed with CHR in [94]. Parallelizing classical algorithms is discussed for Union-Find using confluence analysis [51] and for Preflow-Push [93].

6.2 Software Verification and Testing

The authors of [74, 75] present a new method for automatic test data generation (ATDG) applying to semantically annotated control-flow graphs (CFGs), covering both ATDG based on source code and assembly or virtual machine code. The method supports a generic set of test coverage criteria, including all structural coverage criteria currently in use in industrial software test for safety critical software. The work [11] gives test cases a denotational semantics by viewing them as specification predicates. The authors develop a testing theory and implementation for fault-based mutation testing.

Other applications of CHR in testing include [99, 77, 108, 36]. An an effective methodology for verifying properties of imperative programs is their transformation to constraint-based programs [41, 12, 96]. Somewhat related is lightweight string reasoning for OCL [25].

6.3 Constraints Solving and Reasoning

CHR was originally designed to write or even automatically generate constraint solvers [7, 8, 124, 101]. Solvers written in CHR and applications of CHR in constraint reasoning can be found in [59] and further references in [47, 123, 63]. For example, CHR-based spatio-temporal reasoning is applied to robot path planning in [45, 90]. In the soft constraints framework [22, 24, 23], constraints and partial assignments are given preference or importance levels, and constraints are combined according to combinators which express the desired optimization criteria.

The goal of argumentation-based legal reasoning [118] is to determine the chance of winning a court case, given the probabilities of the judge accepting certain claimed facts and legal rules. In computer linguistics, CHR Grammars (CHRG) [28] execute as robust bottom-up parsers with an inherent treatment of ambiguity. Computational Cognitive Modeling is a research field at the interface of computer science and psychology. It enables researchers to build detailed cognitive models using a cognitive architecture. A popular cognitive architecture, ACT-R, has been implemented in CHR and given a proper formal semantics for the first time [69, 70].

6.4 Multi-Agent Systems and Abduction

The agent-based system FLUX is implemented in CHR [127, 128]. Its application FLUXPLAYER [109] won the General Game Playing competition at the AAAI conference in 2006. SCIFF is a framework to specify and verify interaction in open agent societies [13, 15]. The SCIFF language is equipped with a semantics based on abductive logic programming. Other applications in multi-agent systems and abductive reasoning are for example [115, 14, 95, 72]. HYPROLOG [30] extends Prolog with CHR rules for assumptions, abduction and integrity constraints. Probabilistic Abductive Logic Programs (PALPs) are introduced and and implemented in CHR for solving abductive problems providing minimal explanations together with their probabilities [29].

6.5 Semantic Web

In Chapter 9.3. of [55] a straightforward and effective implementation of description logic with OWL- and SWRL-style rules in CHR is given. For the Semantic Web, the integration and combination of data from different information sources is an important issue that can be handled with CHR [16, 139]. In [17] a composition and verification framework for Semantic Web Services specified using WSSL is proposed, a novel service specification language based on the fluent calculus, that addresses issues related to the frame, ramification and qualification problems. An earlier paper on web service composition using fluent calculus is [106]. The paper [26] proposes a service modeling approach consisting of service contracts and a process model. Service contracts are used as service advertisement and service request in this approach. The Cuypers Multimedia Transformation Engine [76] supports the automatic generation of Web-based presentations adapted to the user’s needs.

6.6 The Diversity of CHR Applications

Scheduling and timetabling are popular constraint-based applications, and this also holds for CHR implementation of course scheduling and room planning for the University of Munich [6, 9], which has become an often-cited standard work in the area.

The tool Popular [60] uses a path-loss model to describe radio-wave transmission and constraint-based programming to optimize the placement of base stations (transmitters) for local wireless communication at company sites.

The Munich Rent Advisor [58] allows the calculation of the estimated fair rent for a flat based on statistical data using an online form. Simply by translating the calculation scheme into CHR-based arithmetic interval constraints, the functionality is significantly extended: The user need not answer all questions, and so an interval range for the possible rent is returned.

The papers [117, 73] present a new system for automatic music generation, in which music is modeled using very high level probabilistic rules in CHRISM [119]. The probabilistic parameters can be learned from examples, resulting in a system for personalized music generation.

The authors of [89] present an algorithm for long-term routing of autonomous sailboats. It is based on the A*-algorithm and incorporates changing weather conditions by dynamically adapting the underlying routing graph. The software also takes individual parameters of the sailboat into account, and proved to be faster than commercial systems. The system was successfully put to test during an attempt to break the world record in long-distance robot sailing with the ASV RoBoat of INNOC (Vienna).