CHR
| Designed by | Thom Frühwirth |
|---|---|
| Appeared in | 1991 |
| Computational class | Turing-complete |
| Reference implementation | defunct |
| Influenced by | Prolog |
| Influenced | Zaddy |
Constraint Handling Rules or CHR is a domain-specific guest language for declaring and managing constraints. Unlike many other languages, CHR is not a standalone language, but is intended to embed into a host language or wrap around host modules. That is, while CHR is not a language on its own, there exist languages like CHR(Prolog), CHR(Java), CHR(C), CHR(Haskell), and CHR(ECMAScript).[1][2]
Abstractly, CHR does constraint rewriting over a multiset of asserted constraints. One form of constraint rewriting is simplification, such as transforming an if-and-only-if into two implications, one in each direction. Simplification eliminates the starting constraints. Another form of constraint rewriting is propagation. Given two implications A=>B and B=>C, one can deduce A=>C. Propagation does not eliminate the starting constraints. So called "simpagation" combines these two paradigms, eliminating some but not all of the starting constraints.
Operationally, CHR stores a database containing all of the constraints which have been asserted. Every time the database is modified, CHR invokes all rules to non-deterministically match zero or more rows of the database. Each rule can then delete some or all of its matched rows and generate zero or more new rows, as well as abort and rollback the current database transaction.
When embedded into relational languages like Prolog, CHR provides multiset semantics; a constraint can be asserted and discharged multiple times. When wrapping imperative languages like C or Java, CHR provides backtracking and choice operators. When wrapping actor languages, CHR provides a tuple space and transactions.
Example
The hello-world of CHR is a wikipedia:partial order over some concrete objects. In addition to the three standard axioms, the rule idempotence gives set semantics to implies by removing duplicates.
reflexivity @ implies(X, X) <=> true. antisymmetry @ implies(X, Y), implies(Y, X) <=> X = Y. transitivity @ implies(X, Y), implies(Y, Z) ==> implies(X, Z). idempotence @ implies(X, Y) \ implies(X, Y) <=> true.
The following CHR(Prolog) rules implement a standard optimized union-find data structure.[3]
make @ make(A) <=> root(A, 0). union @ union(A, B) <=> find(A, X), find(B, Y), link(X, Y). findNode @ A ~> B, find(A, X) <=> find(B, X), A ~> X. findRoot @ root(A, _) \ find(A, X) <=> X = A. linkEq @ link(A, A) <=> true. linkLeft @ link(A, B), root(A, N), root(B, M) <=> N >= M | B ~> A, N1 is max(N, M + 1), root(A, N1). linkRight @ link(B, A), root(A, N), root(B, M) <=> N >= M | B ~> A, N1 is max(N, M + 1), root(A, N1).
External resources
- wikipedia:Constraint Handling Rules
- Documentation of SWI-Prolog's implementation of CHR(Prolog)
- CCHR, an implementation of CHR(C)
- JCHR, an implementation of CHR(Java)
References
- ↑ Sneyers, Jon & Weert, Peter & Schrijvers, Tom & Koninck, Leslie. (2010). As time goes by: Constraint Handling Rules - A survey of CHR research from 1998 to 2007. Theory and Practice of Logic Programming. 10. 1. https://dtai-static.cs.kuleuven.be/CHR/papers/draft_chr_survey.pdf https://arxiv.org/abs/0906.4474
- ↑ Nogatz, F., Frühwirth, T., Seipel, D. (2018). CHR.js: A CHR Implementation in JavaScript. In: Benzmüller, C., Ricca, F., Parent, X., Roman, D. (eds) Rules and Reasoning. RuleML+RR 2018. Lecture Notes in Computer Science(), vol 11092. Springer, Cham. https://doi.org/10.1007/978-3-319-99906-7_9
- ↑ Schrijvers, Tom and Thom W. Frühwirth. “Implementing and Analysing Union-Find in CHR.” (2004). https://www.cs.kuleuven.be/publicaties/rapporten/cw/CW389.pdf