On combinatory complete sets of proper combinators

Sabine Broda and Luís Damas

JFP'97

Abstract

A combinatory system (or equivalently the set of its basic
combinators) is called
combinatorially complete for a functional system, if any member of the
latter can be
defined by an entity of the former system.
In this paper the decision problem of combinatory
completeness for finite sets of proper combinators is studied for three
subsystems of the pure lambda calculus.
Precise characterizations of proper
combinator bases for the linear and the affine lambda calculus are
given and the
respective decision problems are shown to be decidable. Furthermore,
it is determined
which extensions with proper combinators of bases for the linear
lambda calculus are combinatorially complete for the lambda-I-calculus.