Lógica combinatória binária
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]
Definição[editar | editar código-fonte]
Sintaxe[editar | editar código-fonte]
- <term> ::= 00 | 01 | 1 <term> <term>
Semântica[editar | editar código-fonte]
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.)
Ver também[editar | editar código-fonte]
Referências
- ↑ 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.
- ↑ Devine, Sean (2009), "The insights of algorithmic entropy", Entropy 11 (1): 85–110, doi:10.3390/e11010085, MR 2534819 .