InterJournal Complex Systems, 46 Status: Accepted |
Manuscript Number: [46] Submission Date: 963011 |
A logically reversible evaluator for the call-by-name lambda calculus |
Subject(s): CX.07
Category: Brief Article
Abstract:
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 |