Unfolding for CHR programs

DOI10.1017/S1471068413000288MaRDI QIDQ4592981zbMATH OpenFDO

Authors Maurizio Gabbrielli, Maria Chiara Meo, Paolo Tacchella, Herbert Wiklicky

Publication date 9 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1307.0679

zbMATH Keywords

unfoldingconfluenceterminationprogram transformationCHR (constraint handling rules)

Mathematics Subject Classification ID

Logic programming (68N17)

Abstract: Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations which is used by most program transformation systems and which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. This paper defines an unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning. We also prove that, under some suitable conditions, confluence and termination are preserved by the above transformation. To appear in Theory and Practice of Logic Programming (TPLP)

Recommendations

• Logic Programming
• scientific article; zbMATH DE number 1234567
• Unfold/fold transformation of stratified programs
• scientific article; zbMATH DE number 3924119
• Aggregates for CHR through Program Transformation
• Unfolding CSP
• Fold and unfold for program semantics
• Fold and unfold for program semantics
• Visualization of CHR through source-to-source transformation
• Total unfolding: theory and applications

Cites work

• scientific article; zbMATH DE number 1566503 (Why is no real title available?)
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• Attributed Data for CHR Indexing
• CHR(PRISM)-based probabilistic logic learning
• Constraint Handling Rules
• Logic Programming
• Logic Programming
• Logic based program synthesis and transformation. 13th international symposium, LOPSTR 2003, Uppsala, Sweden, August 25--27, 2003. Revised selected papers.
• Specialization of Concurrent Guarded Multi-set Transformation Rules
• Theory and practice of constraint handling rules
• Transactions in Constraint Handling Rules

Cited in

(5)

• Unfolding rules for GHC programs
• Specialization of Concurrent Guarded Multi-set Transformation Rules
• Transactions in Constraint Handling Rules
• scientific article; zbMATH DE number 3924119 (Why is no real title available?)
• Runtime repeated recursion unfolding in CHR: a just-in-time online program optimization strategy that can achieve super-linear speedup

This page was built for publication: Unfolding for CHR programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592981)