@proceedings {ABBF11, title = {Completeness of Unfolding for Rewriting Logic Theories}, journal = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2010}, year = {2010}, pages = {116{\textendash}123}, publisher = {IEEE Computer Society Press}, abstract = {Many transformation systems for program optimization, program synthesis, and program specialization are based on fold/unfold transformations. In this paper, we investigate the semantic properties of a narrowing-based unfolding transformation that is useful to transform rewriting logic theories. We also present a transformation methodology that is able to determine whether an unfolding transformation step would cause incompleteness and avoid this problem by completing the transformed rewrite theory with suitable extra rules. More precisely, our methodology identifies the sources of incompleteness and derives a set of rules that are added to the transformed rewrite theory in order to preserve the semantics of the original theory.}, keywords = {Program Transformation, Rewriting Logic, Unfolding}, author = {Maria Alpuente and Michele Baggi and Demis Ballis and Moreno Falaschi} }