Wednesday, January 16, 2008

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.


Mattox Beckman said...

I spent a *lot* of time trying to come up with things like this for my research. When you self-apply an on-line partial evaluator, you get copies of the evaluator for every single element of the target program. It would have been nice to compress that somehow, either graphically or textually. I think finding an automated way of doing this would certainly be worth an M.S., and get one very far toward a Ph.D.

JFKBits said...

I think a lot of what I'm trying to do is possible in Coq, the theorem proving software from INRIA.

Check out this tutorial on Pcoq, a graphical interface to Coq for "proof by clicking."

Not totally what I had in mind, but for someone looking for a shipped product, there ya go.