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.[1]

ContextoEditar

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áriaEditar

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 B0 = True and B1 = False:

True =  
False =  

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

Agora considere a função de emparelhamento

 

aplicado a dois termos M e N

 .

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

Uma string s = b0b1bn−1 é representada por um emparelhamento repetido como

  o que denotada-se como  .

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

Delimitado versus não delimitadoEditar

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

 , e
 

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.

UniversalidadeEditar

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 LambdaEditar

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

 
 
 

Por exemplo, a função de emparelhamento   é escrita   no formato de De Bruijn, e tem codificação  .

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  . 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):

 
 

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 [1].

Complexidade, concretamenteEditar

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

 
 

Teoremas, concretamenteEditar

O programa identidade   prova que

 

O programa   prova que

 

O programa

   

prova que

 

onde   é o código Levenstein para o x definido por

 

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

 

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 conjuntosEditar

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

 

cujos primeiros 100 bytes de saída são

 

prova que

  (um primo)

enquanto uma simples variação prova que

 

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

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

Simetria da InformaçãoEditar

O programa

     

prova que

 

onde   é 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

 

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  . 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 [2].

Um quineEditar

O termo   concatena duas cópias de sua entrada, provando que

 

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

 

CompressãoEditar

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  , entretanto, nós comprimimos   em   bits.

O que poderia ser o programa mais curto que produz a maior saída? O seguinte é um bom candidato: o programa  , com 55 bits de tamanho, usa Codificação de Church para devolver exatamente   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 paradaEditar

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):

 

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

 

onde a probabilidade .00012 = 2−4 já é uma contribuição nos programas 00100 e 00101 em termos de True e False.

BLC8: E/S com tamanho em bytesEditar

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.

   

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.

BrainfuckEditar

O programa BLC8 a seguir

       

é 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  ).

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)

ReferênciasEditar

  1. a b John Tromp, Binary Lambda Calculus and Combinatory Logic, in Randomness And Complexity, from Leibniz To Chaitin, ed. Cristian S. Calude, World Scientific Publishing Company, October 2008. (The last reference, to an initial Haskell implementation, is dated 2004) (pdf version)
  2. G J Chaitin, Algorithmic information theory, Volume I in Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, October 1987, (pdf version) Arquivado em 15 de dezembro de 2011, no Wayback Machine.

Ligações externasEditar