lambda - a program for solving lambda definability problems
Allen Stoughton <allen@...
1993-10-28 15:03:34 GMT
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