Compact bracket abstraction in combinatory logic
Sabine Broda and Luís Damas
Translations from lambda calculi into combinatory logics can
be used to avoid some implementational problems of the former systems.
However, this scheme can only be efficient if the translation produces
short output with a small number of combinators, in order to reduce
the time and transient storage space spent during reduction of
terms. In this paper we present a combinatory system and an
abstraction algorithm, based on the original bracket
abstraction operator of Schoenfinkel.
The algorithm introduces at most one combinator for each abstraction
in the initial lambda term. This avoids explosive term growth during
successive abstractions and makes the system suitable for practical applications.
We prove the correctness of the
algorithm and establish some relations between the combinatory
system and the lambda calculus.