InterJournal Complex Systems, 46
Status: Accepted
Manuscript Number: [46]
Submission Date: 963011
A logically reversible evaluator for the call-by-name lambda calculus
Author(s): Lorenz Huelsbergen

Subject(s): CX.07

Category: Brief Article


We present an evaluator for the call-by-name lambda calculus that is logically reversible. This evaluator is therefore a candidate for a computation mechanism that does not dissipate energy due to information erasure. Our design extends Landins secd evaluator for the lambda calculus with a history tape H---as in Bennetts constructions of reversible Turing machines---and is hence called secdh. The history tape records sufficient information to supply each state of a computation with a unique predecessor state. H can therefore be used to reverse the computation and to reset the machine. Since the lambda calculus is a model for realistic programming languages, secdh can, unlike a reversible TM, be directly used to simulate reversible computation of large and complex programs. We provide a complete implementation of secdh for such purposes.

Retrieve Manuscript
Submit referee report/comment

Public Comments: