Cálculo lambda binário

Cálculo lambda binário, do inglês binary lambda calculus (BLC), é uma técnica que utiliza o cálculo lambda para estudar a complexidade de Kolmogorov através de uma codificação binária de termos lambda, e o uso de máquina universal. O cálculo lambda binário foi uma nova ideia introduzida por John Tromp em 2004.

Contexto

O cálculo lambda binário foi projetado para fornecer uma definição concreta muito simples e elegante de complexidade descritiva (complexidade de Kolmogorov).

De uma maneira geral, a complexidade de um objeto é o comprimento da sua descrição mais curta.

De modo mais preciso, definimos descrições como cadeias de bits e identificamos um método descirtivo com algum dispositivo computacional, ou máquina que transforme descrições em objetos. Geralmente, os objetos são apenas cadeias de bits, entretanto, podem conter estrutura adicional como, por exemplo, pares de strings.

Originalmente, máquinas de Turing, o mais conhecido formalismo computacional, foram utilizadas para este propósito. Seu uso, no entanto, é dificultado pela dificuldade em sua construção e modularidade reduzida. Outro formalismo computacional clássico, o cálculo lambda, oferece vantagens distintas em termos da facilidade de uso. O cálculo lambda, contudo, não incorpora qualquer noção de entrada e saída (E/S), o que precisa ser projetado.

Entrada e Saída (E/S) Binária

Adicionar uma função primitiva de leitura de bits em cálculo lambda, como Chaitin fez em LISP, destruiria sua transparência referencial, a menos que se faça distinção entre uma ação de E/S e seu resultado, como Haskell faz com a sua E/S monádica. Mas isso requer um sistema de tipagem, o que adiciona complexidade desnecessária.

Em vez disso, BLC requer a tradução de sequências de bits em termos lambda, aos quais a máquina (também um termo lambda) pode ser prontamente aplicada.

Bits 0 e 1 são traduzidos nos booleanos lambda padrão B₀ = True and B₁ = False:

True = $\lambda x\,\lambda y.\,x$

False = $\lambda x\,\lambda y.\,y$

os quais podem ser usados diretamente para implementar o operador if-then-else.

Agora considere a função de emparelhamento

$\langle ,\rangle =\lambda x\,\lambda y\,\lambda z.\,zxy$

aplicado a dois termos M e N

$\langle M,N\rangle =\lambda z.\,zMN$.

Aplicando-se isto a um booleano, é produzido o componente de seleção desejado.

Uma string s = b₀b₁…b_n−1 é representada por um emparelhamento repetido como

$\langle B_{b_{0}},\langle B_{b_{1}}\ldots \langle B_{b_{n-1}},z\rangle \ldots \rangle \rangle$ o que denotada-se como $s:z\$.

O z que aparece na expressão acima demanda alguma explicação adicional.

Delimitado versus não delimitado

Complexidade descritiva possui duas versões distintas, as quais dependem de a entrada ser considerada delimitada ou não.

Conhecer o fim de uma entrada torna mais simples a descrição de objetos. Por exemplo, pode-se apenas copiar toda a entrada para a saída. Esta versão é chamada complexidade plana ou simples.

Entretanto, isto seria informação adicional. Um sistema de arquivos, por exemplo, precisa armazenar separadamente o comprimento de arquivos. A linguagem C usa o caractere nulo para denotar o fim de uma seqüência de caracteres, o que traz o custo de esse caractere não estar disponível para strings.

A outra versão é chamada complexidade de prefixo. Este nome origina-se dos códigos de prefixo, sobre o qual a máquina precisa descobrir, a partir da entrada que leu até o ponto atual, se é necessário ler mais bits. Diz-se que, neste caso, a entrada é auto-delimitada. Isso funciona melhor para canais de comunicação, uma vez que pode-se enviar várias descrições, uma após o outro, e ainda assim diferenciá-las.

No modelo de E/S do BLC, a versão é ditada pela escolha do z. Se for mantido como uma variável livre e for necessário ele apareça como parte da saída, então a máquina deve estar trabalhando de modo auto-delimitado. Se, por outro lado, usamos um termo lambda especificamente projetado para ser fácil de distinguir de qualquer emparelhamento, a entrada torna-se, então, delimitada. BLC escolhe False para este fim, mas lhe dá o nome mais descritivo na alternativa de Nil. Lidar com listas que podem ser Nil é simples: uma vez

$\langle x,y\rangle \ M\ N=M\ x\ y\ N$, e

$Nil\ M\ N=N$

pode-se escrever funções M e N para lidar com os dois casos, a única ressalva é que N será passado para M como seu terceiro argumento.

Universalidade

Podemos encontrar um método de descrição U tal que, para qualquer outro método de descrição D, exista uma constante c (a qual depende somente de D) de tal forma que nenhum objeto precise de mais do que c bits aidionais para descrever com o método U em vez do método D. O BLC é projetado para tornar essas constantes relativamente pequenas. De fato, a constante será o comprimento de uma codificação binária de um D-interpretador escrito em BLC e U será um termo lambda que analisa essa codificação e executa este interpretador decodificado sobre o restante da entrada. Não é preciso que U saiba se a descrição é delimitada ou não; o funcionamento é o mesmo.

Um vez resolvido o problema da tradução de cadeias de bits para cálculo lambda, agora enfrentamos o problema oposto: como codificar termos lambda em cadeias de bits?

Codificação Lambda

Primeiro, precisamos escrever nossos termos lambda em uma notação especial usando o que é conhecido como índices de De Bruijn. A codificação é a definida recursivamente da seguinte maneira

${\widehat {\lambda M}}=00{\widehat {M}}$

${\widehat {M\ N}}=01{\widehat {M}}{\widehat {N}}$

${\widehat {i}}=1^{i}0$

Por exemplo, a função de emparelhamento $\lambda x\lambda y\lambda z.zxy$ é escrita $\lambda \lambda \lambda .132$ no formato de De Bruijn, e tem codificação $00\ 00\ 00\ 01\ 01\ 10\ 1110\ 110$.

Um termo lambda fechado é aquele em que todas as variáveis estão ligadas, isto é, sem quaisquer variáveis livres. No formato de De Bruijn, isso significa que um índice i só pode aparecer dentro de pelo menos i lambdas aninhados. O número de termos fechados de n bits de tamanho é definido (sequência A114852 na OEIS).

O termo fechado mais curto possível é a função identidade ${\widehat {\lambda 1}}=0010$. No modo delimitado, esta máquina apenas copia sua entrada para a sua saída.

Então, qual é essa máquina universal U? Aqui está, em formato de De Bruijn (todos os índices são de um dígito):

$(\lambda 11)(\lambda \lambda \lambda 1(\lambda \lambda \lambda \lambda 3(\lambda 5(3(\lambda 2(3(\lambda \lambda 3(\lambda 123)))(4(\lambda 4(\lambda 31(21))))))$

$(1(2(\lambda 12))(\lambda 4(\lambda 4(\lambda 2(14)))5))))(33)2)(\lambda 1((\lambda 11)(\lambda 11)))$

Em representação binária:

0101000110100000000101011000000000011110000101111110011110

0001011100111100000011110000101101101110011111000011111000

0101111010011101001011001110000110110000101111100001111100

0011100110111101111100111101110110000110010001101000011010

(somente 232 bits (29 bytes) de tamanho)

Uma análise detalhada da máquina U pode ser encontrada em .

Complexidade, concretamente

Em geral, podemos fazer com que a complexidade de um objeto seja definida em termos de vários outros objetos fornecidos como argumento adicional para a máquina universal. Complexidade KS Plana (ou Simples) e complexidade de prefixo KP são definidas por

$KS(x|y_{1},\ldots ,y_{k})=\min\{\ell (p)\ |\ U\ (p:Nil)\ y_{1}\ \ldots \ y_{k}=\ \,x\ \ \ \ \}$

$KP(x|y_{1},\ldots ,y_{k})=\min\{\ell (p)\ |\ U\ (p:\ z\ \ )\ y_{1}\ \ldots \ y_{k}=\langle x,z\rangle \}$

Teoremas, concretamente

O programa identidade $\lambda 1$ prova que

$KS(x)\leq \ell (x)+4$

O programa $\lambda \lambda 1((\lambda 11)(\lambda \lambda \lambda \lambda 2(44)(\lambda \lambda 32(32(2(51(21)))))))(\lambda \lambda 1)(\lambda \lambda \lambda 1(\lambda 4(\lambda 4(\lambda 132))))(\lambda \lambda \lambda 1(3(\lambda \lambda 1))2)(\lambda 1)2$ prova que

$KP(x|\ell (x))\leq \ell (x)+188$

O programa

$(\lambda 11)(\lambda \lambda \lambda 1(\lambda 1(3(\lambda \lambda 1))(44(\lambda 1(\lambda \lambda \lambda 1(\lambda 4(\lambda \lambda 52(52(31(21))))))4(\lambda 1)))))(\lambda \lambda \lambda 1(3((\lambda 11)$ $(\lambda \lambda \lambda \lambda 1(\lambda 55(\lambda \lambda 356(\lambda 1(\lambda \lambda 612)3))(\lambda \lambda 5(\lambda 143)))(31))(\lambda \lambda 1(\lambda \lambda 2)2)(\lambda 1))(\lambda \lambda 1))2)$

prova que

$KP(x)\leq \ell ({\overline {x}})+338$

onde ${\overline {x}}$ é o código Levenstein para o x definido por

${\begin{array}{ll}{\overline {0}}&=0\\{\overline {n+1}}&=1\ {\overline {\ell (n)}}\ n\\\end{array}}$

onde identificamos números e bitstrings de acordo com a ordem lexicográfico. Este código tem uma propriedade para todo k,

$\ell ({\overline {n}})\leq \ell (n)+\ell (\ell (n))+\cdots +\ell ^{k-1}(n)+O(\ell ^{k}(n))$

Além disso, a ordem lexicográfica de números delimitados passa a coincidir com ordem numérica.

Número	String	Delimitado
0		0
1	0	10
2	1	110 0
3	00	110 1
4	01	1110 0 00
5	10	1110 0 01
6	11	1110 0 10
7	000	1110 0 11
8	001	1110 1 000
9	010	1110 1 001

Complexidade dos conjuntos

A complexidade de um conjunto de números naturais é a complexidade de sua seqüência característica, um termo lambda infinito no Cálculo Lambda Infinito.

O programa

$\lambda (\lambda 1(1((\lambda 11)(\lambda \lambda \lambda 1(\lambda \lambda 1)((\lambda 441((\lambda 11)(\lambda 2(11))))(\lambda \lambda \lambda \lambda 13(2(64)))))(\lambda \lambda \lambda 4(13)))))(\lambda \lambda 1(\lambda \lambda 2)2)$

cujos primeiros 100 bytes de saída são

$0011010100010100010100010000010100000100010100010000010000010100000100010100000100010000010000000100$

prova que

${\mathit {KS}}({\mathit {PRIMES}})\leq 167$ (um primo)

enquanto uma simples variação prova que

${\mathit {KP}}({\mathit {PRIMES}})\leq 176$

Isto é ainda mais curto do que a estrutura de Haskell, com 23 bytes de comprimento

 nubBy(((>1).).gcd)[2..]

Simetria da Informação

O programa

$(\lambda 1(\lambda \lambda 2)(\lambda 1(\lambda \lambda 1))(\lambda \lambda \lambda (\lambda 1(32)(\lambda \lambda 31(611(4((\lambda 11)(\lambda \lambda \lambda \lambda \lambda 12(\lambda 1(\lambda \lambda 1)(\lambda \lambda \lambda 82)(\lambda \lambda 1)(4(66)(\lambda 4(\lambda 172))))))5)$ $(\lambda \lambda 1)(\lambda \lambda \lambda \lambda 1)(\lambda \lambda 2)(\lambda \lambda 1))(\lambda \lambda \lambda 1(\lambda 164)2)))(4(\lambda 1)(\lambda 1)(\lambda 1)1))(\lambda 1))(\lambda \lambda (\lambda 11)(\lambda \lambda \lambda \lambda 1(\lambda (\lambda \lambda \lambda \lambda 3(\lambda 6(3(\lambda 2(3$ $(\lambda 14(\lambda 3(\lambda 123))))(4(\lambda 4(\lambda 14(31)(21))))))(1(2(\lambda 12))(\lambda \lambda 5(\lambda 5(\lambda 2(15)))76))(\lambda 6(\lambda 132))))(\lambda 4(\lambda 132)))(44)3))$

prova que

$KP(x,y)\leq KP(x)+KP(y|x^{\ast })+657$

onde $x^{\ast }$ é o programa mais curto para x.

Esta desigualdade representa a metade mais fácil de uma igualdade (a menos de uma constante) conhecido como Simetria de informação. Provar o inverso

$KP(y|x^{\ast })\leq KP(x,y)-KP(x)+O(1)$

envolve simular infinitamente muitos programas de maneira articulada, vendo quais terminam e devolvem como saída o par de x (para o qual um programa mais curto é dado) e algum y, e para cada programa p, solicitar uma nova palavra de código para y com comprimento $\ell (p)-KP(x)$. A desigualdade de Kraft garante que esta enumeração infinito de chamadas pode ser cumprida, e, de fato, palavras de código para y podem ser decodificadas em tempo real, juntamente com a enumeração acima. Detalhes deste resultado fundamental, realizado por Chaitin, podem ser encontradas em .

Um quine

O termo $Q=\lambda 1((\lambda 11)(\lambda \lambda \lambda \lambda \lambda 14(3(55)2)))1$ concatena duas cópias de sua entrada, provando que

$KS(xx)\leq \ell (x)+66$

Aplicá-lo à sua própria codificação devolve um quine com 132 bits:

$U({\widehat {Q}}{\widehat {Q}}:\mathrm {Nil} )={\widehat {Q}}{\widehat {Q}}$

Compressão

Até agora, vimos, de fato, muito pouco sobre um objeto em uma descrição mais curta; no último exemplo, estávamos apenas quebrando o mesmo. Para $\ell (x)>66$, entretanto, nós comprimimos $xx$ em $\ell (x)-66$ bits.

O que poderia ser o programa mais curto que produz a maior saída? O seguinte é um bom candidato: o programa $(\lambda 1111(\lambda \lambda 1(\lambda \lambda 1)2))(\lambda \lambda 2(21))$, com 55 bits de tamanho, usa Codificação de Church para devolver exatamente $2^{2^{2^{2}}}=65536$ bits. Este resultado é superior a ferramentas como gzip e bzip2, compressores que precisam de 344 e 352 bits, respectivamente, para descrever uma mesma saída (como um arquivo com 8192 bytes com um único nome de letra).

Probabilidade de parada

A probabilidade de parada da máquina universal de prefixos é definida como a probabilidade de que ela irá devolver qualquer termo que esteja na forma normal fechado (o que inclui todas as strings traduzidas):

$\Omega _{\lambda }=\sum _{U(p:z)=\langle x,z\rangle ,\,x\in NF}2^{-\ell (p)}$

Com algum esforço, podemos determinar os primeiros 4 bits deste número especial da sabedoria:

$\Omega _{\lambda }=.0001\ldots _{2}$

onde a probabilidade .0001₂ = 2⁻⁴ já é uma contribuição nos programas 00100 e 00101 em termos de True e False.

BLC8: E/S com tamanho em bytes

Enquanto fluxos de bits são bons na teoria, eles performance ruim no mundo real. A linguagem BLC8 é uma variação mais prática do BLC em que os programas operam em um fluxo de bytes, onde cada byte é representado como uma lista delimitada de 8 bits, em ordem big-endian.

BLC8 requer uma máquina universal mais complicada.

$U8=\lambda 1((\lambda 11)(\lambda (\lambda \lambda \lambda 1(\lambda \lambda \lambda 2(\lambda \lambda \lambda (\lambda 7(10(\lambda 5(2(\lambda \lambda 3(\lambda 123)))(11(\lambda 3(\lambda 31(21)))))3)$ $(4(1(\lambda 15)3)(10(\lambda 2(\lambda 2(16)))6)))8)(\lambda 1(\lambda 87(\lambda 162))))(\lambda 1(43)))(11))(\lambda \lambda 2((\lambda 11)(\lambda 11))))$

O interpretador em U8 mantém o controle dos bytes restantes e dos bits restantes no byte atual, descartando os últimos quando a análise é concluída. Assim, o tamanho do U8, que é de 355 bits em um programa BLC, passa a ser de 45 bytes em BLC8.

Brainfuck

O programa BLC8 a seguir

$(\lambda 11)(\lambda (\lambda \lambda \lambda 1(\lambda (\lambda 2111(\lambda \lambda 133(\lambda \lambda 1(\lambda \lambda (\lambda 7(1(3(\lambda \lambda \lambda \lambda \lambda {\underline {10}}(1(\lambda 6143))(\lambda 15(65432)))(\lambda \lambda 2((\lambda 11)(\lambda \lambda \lambda 2$ $(\lambda \lambda \lambda 662(\lambda \lambda 6(\lambda 1(26)3)({\underline {15}}(51(\lambda 1))(5(\lambda 1)1))))(12(\lambda \lambda \lambda 312)))1(\lambda \lambda 2)))))(3(1(\lambda \lambda \lambda \lambda 9(1(\lambda 51(\lambda 154)))$ $(24(\lambda 142))))(5({\underline {11}}(\lambda 1))({\underline {12}}(\lambda 2((\lambda 11)(\lambda \lambda \lambda 1((\lambda 11)(\lambda \lambda \lambda 2(1(33))(\lambda 8(771))))21)))))))(\lambda {\underline {12}}(\lambda {\underline {12}}(\lambda 3$ $(21))))))))(\lambda \lambda 1)))(11))(\lambda (\lambda 11)(\lambda \lambda 1((\lambda 1(1(1(\lambda \lambda 1(\lambda \lambda 2)2))))(\lambda \lambda 2(21))(\lambda \lambda 1))(22))(1(\lambda \lambda \lambda \lambda \lambda \lambda 1))1)$

é um interpretador Brainfuck com fita ilimitada em 829 bits (ou 104 bytes). A formatação obscurece a ocorrência de índices de dois dígitos: um 10 na linha 1, um 15 na linha 2, e um 11 e três 12s na linha 3. Estes índices são marcados com sublinhados para distingui-los dos índices de um dígito.

Isto fornece um bom exemplo da propriedade que métodos de descrição universais diferem em complexidade por no máximo uma constante. Escrever um intérprete BLC8 em Brainfuck, o que proporcionaria um limite superior correspondente na outra direção, fica como um exercício aos programadores Brainfuck.

O interpretador espera que a sua entrada consista de um programa Brainfuck seguido por um ] seguido pela entrada do programa Brainfuck. O interpretador só olha para os bits 0,1,4 de cada caractere para determinar qual entre ,-.+<>][ é. Portanto, quaisquer outros caracteres além destes oito serão retirados de um programa Brainfuck. Consumir mais entrada do que o disponível resulta em um erro (o resultado não-lista $\lambda x.x$).

Este interpretador é uma tradução aproximada da seguinte versão escrita em Haskell.

import System.Environment(getArgs)
import Control.Monad.State
import Control.Monad.Writer
import Control.Applicative hiding ((<|>),many)
import Text.ParserCombinators.Parsec
 
putc = do (     _,      _,b,      _) <- get; tell [b]
getc = do (  left,  right,_,b:input) <- get; put (  left,  right,     b,input)
prev = do (l:left,  right,b,  input) <- get; put (  left,b:right,     l,input)
next = do (  left,r:right,b,  input) <- get; put (b:left,  right,     r,input)
decr = do (  left,  right,b,  input) <- get; put (  left,  right,pred b,input)
incr = do (  left,  right,b,  input) <- get; put (  left,  right,succ b,input)
loop body = do (_,_,b,_) <- get; when (b /= '\0') (body >> loop body)
parseInstr = liftM loop (between (char '[') (char ']') parseInstrs)
             <|> prev <$ char '<'
             <|> next <$ char '>'
             <|> decr <$ char '-'
             <|> incr <$ char '+'
             <|> putc <$ char '.'
             <|> getc <$ char ','
             <|> return () <$ noneOf "]"
parseInstrs = liftM sequence_ (many parseInstr)
main = do [name] <- getArgs
          source <- readFile name
          input <- getContents
          let init = ("", repeat '\0', '\0', input)
          putStrLn $ either show (execWriter . (`evalStateT` init)) (parse parseInstrs name source)

Ligações externas

• John's Lambda Calculus and Combinatory Logic Playground
• A Binary Lambda Calculus interpreter in C for the IOCCC
• Counting Terms in the Binary Lambda Calculus