Artículo
Bonelli, E.; Kesner, D.; Ríos, A.; Bachmair L. "A de bruijn notation for higher-order rewriting" (2000) 11th International Conference on Rewriting Techniques and Applications, RTA 2000. 1833:62-79
Consulte la política de Acceso Abierto del editor
Abstract:
We propose a formalism for higher-order rewriting in de Bruijn notation. This notation not only is used for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express general higher-order rewrite systems. We give formal translations from higher-order rewriting with names to higher-order rewriting with de Bruijn indices, and vice-versa. These translations can be viewed as an interface in programming languages based on higher-order rewrite systems, and they are also used to show some properties, namely, that both formalisms are operationally equivalent, and that confluence is preserved when translating one formalism into the other. © Springer-Verlag Berlin Heidelberg 2000.
Registro:
| Documento: | Artículo |
| Título: | A de bruijn notation for higher-order rewriting |
| Autor: | Bonelli, E.; Kesner, D.; Ríos, A.; Bachmair L. |
| Filiación: | Departamento de Computación, Universidad de Buenos Aires, Pabellón I, Ciudad Universitaria, Buenos Aires, 1428, Argentina LRI (UMR 8623), Université de Paris-Sud, Bât 490, Orsay Cedex, 91405, France |
| Palabras clave: | Artificial intelligence; Computers; De Bruijn; De-Bruijn indices; Higher-order rewrite system; Higher-order rewriting; Meta-terms; Program translators |
| Año: | 2000 |
| Volumen: | 1833 |
| Página de inicio: | 62 |
| Página de fin: | 79 |
| Título revista: | 11th International Conference on Rewriting Techniques and Applications, RTA 2000 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1833_n_p62_Bonelli |
Referencias:
- Barendregt, H.P., The Lambda Calculus: Its Syntax and Semantics (1984) Studies in Logic and the Foundations of Mathematics, , North-Holland, Amsterdam, Revised edition
- Bloo, R., (1997) Preservation of Termination for Explicit Substitution, , PhD thesis, Eindhoven University
- Bloo, R., Rose, K., (1996) Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Normalisation, pp. 169-183. , RTA, LNCS 1103
- Bonelli, E., Kesner, D., Ríos, A., (2000) A De Bruijn Notation for Higher-Order Rewriting, , ftp://ftp.lri.fr/LRI/articles/kesner/dBhor.ps.gz
- Curien, P.-L., Categorical combinators, sequential algorithms and functional programming Progress in Theoretical Computer Science, , Birkhaüser, 1993. Second edition
- Curien, P.-L., Hardin, T., Lévy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions Journal of the ACM, 43 (2), pp. 362-397. , march 1996
- De Bruijn, N., Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem (1972) Indag. Mat, 5 (35), pp. 381-392
- Dowek, G., (1999) La Part Du Calcul, , Univesité de Paris VII, Thése d’Habilitation á diriger des recherches
- Dowek, G., Hardin, T., Kirchner, C., (1995) Higher-Order Unification via Explicit Substitutions, , LICS
- Hindley, R., Seldin, J.P., (1980) Introduction to Combinators and λ-calculus, , London Mathematical Society
- Kamareddine, F., Ríos, A., Bridging de bruijn indices and variable names in explicit substitutions calculi (1998) Logic Journal of the Interest Group of Pure and Applied Logic (IGPL), 6 (6), pp. 843-874
- Khasidashvili, Z., Expression reduction systems (1990) Proceedings of I, 36. , Vekua Institute of Applied Mathematics, Tbilisi
- Khasidashvili, Z., Van Oostrom, V., Context-sensitive Conditional Expression Reduction Systems (1995) Proceedings of the Joint COMPU-GRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation, 2. , ENTCS, (SEG-RAGRA’95), Volterra
- Klop, J.W., Combinatory Reduction Systems, 127. , of Mathematical Centre Tra c t s. CWI, Amsterdam, 1980. PhD Thesis
- Nipkow, T., (1991) Higher Order Critical Pairs, pp. 342-349. , LICS
- Pagano, B., (1998) Des Calculs De Susbtitution Explicite Et Leur Application á La Compilation Des Langages Fonctionnels, , PhD thesis, Université Paris VI
- Pollack, R., (1993) Closure under Alpha-Conversion, , TYPES, LNCS 806
- Rehof, J., Sørensen, M.H., (1994) The <inf>∆</inf> Calculus, 789, pp. 516-542. , TACS, LNCS
- Rose, K., (1992) Explicit Cyclic Substitutions, 656, pp. 36-50. , CTRS, LNCS
- Van Oostrom, V., Van Raamsdonk, F., (1994) Weak Orthogonality Implies Confluence: The Higher-Order Case, 813, pp. 379-392. , LFCS, LNCS
- Van Raamsdonk, F., (1996) Confluence and Normalization for Higher-Order Rewriting, , PhD thesis, Amsterdam University, The Netherlands
- Wolfram, D., (1993) The Clausal Theory of Types, 21. , of Cambridge Tracts in Theoretical Computer Science. Cambridge University PressA4 -
Citas:
---------- APA ----------
Bonelli, E., Kesner, D., Ríos, A. & Bachmair L. (2000) . A de bruijn notation for higher-order rewriting. 11th International Conference on Rewriting Techniques and Applications, RTA 2000, 1833, 62-79.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1833_n_p62_Bonelli [ ]
---------- CHICAGO ----------
Bonelli, E., Kesner, D., Ríos, A., Bachmair L. "A de bruijn notation for higher-order rewriting" . 11th International Conference on Rewriting Techniques and Applications, RTA 2000 1833 (2000) : 62-79.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1833_n_p62_Bonelli [ ]
---------- MLA ----------
Bonelli, E., Kesner, D., Ríos, A., Bachmair L. "A de bruijn notation for higher-order rewriting" . 11th International Conference on Rewriting Techniques and Applications, RTA 2000, vol. 1833, 2000, pp. 62-79.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1833_n_p62_Bonelli [ ]
---------- VANCOUVER ----------
Bonelli, E., Kesner, D., Ríos, A., Bachmair L. A de bruijn notation for higher-order rewriting. Lect. Notes Comput. Sci. 2000;1833:62-79.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v1833_n_p62_Bonelli [ ]
