Lambda

Lambda is a program for solving lambda definability problems of order at most two.

The lambda distribution consists of:

The postscript source for the paper Mechanizing logical relations, which describes the theory on which lambda is based and explains what the program does.
A short manual page describing lambda.
The implementation of lambda. Lambda is written in ANSI C, with the exception of its lexical analyzer and parser, which are written in lex and yacc source, respectively. It uses one UNIX System V system call (also supported by SunOS Release 4.1). The C programs that it generates also conform to the ANSI standard; they use several UNIX System V system calls (also supported by SunOS Release 4.1) in order to implement checkpointing. The makefile that is included with the distribution is set up to use gcc, the GNU C Compiler, but can be easily changed to use another ANSI C Compiler.
A number of example lambda definability problems, together with their solutions.

To obtain a copy of the distribution:

Click here to start the transfer of the tar file lambda.tar.Z to your host.
Tell the dialog box that pops-up where lambda.tar.Z should be stored. (The trailing component of the pathname that you type should be lambda.tar.Z. If your browser automatically uncompresses .tar.Z files, then you should tell the dialog box where lambda.tar should be stored.)
Outside of your browser, issue the shell commands
```
  % uncompress lambda.tar.Z
  % tar xf lambda.tar
```
(after changing directory to the directory in which lambda.tar.Z has been stored, if necessary). This will cause a directory called lambda to be created in the current working directory. This directory will contain a file README and four sub-directories. (Omit the uncompress command, if your browser has automatically uncompressed lambda.tar.Z.)
Delete the file lambda.tar (optional).

Alternatively, you can obtain the distribution by anonymous ftp: