# Semantics-Preserving DPO-Based Term Graph Rewriting

## 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.

## Key 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.