Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00075019
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 5:15:32 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 8:36:59 PM

Identifiers

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

Share

Metrics

Record views

233

Files downloads

120