The weak normalization of the simply typed λse-calculus
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 isomo...
Guardado en:
| Publicado: |
2007
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_13670751_v15_n2_p121_Arbiser http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser |
| Aporte de: |
| id |
paper:paper_13670751_v15_n2_p121_Arbiser |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_13670751_v15_n2_p121_Arbiser2023-06-08T16:12:03Z The weak normalization of the simply typed λse-calculus Explicit substitution Lambda calculus Normalization Simple typing 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. 2007 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_13670751_v15_n2_p121_Arbiser http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Explicit substitution Lambda calculus Normalization Simple typing |
| spellingShingle |
Explicit substitution Lambda calculus Normalization Simple typing The weak normalization of the simply typed λse-calculus |
| topic_facet |
Explicit substitution Lambda calculus Normalization Simple typing |
| description |
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. |
| title |
The weak normalization of the simply typed λse-calculus |
| title_short |
The weak normalization of the simply typed λse-calculus |
| title_full |
The weak normalization of the simply typed λse-calculus |
| title_fullStr |
The weak normalization of the simply typed λse-calculus |
| title_full_unstemmed |
The weak normalization of the simply typed λse-calculus |
| title_sort |
weak normalization of the simply typed λse-calculus |
| publishDate |
2007 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_13670751_v15_n2_p121_Arbiser http://hdl.handle.net/20.500.12110/paper_13670751_v15_n2_p121_Arbiser |
| _version_ |
1768544193976729600 |