IngentaConnect Lambda Calculus with Explicit Recursion

Authors: Ariola Z.M.¹; Klop J.W.^{2, 3}

Source: Information and Computation, Volume 139, Number 2, December 1997 , pp. 154-233(80)

Abstract:

This paper is concerned with the study of lambda-calculuswith explicit recursion, namely of cyclic lambda-graphs. Thestarting point is to treat a lambda-graph as a system of recursionequations involving lambda-terms and to manipulate such systemsin an unrestricted manner, using equational logic, just as ispossible for first-order term rewriting. Surprisingly, now theconfluence property breaks down in an essential way. Confluencecan be restored by introducing a restraining mechanism on thesubstitution operation. This leads to a family of lambda-graphcalculi, which can be seen as an extension of the family oflambdasigma-calculi (lambda-calculi with explicit substitution).While the lambdasigma-calculi treat the let-construct asa first-class citizen, our calculi support the letrec, a featurethat is essential to reason about time and space behavior offunctional languages and also about compilation and optimizationsof programs Copyright 1997 Academic Press

Language: English

Document Type: Research article

Affiliations: 1: Computer and Information Science Department, University of Oregon, Eugene, Oregon, 97401 2: CWI, Amsterdam, 1090 GB, The Netherlands 3: Department of Mathematics and Computer Science, Vrije Universiteit, De Boelelaan 1081a, Amsterdam, 1081 HV, The Netherlands

The full text electronic article is available for purchase. You will be able to download the full text electronic article after payment.

$54.13 plus tax