Navegar

Colección

Datos Estadísticas

Artículo

Bonelli, E.; Kesner, D.; Ríos, A. "From higher-order to first-order rewriting" (2001) 12th International Conference on Rewriting Techniques and Applications, RTA 2001. 2051 LNCS:47-62
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte la política de Acceso Abierto del editor

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. © Springer-Verlag Berlin Heidelberg 2001.

Registro:

Documento: Artículo
Título:From higher-order to first-order rewriting
Autor:Bonelli, E.; Kesner, D.; Ríos, A.
Ciudad:Utrecht
Filiación:Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina
LRI (CNRS URA 410), Bât 490, Université de Paris-Sud, 91405 Orsay Cedex, France
Palabras clave:Artificial intelligence; Computer science; Differentiation (calculus); Equational theory; First-order rewriting; Higher-order; Higher-order rewriting; Extended abstracts; Lambda calculus; Calculations; Calculations
Año:2001
Volumen:2051 LNCS
Página de inicio:47
Página de fin:62
Título revista:12th International Conference on Rewriting Techniques and Applications, RTA 2001
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli

Referencias:

  • Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit substitutions (1991) Journal of Functional Programming, 4 (1), pp. 375-416
  • Arts, T., Giesl, J., Termination of term rewriting using dependency pairs (2000) Theoretical Computer Science, 236, pp. 133-178
  • Bachmair, L., Dershowitz, N., Critical pair criteria for completion (1988) Journal of Symbolic Computation, 6 (1), pp. 1-18
  • Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J., λ υ, a calculus of explicit substitutions which preserves strong normalisation (1996) Journal of Functional Programming, 6 (5), pp. 699-722
  • Bonelli, E., Kesner, D., Ríos, A., A de Bruijn notation for higher-order rewriting (2000) Proc. of the Eleventh Int. Conference on Rewriting Techniques and Applications, , Norwich, UK, July
  • David, R., Guillaume, B., A λ-calculus with explicit weakening and explicit substitutions (2000) Journal of Mathematical Structures in Computer Science, , To appear
  • Dershowitz, N., Orderings for term rewriting systems (1982) Theoretical Computer Science, 17 (3), pp. 279-301
  • Dershowitz, N., Jouannaud, J.-P., Rewrite systems (1990) Handbook of Theoretical Computer Science, B, pp. 243-309. , J. van Leeuwen, editor. North- Holland
  • Dowek, G., Hardin, T., Kirchner, C., Theorem proving modulo (1998) Technical Report RR 3400 INRIA
  • Dowek, G., Hardin, T., Kirchner, C., Pfenning, F., Unification via Explicit Substitutions: The Case of Higher-Order Patterns (1998) Technical Report RR3591. INRIA.
  • Dowek, G., Hardin, T., Kirchner, C., Higher-order unification via explicit substitutions (2000) Information and Computation, 157, pp. 183-235
  • Dowek, G., Hardin, T., Kirchner, C., Hol-lambda-sigma: An intentional first-order expression of higher-order logic (2001) Mathematical Structures in Computer Science, 11, pp. 1-25
  • Hardin, T., Lévy, J.-J., (1989) A Confluent Calculus of Substitutions, , France-Japan Artificial Intelligence and Computer Science Symposium
  • Jouannaud, J.-P., Rubio, A., The higher-order recursive path ordering (1999) Fourteenth Annual IEEE Symposium on Logic in Computer Science, , Trento, Italy
  • Kamareddine, F., Ríos, A., A λ-calculus à la de Bruijn with explicit substitutions (1995) Proc. of the Int. Symposium on Programming Language Implementation and Logic Programming (PLILP), , LNCS 982
  • Kamin, S., Lévy, J.J., (1980) Attempts for Generalizing the Recursive Path Orderings, , University of Illinois
  • Kesner, D., Confluence of extensional and non-extensional lambda-calculi with explicit substitutions (2000) Theoretical Computer Science, 238 (1-2), pp. 183-220
  • Khasidashvili, Z., Expression reduction systems (1990) Proc. of I. Vekua Institute of Applied Mathematics, 36. , Tbilisi
  • Khasidashvili, Z., Ogawa, M., Van Oostrom, V., (2000) Uniform Normalization beyond Orthogonality, , Submitted for publication
  • Lescanne, P., Rouyer-Degli, J., Explicit substitutions with de Bruijn levels (1995) Proc. of the Sixth Int. Conference on Rewriting Techniques and Applications, , LNCS 914
  • Melliès, P.-A., (1996) Description Abstraite des Systèmes de Réécriture. Thèse de l'Université Paris VII, , December
  • Muñoz, C., A left-linear variant of λσ (1997) Proc. of the 6th Int. Conference on Algebraic and Logic Programming (ALP'97), , Michael Hanus, J. Heering, and K. (Karl) Meinke, editors, LNCS 1298
  • Nipkow, T., Higher-order critical pairs (1991) Proc. of the Sixth Annual IEEE Symposium on Logic in Computer Science
  • Pagano, B., (1998) Des Calculs de Susbtitution Explicite et Leur Application À la Compilation des Langages Fonctionnels, , PhD thesis, Université Paris VI
  • Pollack, R., Closure under alpha-conversion (1993) Henk Barendregt and Tobias Nipkow, Editors, Types for Proofs and Programs (TYPES), , LNCS 806
  • Zantema, H., Termination of term rewriting by semantic labelling (1995) Fundamenta Informaticae, 24, pp. 89-105A4 - Centrum voor Wiskunde en Informatica (CWI); et al.; Instituut voor Programmatuurkunde en Algoritmiek (IPA); International Federation for Information Processing (IFIP); University of Amsterdam, Informatics Institute

Citas:

---------- APA ----------
Bonelli, E., Kesner, D. & Ríos, A. (2001) . From higher-order to first-order rewriting. 12th International Conference on Rewriting Techniques and Applications, RTA 2001, 2051 LNCS, 47-62.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli [ ]
---------- CHICAGO ----------
Bonelli, E., Kesner, D., Ríos, A. "From higher-order to first-order rewriting" . 12th International Conference on Rewriting Techniques and Applications, RTA 2001 2051 LNCS (2001) : 47-62.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli [ ]
---------- MLA ----------
Bonelli, E., Kesner, D., Ríos, A. "From higher-order to first-order rewriting" . 12th International Conference on Rewriting Techniques and Applications, RTA 2001, vol. 2051 LNCS, 2001, pp. 47-62.
Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli [ ]
---------- VANCOUVER ----------
Bonelli, E., Kesner, D., Ríos, A. From higher-order to first-order rewriting. Lect. Notes Comput. Sci. 2001;2051 LNCS:47-62.
Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v2051LNCS_n_p47_Bonelli [ ]