TY - GEN
T1 - From higher-order to first-order rewriting
AU - Bonelli, Eduardo
AU - Kesner, Delia
AU - Ríos, Alejandro
PY - 2001
Y1 - 2001
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84888234285&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84888234285&partnerID=8YFLogxK
U2 - 10.1007/3-540-45127-7_6
DO - 10.1007/3-540-45127-7_6
M3 - Conference contribution
AN - SCOPUS:84888234285
SN - 3540421173
SN - 9783540421177
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 47
EP - 62
BT - Rewriting Techniques and Applications - 12th International Conference, RTA 2001, Proceedings
A2 - Middeldorp, Aart
T2 - 12th International Conference on Rewriting Techniques and Applications, RTA 2001
Y2 - 22 May 2001 through 24 May 2001
ER -