Hostname: page-component-74656f9884-j7cmm Total loading time: 0 Render date: 2026-11-09T18:31:16.395Z Has data issue: false hasContentIssue false

A λ-calculus with explicit weakening and explicit substitution

Published online by Cambridge University Press:  07 March 2001

RENÉ DAVID
Affiliation:
Laboratoire de Mathématiques, Université de Savoie, F-73376 Le Bourget du Lac Cedex
BRUNO GUILLAUME
Affiliation:
Laboratoire de Mathématiques, Université de Savoie, F-73376 Le Bourget du Lac Cedex Laboratoire de Recherche en Informatique, Bât. 490 - Université Paris SUD, F-91405 Orsay Cedex
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Since Melliès showed that λσ (a calculus of explicit substitutions) does not preserve the strong normalization of the β-reduction, it has become a challenge to find a calculus satisfying the following properties: step-by-step simulation of the β-reduction, confluence on terms with metavariables, strong normalization of the calculus of substitutions and preservation of the strong normalization of the λ-calculus. We present here such a calculus. The main novelty of this 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.

Information

Type
Research Article
Copyright
© 2001 Cambridge University Press