HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 5:15:32 PM
Last modification on : Friday, February 4, 2022 - 3:15:41 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 8:36:59 PM


  • 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⟩



Record views


Files downloads