Paper Info
Title
Diagrams for meaning preservation
Abstract
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.
Year
DOI
Venue
2003
10.1007/3-540-44881-0_8
RTA
Keywords
Field
DocType
proof burden,multiple diagram-based method,weaker termination property,distinct lift,proof method,termination diagram,step interaction,key proof idea,previous rewriting-based method,abstract framework,operational semantics
Discrete mathematics,Operational semantics,Binary relation,Computer science,Algorithm,Diagram,Critical pair,Rewriting,Confluence,Partition (number theory),Standardization
Conference
Volume
ISSN
ISBN
2706
0302-9743
3-540-40254-3
Citations 
PageRank 
References 
6
0.51
15
Authors
3
Name
Order
Citations
PageRank
Joe B. Wells1243.45
Detlef Plump260462.14
Fairouz Kamareddine332847.92