Semantics-Preserving DPO-Based Term Graph Rewriting
Wolfram Kahl (McMaster University), Yuhang Zhao (McMaster University)
TL;DR
This paper proves that DPO-based term graph rewriting preserves the semantics of functional programs, ensuring correctness in program execution and optimization.
Contribution
It introduces a new proof of semantics preservation for DPO-based term graph rewriting, enhancing the theoretical foundation of program transformation techniques.
Findings
DPO-based rewriting preserves program semantics
Theoretical validation of term graph transformations
Supports correctness in compiler optimizations
Abstract
Term graph rewriting is important as "conceptual implementation" of the execution of functional programs, and of data-flow optimisations in compilers. One way to define term graph transformation rule application is via the well-established and intuitively accessible double-pushout (DPO) approach; we present a new result proving semantics preservation for such DPO-based term graph rewriting.
Click any figure to enlarge with its caption.
Figure 1
Figure 2
Figure 3
Figure 4
Figure 5
Figure 6Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsModel-Driven Software Engineering Techniques · Software Testing and Debugging Techniques · Formal Methods in Verification