Simple Lambda Calculus Interpreter

Simple Lambda Calculus Interpreter

A simple lambda calculus interpreter, using call-by-name semantics. The language is pretty much Church's simple untyped lambda calculus, the only concession for usefulness is the addition of numbers.

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. This program is copyright (C) 1996-1997 and has been made by Colin J. Taylor of the University of Nottingham.


Syntax

The syntax is: 

<Prog> ::=  <Expr>
	|   let <Variable> = <Expr>

<Expr> ::=  <Variable>
        |   <Number>
        |   \ <Variable> . <Expr>
        |   ( <Expr> )
        |   <Expr1> <Expr2>
        |   +
        |   -
Programs entered into the interpreter are either simple expressions for immediate evaluation, or top level bindings of a variable to an expression (these are similar to the the top level bindings of variables in SML). The interpreter supports variables, numbers, lambda abstractions, parenthesised expressions, applications, addition (infix notation only), and subtraction (infix notation only).

How to use the interpreter

Just type your programs in the entry field at the top, and press return to evaluate them. The result is shown in the text area at the bottom. This is a java applet and currently does not use threads, so you may see some sluggish behaviour if you try to evaluate expensive expressions.

The Prelude file

Note also that on initialisation, a small prelude file of top level bindings is loaded, and the bound variables are listed. This prelude includes simple support for booleans, pairs, and church numerals. A non-terminating expression is also included to illustrate the lazy evaluation. The fixpoint combinator Y is in the Prelude, along with a simple example of a recursively defined function, factorial.

Example expressions

Here are some interesting expressions to try:
(\x . x) (\x . x)
(\x . (\y . x)) (\x . x)
(\x . x x) (\x . x x)

NOTE: The last of these expressions may well hang your web browser, as the reduction sequence for it never terminates. This expression is not type-safe and illustrates why types can be useful.

Here is the interpreter