Detecting Non-Termination in Constraint Handling Rules

Abstract

<p> Constraint Handling Rules ( CHRs) are a high level language extension to introduce user-defined constraints into a host language. Application of CHRs to reformulate functional dependencies (FDs) in the Haskell type system gives us a more precise definition of this concept, and a better understanding of FD behavior. But to preserve the confluence and termination properties of CHRs generated from FDs, some restrictions on the syntax of FDs and type class definitions have been imposed which confines the expressiveness power of Haskell type system. </p> <p> In this thesis we use this problem as a motivation to find a solution for the confluence and non-termination problem in CHRs. We build a formal framework for CHRs and model their different aspects mathematically to study how non-confluence and non-termination happens. Based on this formalization we introduce prioritized CHRs as a solution for the confluence problem. To solve the non-termination problem, we propose a method to detect non-termination in the constraint solver. We define a repetition candidate as a special type of derivation and prove that a derivation having this property can cause non-terminating rule applications in the system. Finally we define a deduction tree structure for a set of rules that can be used to find all the possible repetition candidates for a set of constraint rules. </p>