Church-Rosser Properties of Normal Rewriting
Jean-Pierre Jouannaud, Li, Jianqi · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2012
We prove a general purpose abstract Church-Rosser result that captures most existing such results that rely on termination of computations. This is achieved by studying abstract normal rewriting in a way that allows to incorporate positions at the abstract level. New concrete Church-Rosser results are obtained, in particular for higher-order rewriting at higher types.