Evaluation Animation and Debugging

In Presenting Step-by-Step Evaluations, I outlined some things I'd like to do for studying and presenting lambda calculus (or other) evaluations. In recent reflections on that, I noticed the word "step", and realized that what I wanted was almost identical to single-step debugging support. I'd like an animation of reducing expr to follow these steps, each rendered as a few seconds of a still possibly with a dissolve between them:

1. Show expression, highlighting the next application to be reduced, possibly use coloring to highlight the function and argument expressions
2. If occurs check would result in variable capture, display a message announcing there will be an alpha-conversion, followed by expr rewritten with the alpha conversion
3. Announce the beta-conversion
4. Show the result of the beta conversion

Writing this as a function f(expr, stage), where stage is one of the above steps, which returns the reduced-once expression and the next stage should be sufficient to wrap in either a simple loop to produce an animation sequence, or it could be driven by a debugger GUI.

It is especially obvious from this that even at the lambda calculus level, sometimes you want to skip lots at a time and sometimes you need to drill down to the finest level of evaluation possible. Seeing even the alpha conversion step may be useful at some points, at other times you want to set a breakpoint.

That brings up another point -- what is a "single step" in functional language debugging? It's all function applications, there are no lines to step over. Breakpoints have to be set on function expressions: "stop when this function is about to be evaluated."

In conclusion, even this exercise points out how useful lambda calculus can be for studying all kinds of phenomenon at its core: database-like transactional storage, undo/redo stacks, or marshalling. It doesn't have to be lambda calculus, it can be some arbitrary toy language, but lambda calculus has the essential features: variable reference, function definition, and function application. If you're studying a phenomenon like persisting code, you'll find that it's not the data structures (figuring out a way to store lambdas) that are a challenge but the variable references between structures (the swizzling problem). Lambda calculus is a simple 3-feature model that's easy to fit in your head and let you concentrate on the phenomenon of interest.