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.