(Co-)inductive semantics for constraint handling rules

DOI10.1017/S1471068411000196zbMATH Open1218.68099arXiv1108.0330OpenAlexW3099263915MaRDI QIDQ3087447FDOQ3087447

Authors: Rémy Haemmerlé 

Publication date: 16 August 2011

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

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.

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

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

zbMATH Keywords

coinductionfixpointdeclarative semanticsCHRpersistent constraints

Mathematics Subject Classification ID

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

Cites Work

• A lattice-theoretical fixpoint theorem and its applications
• Title not available (Why is that?)
• A compositional semantics for CHR

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)