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
Abstract
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.