|
J. B. Wells, Detlef Plump, and Fairouz Kamareddine
Diagrams for meaning
preservation
In Rewriting Techniques & Applications, 14th Int'l Conf., RTA
2003, volume 2706 of LNCS, pages 88-106 Springer-Verlag, 2003
A long version is [36]
This paper presents an abstract framework and
multiple diagram-based methods for proving
meaning preservation, i.e., that all rewrite
steps of a rewriting system preserve the meaning
given by an operational semantics based on a
rewriting strategy. While previous rewriting-based
methods have generally needed the treated rewriting
system as a whole to have such properties as, e.g.,
confluence, standardization, and/or
termination or boundedness of
developments, our methods can work when
all of these conditions fail, and thus can
handle more rewriting systems. We isolate the new
lift/project with termination diagram as the
key proof idea and show that previous
rewriting-based methods (Plotkin's method based on
confluence and standardization and
Machkasova and Turbak's method based on distinct
lift and project properties)
implicitly use this diagram. Furthermore, our
framework and proof methods help reduce the proof
burden substantially by, e.g., supporting separate
treatment of partitions of the rewrite steps,
needing only elementary diagrams for rewrite
step interactions, excluding many rewrite step
interactions from consideration, needing weaker
termination properties, and providing generic
support for using developments in combination with
any method.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
