Expression Reduction Systems and Extensions: An Overview

John R. W. Glauert, Delia Kesner, Zurab Khasidashvili

Research output: Chapter in Book/Report/Conference proceedingChapter

9 Citations (Scopus)


Expression Reduction Systems is a formalism for higher-order rewriting, extending Term Rewriting Systems and the lambda-calculus. Here we give an overview of results in the literature concerning ERSs. We review confluence, normalization and perpetuality results for orthogonal ERSs. Some of these results are extended to orthogonal conditional ERSs. Further, ERSs with patterns are introduced and their confluence is discussed. Finally, higher-order rewriting is translated into equational first-order rewriting. The technique develops an isomorphic model of ERSs with variable names, based on de Bruijn indices.
Original languageEnglish
Title of host publicationProcesses, Terms and Cycles: Steps on the Road to Infinity. Essays dedicated to Jan Willem Klop on the Occasion of His 60th Birthday
EditorsAart Middledorp, Vincent van Oostrom, Femke van Raamsdonk, Roel De Vrijer
Place of PublicationBerlin / Heidelberg
Number of pages58
ISBN (Print)978-3-540-30911-6
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science

Cite this