Towards a constraint solver for proving confluence with invariant and equivalence of realistic CHR programs

TL;DR

This paper develops a practical constraint solver to prove confluence with invariants and equivalence in realistic CHR programs, enabling more reliable and optimized logic programming implementations.

Contribution

It introduces a meta-level constraint language for expressing invariants and equivalences, extending previous theoretical results towards practical confluence proofs in CHR.

Findings

A semantics compatible with standard Prolog implementations

A constraint solver for confluence with invariants and equivalence

Extension of theoretical results towards practical verification

Abstract

Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated, extending our previous theoretical results towards a practical implementation.