The Origins of lambda-calculus and term rewriting systems

Yves Bertot 1
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We use origin functions to describe the notion of descendance and residuals in reduction systems such as the lambda-calculus and lineart term rewriting systems. We compare the origin functions for the lambda-calculus and for term rewriting systems that implement this calculus, lambda-sigma and lambda Env. We show that the notions of origin do not correspond exactly, but we describe an extension of lambda Env. We show that this extension is not sufficient to give the same result for lambda-sigma and we give another extension for that system. This work is interesting as it provides with a distinction between the two term rewriting systems. This work has applications in the debugging of languages based on the lambda-calculus or environments.
Type de document :
[Research Report] RR-1543, INRIA. 1991, pp.19
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 17:15:32
Dernière modification le : lundi 3 septembre 2018 - 10:56:02
Document(s) archivé(s) le : mardi 12 avril 2011 - 20:36:59



  • HAL Id : inria-00075019, version 1



Yves Bertot. The Origins of lambda-calculus and term rewriting systems. [Research Report] RR-1543, INRIA. 1991, pp.19. 〈inria-00075019〉



Consultations de la notice


Téléchargements de fichiers