On proving confluence modulo equivalence for Constraint Handling Rules

DOI10.1007/S00165-016-0396-9zbMATH Open1355.68050arXiv1611.03628OpenAlexW3099526688WikidataQ125525925 ScholiaQ125525925MaRDI QIDQ511019FDOQ511019

Henning Christiansen, Maja H. Kirkeby

Publication date: 14 February 2017

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Abstract: Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var/1 and incomplete ones such as is/2, that are ignored in previous work on confluence. To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR. For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.

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

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Biological Sequence Analysis
• Error bounds for convolutional codes and an asymptotically optimum decoding algorithm
• On theories with a combinatorial definition of 'equivalence'
• Term Rewriting and All That
• Worst-case Analysis of Set Union Algorithms
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A complete and terminating execution model for Constraint Handling Rules
• Theory and practice of constraint handling rules
• Logic Programming
• Higher-order rewrite systems and their confluence
• Constraint Handling Rules. Current research topics
• Confluence and semantics of constraint simplification rules
• A declarative approach for first-order built-in's of Prolog
• Confluence in concurrent constraint programming
• Confluence Modulo Equivalence in Constraint Handling Rules
• As time goes by: Constraint Handling Rules
• Observable Confluence for Constraint Handling Rules
• Constraint Handling Rules
• Testing for the Church-Rosser Property
• Uniform confluence in concurrent computation
• Diagrammatic confluence for Constraint Handling Rules
• A confluent relational calculus for higher-order programming with constraints
• CHR grammars
• Logic Based Program Synthesis and Transformation

Cited In (1)

• Confluence and convergence modulo equivalence in probabilistically terminating reduction systems

This page was built for publication: On proving confluence modulo equivalence for Constraint Handling Rules

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