A compositional semantics for CHR

DOI10.1145/1462179.1462183MaRDI QIDQ2946569zbMATH OpenOpenAlexFDO

Authors Maurizio Gabbrielli, Maria Chiara Meo

Publication date 17 September 2015

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

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

zbMATH Keywords

semanticsConstraint Handling Rules

Mathematics Subject Classification ID

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

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.

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

Cited in

(20)

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

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)