Cálculo de Árvores

 (treecalcul.us)
1 pontos por GN⁺ 2024-12-11 | 1 comentários | Compartilhar no WhatsApp
  • Um sistema que busca compor computações com o mínimo de sintaxe, tratando minimalidade, completude de Turing, reflexão e modularidade usando apenas um operador △ e aplicação
  • A gramática é E::= △ | E E, e quando △ atua sobre três valores ocorre a computação; os valores são árvores binárias naturais formadas por nós folha, caule e bifurcação
  • É possível expressar K e S da lógica combinatória dentro do Tree Calculus, o que lhe dá completude de Turing; ao contrário do λ-calculus, funções recursivas podem ser expressas em forma normal
  • Como programas também são tratados como valores, introspecção e reflexão por autoaplicação são possíveis, e há um exemplo em que size size é avaliado como 168
  • Subtermos aparecem como subárvores, o que leva a demos de bootstrap de funcionalidades comuns, serialização, análise e otimização de programas, e tipagem estática e dinâmica

Árvores binárias naturais com um único operador

  • O Tree Calculus foi descoberto por Barry Jay, e o site traz links para seu livro e blog, além de demos desenvolvidas por Johannes Bader
  • As características centrais são resumidas em quatro pontos: minimal, Turing-complete, reflective e modular

  • Minimalidade

    • No Tree Calculus existe apenas um operador, △
    • A gramática tem a forma E ::= △ | E E
    • Visualmente, △ é um nó de árvore, e ao aplicar E1 a E2, E2 é anexado à direita da raiz de E1
    • Os valores são árvores binárias naturais, e os nós são chamados de leaf, stem e fork
    • Demos práticas
      • portability: permite criar interpretadores simples e seguros em várias plataformas
      • emit-json: mostra um exemplo adequado para geração de configurações multiplataforma

Completude de Turing e reflexão

  • Completude de Turing

    • Os operadores K e S da lógica combinatória podem ser expressos em Tree Calculus
    • K = △ △
    • S x = △ (△ x)
    • Como a base K/S da lógica combinatória é completa, o Tree Calculus também é Turing-complete
    • Diferentemente do λ-calculus, construções de ponto fixo como orange/brown permitem expressar funções recursivas em forma normal

  • Reflexão

    • triage {l, s, f} = △ (△ l s) f realiza análise de casos para leaf, stem e fork
    • Um número natural n pode ser representado como △^n △
    • O teste de zero é construído como triage {true, K false, K² false}
    • Como programas também são valores, programas intensional podem realizar introspecção e reflexão por autoaplicação
    • O programa de exemplo size calcula o número de nós do argumento, e size size é avaliado como 168
    • Demos práticas
      • serialize-anything: trata da possibilidade de serializar programas
      • halting-problem: formula o problema da parada de forma mais simples
      • fusion: expressa análise e otimização de programas como funções
      • gradual-typing: oferece um exemplo de tratamento de tipagem estática e dinâmica como chamadas de função

Modularidade e demos

  • Subtermos são representados como subárvores
  • O programa size no topo da página usa triage para contar nós recursivamente
  • Demos práticas

Leituras relacionadas

1 comentários

 
GN⁺ 2024-12-11
Opiniões no Hacker News

  • Tree Calculus é um tema fascinante, com implicações que vão além deste site
    Só é uma pena que o site não destaque explicitamente o criador e autor, Prof. Barry Jay. Se quiser saber mais, vale ver o livro de Jay: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • A página “Specification” até referencia o livro dele
      A atribuição poderia ser mais clara, e vamos torná-la mais clara, mas não há nenhuma intenção de tomar o crédito. Deixei mais contexto nesta resposta: https://news.ycombinator.com/item?id=42375914
    • Assim que vi isso, pensei primeiro na Bondi Language / Pattern Calculus do Barry Jay, então parece que eu não estava totalmente fora da pista

  • Parece interessante, mas esta página dá orientação de menos, então é difícil entender
    Seria bom ter algo como uma explicação “para iniciantes”

    • Assim como o cálculo SKI ou seu primo, o cálculo lambda, é um modelo simples de computação com regras exatas para avaliar ou reduzir expressões mecanicamente: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      A diferença em relação ao cálculo SKI é que ele consegue refletir sobre a estrutura dos próprios programas; por exemplo, é possível determinar se dois programas são iguais: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Além disso, ao contrário do cálculo lambda, aplicar as regras de redução dadas faz o programa convergir para uma forma normal estável, evitando casos em que ele poderia cair em uma cadeia infinita de reduções: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Por isso, a reflexão é possível sem precisar colocar o programa entre aspas ou serializá-lo para contornar o problema usando uma estrutura de dados estável, e há um aspecto parecido com a homoiconicidade do Lisp
    • A composição da landing page principal é bem estranha
      Ela usa um título de uma palavra, uma frase meio buzzword e exemplos de código em movimento, como sites de linguagens de programação ou frameworks da moda, mas o corpo do texto é acadêmico demais, denso e longo. Só que esse estilo acadêmico, por si só, não traz detalhes suficientes para entender o que está acontecendo
      Passei um bom tempo tentando destrinchar os parágrafos, mas, apesar da verbosidade, como uma landing page comum de linguagem de programação, ela só diz “o que o autor acha bom nesta linguagem” e não explica como ela funciona. No fim, parece que é preciso olhar a especificação
    • A gramática da especificação, E ::= t | E E, à primeira vista facilita a impressão equivocada de que todas as expressões simplesmente parecem t t t t t t t
      Na prática, é preciso preservar a estrutura de parênteses, então elas têm formas como (t t) (t ((t t) (t t))), e no nível superior e dentro de cada parêntese sempre há exatamente duas subexpressões. Ou seja, o caractere de espaço funciona como um operador binário
      Como essa expressão tem muitos parênteses, esse operador binário é visto como associativo à esquerda. a b c é interpretado como (a b) c, e a b c d como ((a b) c) d
      Vendo dessa forma, dá para perceber de onde vem a árvore. Como há apenas um símbolo terminal, t, ao remover os parênteses desnecessários, toda expressão sempre começa com t e é seguida por várias expressões. Basta desenhar o primeiro t como um nó e, para cada expressão seguinte, desenhar uma subárvore pelo mesmo procedimento
      As regras semânticas da página de especificação dizem como “simplificar” um nó com três ou mais subárvores, isto é, como reduzir uma expressão em que t é seguido por três ou mais subexpressões
    • Ajudaria se no topo da página houvesse uma frase de definição, como “Tree Calculus é [um sintagma nominal] para [resumo do objetivo]”
      É o jeito como artigos da Wikipédia costumam começar, por exemplo: “Lambda calculus é um sistema formal para…”, “Matrix calculus é uma notação especializada para…”
    • Em resumo, é uma linguagem de programação em que programas e valores são todos árvores sem rótulos
      Uma árvore sem rótulos é uma estrutura de dados em árvore cujos nós não têm dados, mas em que a ordem dos filhos existe. Tree Calculus define um conjunto de regras que avalia árvores sem rótulos e produz outras árvores sem rótulos
      Ao aplicar as regras repetidamente, ou você cai em um loop infinito, ou chega a uma árvore que não muda mais. As regras foram projetadas para não afetar árvores binárias; portanto, ao avaliar uma árvore binária, o resultado é a mesma árvore, em um estado em que a computação terminou
      Essas regras estão escritas na página “Specification” no formato de semântica de pequenos passos, comum na teoria de linguagens de programação
      A alegação é que as regras de avaliação são Turing-completas, então qualquer computação pode ser expressa, e que a avaliação é assintoticamente ótima, de modo que programas de qualquer linguagem podem ser executados em Tree Calculus com uma sobrecarga quase constante. À primeira vista, não parece uma afirmação absurda, mas não está claro o quanto isso é realmente importante
      A utilidade disso pode ser interessante para alguns pesquisadores de teoria de linguagens de programação e talvez sirva para simplificar provas em teoria da computação. Se esse tipo de coisa interessa, eu recomendaria aprender primeiro o cálculo lambda, que é mais simples, mais conhecido e mais útil que Tree Calculus

  • Na página inicial aparece “Democratizing Functions”, “Democratizing Metatheory”, mas, seja lá o que isso queira dizer, dá uma forte sensação de uso abusivo da palavra democratizing

  • Fiz um desenho por conta própria para tentar entender “no tato” a lógica das regras de redução do Tree Calculus: https://latypoff.com/tree-calculus-visualized/
    Pode ajudar quem pensa visualmente

    • Ajuda muito. Gosto especialmente do texto escrito com cuidado
      Mas parece haver um erro na segunda figura, “Stem with a single leaf child”. A linha que desce do triângulo vai para um quadrado, mas acho que esse quadrado deveria ser um círculo
    • Muito bom. Se isso fosse feito em uma forma animável, combinaria muito bem com a página Specification do site

  • Fico curioso se as pessoas que recomendaram isso realmente entenderam o que é antes de recomendar

    • Aos meus olhos, parece mais uma implementação do cálculo lambda, e a página web também decepciona por não explicar por que isso é interessante
    • Recomendei porque achei que poderia gerar uma discussão interessante
    • Recomendei na esperança de que alguém explicasse

  • Alguém consegue explicar por que isso não é apenas Lisp ou Forth com outra sintaxe?
    Não estou criticando nem tentando descartar de forma rasa; quero mesmo entender

    • Lisp se baseia no cálculo lambda, mas o cálculo lambda em si não tem ferramentas para modificar programas escritos dentro dele próprio
      Como essa funcionalidade é útil, linguagens da família Lisp foram acrescentando coisas como macros, com várias formas de implementação. Mesmo o eval, comum na família Lisp, não faz parte do cálculo lambda. No cálculo lambda há apenas abstração, aplicação e variáveis; não há ambiente
      Se o conceito de reflexão é bem definido e o Tree Calculus é reflexivo, então ele definitivamente não é apenas Lisp com outra sintaxe, e muito menos Forth
      Não sou especialista, então leve isso com bastante cautela. Na prática, pode parecer um Lisp lento, mas, teoricamente, é diferente do cálculo lambda e pode servir como base para implementar de modo mais simples algo parecido com um Lisp lento
    • Se não houver parênteses obrigatórios nem sensibilidade a indentação, para o meu gosto isso já é uma grande vantagem
      Outros gostos são obviamente válidos, mas é uma pena que a homoiconicidade esteja em grande parte confinada aos dialetos de Lisp

  • Peguei o combinador Z do SKI, passei por um exemplo em cálculo lambda, converti para Tree Calculus e gerei a saída como árvore
    Não testei, mas o original é código não otimizado convertido por uma ferramenta. Para o contexto relacionado, veja o artigo sobre combinadores de ponto fixo: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • O combinador Z pode ser escrito de forma muito mais simples como Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)), e também pode ser expresso de modo mais curto em SKI

  • É bom ver Johannes experimentando com Tree Calculus e mostrando explicitamente possibilidades que estavam apenas implícitas no meu livro GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf
    Finalmente existe um Tree Calculus tipado, e por isso comecei a escrever um blog em GitHub.com/barry-jay-personal

  • Passei um bom tempo olhando para isso e tive algumas percepções. Elas podem ajudar especialmente quem já tem alguma familiaridade com cálculo lambda ou semântica formal a encontrar um ponto de apoio
    Tive de descer até a implementação em OCaml para entender o que a semântica de pequenos passos queria dizer, porque a estrutura básica de árvore não estava bem visível. Nas quatro fórmulas de redução dos elementos da definição, se você colocar parênteses nos três primeiros termos, dá para ver o que está sendo aplicado a quê. No lado direito também parecem faltar parênteses
    Por exemplo, é melhor ler como (t (t) a) b -> a, (t (t a) b) c -> (a c) (b c), (t (t a b) c) t -> a, (t (t a b) c) (t u) -> b u, (t (t a b) c) (t u v) -> (c u) v
    Além disso, a tabela omite casos que aparentemente foram considerados “óbvios” pela associatividade da gramática; se você acrescentar t a -> (t a), (t a) b -> (t a b), fica mais limpo aplicar a redução semântica às expressões da gramática E E
    O ponto central é que, assim como no cálculo lambda se amarra uma lambda para fazê-la “escolher” uma entre duas opções, este Tree Calculus foi feito para realizar três escolhas conforme um dado nó seja folha, caule ou ramo. Esse é o núcleo das regras 3a, 3b e 3c, e o restante da funcionalidade do sistema é construído sobre essa escolha em três vias

    • Essa explicação deveria estar na primeira página
      Graças a ela, parece uma forma de cálculo interessante, mas outra questão é se ela é mais adequada que SKI ou cálculo lambda para descompilação, serialização e compilação. Descompilação é difícil, serialização é fácil, e compilação é razoavelmente fácil

  • Em Python, é possível representar Leaf como uma lista vazia, Stem como uma lista de um único elemento e Fork como uma lista de dois elementos, implementando apply de acordo com o código OCaml da especificação
    Ao definir false, true e not como árvores, not false -> true e not true -> false funcionam

    • Também é possível usar a mesma ideia em Racket ou Scheme
      Basta representar Leaf como null, Stem como list e Fork como cons, e verificar o mesmo resultado com apply t-not t-false e apply t-not t-true