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
Sintaxe
Formalismo de Backus–Naur:
- <term> ::= 00 | 01 | 1 <term> <term>
Semântica
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
- Iota e Jot
- Cálculo lambda binário
Referências
Ligações externas
- John's Lambda Calculus and Combinatory Logic Playground (em inglês)