Artículo
Abstract:
In this paper, we show the weak normalization (WN) of the simply-typed λse-calculus with open terms where abstractions are decorated with types, and metavariables, de Bruijn indices and updating operators are decorated with environments. We show a proof of WN using the λωe-calculus, a calculus isomorphic to λse→. This proof is strongly influenced by Goubault-Larrecq's proof of WN for the λσ-calculus but with subtle differences which show that the two styles require different attention. Furthermore, we give a new calculus λω′e which works like λse but which is closer to λσ than λωe. For both λωe and λω′e we prove WN for typed semi-open terms (i.e. those which allow term variables but no substitution variables), unlike the result of Goubault-Larrecq which covered all λσ open terms. © The Author, 2007. Published by Oxford University Press. All rights reserved.
Registro:
| Documento: | Artículo |
| Título: | The weak normalization of the simply typed λse-calculus |
| Autor: | Arbiser, A.; Kamareddine, F.; Rios, A. |
| Filiación: | Department of Computer Science, University of Buenos Aires, Pabellón I, 1428 Buenos Aires, Argentina School of Mathematical and Computer Sciences, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, United Kingdom |
| Palabras clave: | Explicit substitution; Lambda calculus; Normalization; Simple typing |
| Año: | 2007 |
| Volumen: | 15 |
| Número: | 2 |
| Página de inicio: | 121 |
| Página de fin: | 147 |
| DOI: | http://dx.doi.org/10.1093/jigpal/jzm003 |
| Título revista: | Logic Journal of the IGPL |
| Título revista abreviado: | Logic J. IGPL |
| ISSN: | 13670751 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_13670751_v15_n2_p121_Arbiser |
Referencias:
- Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J., Explicit Substitutions (1991) Journal of Functional Programming, 1 (4), pp. 375-416
- Benaissa, Z., Briaud, D., Lescanne, P., Rouyer-Degli, J., λν, a calculus of explicit substitutions which preserves strong normalisation (1996) Functional Programming, 6 (5)
- P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. Pitman, 1986. Revised edition, Birkhäuser (1993); Curien, P.-L., Hardin, T., Lévy, J.-J., Confluence properties of weak and strong calculi of explicit substitutions (1617) Technical Report RR, , INRIA, Rocquencourt
- 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, 34 (5), pp. 381-392
- Goubault-Larrecq, J., A proof of weak termination of the simply typed λσ-calculus (1998) LNCS, 1512, pp. 134-151. , Proc. Int. Workshop on Types for Proofs and Programs TYPES'96
- Guillaume, B., (1999) Un calcul des substitutions avec étiquettes, , PhD thesis, Université de Savoie, Chambéry, France
- Kamareddine, F., Ríos, A., Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms (1997) Journal of Functional Programming, 7 (4), pp. 395-420
- Kamareddine, F., Ríos, A., Relating the λσ- and λs-styles of explicit substitutions (2000) Logic and Computation, 10 (3), pp. 349-380
- Ríos, A., (1993) Contribution à l'étude des λ-calculs avec substitutions explicites, , PhD thesis, Université de Paris 7
Citas:
---------- APA ----------
Arbiser, A., Kamareddine, F. & Rios, A. (2007) . The weak normalization of the simply typed λse-calculus. Logic Journal of the IGPL, 15(2), 121-147.http://dx.doi.org/10.1093/jigpal/jzm003
---------- CHICAGO ----------
Arbiser, A., Kamareddine, F., Rios, A. "The weak normalization of the simply typed λse-calculus" . Logic Journal of the IGPL 15, no. 2 (2007) : 121-147.http://dx.doi.org/10.1093/jigpal/jzm003
---------- MLA ----------
Arbiser, A., Kamareddine, F., Rios, A. "The weak normalization of the simply typed λse-calculus" . Logic Journal of the IGPL, vol. 15, no. 2, 2007, pp. 121-147.http://dx.doi.org/10.1093/jigpal/jzm003
---------- VANCOUVER ----------
Arbiser, A., Kamareddine, F., Rios, A. The weak normalization of the simply typed λse-calculus. Logic J. IGPL. 2007;15(2):121-147.http://dx.doi.org/10.1093/jigpal/jzm003
