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