ITEM METADATA RECORD
Title: Scaling termination proofs by a characterization of cycles in CHR
Authors: Pilozzi, Paolo
De Schreye, Danny
Issue Date: Apr-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW541
Abstract: In the current paper, we discuss cycles in Constraint Handling Rules for the purpose of scaling termination proofs. In order to obtain a useful characterization, our approach differs from the ones used in other declarative languages, such as Logic Programming and Term Rewrite Systems. Due to multi-headed rules, the notion of a cycle is not in direct correspondence with the recursive calls of a program. Our characterization has to be more refined as we have to consider also partner constraints. Furthermore, a second, more challenging problem, due to the multi-set semantics of CHR, makes it unclear how cycles structurally compose. To tackle this problem, we develop a new abstraction for computations in CHR based on hypergraphs. On the basis of this abstraction, we define CHR constructs as a representation for sub-computations. These constructs introduce a concept of minimality and structural composability, making it is a useful abstraction. On the basis of this abstraction we define the meaning of a CHR cycle. These are special kinds of CHR constructs. We have developed a verification for detecting whether constructs are CHR cycles and for deriving the minimal CHR cycles of a program. We motivate why and how this will lead to scalable automated termination proof procedures for CHR.
URI: 
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW541.pdfDocument Published 384KbAdobe PDFView/Open

 


All items in Lirias are protected by copyright, with all rights reserved.