Calcul des arbres

 (treecalcul.us)
1 points par GN⁺ 2024-12-11 | 1 commentaires | Partager sur WhatsApp
  • Un système qui cherche à construire le calcul avec une grammaire minimale, et qui traite à la fois la minimalité, la complétude de Turing, la réflexivité et la modularité avec un seul opérateur △ et l’application
  • La grammaire est E::= △ | E E, et le calcul s’effectue lorsque △ agit sur trois valeurs ; les valeurs sont des arbres binaires naturels composés de nœuds feuille, tige et embranchement
  • Il est possible d’exprimer K et S de la logique combinatoire dans Tree Calculus, ce qui lui donne la complétude de Turing ; contrairement au λ-calculus, il permet d’exprimer des fonctions récursives en forme normale
  • Les programmes étant eux aussi traités comme des valeurs, l’introspection et la réflexion par auto-application sont possibles ; il existe par exemple un cas où size size s’évalue à 168
  • Les sous-termes apparaissent comme des sous-arbres, ce qui mène à des démos comme le bootstrap de fonctionnalités communes, la sérialisation, l’analyse et l’optimisation de programmes, ainsi que le typage statique et dynamique

Des arbres binaires naturels avec un seul opérateur

  • Tree Calculus a été découvert par Barry Jay ; le site renvoie vers ses livres et son blog, ainsi que vers des démos développées par Johannes Bader
  • Les caractéristiques essentielles sont résumées en quatre points : minimal, Turing-complete, reflective, modular

  • Minimalité

    • Tree Calculus ne comporte qu’un seul opérateur, △
    • La grammaire prend la forme E ::= △ | E E
    • Visuellement, △ est un nœud d’arbre, et lorsqu’on applique E1 à E2, E2 est attaché à droite de la racine de E1
    • Les valeurs sont des arbres binaires naturels, et les nœuds sont appelés leaf, stem et fork
    • Démonstrations pratiques
      • portability: permet de créer des interpréteurs simples et sûrs sur plusieurs plateformes
      • emit-json: montre un exemple adapté à la génération de configuration cross-platform

Complétude de Turing et réflexion

  • Complétude de Turing

    • Les opérateurs K et S de la logique combinatoire peuvent être exprimés en Tree Calculus
    • K = △ △
    • S x = △ (△ x)
    • Comme la base K/S de la logique combinatoire est complète, Tree Calculus est lui aussi Turing-complete
    • Contrairement au λ-calculus, des constructions de point fixe comme orange/brown permettent d’exprimer des fonctions récursives en forme normale

  • Réflexivité

    • triage {l, s, f} = △ (△ l s) f effectue une analyse de cas sur leaf, stem et fork
    • Un entier naturel n peut être représenté par △^n △
    • Le test de zéro se construit avec triage {true, K false, K² false}
    • Comme les programmes sont aussi des valeurs, les programmes intensionnels peuvent effectuer de l’introspection et de la réflexion par auto-application
    • Le programme d’exemple size calcule le nombre de nœuds de son argument, et size size s’évalue à 168
    • Démonstrations pratiques
      • serialize-anything: traite de la possibilité de sérialiser des programmes
      • halting-problem: formule le problème de l’arrêt de manière plus simple
      • fusion: exprime l’analyse et l’optimisation de programmes sous forme de fonctions
      • gradual-typing: fournit un exemple où le typage statique et dynamique est traité comme des appels de fonction

Modularité et démos

  • Les sous-termes sont représentés comme des sous-arbres
  • Le programme size en haut de la page utilise triage pour compter récursivement les nœuds
  • Démonstrations pratiques

À lire aussi

1 commentaires

 
GN⁺ 2024-12-11
Avis sur Hacker News

  • Tree Calculus est un sujet passionnant dont les implications dépassent ce site web
    Il est toutefois dommage que le site ne mentionne pas explicitement Prof. Barry Jay, son créateur et auteur. Pour en savoir plus, on peut consulter le livre de Jay : https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • La page “Specification” fait bien référence à son livre
      L’attribution pourrait être plus claire, et elle le sera, mais il n’y a absolument aucune intention de s’approprier son travail. J’ai ajouté davantage de contexte dans cette réponse : https://news.ycombinator.com/item?id=42375914
    • En voyant ça, j’ai immédiatement pensé au Bondi Language / Pattern Calculus de Barry Jay, et il semble que je n’étais pas complètement à côté

  • Ça a l’air intéressant, mais cette page donne trop peu d’indications pour que ce soit facile à comprendre
    Une explication “pour débutants” serait bienvenue

    • Comme le calcul SKI, ou son cousin le lambda-calcul, c’est un modèle de calcul simple doté de règles exactes pour évaluer ou réduire mécaniquement des expressions : https://en.wikipedia.org/wiki/SKI_combinator_calculus
      La différence avec le calcul SKI est qu’il peut introspecter la structure de ses propres programmes, par exemple déterminer si deux programmes sont identiques : https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      De plus, contrairement au lambda-calcul, l’application des règles de réduction données fait converger un programme vers une forme normale stable, en évitant les cas où il pourrait tomber dans une chaîne infinie de réductions : https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Cela permet donc l’introspection sans devoir mettre les programmes entre guillemets ou les sérialiser pour passer par une structure de données stable, avec un côté proche de l’homoiconicité de Lisp
    • La structure de la page d’accueil principale est assez étrange
      Elle reprend les codes des sites de langages de programmation ou de frameworks à la mode, avec un titre en un mot, une phrase un peu buzzword et un exemple de code animé, mais le corps du texte est écrit dans un style académique trop dense et long. Et pourtant, ce style académique ne fournit pas assez de détails pour comprendre ce qui se passe
      J’ai passé un bon moment à analyser les paragraphes, mais malgré leur longueur, ils se contentent, comme les landing pages habituelles de langages de programmation, de dire “ce que l’auteur pense être bien dans ce langage”, sans expliquer son fonctionnement. Il faudra probablement aller lire la spécification
    • Dans la spécification, la grammaire E ::= t | E E peut donner au premier abord l’impression que toutes les expressions ressemblent simplement à t t t t t t t
      En réalité, il faut conserver la structure des parenthèses, ce qui donne des formes comme (t t) (t ((t t) (t t))), avec toujours exactement deux sous-expressions au niveau supérieur et à l’intérieur de chaque paire de parenthèses. Autrement dit, le caractère espace se comporte comme un opérateur binaire
      Comme cette expression comporte beaucoup de parenthèses, on considère cet opérateur binaire comme associatif à gauche. a b c s’interprète comme (a b) c, et a b c d comme ((a b) c) d
      Vu ainsi, on voit d’où vient l’arbre. Comme l’unique symbole terminal est t, si l’on supprime les parenthèses inutiles, toutes les expressions commencent toujours par t, suivi de plusieurs expressions. Il suffit de dessiner le premier t comme un nœud, puis, pour chaque expression qui suit, de dessiner récursivement le sous-arbre correspondant
      Les règles sémantiques de la page de spécification décrivent comment “simplifier” les nœuds ayant trois sous-arbres ou plus, autrement dit comment réduire une expression où t est suivi d’au moins trois sous-expressions
    • Il serait utile d’avoir tout en haut de la page une phrase de définition du type “Tree Calculus est [un groupe nominal] pour [résumé de l’objectif]”
      C’est la manière dont commencent généralement les articles Wikipédia, par exemple “Le lambda-calcul est un système formel pour…”, “Le calcul matriciel est une notation spécialisée pour…”
    • En résumé, c’est un langage de programmation dans lequel les programmes et les valeurs sont tous des arbres non étiquetés
      Un arbre non étiqueté est une structure de données arborescente dont les nœuds ne contiennent pas de données, mais où l’ordre des enfants compte. Tree Calculus définit un ensemble de règles permettant d’évaluer des arbres non étiquetés pour obtenir d’autres arbres non étiquetés
      Si l’on applique les règles de manière répétée, soit on tombe dans une boucle infinie, soit on atteint un arbre qui ne change plus. Les règles sont conçues pour ne pas affecter les arbres binaires : évaluer un arbre binaire renvoie donc le même arbre, et le calcul est alors terminé
      Ces règles sont écrites sur la page “Specification” sous la forme d’une sémantique à petits pas, courante en théorie des langages de programmation
      L’affirmation est que les règles d’évaluation sont Turing-complètes, donc capables d’exprimer n’importe quel calcul, et que l’évaluation est asymptotiquement optimale, si bien que le programme de n’importe quel langage peut s’exécuter dans Tree Calculus avec un surcoût presque constant. À première vue, ce n’est pas une affirmation absurde, mais son importance réelle n’est pas évidente
      Quant à l’usage, cela peut intéresser certains chercheurs en théorie des langages de programmation, et éventuellement simplifier des preuves en théorie du calcul. Si ce genre de sujet vous intéresse, je recommanderais d’apprendre d’abord le lambda-calcul, qui est plus simple, plus connu et plus utile que Tree Calculus

  • La page d’accueil parle de « Democratizing Functions » et de « Democratizing Metatheory » ; quel que soit le sens voulu, j’ai fortement l’impression que le mot democratizing est employé à l’excès

    • Cet usage est assez courant
      La deuxième définition de Britannica est aussi « rendre quelque chose accessible à tous, rendre quelque chose compréhensible par tous » : https://www.britannica.com/dictionary/democratize
    • D’accord. « What democratize really means » vaut aussi le détour : https://intage.us/articles/words/democratize/
      « La langue est façonnée par la culture, et vous faites partie de cette culture. Vous n’avez pas à renoncer à votre responsabilité. Vous avez le choix »

  • Pour comprendre « à l’instinct » la logique des règles de réduction du Tree Calculus, j’ai fait moi-même des schémas : https://latypoff.com/tree-calculus-visualized/
    Cela peut aider les personnes qui pensent visuellement

    • Très utile. J’apprécie particulièrement le texte, écrit avec soin
      En revanche, il semble y avoir une erreur dans la deuxième figure, « Stem with a single leaf child ». La ligne qui descend du triangle mène à un carré, mais ce carré devrait apparemment être un cercle
    • Vraiment excellent. Si on en faisait une version animable, elle irait très bien sur la page Specification du site

  • Je me demande si les personnes qui ont recommandé ça comprenaient vraiment ce que c’était

    • À mes yeux, cela ressemble à une autre implémentation du lambda-calcul, et je trouve dommage que la page web n’explique pas pourquoi c’est intéressant
    • Je l’ai recommandé parce que je pensais que cela donnerait lieu à une discussion intéressante
    • Je l’ai recommandé en espérant que quelqu’un l’explique

  • Quelqu’un peut-il expliquer pourquoi ce n’est pas simplement Lisp ou Forth avec une syntaxe différente ?
    Ce n’est pas pour critiquer ni pour balayer le sujet comme superficiel ; je veux vraiment comprendre

    • Lisp repose sur le lambda-calcul, mais le lambda-calcul lui-même n’a pas d’outils permettant de modifier les programmes écrits en son sein
      Comme cette fonctionnalité est utile, les langages de la famille Lisp y ont ajouté des choses comme les macros, avec des modes d’implémentation variés. Même eval, courant dans la famille Lisp, ne fait pas partie du lambda-calcul. Le lambda-calcul n’a que l’abstraction, l’application et les variables ; il n’a pas d’environnement
      Si la notion de réflexion y est bien définie et que Tree Calculus est réflexif, alors ce n’est clairement pas juste Lisp avec une autre syntaxe, et encore moins Forth
      Je ne suis pas spécialiste, donc à prendre avec beaucoup de recul. En pratique, cela peut ressembler à un Lisp lent, mais théoriquement c’est différent du lambda-calcul, et cela peut servir de base plus simple pour implémenter quelque chose qui ressemble à un Lisp lent
    • S’il n’y a ni parenthèses obligatoires ni sensibilité à l’indentation, c’est déjà un gros avantage à mon goût
      Les autres préférences sont évidemment tout à fait valables, mais je trouve dommage que l’homoiconicité soit en grande partie confinée aux dialectes de Lisp

  • J’ai pris le combinateur Z de SKI, je l’ai converti en Tree Calculus en passant par un exemple en lambda-calcul, puis je l’ai affiché sous forme d’arbre
    Je ne l’ai pas testé, mais l’original est du code non optimisé converti par un outil. Pour le contexte, voir l’article sur les combinateurs de point fixe : https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Le combinateur Z peut s’écrire beaucoup plus simplement sous la forme Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)), et il peut aussi être exprimé plus brièvement en SKI

  • Je suis content de voir Johannes expérimenter avec Tree Calculus et rendre explicites des possibilités qui n’étaient qu’implicites dans mon livre GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf
    Il existe enfin un Tree Calculus typé, et j’ai donc commencé à tenir un blog sur GitHub.com/barry-jay-personal

    • Voici un lien fonctionnel vers le livre : https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Il suffit de chercher le bouton de téléchargement à droite
    • Je suis très intéressé par l’article « Typed Program Analysis Without Encodings », mais je n’arrive pas à le trouver en ligne. Où devrais-je regarder ?

  • J’ai passé un bon moment à examiner tout ça et j’en ai tiré quelques enseignements. Cela peut notamment aider les personnes qui connaissent déjà un peu le lambda-calcul ou la sémantique formelle à prendre pied
    Pour comprendre ce que voulait dire la sémantique à petits pas, j’ai dû descendre jusqu’à l’implémentation OCaml, parce que la structure d’arbre de base n’était pas très visible. Dans les réductions à quatre éléments de la définition, si l’on met des parenthèses autour des trois premiers termes, on voit ce qui est appliqué à quoi. Il semble aussi manquer des parenthèses à droite
    Par exemple, il vaut mieux lire cela comme (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
    Le tableau omet aussi des cas qui semblent considérés comme découlant « évidemment » de l’associativité de la syntaxe ; si on ajoute t a -> (t a), (t a) b -> (t a b), on peut appliquer plus proprement la réduction sémantique aux expressions de la grammaire E E
    L’idée centrale est que, de même qu’en lambda-calcul on regroupe les lambdas pour faire « choisir » l’une de deux options, ce Tree Calculus est conçu pour effectuer trois choix selon que le nœud donné est une feuille, une tige ou une branche. C’est le cœur des règles 3a, 3b et 3c, et le reste des fonctionnalités du système est construit sur ce choix à trois branches

    • Cette explication aurait dû figurer sur la première page
      Grâce à elle, cela ressemble bien à un calcul intéressant, mais savoir s’il est plus adapté que SKI ou le lambda-calcul à la rétroconversion, à la sérialisation ou à la compilation est une autre question. La rétroconversion est difficile, la sérialisation est facile, et la compilation est relativement facile

  • En Python, on peut représenter Leaf par une liste vide, Stem par une liste à un seul élément, et Fork par une liste à deux éléments, puis implémenter apply conformément au code OCaml de la spécification
    Si l’on définit false, true et not sous forme d’arbres, not false -> true et not true -> false fonctionnent

    • On peut utiliser la même idée en Racket ou en Scheme
      Il suffit de représenter Leaf par null, Stem par list et Fork par cons, puis de vérifier le même résultat avec apply t-not t-false et apply t-not t-true