(Co-)inductive semantics for constraint handling rules

DOI10.1017/S1471068411000196MaRDI QIDQ3087447zbMATH OpenOpenAlexFDO

Authors Rémy Haemmerlé

Publication date 16 August 2011

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

coinductionfixpointdeclarative semanticsCHRpersistent constraints

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55)

Abstract: In this paper, we address the problem of defining a fixpoint semantics for Constraint Handling Rules (CHR) that captures the behavior of both simplification and propagation rules in a sound and complete way with respect to their declarative semantics. Firstly, we show that the logical reading of states with respect to a set of simplification rules can be characterized by a least fixpoint over the transition system generated by the abstract operational semantics of CHR. Similarly, we demonstrate that the logical reading of states with respect to a set of propagation rules can be characterized by a greatest fixpoint. Then, in order to take advantage of both types of rules without losing fixpoint characterization, we present an operational semantics with persistent. We finally establish that this semantics can be characterized by two nested fixpoints, and we show the resulting language is an elegant framework to program using coinductive reasoning.

Recommendations

• A compositional semantics for CHR
• A Compositional Semantics for CHR with Propagation Rules
• A Linear-Logic Semantics for Constraint Handling Rules
• A Unified Semantics for Constraint Handling Rules in Transaction Logic
• Coinductive constraint logic programming

Cites work

• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• A compositional semantics for CHR
• A lattice-theoretical fixpoint theorem and its applications

Cited in

(2)

• A Compositional Semantics for CHR with Propagation Rules
• A Unified Semantics for Constraint Handling Rules in Transaction Logic

This page was built for publication: (Co-)inductive semantics for constraint handling rules

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