Structural preservation and reflection of diagrams
Michael Norrish, René Vestergaard · Institutional Repositories DataBase (IRDB) · 2006
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 λ-calculus, with its notion of α-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.