Return to search

Detecting Non-Termination in Constraint Handling Rules

<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> / Thesis / Master of Science (MSc)

Identiferoai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/21268
Date24 September 2007
CreatorsRahimikia, Ershad
ContributorsKahl, Wolfram, Computing and Software
Source SetsMcMaster University
LanguageEnglish
Detected LanguageEnglish

Page generated in 0.0018 seconds