Animated Lambda Calculus Evaluator

ALCE, version 0.9.2

What is ALCE?

ALCE means Animated Lambda Calculus Evaluator.

It is a small lambda calculus interpreter written in ActionScript 3. The special thing about it is that it draws the terms and animates them while the term reduction happens. Another more or less special thing is that it can mix call-by-name and call-by-value evaluation. It can be used for fun and/or education; real programs are not possible, of course.

... and why?

When the project was started, there were at least three motivational aspects:

• Fun: If you are learning a new programming language (in my case it was AS3), writing a lambda calculus evaluator is a good exercise and it's a lot of fun.
• Beauty: Term reduction is something very beautiful, at least in mind. So I was looking for a way to show other people of what I dream at night (at least when I dream in haskell or scheme).
• Education: Lambda calculus is simple. It's all about substitution and scope, no magic. But a sheet of paper full of x's, y's and greek letters seems to disgust many people.
  If you can't see the systematic moving of the symbols, you only see clutter. So a visualization of term reduction could make the life more easy for someone just starting with this stuff.

Originally I planned to create an educational tool with a documentation, a help manual, some examples and, maybe, a general tutorial on lambda calculus. Something like an interactive tutorial. But at the moment the program was running I suspended the further work on it because of the usual reasons (T&M). So this is a hermetic project: It is only usable for people who know already something about the lambda calculus. Nevertheless:

Here it is:

ALCE-0.9.2

Screenshot:

How to use it

a) You can select a built-in example from the dropdown menu and evaluate it step-by-step, by clicking on the button 'reduce term'.  Check 'auto-reduce' to start the automatic reduction.

b) You can type in your own program and parse it by clicking 'read editor'. The syntax of the source code is described below.

  T := x           identifier: sequences of lower-case characters
       @ T T       application
       \ x . T     function, application order depends on global setting (CBN/CBV)
       ! x . T     function, guaranteed strict (CBV)
       $ x . T     function, guaranteed call-by-name (CBN)
       123         number: sequence of digits (N, but internal float)
       + T T       op2: + - * / % < > <= >= <> == & |
       not T       op1: not pair car cdr put
       get         op0: get	reads some digits followed by space or newline from the input
       : T T       non-strict cons
       if T T T    if: 0 means false, /=0 means true (not 0 returns 1)
       ( T )       parentheses, for readability
       beep T      evaluates T and plays an beep-like sound depending on T's result

  ...and some syntactic sugar:
       let a b c   ===>   @ \a. c b
       do a b      ===>   @ \_. b a
       => a b      ===>   @ b a
       cons a b    ===>   @ @ \x.\y. : x y a b

  All Symbols
       ! $ \ .
       @
       + - * / % < > <= >= <> == & |
       :
       not pair car cdr put
       get
       if
       let
       do
       cons
       beep
       =>

Example: quicksort

The following program (a quicksort port) expects some user-input:
First, the length of the number-list to sort, then the numbers itself.
The input "4 7 9 8 6 " (space or newline at the end) will result in
"6 7 8 9" after 1175 reductions for call-by-value. For call-by-name
it takes 22055 reductions.

 let rec @ \y.\f.@f@@y y f  \y.\f.@f@@y y f
 let print @ rec $pr.\x.if pair x do put car x @ pr cdr x 0
 let append @ rec $app.\x.\y.if pair x @@cons car x @@app cdr x y y 
 let split @ rec $split.\x.\yss.if pair yss
                                let lr @@ split x cdr yss beep
                                if < car yss x
                                   : (: car yss car lr) cdr lr
                                   : car lr (: car yss cdr lr)
                                : 0 0
 let qsort @ rec $qsort.\xss.if pair xss
                             let lr @@ split car xss cdr xss
                             @@ append @ qsort car lr (: car xss @ qsort cdr lr)
                             0
 let read @ rec $read.\n.if < n 1 
                         0
                         => get !inp.
                         => @ read - n 1 !r. : inp r
 => get !n.
 => @ read n !input.
 @print@qsort input

Example: fibonacci

works only with call-by-name, but not very efficiently...

 let y \x.@x x
 let rec @y \y.\f.@f@@ y y f  
 let print @ rec $pr.$x.if pair x do put car x @pr cdr x 0
 let fibhelp @ rec $fib.\x.\y. @@cons x @@fib y + x y
 @print @@fibhelp 0 1

Example: sound

Just a simple sound:

 beep 20

A simple melody.

 do beep 36
 do beep 48
 do beep 60
 do beep 36
 do beep 48
 do beep 60
 do beep 35
 do beep 47
 do beep 59
 do beep 38
 do beep 50
 do beep 62
 0

The following is one of the built-in examples:

 let loop @\loop.\n.do beep n @@loop loop + n 1 \loop.\n.do beep n @@loop loop + n 1
 @loop 0