A Complete and Terminating Execution Model for Constraint Handling Rules
Logic in Computer Science
2010-07-23 v1
Abstract
We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.
Cite
@article{arxiv.1007.3829,
title = {A Complete and Terminating Execution Model for Constraint Handling Rules},
author = {Hariolf Betz and Frank Raiser and Thom Frühwirth},
journal= {arXiv preprint arXiv:1007.3829},
year = {2010}
}
Comments
15 pages