Abrir menu principal

Lógica binária combinatória, do inglês binary combinatory logic (BCL) é uma formulação de lógica combinatória que utiliza somente os símbolos 0 e 1.[1] BCL tem aplicação em teoria da complexidade de programas (complexidade de Kolmogorov).[1][2]

Índice

DefiniçãoEditar

SintaxeEditar

Formalismo de Backus–Naur:

  • <term> ::= 00 | 01 | 1 <term> <term>

SemânticaEditar

A semântica denotacional de BCL pode ser especificada da seguinte maneira:

  • [ 00 ] == K
  • [ 01 ] == S
  • [ 1 <term1> <term2> ] == ( [<term1>] [<term2>] )

onde "[...]" abrevia "o sentido de ...". Aqui K e S são os combinadores da KS-base e ( ) é a operação de aplicação de lógica combinatória. (O prefixo 1 corresponde a um parênteses da esquerda, sendo o parênteses da direita desnecessário para a desambiguação.)

Portanto, existem quatro formas equivalentes de BCL, dependendo do modo como é codificada a tripla (K, S, parênteses esquerdo). As maneiras podem ser(00, 01, 1) (na versão atual), (01, 00, 1), (10, 11, 0) e (11, 10, 0).

A semântica operacional de BCL, além da eta-redução (a qual não é necessária Turing completude), pode ser especificada de maneira bastante compacta com a seguintes regras de reescrita para subtermos de um dado termo, interpretando a partir da esquerda:

  •  1100xy  → x
  • 11101xyz → 11xz1yz

onde x, y e z são subtermos arbitrários. (Note, por exemplo, que, uma vez que a interpretação é feita a partir da esquerda, 10000 não é um subtermo de 11010000.)

Veja tambémEditar

Referências

  1. a b Tromp, John (2007), "Binary lambda calculus and combinatory logic", Randomness and complexity Arquivado em 12 de maio de 2014, no Wayback Machine. (PDF), World Sci.
  2. Devine, Sean (2009), "The insights of algorithmic entropy", Entropy 11 (1): 85–110, doi:10.3390/e11010085, MR 2534819 .

Links externosEditar