Universal Algebra for Termination of Higher-Order Rewriting

Abstract. We show that the structures of binding algebras and Σmonoids by Fiore, Plotkin and Turi are sound and complete models of Klop’s Combinatory Reduction Systems (CRSs). These algebraic structures play the same role of universal algebra for term rewriting systems. Restricting the algebraic structures to the ones equipped with wellfounded relations, we obtain a complete characterisation of terminating CRSs. We can also naturally extend the characterisation to rewriting on meta-terms by using the notion of Σ-monoids.

• Type: Conference
• Year: 2005
• Where: RTA
• Authors: Makoto Hamana
• Keywords: Algebraic Structures, Klop’s Combinatory Reduction, RTA 2005, Term Rewriting Systems, Theoretical Computer Science