Sobre Bases de Combinadores para Sistemas de Lambda Calculus
Sabine Broda
Departamento de Ciência de Computadores & LIACC
Faculdade de Ciências, Universidade do Porto
Rua do Campo Alegre, 823 4150 Porto, Portugal
February 1997
Abstract
In this thesis we present a study on combinator bases for the
lambda calculus, with special emphasis on three of its subsystems,
namely the lambda-I-calculus, the linear and the affine
lambda calculus. In particular, we treat aspects related to the
decidability of combinatory completeness and characterizations of (proper)
combinator bases in the four systems. We show that combinatory completeness
is decidable for finite sets of proper combinators in the linear and in the
affine lambda calculus, presenting constructive proofs which allow one to
represent any linear (resp. affine) lambda term by a combination of
elements of a given basis.
From these results follows a necessary, and easy to check, condition on arbitrary linear
(resp. affine) bases.
In the lambda-I-calculus we prove the indecidability of combinatory
completeness for finite sets of combinators in normal form, hence for
sets of combinators in general.
We give, however, a precise characterization of the lambda-I-bases which
are extensions of bases for the linear lambda calculus and, furthermore,
we establish a necessary condition on proper combinator bases in this
system.
In order to obtain other characterizations of the combinator bases in the
four systems, we study the relation between the combinatory completeness
of a set of (typable) combinators in a system of lambda calculus and
the axiomatic completeness of the respective set of principal types,
regarded
as
formulas, in the corresponding system of propositional calculus.
We show
that the two problems are equivalent in the linear and the affine systems,
and that for the other two cases axiomatic completeness is a sufficient, but
not necessary, condition for combinatory completeness.
Furthermore we
present an alternative proof for the fact that affine lambda terms in
normal form are completely determined by their principal types.
As a consequence, it follows that two linear terms are beta-convertible if and only
if they have the same principal types.
Finally we introduce the combinator
system Cl(K), together with an associated abstraction algorithm. This algorithm
represents each abstraction by only one combinator, which makes the system
particularly adequate for practical applications. We prove the correctness
of the algorithm, establish some relations between the pure
lambda calculus and the system Cl(K) and moreover we present three
subsystems that correspond respectively to the lambda-I-calculus,
the linear lambda calculus and the affine lambda calculus.
