§
Lazy reversible computation?
Lazy programs are hard to analyze because we need to reason abot them backwards.
Suppose we limit ourselves to reversible programs. Does it then become easy?