Mini Interactive λ-Calculus Expression Editor ​

I developed an interactive editor that makes lambda calculus more tangible by treating expressions as manipulable structures. The editor, available here, provides direct manipulation capabilities that respect the structure of valid terms. The tool was developed using JavaScript, and the code is available on GitHub.

To build an expression, you use placeholders for not-yet-determined subexpressions, called “holes”. When interacting with a hole, users are presented with the three fundamental building blocks of lambda calculus to fill it:

• Variables (e.g. $x$ or $y$)
• Abstractions (i.e., lambda expressions, e.g. $\lambda x. x$)
• Function application (e.g. $(f\;x)$)

The user interface only presents valid expression transformations, while still allowing to build any possible term; so an expression can be constructed iff it is syntactically valid.

Clicking any part of a non-hole expression presents operations to:

• Remove the expression (replacing it with a hole)
• Wrap it in a lambda abstraction
• Wrap it in an application (as either function or argument)

Additionally, bound variables can be renamed by clicking their binding occurrence (next to the $\lambda$ symbol), automatically updating all corresponding references. It does not avoid variable capturing, so this implementation cannot be considered as a refactoring in general.

The editor can also perform a transitive beta-reduction of the current expression. The result remains in the editor, so the reduced form can be further manipulated.