[Prev][Next][Index][Thread]
lambda  a program for solving lambda definability problems

To: types@dcs.gla.ac.uk

Subject: lambda  a program for solving lambda definability problems

From: allen@cis.ksu.edu (Allen Stoughton)

Date: Thu, 28 Oct 1993 10:03:34 0500

Approved: types@dcs.gla.ac.uk
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. ?,
SpringerVerlag, 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 email address as password.
* Change directory to pub/CIS/Stoughton/lambda.
* Put ftp in binary mode ("binary").
* Get the file lambdatar.Z
* Exit from ftp
* Issue the command
% zcat lambdatar.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 subdirectories.)
* Delete the file lambdatar.Z (optional).

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