The expansion problem in lambda calculi with explicit substitution
In this article, we address the problem of expansion with respect to rules of a calculus with explicit substitution. Mainly, we analyse the λυ- and λs-calculi sets of terms having the property of expansion to pure terms, as minimal sets of terms for these calculi. We prove that, contrarily to what h...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | JOUR |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_0955792X_v18_n6_p849_Arbiser |
| Aporte de: |
| Sumario: | In this article, we address the problem of expansion with respect to rules of a calculus with explicit substitution. Mainly, we analyse the λυ- and λs-calculi sets of terms having the property of expansion to pure terms, as minimal sets of terms for these calculi. We prove that, contrarily to what happens in the λx-calculus in which this set is trivial, for λυ and λs they are proper and non-recursive, so a calculus based on a minimal set of terms has a syntax which is not context-free and hence cannot be presented in the usual way. © The Author, 2008. Published by Oxford University Press. All rights reserved. |
|---|