[Prev][Next][Index][Thread]

lambda - a program for solving lambda definability problems


An initial release of lambda, a program for solving lambda definability
problems of order at most two, is now available.

The lambda distribution consists of:

* The postscript source for the paper "Mechanizing Logical Relations",
by Allen Stoughton, which describes the theory on which lambda is
based and explains what the program does.  This paper will appear in
the proceedings of the Ninth International Conference on the
Mathematical Foundations of Programming Semantics, LNCS, vol. ?,
Springer-Verlag, 1994, pp. ?-?.  The paper's abstract is:

  We give an algorithm for deciding whether there exists a definable
  element of a finite model of an applied typed lambda calculus that
  passes certain tests, in the special case when all the constants and
  test arguments are of order at most one.  When there is such an
  element, the algorithm outputs a term that passes the tests;
  otherwise, the algorithm outputs a logical relation that demonstrates
  the nonexistence of such an element.  Several example applications of
  the C implementation of this algorithm are considered.

* 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 by anonymous ftp:

* Connect to ftp.cis.ksu.edu (129.130.10.80).

* Login as "anonymous" with your e-mail address as password.

* Change directory to pub/CIS/Stoughton/lambda.

* Put ftp in binary mode ("binary").

* Get the file lambda-tar.Z

* Exit from ftp

* Issue the command

  % zcat lambda-tar.Z | tar xf -

  This will cause a directory called lambda to be created in the
  current working directory.  (lambda contains a file README and
  four sub-directories.)

* Delete the file lambda-tar.Z (optional).

------------------------------------------------------------------------------

Comments and reports of problems should be e-mailed to
allen@cis.ksu.edu (Allen Stoughton).