A lambda-calculus with explicit weakening and explicit substitution
David, René ; Guillaume, Bruno
HAL, hal-00384683 / Harvested from HAL
Since Melliès has shown that lambda-sigma (a calculus of explicit substitutions) does not preserve the strong normalization of the beta-reduction, it became a challenge to find a calculus satisfying the following properties: step by step simulation of the beta-reduction, confluence on terms with metavariables, strong normalization of the calculus of substitutions and preservation of the strong normalization of the lambda-calculus. We present here such a calculus. The main novelty of the calculus (given with de Bruijn indices) is the use of labels that represent updating functions and correspond to explicit weakening. A typed version is also presented.
Publié le : 2001-01-01
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
@article{hal-00384683,
     author = {David, Ren\'e and Guillaume, Bruno},
     title = {A lambda-calculus with explicit weakening and explicit substitution},
     journal = {HAL},
     volume = {2001},
     number = {0},
     year = {2001},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00384683}
}
David, René; Guillaume, Bruno. A lambda-calculus with explicit weakening and explicit substitution. HAL, Tome 2001 (2001) no. 0, . http://gdmltest.u-ga.fr/item/hal-00384683/