Presenting Step-by-Step Evaluations

For the past few posts, such as Pairs and Y, I've been wanting to present my pen and paper lambda calculus derivations with the aid of a program. Rather than encoding an evaluator to reduce a lambda calculus expression to normal form, I wanted to imitate the pen and paper process:

1. Write an expression
2. Identify how you want to transform it, and justify
3. Write the transformed expression and repeat as needed

The idea is to provide a set of tools so that you can write sequences like

line1 = expr
display(line1, "Beta reduce by replacing body of Y combinator with argument")
line2 = betaReduce(line1)
display(line2,"Call this form Ybound for future reference.")

Do I have a set of tree modifying functions like betaReduce, or abstract everything into a do-it-all function, like reduceOnce? That would show which subexpression needs to be evaluated next, and emits the reduced expression. But I'd like to add human comments on a line by line basis. I'd like to show currently uninteresting subexpressions in abbreviated form, and control that on a line by line basis.

The thing is you can't just have "betaReduce(expr)", you'd like to give an expression and somehow identify which subexpression to beta-reduce. Every lambda calculus expression may have more than one application ready to be reduced, and as the proof writer you'd like to pick which to work on.

Another issue is the symbol/definition issue. I've noticed is sometimes in my pen and paper proofs, I'd like to write a symbol like 1, Y, or fixtup for clarity, and expand to its full lambda calculus expression at need. This especially happens with Y and its forms which keep recreating themselves :).

My pipe dream vision of this is something pretty graphical, where each expression has some buttons (show free variables, alpha convert, beta reduce), and there's a notes section below expressions where you can comment on. The undo/redo stack then is the serialized form of your derivation and can be rendered to a nice little movie.