Graph transformation systems in Constraint Handling Rules: improved methods for program analysis

Abstract

Constraint Handling Rules (CHR) is a rule- and logic-based formalism and has established itself as an active research topic. In contrast to other rule-based approaches, CHR is both, a theoretical formalism related to first-order and linear-logic, and a practical rule-based programming language. Other rule- and logic-based approaches have been successfully embedded in CHR. For this reason, it is considered a candidate for a lingua-franca of such approaches. We investigate CHR´s suitability for this purpose exemplarily, by considering an embedding of graph transformation systems (GTSs) in CHR, which helps us in identifying points of improvements for strengthening the lingua-franca argument further. In particular, we present a novel formulation of the operational semantics of CHR, which is founded on an equivalence relation over CHR states. It justifies the perspective on CHR as a rule-based rewriting system of equivalence classes, which abstracts over infinitely many possible syntactic variations of a CHR state. Overall, this equivalence-based operational semantics provides a powerful formal analysis tool for CHR, which can significantly reduce proof complexity. The lingua-franca argument implies a potential for cross-fertilization of research. Hence, we revisit program analysis methods available in the CHR literature. Our extended methods apply an invariant to make implicit assumptions explicitly available during analysis, hence, effectively eliminating irrelevant states. The resulting methods are applicable to strictly larger classes of CHR programs and provide more promising approaches towards analyzing more complex programs. Finally, we compare program analysis methods in GTSs and CHR. We find that the adapted CHR confluence test, when applied to a GTS embedded in CHR, corresponds to a sufficient criterion for confluence of the GTS. Similarly, we introduce program equivalence for GTSs with a sufficient criterion based on the CHR program equivalence test.