Structural Preservation and Reflection of Diagrams

    Michael Norrish, NICTA   Rene Vestergaard, JAIST


We present a formal notion of diagram that captures standard
rewriting properties such as confluence, commuting relations,
semi-standardisation, the triangle property, etc. We prove a number
of results that imply diagram equivalence between abstractly related
rewrite relations, i.e., that show that one enjoys a
diagram-expressed property iff the other one does. In particular, we
focus on the case where one rewrite system is over structurally
collapsed terms of the other. We apply the results to various
concrete systems, including the lambda-calculus, with its notion of
alpha-equivalence, and cut-elimination, with its notion of
permutative conversions. The core theory and substantial
applications have been formally verified in the HOL4 proof
assistant.