ONE POINT BASES IN LAMBDA-CALCULI WITH CONSTANTS
Mayer Goldberg
Ben Gurion University

ABSTRACT: Intuitively, a basis is a set of lambda-terms that
generates, by application, all other lambda-terms. For example, the
set {S, K}, where S = lambda a b c . ac(bc) and K = lambda a b . a, is
one of the best known bases for the lambda-K-calculus.

One-point bases (i.e., bases consisting of a single lambda-term)
constitute classical material by now, addressed, e.g., in Barendregt's
textbook on the lambda-calculus.

There is no systematic way of tackling these two scenarios in
general. Depending on the specifics of each problem and the
constraints they impose, varying degrees of intuition, educated
guesswork and knowledge about solving systems of equations are
required (e.g., Fokker's construction for a one-point basis).

Two fundamental questions about one-point bases, that we have seen
addressed in a general setting are:

- For what lambda-calculi do one-point bases exist?

- How many one-point bases exist for a given calculus?

In this work we begin to answer these questions by presenting a
systematic way by which infinitely-many one-point bases can be
constructed for lambda-calculi with at most finitely-many
constants. Starting up with a set of terms (e.g., S, K, and
finitely-many constants c_1, ... c_n, for any n) we construct a
one-point basis that generates these terms. Because we have no rules
for reducing applications of the constants to other terms, our
construction must avoid applying these constants. The approach we take
can be called ``generic packaging'' of terms: A way of combining
together terms without making any assumptions about them (e.g., that
they are combinators), in a way that lets us recover the original
terms without ever applying them in the process.