A new translation algorithm from Lambda Calculus
into Combinatory Logic

Sabine Broda and Luís Damas

EPIA'95

Abstract

Systems of lambda calculus are of importance for most
knowledge representation theories and in particular for several systems
for Natural Language Processing. During the implementation of
lambda systems several problems arise, which are directly related to
the presence of bounded variables. These problems can be avoided using
translations from lambda calculus into combinatory systems, which
give origin to extremely simple reduction machines.
In this article we present and prove the correctness of a translation
algorithm, that, when compared with other systems, has quite good
properties in terms of
memory space as well as in terms of length of evaluations.