Load file:

Definitions (substitutions , pretty )

Results (collapse reduce )

Lambda Calculus compiler and interpreter (now with an IO Monad -- see below!)

Copyright (C) 2011, Bill Burdick, Tiny Concepts: http://tinyconcepts.com/fs.pl/lambda.fsl
Licensed with the ZLIB license. See source code for details.

Use the text field below to enter Lambda Calculus expressions. You can use normal Lambda Calculus syntax, with \ meaning λ, but you have to separate your variables with spaces (click edit on any of the definitions for an example). Try testing it out with this (you need to hit enter after you click this): (\x y . x) 1 2

You can define terms using NAME = EXPR. Try this: pickThird = \x y z . z

You can evaluate lambda calculus expressions in 3 ways:
  1. The 'Run' button will compile into JavaScript and run it
  2. The 'Reduce' button will use alpha conversion, beta reduction, and eta conversion to simplify it
  3. The 'VM' button will compile it into byte code and display another 'Run' button you can use to run it (the VM is still a work-in-progress)
The evaluator displays lists for 'Run' (of the first kind) and 'Reduce' results, but not VM's 'Run' results, yet. It cannot display detailed function results of other types for 'Run' (both kinds), but it can for Reduce. Eventually, the VM will display fully detailed results, just like 'Reduce' can.
You can modify the parser in these ways:
  • You can make your definition a token to the parser using
    NAME =.= EXPR
    this means that you won't need spaces around NAME. Good for punctuation, etc.
  • You can make your definition a grouping token with
    CLOSE =)= EXPR
    (for the corresponding closing token).
I use these in the example definitions to create an array-like syntax for lists, using normal Lambda Calculus functions. This demonstrates a way to define functions that act like syntactic sugar. It's really not sugar, though; these are real functions but the point of them is to make things more convenient for the programmer, like syntactic sugar does: [1,2,3] is the same as saying cons 1 (cons 2 (cons 3 nil)) and [1,2|list] is the same as cons 1 (cons 2 list) (like in Prolog). The definitions of '[', ',', '|', and ']' are:
[ =(]= λitem c . c λcont rest . cons item rest
, =.= λf . λitem c . c λcont rest . f true (cons item rest)
] =)= λf . f false nil
| =.= λf rest g . f false rest

IO Monad

If you make an IO monad, a "Step" button will appear that you can use to step through your code. Try testM1-testM10 to see it. Just run one of the tests and Click the "Step" button that appears until you see the final result.
The "stepIO" function in lc.js is the driver for the io monad. The "Step" button calls it with the queued commands in the current IO monad and the latest return value. If there is more computation left, it returns a two-element array containing the rest of the command list and the latest return value otherwise, it returns a one-element array containing only the final return value.
A "real" environment would repeatedly call stepIO until it reaches the final value. This is just a first crack at an IO monad. It's relatively efficient, because it uses difference lists, but the main point is that it demonstrates how to do IO without side effects.

Have fun!
Bill Burdick (you can send me mail at bill dot burdick on gmail)

To do

save button