Hyperlamb is a hypermedia-driven lambda calculus evaluator. Yes.
This is very much work in progress.
If you want, you can clone the repository, build the project, open a browser and navigate to http://localhost:8080/hyperlamb. However, it's even easier to go to http://hyperlamb.azurewebsites.net
In either case, you should see a text box where you can enter a lambda expression.
You might want to start with something simple, like the identity function:
λx.x
Note: if you find it cumbersome to type lambdas, you can use backslash as a poor man's lambdas. So the following is also an acceptable way of writing the identity function:
\x.x
Either way, there's not a whole lot you can do with an expression like that. It is already on normal form, which means it cannot be reduced further. So you might want to try something more involved, like this:
(λn.λf.λx.f (n f x)) (λf.λx.x)
Which can be interpreted as applying the successor function to the Church encoding of the number zero. In general when a lambda expression can be reduced further, there will be a next link available to perform a reduction step. If the evaluation process terminates (as it will in this case), we will eventually end up with an expression on normal form again.
Lambda expressions may be named to make them slightly more wieldy to work with. Adding a name to a lambda expression creates an alias hyperlink for navigating to the expression.
An example should make things clearer. Say we have the expression for the Church encoding of zero:
λf.λx.x
We find it useful to add the name zero for this expression. This adds a hyperlink, /names/zero, that can be used to navigate to the expression (send it to a friend!). In addition, the name will be shown whenever we look at that particular lambda expression. You can also use the name as an expanding text macro in your lambda expressions, by prefixing the name with a dollar sign. For example, you can write $zero in a lambda expression and have it expand to the expression with that name.
If you proceed to add the name succ to the following expression:
λn.λf.λx.f (n f x)
You can now write $succ $zero and have it expand to this:
(λn.λf.λx.f (n f x)) (λf.λx.x)