Combinadores SKI

Os combinadores SKI são um modelo computacional que pode ser percebido como uma versão reduzida do cálculo lambda não tipado. Ele pode ser pensado como uma linguagem de programação de computador, apesar de não ser útil para escrever software. Em vez disso, é importante na teoria matemática de algoritmos porque é uma linguagem Turing completa e extremamente simples.

Todas as operações em cálculo lambda são expressas em SKI como árvores binárias, cujas folhas são um dos três símbolos S, K e I (chamados de combinadores). Na verdade, o símbolo I está incluído apenas por conveniência, pois os outros dois são suficiente para todos os efeitos do sistema SKI.

Embora a representação mais formal dos objetos neste sistema exija árvores binárias, são representados geralmente, por typesetability, como expressões entre parênteses, quer com todas as subárvores entre parênteses, ou apenas os do lado direito das subárvores entre parênteses. Assim, a árvore cuja esquerda subárvore é a árvore KS e cuja subárvore direita é a árvore SK, normalmente é digitada como ((KS) (SK)), ou mais simplesmente como KS (SK), em vez de ser totalmente desenhado como uma árvore (como a formalidade e a legibilidade exigiria).

Descrição informal

Informalmente, na linguagem de programação, uma árvore (xy) pode ser pensada como uma "função" x aplicada a um "argumento" de y. Quando "avaliadas" (i.e., quando a função é "aplicada" ao argumento), a árvore "retorna um valor", ou seja, se transforma em outra árvore. Claro, todos os três da "função", o "argumento" e o "valor" ou são combinadores, ou árvores binárias, e se eles são árvores binárias eles também podem ser considerados como funções, sempre que for necessário.

A operação de avaliação é definida como se segue:

(x, y, representam expressões feitas a partir das funções S, K e I, e valores definidos):

I retorna seu argumento:

Ix = x

K, quando aplicado a qualquer argumento x, origina uma função constante a um argumento Kx, que, quando aplicado a qualquer tese, retorna x:

Kxy = x

S é um operador de substituição. Leva três argumentos e, em seguida, retorna o primeiro argumento aplicado ao terceiro, o qual é então aplicado ao resultado do segundo argumento aplicado ao terceiro. Mais claramente:

Sxyz = xz(yz)

Exemplo de cálculo: SKSK avaliada como KK (SK) pela regra-S. Em seguida, se avaliarmos KK (SK), obtemos K pela regra-K. Como nenhuma outra regra pode ser aplicada, o cálculo para aqui.

Note que para todas as árvores x e todas as árvores y, SKxy será sempre avaliada como y em duas etapas, Ky(xy) = y, de modo que o resultado final da avaliação SKxy sempre será igual ao resultado da avaliação y. Dizemos que SKx e Isão "funcionalmente equivalentes" porque eles sempre produzem o mesmo resultado quando aplicado a qualquer y.

Percebe-se que a partir destas definições pode ser mostrado que o cálculo SKI não é o sistema mínimo que pode desempenhar plenamente os cálculos do cálculo lambda, como todas as ocorrências do I em qualquer expressão pode ser substituída por (SKK) ou (SKS) ou (SK qualquer que seja) e a expressão resultante irá produzir o mesmo resultado. Assim, o "I" é apenas açúcar sintático.

Na verdade, é possível definir um sistema completo utilizando apenas um combinador. Um exemplo é o combinador iota de Chris Barker's, que pode ser expresso em termos de S e K como segue:

ιx = xSK

É possível reconstruir S, K e I a partir do combinador iota. Aplicando-se ι a si dá ιι = ιSK = SSKK = SK(KK) que é funcionalmente equivalente a I. K pode ser calculado aplicando ι duas vezes a I (que é equivalente à aplicação de ι a si): ι(ι(ιι)) = ι(ιI) produz ι(ISK) = ι(SK) = SKSK = K. Aplicando ι mais uma vez dá ι(ι(ι(ιι))) = ιK = KSK = S.

Definição formal

Os termos e as derivações no presente sistema podem também ser mais formalmente definidos:

Termos: O conjunto T de termos é definido recursivamente pelas seguintes regras.

1. S, K e I são termos.
2. Se τ₁ e τ₂ são termos, então (τ₁τ₂) é um termo.
3. Nada é um termo se não for necessário para ser, essas duas primeiras regras.

Derivações: uma derivação é uma sequência finita de termos definido recursivamente pelas seguintes regras (onde todas as letras gregas representam termos ou expressões com parênteses balanceados totalmente válidos):

1. Se Δ é uma derivação que termina em uma expressão da forma α(Iβ)ι, então Δ seguido pelo termo αβι é uma derivação.
2. Se Δ é uma derivação que termina em uma expressão da forma α((Kβ)γ)ι, então Δ seguido pelo termo αβι é uma derivação.
3. Se Δ é uma derivação que termina em uma expressão da forma α(((Sβ)γ)δ)ι, então Δ seguido pelo termo α((βδ)(γδ))ι é uma derivação.

Assumindo que uma sequência é uma derivação válida para começar, ela pode ser estendida utilizando estas regras.[1]

Expressões SKI

Autoaplicação e recursão

SII é uma expressão que tem um argumento e aplica esse argumento a si mesmo:

SIIα = Iα(Iα) = αα

Uma propriedade interessante deste é que faz a expressão SII(SII) irredutível:

SII(SII) = I(SII)(I(SII)) = I(SII)(SII) = SII(SII)

Outra coisa que resulta disso é que ele permite que você escreva uma função que se aplica a alguma coisa para a autoaplicação de outra coisa:

(S(Kα)(SII))β = Kαβ(SIIβ) = α(SIIβ) = α(ββ)

Esta função pode ser usada para atingir a recursividade. Se β é a função que se aplica α para a autoaplicação de outra coisa, executa beta, em seguida, a autoaplicação de alfa recursivamente em ββ. Mais claramente, se:

β = S(Kα)(SII)

então:

SIIβ = ββ = α(ββ) = α(α(ββ)) = $\ldots$

A expressão reversão

S(K(SI))K inverte os dois termos seguintes:

S(K(SI))Kαβ →

K(SI)α(Kα)β →

SI(Kα)β →

Iβ(Kαβ) →

Iβα →

βα

Lógica booleana

Os combinadores SKI também podem ser implementados em lógica booleana sob a forma de uma estrutura if-then-else. Uma estrutura if-then-else consiste em uma expressão booleana que é verdadeiro (T) ou falso (F) e dois argumentos, de forma que:

Txy = x

e

Fxy = y

A chave é a definição das duas expressões booleanas. Os primeiros trabalhos apenas como um dos nossos combinadores básicos:

T = K

Kxy = x

O segundo também é bastante simples:

F = SK

SKxy = Ky(xy) = y

Uma vez que o verdadeiro e o falso são definidos, toda a lógica booleana pode ser implementada em termos de estruturas if-then-else.

NOT booleano (que retorna o oposto de um dado booleano) funciona da mesma maneira como a estrutura if-then-else, com o F e T como segundo e terceiro valores, de modo que pode ser implementado como uma operação de postfix:

NOT = (F)(T) = (SK)(K)

Se este é colocado em uma estrutura if-then-else, pode ser mostrado que este tem o resultado esperado

(T)NOT = T(F)(T) = F

(F)NOT = F(F)(T) = T

OR booleano (que retorna T se qualquer um dos dois valores booleanos é T) funciona da mesma forma que uma estrutura if-then-else com T como o segundo valor, por isso pode ser implementado como uma operação infix:

OR = T = K

Se este é colocado em uma estrutura if-then-else, pode ser mostrado que este tem o resultado esperado

(T)OR(T) = T(T)(T) = T

(T)OR(F) = T(T)(F) = T

(F)OR(T) = F(T)(T) = T

(F)OR(F) = F(T)(F) = F

AND booleano (que retorna T se ambos os dois valores booleanos são T) funciona da mesma forma que uma estrutura if-then-else com F como o terceiro valor, por isso pode ser implementado como uma operação postfix:

AND = F = SK

Se este é colocado em uma estrutura if-then-else, pode ser mostrado que este tem o resultado esperado

(T)(T)AND = T(T)(F) = T

(T)(F)AND = T(F)(F) = F

(F)(T)AND = F(T)(F) = F

(F)(F)AND = F(F)(F) = F

Porque isso define T, F, NOT (como um operador postfix), OR (como um operador infix), e AND (como um operador postfix) em termos de notação SKI, isso prova que o sistema SKI pode expressar plenamente a lógica booleana.

Conexão com a lógica intuicionista

Os combinadores K e S correspondem a dois axiomas bem conhecidos da lógica proposicional:

AK: A → (B → A),

AS: (A → (B → C)) → ((A → B) → (A → C)).

Aplicação de função corresponde a regra modus ponens:

MP: from A and A → B, infer B.

Os axiomas AK e AS, e a regra MP estão completos para o fragmento de implicação da lógica intuicionista. Para lógica combinatória ter como modelo:

• O fragmento implicacional da logica clássica, exigiria o análogo da lógica combinatória à lei do terceiro excluído, por exemplo, lei de Peirce;
• A lógica clássica completa, exigiria o análogo da lógica combinatória para o axioma proposicional  F → A.

Veja também

• Lógica combinatória
• B,C,K,W system
• Combinador de ponto fixo
• Cálculo lambda
• Programação funcional
• Linguagem de programação Unlambda
• To Mock a Mockingbird

Referências

• Smullyan, Raymond, 1985. To Mock a Mockingbird. Knopf.  ISBN 0-394-53491-3. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
• --------, 1994. Diagonalization and Self-Reference. Oxford Univ. Press. Chpts. 17-20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
• Lambda-Calculus and Combinators: An Introduction, J. Roger Hindley & Jonathan P. Seldin, Cambridge University Press, 2nd edition (August 11, 2008), ISBN 0521898854. (Primeira edição: Introduction to Combinators and Lambda-Calculus, London Mathematical Society Student Texts 1, CUP, 1986.)