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
Fevereiro de 1997
Abstract
Nesta dissertação apresentamos um estudo sobre
bases de combinadores no lambda calculus, dando
ênfase especial a
três dos seus subsistemas, nomeadamente ao lambda-I-calculus, ao
lambda calculus linear e ao lambda calculus afim.
Em particular,
abordamos noções relacionadas
com a decidibilidade da completude combinatória e com a caracterização das
bases de
combinadores (próprios) dos quatro
sistemas referidos.
Mostramos a decidibilidade da completude combinatória para conjuntos
finitos de combinadores próprios no lambda calculus linear e no
lambda calculus afim, apresentando provas construtivas que permitem
representar qualquer lambda termo linear (resp. afim) a partir de uma
base de combinadores próprios dada.
Destes resultados segue uma condição necessária, facilmente
verificável, para
bases de combinadores lineares (resp. afins) em geral.
No lambda-I-calculus provamos a indecidibilidade do mesmo problema
para bases de combinadores em forma normal e consequentemente para bases em
geral. Apresentamos no entanto uma caracterização das bases deste sistema,
que são
extensões de bases lineares com combinadores próprios e estabelecemos
também uma condição necessária sobre as bases finitas de combinadores
próprios.
Com o propósito de obter outras caracterizações das bases de
combinadores
nos quatro sistemas considerados,
relacionamos ainda a completude combinatória de
um conjunto de combinadores (tipáveis) num sistema de
lambda calculus e a completude axiomática do conjunto dos
respectivos tipos principais, interpretados como fórmulas, no
cálculo proposicional minimal correspondente à versão tipada do
sistema de lambda calculus.
Mostramos que se verifica a equivalência dos respectivos
problemas somente no sistema linear e no sistema afim, enquanto
que nos restantes casos a completude axiomática é condição suficiente,
mas não necessária,
para a completude combinatória.
Apresentamos ainda uma prova alternativa para o facto de qualquer
lambda termo
afim em forma normal ficar completamente determinado pelo seu tipo
principal, donde resulta a equivalência da igualdade, módulo-beta,
entre lambda termos lineares e da igualdade, a menos de variantes, entre
os respectivos tipos principais.
Finalmente introduzimos o sistema
combinatório CL(K), juntamente com um
algoritmo de abstracção associado. Este algoritmo permite representar
cada
abstracção por um só combinador, o que torna o sistema particularmente
adequado para aplicações prácticas. Mostramos a correcção do algoritmo,
estabelecemos algumas relações entre o lambda calculus puro e o sistema
CL(K) e apresentamos ainda três subsistemas, que correspondem
respectivamente ao lambda-I-calculus, ao lambda calculus linear e
ao lambda calculus afim.
