Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. CHR has received considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multiheaded 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 article 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. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory—Semantics; D.3.3 [Programming Languages]: Language Constructs and Features— Constraints General Terms: Languages, Theory Additional Key Words and Phrases: Semantics
A compositional Semantics for CHR
MEO, MARIA CHIARA
2009-01-01
Abstract
Constraint Handling Rules (CHR) is a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. CHR has received considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multiheaded 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 article 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. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory—Semantics; D.3.3 [Programming Languages]: Language Constructs and Features— Constraints General Terms: Languages, Theory Additional Key Words and Phrases: SemanticsI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
