Lambda extensions of rewrite orderings
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/96993
Tipus de documentReport de recerca
Data publicació1995-10
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
In this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof proceeds via the explicit lifting of a rewrite ordering on first-order terms to a rewrite ordering on (first-order) algebraic lambda-terms. For the definition of the ordering, we have used a technique developed by Kfoury and Wells, in order to delay the erasing beta-reductions (also called K-reductions) which may destroy the monotonicity property. This technique is extended to be able to handle the extensionality rule. As a particular case, the above construction yields an extension of the recursive path ordering of Dershowitz to a rewrite-ordering on (first-order) algebraic lambda-terms which contains simply typed lambda-derivations.
CitacióJouannaud, J., Rubio, A. "Lambda extensions of rewrite orderings". 1995.
Forma partLSI-95-50-R
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
1400191459.pdf | 1,633Mb | Visualitza/Obre |