A unified analytical foundation for constraint handling rules
Hariolf Betz · OPen Access Repositorium der Universität Ulm (OPARU) (Ulm University) · 2013
The non-deterministic rule-based programming language of Constraint Handling Rules (CHR) features a remarkable combination of desirable properties: a foundation in classical logic, powerful analysis methods for deciding program properties - especially confluence - and an efficient execution model. Upon a closer look, we observe several limitations to this asset. (1) The traditional theoretical formulation of the operational semantics makes program analysis unnecessarily complicated. (2) Diverging branches of research weaken the applicability of theoretical analysis results to program behavior in a concrete implementation. (3) The foundation on classical logic is of limited use as the relationship between CHR and classical logic is too weak for significant reasoning on program behavior. In this thesis, we introduce several concepts to amend for these shortcomings. Firstly, we propose an unusually concise formulation of the two most important semantic interpretations of CHR. We achieve this by providing a well-motivated notion of state equivalence for each of these interpretations. Secondly, we analyse the relationship between the major diverging interpretations of CHR. Our analysis leads to a novel well-behavedness property that restores the applicability of many theoretical analysis methods to implementation-oriented interpretations of CHR. Finally, we found CHR on intuitionistic linear logic. We show that this substructural logical formalism is substantially better-suited than classical logic to express the operational behavior of CHR. Our non-classical logical foundation entails novel analysis methods for program behavior.