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.

1. First Order: these examples use only first-order terms and unification.
   1. quicksort: a standard Prolog implementation of the familiar sorting routine.
   2. pubkey: An implementation of a public key security protocol (by Giorgio Delzanno). This program uses the new scoping devices of Lambda Prolog.
2. Reductions: these examples involve lambda-term reduction but only first-order unification.
   1. hnorm: A head normalization routine used to reduce a collection of randomly generated lambda terms. (deprecated)
   2. SKI: Head normalization of random combinations of the S, K and I combinators.
   3. church A program that involves arithmetic computations with Church numerals and associated combinators.
3. L-lambda: examples that involves L-lambda (or higher order pattern) unification
   1. typeinf: a program that infers principal type schemes for ML-like programs.
   2. compiler: a compiler for a small imperative language. There is an independent page for this project.
4. Higher-Order: examples that makes proper use of higher order unification.
   1. hilbert: a Lambda Prolog encoding of Hilbert's Tenth Problem (by Dale Miller).
   2. 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

Please contact Gopalan Nadathur at gopalan@cs.umn.edu or Chuck Liang at liang@cs.umn.edu for questions.