Lógica combinatória - Combinatory logic

Não deve ser confundido com lógica combinacional , um tópico da eletrônica digital.

A lógica combinatória é uma notação para eliminar a necessidade de variáveis quantificadas na lógica matemática . Foi introduzido por Moses Schönfinkel e Haskell Curry e, mais recentemente, foi usado na ciência da computação como um modelo teórico de computação e também como base para o projeto de linguagens de programação funcional . É baseado em combinadores que foram introduzidos por Schönfinkel em 1920 com a ideia de fornecer uma maneira análoga de construir funções - e remover qualquer menção de variáveis ​​- particularmente na lógica de predicados . Um combinador é uma função de ordem superior que usa apenas aplicação de função e combinadores definidos anteriormente para definir um resultado a partir de seus argumentos.

Na matemática

A lógica combinatória foi originalmente concebida como uma 'pré-lógica' que esclareceria o papel das variáveis ​​quantificadas na lógica, essencialmente por eliminá-las. Outra maneira de eliminar variáveis ​​quantificadas é a lógica do functor de predicado de Quine . Enquanto o poder expressivo da lógica combinatória normalmente excede o da lógica de primeira ordem , o poder expressivo da lógica do functor de predicado é idêntico ao da lógica de primeira ordem ( Quine 1960, 1966, 1976 ).

O inventor original da lógica combinatória, Moses Schönfinkel , não publicou nada sobre lógica combinatória depois de seu artigo original de 1924. Haskell Curry redescobriu os combinadores enquanto trabalhava como instrutor na Universidade de Princeton no final de 1927. No final dos anos 1930, Alonzo Church e seus alunos em Princeton inventaram um formalismo rival para abstração funcional, o cálculo lambda , que se mostrou mais popular do que a lógica combinatória. O resultado dessas contingências históricas foi que, até que a ciência da computação teórica começasse a se interessar pela lógica combinatória nas décadas de 1960 e 1970, quase todos os trabalhos sobre o assunto eram de Haskell Curry e seus alunos, ou de Robert Feys na Bélgica . Curry e Feys (1958) e Curry et al. (1972) examina a história inicial da lógica combinatória. Para um tratamento mais moderno da lógica combinatória e do cálculo lambda juntos, consulte o livro de Barendregt , que analisa os modelos que Dana Scott idealizou para a lógica combinatória nas décadas de 1960 e 1970.

Em 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 prova . Apesar de sua simplicidade, a lógica combinatória captura muitos recursos essenciais da computação.

A lógica combinatória pode ser vista como uma variante do cálculo lambda , em que expressões lambda (representando abstração funcional) são substituídas por um conjunto limitado de combinadores , funções primitivas sem variáveis ​​livres . É fácil transformar expressões lambda em expressões combinadoras, e a redução combinadora é muito mais simples do que a redução lambda. Conseqüentemente, a lógica combinatória foi usada para modelar algumas linguagens de programação funcionais não estritas e hardware . A forma mais pura dessa visão é a linguagem de programação Unlambda , cujas únicas primitivas são os combinadores S e K aumentados com entrada / saída de caracteres. Embora não seja uma linguagem de programação prática, Unlambda tem algum interesse teórico.

A lógica combinatória pode receber uma variedade de interpretações. Muitos dos primeiros artigos de Curry mostraram como traduzir conjuntos de axiomas para lógica convencional em equações lógicas combinatórias (Hindley e Meredith 1990). Dana Scott nas décadas de 1960 e 1970 mostrou como casar a teoria do modelo e a lógica combinatória.

Resumo do cálculo lambda

Artigo principal: cálculo Lambda

O cálculo lambda está relacionado a objetos chamados termos lambda , que podem ser representados pelas três formas de strings a seguir:

onde é um nome de variável retirado de um conjunto infinito predefinido de nomes de variáveis ​​e e são termos lambda.

Os termos do formulário são chamados de abstrações . A variável v é chamada de parâmetro formal da abstração e é o corpo da abstração. O termo representa a função que, aplicada a um argumento, liga o parâmetro formal v ao argumento e então calcula o valor resultante de - isto é, ele retorna , com cada ocorrência de v substituída pelo argumento.

Os termos do formulário são chamados de aplicativos . Chamada ou execução de função de modelo de aplicativos: a função representada por deve ser chamada, com seu argumento, e o resultado é calculado. Se (às vezes chamado de applicand ) é uma abstração, o termo pode ser reduzido : o argumento, pode ser substituído no corpo de no lugar do parâmetro formal , eo resultado é um novo termo lambda que é equivalente à antiga 1. Se um termo lambda não contém subtermos da forma , ele não pode ser reduzido e é considerado normal .

A expressão representa o resultado de tomar o termo E e substituir todas as ocorrências livres de v nele por a . Assim nós escrevemos

Por convenção, consideramos a abreviação de (isto é, a aplicação é associativa à esquerda ).

A motivação para esta definição de redução é que ela captura o comportamento essencial de todas as funções matemáticas. Por exemplo, considere a função que calcula o quadrado de um número. Podemos escrever

O quadrado de x é

(Usando " " para indicar multiplicação.) X aqui é o parâmetro formal da função. Para avaliar o quadrado de um argumento específico, digamos 3, nós o inserimos na definição no lugar do parâmetro formal:

O quadrado de 3 é

Para avaliar a expressão resultante , teríamos que recorrer ao nosso conhecimento de multiplicação e do número 3. Uma vez que qualquer cálculo é simplesmente uma composição da avaliação de funções adequadas em argumentos primitivos adequados, este princípio de substituição simples é suficiente para capturar o mecanismo essencial de computação. Além disso, no cálculo lambda, noções como '3' e ' ' podem ser representadas sem qualquer necessidade de operadores primitivos definidos externamente ou constantes. É possível identificar termos no cálculo lambda, que, quando adequadamente interpretados, se comportam como o número 3 e como o operador de multiplicação, qv Codificação de Igreja .

O cálculo lambda é conhecido por ser computacionalmente equivalente em poder a muitos outros modelos plausíveis de computação (incluindo máquinas de Turing ); ou seja, qualquer cálculo que possa ser realizado em qualquer um desses outros modelos pode ser expresso em cálculo lambda e vice-versa. De acordo com a tese de Church-Turing , ambos os modelos podem expressar qualquer computação possível.

Talvez seja surpreendente que lambda-calculus possa representar qualquer computação concebível usando apenas as noções simples de abstração de função e aplicação com base na substituição textual simples de termos por variáveis. Mas ainda mais notável é que a abstração nem mesmo é necessária. A lógica combinatória é um modelo de computação equivalente ao cálculo lambda, mas sem abstração. A vantagem disso é que avaliar expressões no cálculo lambda é bastante complicado porque a semântica de substituição deve ser especificada com muito cuidado para evitar problemas de captura de variáveis. Em contraste, avaliar expressões em lógica combinatória é muito mais simples, porque não há noção de substituição.

Cálculos combinatórios

Visto que a abstração é a única maneira de fabricar funções no cálculo lambda, algo deve substituí-la no cálculo combinatório. Em vez de abstração, o cálculo combinatório fornece um conjunto limitado de funções primitivas a partir das quais outras funções podem ser construídas.

Termos combinatórios

Um termo combinatório tem uma das seguintes formas:

Sintaxe Nome Descrição
x Variável Um caractere ou string que representa um termo combinatório.
P Função primitiva Um dos símbolos de combinadores I , K , S .
(MN) Aplicativo Aplicando uma função a um argumento. M e N são termos combinatórios.

As funções primitivas são combinadores , ou funções que, quando vistas como termos lambda, não contêm variáveis ​​livres .

Para encurtar as notações, uma convenção geral é que , ou mesmo , denota o termo . Esta é a mesma convenção geral (associatividade à esquerda) para aplicações múltiplas no cálculo lambda.

Redução na lógica combinatória

Na lógica combinatória, cada combinador primitivo vem com uma regra de redução da forma

( P x 1 ... x n ) = E

onde E é um termo que menciona apenas variáveis ​​do conjunto { x 1 ... x n } . É dessa maneira que os combinadores primitivos se comportam como funções.

Exemplos de combinadores

O exemplo mais simples de um combinador é I , o combinador de identidade, definido por

( I x ) = x

para todos os termos x . Outro combinador simples é K , que fabrica funções constantes: ( K x ) é a função que, para qualquer argumento, retorna x , então dizemos

(( K x ) y ) = x

para todos os termos x e y . Ou, seguindo a convenção para aplicativos múltiplos,

( K x y ) = x

Um terceiro combinador é S , que é uma versão generalizada do aplicativo:

( S x yz ) = ( xz ( yz ))

S aplica- x para y após a primeira substituinte Z em cada um deles. Ou dito de outra forma, x é aplicado ay dentro do ambiente z .

Dados S e K , o próprio I é desnecessário, uma vez que pode ser construído a partir dos outros dois:

(( SKK ) x )
= ( SKK x )
= ( K x ( K x ))
= x

para qualquer termo x . Note que, embora (( SKK ) x ) = ( I x ) para qualquer x , ( SKK ) em si não é igual a eu . Dizemos que os termos são extensionalmente iguais . A igualdade extensional captura a noção matemática da igualdade das funções: que duas funções são iguais se sempre produzem os mesmos resultados para os mesmos argumentos. Em contraste, os próprios termos, junto com a redução de combinadores primitivos, capturam a noção de igualdade intensional de funções: que duas funções são iguais apenas se tiverem implementações idênticas até a expansão de combinadores primitivos. Existem muitas maneiras de implementar uma função de identidade; ( SKK ) e eu estamos entre essas formas. ( SKS ) é outra. Usaremos a palavra equivalente para indicar igualdade extensional, reservando igual para termos combinatórios idênticos.

Um combinador mais interessante é o combinador de ponto fixo ou combinador Y , que pode ser usado para implementar a recursão .

Completude da base SK

S e K podem ser compostos para produzir combinadores que são extensionalmente iguais a qualquer termo lambda e, portanto, pela tese de Church, a qualquer função computável qualquer. A prova é apresentar uma transformação, T [], que converte um termo lambda arbitrário em um combinador equivalente.

T [] pode ser definido como segue:

  1. T [ x ] => x
  2. T [( E ₁ E ₂)] => ( T [ E ₁] T [ E ₂])
  3. T [ λx . E ] => ( K T [ E ]) (se x não ocorrer livre em E )
  4. T [ λx . x ] => I
  5. T [ λx . λy . E ] => T [ λx . T [ λy . E ]] (se x ocorre livre em E )
  6. T [ λx . ( E ₁ E ₂)] => ( S T [ λx . E ₁] T [ λx . E₂ ]) (se x ocorre livremente em E ₁ ou E ₂)

Observe que T [] conforme dado não é uma função matemática bem tipada, mas sim um reescritor de termos: embora eventualmente produza um combinador, a transformação pode gerar expressões intermediárias que não são nem termos lambda nem combinadores, via regra (5).

Esse processo também é conhecido como eliminação de abstração . Esta definição é exaustiva: qualquer expressão lambda estará sujeita a exatamente uma dessas regras (consulte Resumo do cálculo lambda acima).

Está relacionado ao processo de abstração de colchetes , que toma uma expressão E construída a partir de variáveis ​​e aplicação e produz uma expressão combinadora [x] E na qual a variável x não é livre, tal que [ x ] E x = E é válido. Um algoritmo muito simples para abstração de colchetes é definido por indução na estrutura das expressões da seguinte forma:

  1. [ x ] y  : = K y
  2. [ x ] x  : = I
  3. [ x ] ( E₁ E₂ ): = S ([ x ] E₁ ) ([ x ] E₂ )

A abstração de colchetes induz uma tradução de termos lambda para expressões combinadoras, interpretando abstrações lambda usando o algoritmo de abstração de colchetes.

Conversão de um termo lambda em um termo combinatório equivalente

Por exemplo, converteremos o termo lambda λx . λy . ( y x ) a um termo combinatório:

T [ λx . λy . ( y x )]
= T [ λx . T [ λy . ( Y x )]] (por 5)
= T [ λx . ( S T [ λy . Y ] T [ λy . X ])] (por 6)
= T [ λx . ( SI T [ λy . X ])] (por 4)
= T [ λx . ( SI ( K T [ x ]))] (por 3)
= T [ λx . ( SI ( K x ))] (por 1)
= ( S T [ λx . ( SI )] T [ λx . ( K x )]) (por 6)
= ( S ( K ( SI )) T [ λx . ( K x )]) (por 3)
= ( S ( K ( SI )) ( S T [ λx . K ] T [ λx . X ])) (por 6)
= ( S ( K ( SI )) ( S ( KK ) T [ λx . X ])) (por 3)
= ( S ( K ( SI )) ( S ( KK ) I )) (por 4)

Se aplicarmos este termo combinatório a quaisquer dois termos x e y (alimentando-os em forma de fila no combinador 'da direita'), ele se reduzirá da seguinte forma:

( S ( K ( S I )) ( S ( K K ) I ) xy)
= ( K ( S I ) x ( S ( K K ) I x) y)
= ( S I ( S ( K K ) I x) y)
= ( I y ( S ( K K ) I xy))
= (y ( S ( K K ) I xy))
= (y ( K K x ( I x) y))
= (y ( K ( I x) y))
= (y ( I x))
= (yx)

A representação combinatória, ( S ( K ( SI )) ( S ( KK ) I )) é muito mais longa do que a representação como um termo lambda, λx . λy . (yx). Isso é típico. Em geral, a construção T [] pode expandir um termo lambda de comprimento n para um termo combinatório de comprimento Θ ( n 3 ).

Explicação da transformação T []

A transformação T [] é motivada por um desejo de eliminar a abstração. Dois casos especiais, regras 3 e 4, são triviais: λx . x é claramente equivalente a I e λx . E é claramente equivalente a ( K T [ E ]) se x não aparecer livre em E .

As duas primeiras regras também são simples: as variáveis ​​são convertidas em si mesmas e os aplicativos, que são permitidos em termos combinatórios, são convertidos em combinadores simplesmente convertendo o aplicativo e o argumento em combinadores.

São as regras 5 e 6 que interessam. A regra 5 simplesmente diz que para converter uma abstração complexa em um combinador, devemos primeiro converter seu corpo em um combinador e, em seguida, eliminar a abstração. A regra 6 realmente elimina a abstração.

λx . ( E ₁ E ₂) é uma função que pega um argumento, digamos a , e o substitui no termo lambda ( E ₁ E ₂) no lugar de x , resultando em ( E ₁ E ₂) [ x  : = a ] . Mas substituir a em ( E ₁ E ₂) no lugar de x é exatamente o mesmo que substituí-lo em E ₁ e E ₂, então

( E ₁ E ₂) [ x  : = a ] = ( E ₁ [ x  : = a ] E ₂ [ x  : = a ])
( λx . ( E ₁ E ₂) a ) = (( λx . E ₁ a ) ( λx . E ₂ a ))
= ( S λx . E ₁ λx . E ₂ a )
= (( S λx . E₁ λx . E ₂) a )

Por igualdade extensional,

λx . ( E ₁ E ₂) = ( S λx . E ₁ λx . E ₂)

Portanto, para encontrar um combinador equivalente a λx . ( E ₁ E ₂), é suficiente encontrar um combinador equivalente a ( S λx . E ₁ λx . E ₂), e

( S T [ λx . E ₁] T [ λx . E ₂])

evidentemente se encaixa no projeto. E ₁ e E ₂ cada um contém estritamente menos aplicações do que ( E ₁ E ₂), então a recursão deve terminar em um termo lambda sem nenhuma aplicação - uma variável ou um termo na forma λx . E .

Simplificações da transformação

redução η

Os combinadores gerados pela transformação T [] podem ser menores se levarmos em consideração a regra de redução de η :

T [ λx . ( E x )] = T [ E ] (se x não for livre em E )

λx . ( E x) é a função que recebe um argumento, x , e aplica a função E a ele; Este é adicionalmente igual à função de E em si. Portanto, é suficiente converter E para a forma combinatória.

Levando essa simplificação em consideração, o exemplo acima torna-se:

  T [ λx . λy . ( y x )]
= ...
= ( S ( K ( SI )) T [ λx . ( K x )])
= ( S ( K ( SI )) K ) (por redução de η)

Este combinador é equivalente ao anterior, mais longo:

  ( S ( K ( SI )) K x y )
= ( K ( SI ) x ( K x ) y )
= ( SI ( K x ) y )
= ( I y ( K x y ))
= ( y ( K x y ))
= ( yx )

Da mesma forma, a versão original da transformação T [] transformou a função de identidade λf . λx . ( f x ) em ( S ( S ( KS ) ( S ( KK ) I )) ( KI )). Com a regra de redução η, λf . λx . ( f x ) é transformado em I .

Base de um ponto

Existem bases de um ponto a partir das quais cada combinador pode ser composto extensionalmente igual a qualquer termo lambda. O exemplo mais simples de tal base é { X } onde:

X ≡ λx . ((X S ) K )

Não é difícil verificar que:

X ( X ( X X )) = β K e
X ( X ( X ( X X ))) = β S .

Visto que { K , S } é uma base, segue-se que { X } também é uma base. A linguagem de programação Iota usa X como seu único combinador.

Outro exemplo simples de uma base de um ponto é:

X ' ≡ λx . (X K S K ) com
( X ' X' ) X ' = β K e
X ' ( X' X ' ) = β S

Na verdade, existem infinitas bases desse tipo.

Combinadores B, C

Além de S e K , o artigo de Schönfinkel incluía dois combinadores que agora são chamados de B e C , com as seguintes reduções:

( C f g x ) = (( f x ) g )
( B f g x ) = ( f ( g x ))

Ele também explica como eles, por sua vez, podem ser expressos usando apenas S e K :

B = ( S ( KS ) K )
C = ( S ( S ( K ( S ( KS ) K )) S ) ( KK ))

Esses combinadores são extremamente úteis ao traduzir lógica de predicado ou cálculo lambda em expressões combinadoras. Eles também foram usados ​​por Curry , e muito mais tarde por David Turner , cujo nome foi associado ao seu uso computacional. Usando-os, podemos estender as regras para a transformação da seguinte maneira:

  1. T [ x ] ⇒ x
  2. T [( E₁ E₂ )] ⇒ ( T [ E₁ ] T [ E₂ ])
  3. T [ λx . E ] ⇒ ( K T [ E ]) (se x não estiver livre em E )
  4. T [ λx . x ] ⇒ I
  5. T [ λx . λy . E ] ⇒ T [ λx . T [ λy . E ]] (se x estiver livre em E )
  6. T [ λx . ( E₁ E₂ )] ⇒ ( S T [ λx . E₁ ] T [ λx . E₂ ]) (se x for livre em E₁ e E₂ )
  7. T [ λx . ( E₁ E₂ )] ⇒ ( C T [ λx . E₁ ] T [ E₂ ]) (se x for livre em E₁, mas não E₂ )
  8. T [ λx . ( E₁ E₂ )] ⇒ ( B T [ E₁ ] T [ λx . E₂ ]) (se x for livre em E₂, mas não E₁ )

Usando combinadores B e C , a transformação de λx . λy . ( y x ) tem esta aparência:

   T [ λx . λy . ( y x )]
= T [ λx . T [ λy . ( Y x )]]
= T [ λx . ( C T [ λy . Y ] x )] (pela regra 7)
= T [ λx . ( C I x )]
= ( C I ) (redução η)
= (Notação canónica tradicional: )
= (Notação canónica tradicional: )

E, de fato, ( C I x y ) se reduz a ( y x ):

   ( C I x y )
= ( I y x )
= ( y x )

A motivação aqui é que B e C são versões limitadas de S . Enquanto S pega um valor e o substitui no aplicativo e em seu argumento antes de executar a aplicação, C realiza a substituição apenas no aplicativo e B apenas no argumento.

Os nomes modernos para os combinadores vêm da tese de doutorado de Haskell Curry de 1930 (ver B, C, K, W System ). No artigo original de Schönfinkel , o que agora chamamos de S , K , I , B e C eram chamados de S , C , I , Z e T respectivamente.

A redução no tamanho do combinador que resulta das novas regras de transformação também pode ser alcançada sem a introdução de B e C , conforme demonstrado na Seção 3.2 de.

CL K versus cálculo CL I

Uma distinção deve ser feita entre o CL K conforme descrito neste artigo e o cálculo CL I. A distinção corresponde àquela entre o cálculo de λ K e o λ I. Ao contrário do cálculo λ K , o cálculo λ I restringe as abstrações a:

λx . E onde x tem, pelo menos, uma ocorrência livre na E .

Como consequência, o combinador K não está presente no cálculo λ I nem no cálculo CL I. As constantes de CL I são: I , B , C e S , que formam uma base a partir da qual todos os termos CL I podem ser compostos (igualdade de módulo). Cada termo λ I pode ser convertido em um combinador CL I igual de acordo com regras semelhantes às apresentadas acima para a conversão de termos λ K em combinadores CL K. Veja o capítulo 9 em Barendregt (1984).

Conversão reversa

A conversão L [] de termos combinatórios para termos lambda é trivial:

L [ I ] = λx . x
L [ K ] = λx . λy . x
L [ C ] = λx . λy . λz . ( x z y )
L [ B ] = λx . λy . λz . ( x ( y z ))
L [ S ] = λx . λy . λz . ( x z ( y z ))
L [( E₁ E₂ )] = ( L [ E₁ ] L [ E₂ ])

Observe, no entanto, que essa transformação não é a transformação inversa de nenhuma das versões de T [] que vimos.

Indecidibilidade do cálculo combinatório

Uma forma normal é qualquer termo combinatório no qual os combinadores primitivos que ocorrem, se houver, não são aplicados a argumentos suficientes para serem simplificados. É indecidível se um termo combinatório geral tem uma forma normal; se dois termos combinatórios são equivalentes, etc. Isso é equivalente à indecidibilidade dos problemas correspondentes para termos lambda. No entanto, uma prova direta é a seguinte:

Primeiro, o termo

Ω = ( S I I ( S I I ))

não tem forma normal, pois se reduz a si mesmo após três etapas, da seguinte forma:

   ( S I I ( S I I ))
= ( I ( S I I ) ( I ( S I I )))
= ( S I I ( I ( S I I )))
= ( S I I ( S I I ))

e claramente nenhuma outra ordem de redução pode tornar a expressão mais curta.

Agora, suponha que N fosse um combinador para detectar formas normais, de modo que

(Onde T e F representam as codificações convencionais de Church verdadeiro e falso, λx . Λy . X e λx . Λy . Y , transformados em lógica combinatória. As versões combinatórias têm T = K e F = ( K I ) .)

Agora deixe

Z = ( C ( C ( B N ( S I I )) Ω ) I )

agora considere o termo ( S I I Z ). ( S I I Z ) tem uma forma normal? Isso acontece se e somente se o seguinte também:

  ( S I I Z )
= ( I Z ( I Z ))
= ( Z ( I Z ))
= ( Z Z )
= ( C ( C ( B N ( S I I )) Ω ) I Z ) (definição de Z )
= ( C ( B N ( S I I )) Ω Z I )
= ( B N ( S I I ) Z Ω I )
= ( N ( S I I Z ) Ω I )

Agora precisamos aplicar N a ( S I I Z ). Ou ( S I I Z ) tem uma forma normal ou não. Se ele não tem uma forma normal, em seguida, o que precede reduz como se segue:

  ( N ( S I I Z ) Ω I )
= ( K Ω I ) (definição de N )
= Ω

mas Ω que não têm uma forma normal, por isso temos uma contradição. Mas se ( S I I Z ) não tem uma forma normal, o precedente se reduz da seguinte forma:

  ( N ( S I I Z ) Ω I )
= ( K I Ω I ) (definição de N )
= ( Eu eu )
= Eu

o que significa que a forma normal de ( S I I Z ) é simplesmente I , outra contradição. Portanto, o hipotético combinador de forma normal N não pode existir.

O análogo lógico combinatório do teorema de Rice diz que não existe um predicado não trivial completo. Um predicado é um elemento de combinação que, quando aplicado, retornos, quer T ou F . Um predicado N é não trivial se houver dois argumentos A e B de tal forma que N A = T e N B = M . Um combinador N é completa , se e somente se N H tem uma forma normal para cada argumento M . O análogo do teorema de Rice diz então que todo predicado completo é trivial. A prova deste teorema é bastante simples.

Prova: por reductio ad absurdum. Suponha que há um predicado trivial não completa, dizem N . Porque N é suposto ser não trivial, existem combinadores A e B tais que

( N A ) = T e
( N B ) = F .
Defina NEGAÇÃO ≡ λx . ( If ( N x ) then B else A ) ≡ λx . (( N x ) B A )
Definir ABSURDUM ≡ ( Y NEGAÇÃO )

Teorema do ponto fixo fornece: ABSURDUM = (NEGATION ABSURDUM), para

ABSURDO ≡ (NEGAÇÃO Y ) = ( NEGAÇÃO (NEGAÇÃO Y )) ≡ (NEGAÇÃO ABSURDO).

Porque N deve ser completo:

  1. ( N ABSURDUM) = F ou
  2. ( N ABSURDUM) = T
  • Caso 1: F = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N A ) = T , uma contradição.
  • Caso 2: T = ( N ABSURDUM) = N (NEGATION ABSURDUM) = ( N B ) = F , novamente uma contradição.

Logo, ( N ABSURDUM) não é nem T nem F , o que contradiz a pressuposição de que N seria um predicado não trivial completo. QED

A partir desse teorema da indecidibilidade, segue-se imediatamente que não existe um predicado completo que pode discriminar entre termos que têm uma forma normal e termos que não têm uma forma normal. Conclui-se também que não existe um predicado completo, digamos EQUAL, tal que:

(IGUAL AB ) = T se A = B e
(IGUAL AB ) = F se uma ≠ B .

Se existir IGUAL, então para todo A , λx. (EQUAL x A ) teria que ser um predicado não trivial completo.

Formulários

Compilação de linguagens funcionais

David Turner usou seus combinadores para implementar a linguagem de programação SASL .

Kenneth E. Iverson usou primitivos baseados nos combinadores de Curry em sua linguagem de programação J , um sucessor do APL . Isso possibilitou o que Iverson chamou de programação tácita , ou seja, programar em expressões funcionais sem variáveis, junto com ferramentas poderosas para trabalhar com tais programas. Acontece que a programação tácita é possível em qualquer linguagem do tipo APL com operadores definidos pelo usuário.

Lógica

O isomorfismo de Curry-Howard implica uma conexão entre lógica e programação: toda prova de um teorema de lógica intuicionista corresponde a uma redução de um termo lambda tipado, e vice-versa. Além disso, os teoremas podem ser identificados com assinaturas de tipo de função. Especificamente, uma lógica combinatória tipada corresponde a um sistema de Hilbert na teoria da prova .

Os combinadores K e S correspondem aos axiomas

AK : A → ( B → A ),
AS : ( A → ( B → C )) → (( A → B ) → ( A → C )),

e a aplicação da função corresponde à regra de desprendimento (modus ponens)

MP : a partir de um e Um → B inferir B .

O cálculo que consiste em AK , AS e MP é completo para o fragmento implicacional da lógica intuicionista, que pode ser visto como segue. Considere o conjunto W de todos os conjuntos de fórmulas dedutivamente fechados, ordenados por inclusão . Então é um quadro de Kripke intuicionista , e definimos um modelo neste quadro por

Esta definição obedece às condições de satisfação de →: por um lado, se , e é tal que e , então por modus ponens. Por outro lado, se , então pelo Teorema de dedução , assim o fecho de deductive é um elemento tal que , e .

Seja A qualquer fórmula que não seja demonstrável no cálculo. Então A não pertence ao fechamento dedutivo X do conjunto vazio, portanto , e A não é intuicionisticamente válido.

Veja também

Referências

Leitura adicional

links externos