A Model for Comparing the Space Usage of Lazy Evaluators

Adam Bakewell and Colin Runciman

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000


Identifying the source of space faults in functional programs is hard. The problem is compounded as space usage can vary enormously from one implementation to another. We use a term-graph rewriting model to describe evaluators with explicit space usage. Given descriptions for two evaluators E1 and E2, if E1 never has asymptotically worse space usage than E2, we can use a bisimulation-like proof method to prove it. Conversely, if E1 is leakier than E2, we characterise a class of computations that expose the difference between them.