Benchmarks for Lambda Term Representations
This page contains a suite of Teyjus Lambda Prolog programs
used as benchmarks in an ongoing project at the University of
Minnesota and Hofstra University. The project studies experimentally
the tradeoffs between the alternative representation of lambda terms.
Some of these tradeoffs involve De Bruijn versus named representation
of variables, various ways to employ explicit substitutions, and the
use of annotations. Data collected from these examples were used in
the paper Tradeoffs In the Intensional Use of Lambda Terms (RTA 2002), and
in
Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts. (Submitted).
The examples are organized by the "degree" to which they use lambda-terms and
higher-order unification. Each of the following subdirectories contain
a README file with further information.
- First Order: these examples use only
first-order terms and unification.
- quicksort: a standard Prolog implementation of the familiar sorting routine.
- pubkey: An implementation of
a public
key security protocol (by Giorgio Delzanno). This program uses the new scoping devices
of Lambda Prolog.
- Reductions: these examples involve
lambda-term reduction but only first-order unification.
- hnorm: A head normalization
routine used to reduce a collection of randomly generated lambda
terms. (deprecated)
- SKI: Head normalization of random
combinations of the S, K and I combinators.
- church A program that involves arithmetic computations with
Church numerals and associated combinators.
- L-lambda: examples that involves L-lambda
(or higher order pattern) unification
- typeinf: a program that infers principal type schemes for ML-like programs.
- compiler: a compiler for a small imperative language. There is an independent page for this project.
- Higher-Order: examples that makes proper
use of higher order unification.
- hilbert: a Lambda Prolog encoding of Hilbert's Tenth Problem (by Dale Miller).
- funtrans: A set of transformers for functional programs (by Marcus Mottl).
Additional Material:
- The others directory contain additional examples yet to be employed in the
bechmark suite.
- The data directory contains complete data collected for a number of examples (used 2002).
- Spread sheet of tests from summer 2003.
legend
tar ball of benchmark suite.
Please contact Gopalan Nadathur at gopalan@cs.umn.edu or Chuck Liang at liang@cs.umn.edu for questions.