Lambda

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

The Lambda distribution consists of:

The PDF 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 (Flex) and Yacc (Bison) source, respectively. It uses one UNIX System V system call. The C programs that it generates also conform to the ANSI standard; they use several UNIX System V system calls 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. Also, the makefile is set up to use Flex and Bison, but can be easily changed to use Lex and Yacc instead.
A number of example lambda definability problems, together with their solutions.

To obtain a copy of the distribution:

Transfer the compressed tar file lambda.tar.gz to your host.
Tell the dialog box that pops-up where lambda.tar.gz should be stored. (The trailing component of the pathname that you type should be lambda.tar.gz. If your browser automatically uncompresses .tar.gz files, then you should tell the dialog box where lambda.tar should be stored.)
Outside of your browser, issue the shell commands
```
  % gunzip lambda.tar.gz
  % tar xf lambda.tar
```
(after changing directory to the directory in which lambda.tar.gz 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.txt and and four sub-directories. (Omit the gunzip, if your browser has automatically uncompressed lambda.tar.gz.)
Delete the file lambda.tar (optional).

Related links