Summary

This module allows simple experimentation with the lambda calculus, first developed by Church. It understands the different types of lambda expressions, can extract lists of variables (both free and bound) and subterms, and can simplify complicated by expression by means of application.

Getting the software

The software is available in a tarball here: http://www.alcyone.com/pyos/church/church-latest.tar.gz.

The official URL for this Web site is http://www.alcyone.com/pyos/church/.

Notation

Notations for lambda expressions vary slightly, so it is instructive to detail the precise notation used by this module. A variable is expressed with a string of alphanumeric characters, e.g., x or abc1. There are three types of lambda expressions:

variable expression

A variable expression is simply an expression consisting of a single variable, e.g., x.

lambda expression

A lambda expression consists of a backslash (\), one or more variables separated by spaces, a dot (.), and a final expression. For example, \x.M where x is a variable and M is an expression. Repeated variables are equivalent to recursed lambda expressions, so \x y.M is equivalent to \x.\y.M.

application expression

An application expression consists of two or more adjacent expressions surrounded by parentheses: (M N), where M and N are expressions. Applications are left associative, so (M N P) is equivalent to ((M N) P).

Usage

The module is intended to be used as a module imported by Python programs; when run as a standalone program it runs some algorithms on some test expressions and prints the results. Doing this is helpful for becoming familiar with the notation used by the module.

Known problems

• Engine written entirely in Python and not designed for speed.

• The parser is extremely simple and could be improved.

Wish list

• An interactive interpreter would be helpful.

• Automatic substitution of conflicting bound vs. free variables is an obvious effect.

• A brief introduction to lambda calculus might be nice.

License

This code is released under the GPL. If you use this software, I'd like to know about it.

Release history

• 1.0; 2002 Feb 2. Initial release.

Author

This module was written by Erik Max Francis.

Version

Version 1.0a $Date: 2002/07/29 $ $Author: max $