Substitution in the lambda Calculus and the role of the Curry School
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917559523082240 |
|---|---|
| author | Kamareddine, Fairouz |
| author_facet | Kamareddine, Fairouz |
| contents | Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_02745 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Substitution in the lambda Calculus and the role of the Curry School Kamareddine, Fairouz Logic in Computer Science Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha congruence without a form of substitution but for substitution and reduction to work, we need to assume a form of alpha congruence (e.g., when we take lambda terms modulo bound variables). Students on a lambda calculus course usually find this confusing. The elegant writings and research of the Curry school have settled this problem very well. This article is an ode to the contributions of the Curry school (especially the excellent book of Hindley and Seldin) on the subject of alpha congruence and substitution. |
| title | Substitution in the lambda Calculus and the role of the Curry School |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2401.02745 |