Lógica combinatória

Lógica combinatória é uma notação introduzida por Moses Schönfinkel e Haskell Curry para eliminar a necessidade de variáveis em lógica matemática. Vem sendo mais usada recentemente na ciência da computação como um modelo de computação e como base para o desenvolvimento de linguagens de programação funcionais. Ela é baseada em combinadores, funções de ordem superior somente usam aplicações de funções e outros combinadores para definir um resultado a partir de seus parâmetros.

Matemática

A lógica combinatória visava originalmente servir como uma "pré-lógica" que clarificasse o papel das variáveis quantificadas na lógica, eliminando-as do processo. Inventor original da lógica combinatória, Moses Schönfinkel não publicou nada mais sobre o assunto após seu artigo original de 1924, e parou de publicar após a consolidação do poder de Stalin em 1929. Haskell Curry redescobriu os combinadores enquanto trabalhava como instrutor na Universidade de Princeton no final de 1927. No final da década de 1930, Alonzo Church e seus estudantes da Princeton inventaram um formalismo rival para a abstração funcional, o cálculo lambda, que se tornou mais popular que a lógica combinatória. Até que a ciência da computação tomasse interesse no assunto entre as décadas de 1960 e 1970, quase todo o trabalho no assunto foi publicado por Curry e seus estudantes, ou por Robert Feys na Bélgica. Curry e Feys (1958) e Curry et al. (1972) traçaram os primórdios dessa notação.

Ciência da computação

Na ciência da computação, a lógica combinatória é usada como um modelo simplificado de computação, usado na teoria da computabilidade e na teoria da demonstração. Apesar de sua simplicidade, ela captura diversos elementos essenciais da computação.

A lógica combinatória pode ser vista como uma variação do cálculo lambda, em que as expressões lambda (representando a abstração funcional) são substituídas por um conjunto limitado de combinadores, funções primitivas sem a presença de variáveis livres. É trivial transformar expressões lambda em expressões de combinadores, e a redução de combinadores é muito mais simples que a de lambda. Portanto, a lógica combinatória tem sido usada para modelar algumas linguagens de programação funcionais não rígidas e hardware. A visão mais pura dessa notação é a linguagem de programação Unlambda, cujas únicas primitivas são os combinadores S e K. Apesar da carência de praticidade, a linguagem promove certo interesse teórico.

Cálculo combinatório

Como a abstração é a única forma de montagem de funções em lambda cálculo, deve-se criar um substituto no cálculo combinatório. Ao invés de abstração, o cálculo combinatório prove um conjunto limitado de funções a partir das quais outras podem ser construídas.

Termos

Um termo combinatório possui uma das seguintes formas:

• $x$
• $P$
• $(E_{1}E_{2})$

em que $x$ é uma variável, $P$ é uma das funções primitivas e $(E_{1}E_{2})$ é a aplicação dos termos combinatórios $E_{1}$ e $E_{2}$. As funções primitivas são combinadores, ou funções que, quando vistas como termos lambda, não possuem variáveis livres. Para facilitar a notação, convenciona-se que $(E_{1}E_{2}E_{3}\ldots E_{n})$ ou mesmo $E_{1}E_{2}E_{3}\ldots E_{n}$ denotam o termo $(\ldots ((E_{1}E_{2})E_{3})\ldots E_{n})$. A mesma convenção é usada na aplicação múltipla do cálculo lambda.

Redução

Cada combinador primitivo possui uma regra de redução da forma:

$(Px_{1}\ldots x_{n})=E$

em que $E$ é um termo mencionando somente variáveis do conjunto $x_{1}\ldots x_{n}$. É assim que os combinadores primitivos atuam como funções.

Exemplos de combinadores

O exemplo mais simples de combinador é $I$, o combinador identidade, definido por $(Ix)=x$ para todos os termos $x$.

Outro combinador simples é $K$, que monta funções constantes. $(Kx)$ é uma função que, para qualquer parâmetro, retorna $x$, de forma que $((Kx)y)=x$ para todos os termos $x$ e $y$. Ou, a seguinte convenção para múltipla aplicação: $(Kxy)=x$.

Mais um combinador é $S$, uma forma generalizada de aplicação, de forma que $(Sxyz)=(xz(yz))$. $S$ aplica $x$ a $y$ após substituir $z$ em ambos.

Uma característica interessante é que, dados $S$ e $K$, $I$ pode ser construído da seguinte forma:

${\begin{aligned}((SKK)x)&=(SKKx)\\&=(Kx(Kx))\\&=x\\\end{aligned}}$

para qualquer termo $x$. Notar que apesar de $((SKK)x)=(Ix)$ para qualquer $x$, $(SKK)\neq I$. Diz-se que os termos são estencionalimente iguais. Esse conceito captura a noção matemática de igualidade de funções, em que duas funções são iguais se elas produzem a mesma saída para a mesma entrada. Em contraste, os termos em si, juntos com a redução dos combinadoers primitivos, capturam a noção de igualidade intencional, isto é, duas funções são iguais se e somente se elas possuem implementações idênticas até a expansão dos combinadores primitivos, quando estes são aplicados aos parâmetros. Há várias formas de implementação da função identidade, e entre elas estão $(SKK)$, $I$ e $(SKS)$. Um combinador mais interessante é o combinador de ponto fixo, ou $Y$, que pode ser usado para implementar recursividade.

Completude da base S-K

$S$ e $K$ podem ser compostas para produzir combinadores equivalentes a qualquer termo lambda, e portanto, segundo a tese de Church, para qualquer função computável. A demonstração é apresentar uma transformação $T[]$ que converte um termo lambda qualquer em um combinador equivalente. Pode-se definir $T[]$ da seguinte forma:

1. $T[x]\Rightarrow x$
2. $T[(E_{1}E_{2})]\Rightarrow (T[E_{1}]T[E_{2}])$
3. $T[\lambda x.E]\Rightarrow (KT[E])$
4. $T[\lambda x.x]\Rightarrow I$
5. $T[\lambda x.\lambda y.E]\Rightarrow T[\lambda x.T[\lambda y.E]]$
6. $T[\lambda x.(E_{1}E_{2})]\Rightarrow (ST[\lambda x.E_{1}]T[\lambda x.E_{2}])$

Esse processo é também conhecido como eliminação de abstração.

Exemplo de conversão

Por exemplo, pode-se converter o termo lambda $\lambda x.\lambda y.(yx)$ em um combinador:

${\begin{aligned}T[\lambda x.\lambda y.(yx)]&=T[\lambda x.T[\lambda y.(yx)]]\\&=T[\lambda x.(ST[\lambda y.y]T[\lambda y.x])]\\&=T[\lambda x.(SIT[\lambda y.x])]\\&=T[\lambda x.(SI(Kx))]\\&=(ST[\lambda x.(SI)]T[\lambda x.(Kx)])\\&=(S(K(SI))T[\lambda x.(Kx)])\\&=(S(K(SI))(ST[\lambda x.K]T[\lambda x.x)])\\&=(S(K(SI))(S(KK)T[\lambda x.x)])\\&=(S(K(SI))(S(KK)I))\\\end{aligned}}$

Se aplicarmos esse combinador a quaisquer termos $x$ e $y$, reduz-se da seguinte forma:

${\begin{aligned}(S(K(SI))(S(KK)I)xy)&=(K(SI)x(S(KK)Ix)y)\\&=(SI(S(KK)Ix)y)\\&=(Iy(S(KK)Ixy))\\&=(y(S(KK)Ixy))\\&=(y(KKx(Ix)y))\\&=(y(K(Ix)y))\\&=(y(Ix))\\&=(yx)\\\end{aligned}}$

Ver também

• Cálculo lambda
• Álgebra cilíndrica