A compositional semantics for CHR

DOI10.1145/1462179.1462183zbMATH Open1351.68050arXivcs/0603079OpenAlexW2045796613MaRDI QIDQ2946569FDOQ2946569

Authors: Maurizio Gabbrielli, Maria Chiara Meo 

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached. CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far. In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.

Full work available at URL: https://arxiv.org/abs/cs/0603079

Recommendations

• A Compositional Semantics for CHR with Propagation Rules
• Theory and practice of constraint handling rules
• On the expressive power of multiple heads in CHR
• Logic Programming
• Constraint solving with constraint handling rules

zbMATH Keywords

semanticsConstraint Handling Rules

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Cited In (20)

• A Compositional Semantics for CHR with Propagation Rules
• As time goes by: constraint handling rules
• Linear-logic based analysis of Constraint Handling Rules with disjunction
• SMCHR: satisfiability modulo constraint handling rules
• A complete and terminating execution model for constraint handling rules
• On the expressive power of multiple heads in CHR
• On the number of rule applications in constraint programs
• Formal Modeling and Analysis of Timed Systems
• Transactions in Constraint Handling Rules
• Observable Confluence for Constraint Handling Rules
• Complexity of a CHR Solver for Existentially Quantified Conjunctions of Equations over Trees
• Expressiveness of Multiple Heads in CHR
• A Linear-Logic Semantics for Constraint Handling Rules
• Logic Programming
• Constraint solving with constraint handling rules
• Logical Algorithms meets CHR: A meta-complexity result for Constraint Handling Rules with rule priorities
• CHR grammars
• (Co-)inductive semantics for constraint handling rules
• Guard Reasoning in the Refined Operational Semantics of CHR
• CHR in action

This page was built for publication: A compositional semantics for CHR

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946569)