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 :
Rapport
[Research Report] RR-1543, INRIA. 1991, pp.19
Liste complète des métadonnées

https://hal.inria.fr/inria-00075019
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 17:15:32
Dernière modification le : samedi 27 janvier 2018 - 01:30:57
Document(s) archivé(s) le : mardi 12 avril 2011 - 20:36:59

Fichiers

Identifiants

  • HAL Id : inria-00075019, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

157

Téléchargements de fichiers

63