Combinatory reduction systems: Introduction and survey
This paper investigates combinatory reduction systems (CRSs), i.e. usual first-order term rewriting systems with the presence of bound variables. It introduces orthogonal CRSs (illustrated with many examples) and gives an outline of the proof of confluence. It also shows an extension of the finite development theorem.
extension of the finite developments theorem
scientific article; zbMATH DE number 501171
scientific article