cdparks/lambda-machine

What?

It's a machine for evaluating expressions in the untyped lambda calculus. You get lambdas, variables, applications, and top-level definitions. You can try it here.

Really?

Yep. Here's a grammar:

<definition>
    ::= <name> [<name> ...] = <expression>       -- Definition

<expression>
    ::= \ <name> . <expression>                  -- Lambda
    |   <name>                                   -- Variable
    |   <expression> <expression>                -- Application
    |   ( <expression> )                         -- Parenthesization

<name>
    ::= [<lower> <underscore>]
        [<lower> <digit> <hyphen>]*
        [<question-mark>]?
        ([<prime>]* | [<subscript>]*)

There is also optional syntax for natural numbers and lists, but these are desugared to plain lambda calculus at parse time:

[a, b, c]
    -> λcons. λnil. cons a (cons b (cons c nil))
3
    -> λs. λz. s (s (s z))
[1]
    -> λcons. λnil. cons (λs. λz. s z) nil

Why?

I've been working through the exercises in Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and some of these expressions have become rather tedious to reduce by hand. It'd be nice to have something that would do it for me step-by-step, ya know?

How?

It's written in PureScript and React using the Thermite library. Expressions are converted to a locally nameless representation before being evaluated in normal order.

You can run it like this:

npm install
bower install
pulp browserify --optimise --to static/js/main.js
open index.html

Who?

Me, Chris Parks. Feel free to say hi!