|InterJournal Complex Systems, 46
|Manuscript Number: |
Submission Date: 963011
|A logically reversible evaluator for the call-by-name lambda calculus|
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.
|Submit referee report/comment|