From higher-order to first-order rewriting

Eduardo Bonelli, Delia Kesner, Alejandro Ríos

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Scopus citations

Abstract

We show how higher-order rewriting may be encoded into first-order rewriting modulo an equational theory ε. We obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty theory (that is, ε =ø). This class includes of course the λ-calculus. Our technique does not rely on a particular substitution calculus but on a set of abstract properties to be verified by the substitution calculus used in the translation.

Original languageEnglish
Title of host publicationRewriting Techniques and Applications - 12th International Conference, RTA 2001, Proceedings
EditorsAart Middeldorp
Pages47-62
Number of pages16
DOIs
StatePublished - 2001
Event12th International Conference on Rewriting Techniques and Applications, RTA 2001 - Utrecht, Netherlands
Duration: 22 May 200124 May 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2051 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on Rewriting Techniques and Applications, RTA 2001
Country/TerritoryNetherlands
CityUtrecht
Period22/05/0124/05/01

Fingerprint

Dive into the research topics of 'From higher-order to first-order rewriting'. Together they form a unique fingerprint.

Cite this