Tree Calculus

 (treecalcul.us)
1 Punkte von GN⁺ 2024-12-11 | 1 Kommentare | Auf WhatsApp teilen
  • Ein System, das Berechnungen mit minimaler Syntax aufbauen will und mit nur einem Operator △ sowie bloßer Anwendung zugleich Minimalität, Turing-Vollständigkeit, Reflexivität und Modularität abdeckt
  • Die Grammatik ist E::= △ | E E; berechnet wird, wenn △ auf drei Werte wirkt, und die Werte sind natürliche binäre Bäume aus Blatt-, Stamm- und Gabelknoten
  • Die kombinatorische Logik K und S lassen sich innerhalb des Tree Calculus ausdrücken, wodurch er Turing-vollständig ist; anders als im λ-Kalkül können rekursive Funktionen in Normalform dargestellt werden
  • Da auch Programme als Werte behandelt werden, sind Introspektion durch Selbstanwendung und Reflexion möglich; ein Beispiel ist, dass size size zu 168 ausgewertet wird
  • Unterterme treten als Unterbäume hervor, was zu Demos für das Bootstrapping gemeinsamer Funktionen, Serialisierung, Programmanalyse und -optimierung sowie statische und dynamische Typisierung führt

Natürliche binäre Bäume mit einem Operator

  • Tree Calculus wurde von Barry Jay entdeckt; auf der Website sind sein Buch und Blog sowie von Johannes Bader entwickelte Demos verlinkt
  • Die vier Kerneigenschaften werden als minimal, Turing-complete, reflective und modular zusammengefasst

  • Minimalität

    • Tree Calculus hat nur einen Operator, △
    • Die Grammatik hat die Form E ::= △ | E E
    • Visuell ist △ ein Baumknoten; wird E1 auf E2 angewendet, wird E2 rechts an die Wurzel von E1 angehängt
    • Die Werte sind natürliche binäre Bäume, deren Knoten leaf, stem und fork heißen
    • Praktische Demos
      • portability: zeigt, dass sich einfache und sichere Interpreter für mehrere Plattformen erstellen lassen
      • emit-json: zeigt ein Beispiel, das sich für die plattformübergreifende Erzeugung von Konfigurationen eignet

Turing-Vollständigkeit und Reflexion

  • Turing-Vollständigkeit

    • Die Operatoren K und S der kombinatorischen Logik lassen sich im Tree Calculus ausdrücken
    • K = △ △
    • S x = △ (△ x)
    • Da die auf K/S basierende kombinatorische Logik vollständig ist, ist auch Tree Calculus Turing-vollständig
    • Anders als im λ-Kalkül lassen sich rekursive Funktionen mit Fixpunktkonstruktionen wie orange/brown in Normalform darstellen

  • Reflexivität

    • triage {l, s, f} = △ (△ l s) f führt eine Fallunterscheidung für leaf, stem und fork durch
    • Die natürliche Zahl n lässt sich als △^n △ darstellen
    • Ein 0-Test wird als triage {true, K false, K² false} konstruiert
    • Da auch Programme Werte sind, können intensionale Programme durch Selbstanwendung Introspektion und Reflexion durchführen
    • Das Beispielprogramm size berechnet die Knotenzahl seines Arguments, und size size wird zu 168 ausgewertet
    • Praktische Demos
      • serialize-anything: behandelt die Möglichkeit der Programmserialisierung
      • halting-problem: formuliert das Halteproblem einfacher
      • fusion: drückt Programmanalyse und -optimierung als Funktionen aus
      • gradual-typing: bietet ein Beispiel, das statische und dynamische Typisierung als Funktionsaufrufe behandelt

Modularität und Demos

  • Unterterme werden als Unterbäume dargestellt
  • Das oben auf der Seite gezeigte Programm size verwendet triage, um Knoten rekursiv zu zählen
  • Praktische Demos

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-12-11
Meinungen auf Hacker News

  • Tree Calculus ist ein spannendes Thema mit Implikationen, die über diese Website hinausgehen.
    Schade ist allerdings, dass die Website Prof. Barry Jay, den Begründer und Autor, nicht ausdrücklich nennt. Wer mehr erfahren möchte, kann Jays Buch lesen: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • Auf der Seite „Specification“ wird sein Buch zwar referenziert.
      Die Quellenangabe könnte klarer sein, und das wird auch noch verbessert, aber es gibt keinerlei Absicht, sich fremde Verdienste anzueignen. Mehr Hintergrund steht in dieser Antwort: https://news.ycombinator.com/item?id=42375914
    • Als ich das sah, dachte ich zuerst an Barry Jays Bondi Language / Pattern Calculus; offenbar lag ich damit nicht völlig daneben.

  • Sieht cool aus, aber die Seite gibt viel zu wenig Orientierung, sodass es schwer zu verstehen ist.
    Eine Erklärung „für Einsteiger“ wäre gut.

    • Wie der SKI-Kalkül oder sein Verwandter, der Lambda-Kalkül, ist es ein einfaches Berechnungsmodell mit exakten Regeln, nach denen Ausdrücke mechanisch ausgewertet oder reduziert werden: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      Der Unterschied zum SKI-Kalkül besteht darin, dass es die Struktur seiner eigenen Programme reflektieren kann, zum Beispiel um zu entscheiden, ob zwei Programme gleich sind: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Außerdem konvergiert ein Programm bei Anwendung der vorgegebenen Reduktionsregeln, anders als beim Lambda-Kalkül, gegen eine stabile Normalform; Fälle, in denen man in eine unendliche Reduktionskette geraten kann, werden vermieden: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Dadurch ist Reflexion möglich, ohne Programme zu quoten oder zu serialisieren und auf stabile Datenstrukturen auszuweichen; es hat also gewisse Ähnlichkeiten mit der Homoikonizität von Lisp.
    • Die Haupt-Landingpage ist ziemlich merkwürdig aufgebaut.
      Sie verwendet einen Ein-Wort-Titel, leicht buzzwordartige Formulierungen und animierte Codebeispiele wie Websites trendiger Programmiersprachen oder Frameworks, während der Fließtext übermäßig dicht und lang im akademischen Stil gehalten ist. Zugleich enthält selbst dieser akademische Stil nicht genug Details, um zu verstehen, was eigentlich passiert.
      Ich habe eine ganze Weile versucht, die Absätze zu parsen, aber trotz der Weitschweifigkeit sagt die Seite im Grunde nur, wie bei einer normalen Landingpage für eine Programmiersprache, „was der Autor an dieser Sprache gut findet“, ohne zu erklären, wie sie funktioniert. Am Ende muss man wohl doch die Spezifikation lesen.
    • Die Grammatik E ::= t | E E in der Spezifikation verleitet beim ersten Lesen leicht zu der falschen Annahme, alle Ausdrücke sähen einfach wie t t t t t t t aus.
      Tatsächlich muss die Klammerstruktur erhalten bleiben, sodass Formen wie (t t) (t ((t t) (t t))) entstehen; auf der obersten Ebene und innerhalb jeder Klammer gibt es immer genau zwei Teilausdrücke. Das Leerzeichen verhält sich also wie ein binärer Operator.
      Da dieser Ausdruck viele Klammern enthält, betrachtet man diesen binären Operator als linksassoziativ. a b c wird als (a b) c interpretiert, a b c d als ((a b) c) d.
      So erkennt man, woher der Baum kommt. Da es nur ein einziges Blattsymbol t gibt, beginnen alle Ausdrücke nach Entfernen unnötiger Klammern immer mit t, gefolgt von mehreren Ausdrücken. Man zeichnet das erste t als Knoten und zeichnet dann für jeden folgenden Ausdruck nach demselben Verfahren einen Teilbaum.
      Die semantischen Regeln auf der Spezifikationsseite beschreiben, wie man Knoten mit drei oder mehr Teilbäumen „vereinfacht“, also wie man Ausdrücke reduziert, bei denen auf t drei oder mehr Teilausdrücke folgen.
    • Oben auf der Seite wäre ein Definitionssatz hilfreich, etwa „Tree Calculus ist eine [Nominalphrase] für [Zweckzusammenfassung]“.
      Wikipedia-Artikel beginnen ja meist mit Sätzen wie „Lambda-Kalkül ist ein formales System für …“ oder „Matrix calculus ist eine spezielle Notation für …“.
    • Kurz gesagt: Es ist eine Programmiersprache, in der Programme und Werte beide unbeschriftete Bäume sind.
      Ein unbeschrifteter Baum ist eine baumförmige Datenstruktur, deren Knoten keine Daten tragen; die Reihenfolge der Kinder ist jedoch vorhanden. Tree Calculus definiert eine Menge von Regeln, die unbeschriftete Bäume auswerten und daraus andere unbeschriftete Bäume erzeugen.
      Wendet man die Regeln wiederholt an, gerät man entweder in eine Endlosschleife oder erreicht einen Baum, der sich nicht mehr verändert. Die Regeln sind so entworfen, dass sie binäre Bäume nicht beeinflussen; wertet man einen binären Baum aus, kommt derselbe Baum heraus, und die Berechnung ist beendet.
      Diese Regeln sind auf der Seite „Specification“ in der in der Programmiersprachentheorie üblichen Form einer Small-Step-Semantik notiert.
      Die Behauptung lautet, dass die Auswertungsregeln Turing-vollständig sind, also jede Berechnung ausdrücken können, und dass die Auswertung asymptotisch optimal ist, sodass Programme jeder Sprache in Tree Calculus mit nahezu konstantem Overhead ausgeführt werden können. Auf den ersten Blick ist das keine abwegige Behauptung, aber wie wichtig das praktisch ist, ist unklar.
      Als Anwendungsgebiet ist es für einige Forschende in der Programmiersprachentheorie interessant und könnte vielleicht dazu dienen, Beweise in der Berechnungstheorie zu vereinfachen. Wenn dich so etwas interessiert, würde ich empfehlen, zuerst den Lambda-Kalkül zu lernen, der einfacher, bekannter und nützlicher ist als Tree Calculus.

  • Auf der Homepage stehen „Democratizing Functions“ und „Democratizing Metatheory“; unabhängig davon, was gemeint ist, wirkt es stark so, als werde das Wort democratizing überstrapaziert

    • Diese Verwendung ist ziemlich verbreitet
      Auch die zweite Definition von Britannica lautet „etwas für alle verfügbar machen, für alle verständlich machen“: https://www.britannica.com/dictionary/democratize
    • Stimme zu. „What democratize really means“ ist ebenfalls lesenswert: https://intage.us/articles/words/democratize/
      „Sprache wird von Kultur geformt, und du bist Teil dieser Kultur. Du musst die Verantwortung nicht abgeben. Es gibt Wahlmöglichkeiten“

  • Ich habe selbst eine Zeichnung erstellt, um die Logik der Reduktionsregeln des Tree Calculus „intuitiv“ zu verstehen: https://latypoff.com/tree-calculus-visualized/
    Für visuell denkende Menschen könnte das hilfreich sein

    • Sehr hilfreich. Besonders der sorgfältig geschriebene Text ist gut
      Allerdings scheint im zweiten Bild „Stem with a single leaf child“ ein Fehler zu sein. Die Linie, die vom Dreieck nach unten führt, geht zu einem Quadrat; dieses Quadrat müsste wohl ein Kreis sein
    • Wirklich gut. Wenn man das in eine animierbare Form brächte, würde es sehr gut auf die Specification-Seite der Website passen

  • Ich frage mich, ob die Leute, die das empfohlen haben, wirklich verstanden haben, was es ist, und es deshalb empfohlen haben

    • In meinen Augen sieht es wie eine weitere Implementierung des Lambda-Kalküls aus, und die Webseite ist enttäuschend, weil sie nicht erklärt, warum es interessant ist
    • Ich habe es empfohlen, weil ich dachte, dass daraus eine interessante Diskussion entstehen könnte
    • Ich habe es empfohlen in der Hoffnung, dass es jemand erklärt

  • Kann jemand erklären, warum das nicht einfach Lisp oder Forth mit anderer Syntax ist?
    Ich will es nicht kritisieren oder oberflächlich abtun, sondern es wirklich verstehen

    • Lisp basiert auf dem Lambda-Kalkül, aber der Lambda-Kalkül selbst hat kein Werkzeug, um Programme zu verändern, die in ihm selbst geschrieben sind
      Da diese Fähigkeit nützlich ist, wurden Lisp-Sprachen Dinge wie Makros hinzugefügt, und auch die Implementierungsweisen unterscheiden sich. Selbst das in Lisp-Sprachen verbreitete eval ist kein Teil des Lambda-Kalküls. Im Lambda-Kalkül gibt es nur Abstraktion, Anwendung und Variablen, aber keine Umgebung
      Wenn der Begriff der Reflexion gut definiert ist und Tree Calculus reflexiv ist, dann ist es sicher nicht nur Lisp mit anderer Syntax, und Forth erst recht nicht
      Ich bin kein Experte, also bitte mit Vorsicht genießen. Praktisch kann es wie ein langsames Lisp aussehen, theoretisch aber unterscheidet es sich vom Lambda-Kalkül und kann als Grundlage dienen, um etwas wie ein langsames Lisp einfacher zu implementieren
    • Wenn es keine verpflichtenden Klammern und keine Einrückungssensitivität gibt, ist das für meinen Geschmack schon ein großer Vorteil
      Andere Vorlieben sind natürlich völlig in Ordnung, aber es ist schade, dass Homoikonizität größtenteils in Lisp-Dialekten eingeschlossen ist

  • Ich habe den Z-Kombinator aus SKI über ein Beispiel im Lambda-Kalkül in Tree Calculus umgewandelt und als Baum ausgegeben
    Getestet habe ich es nicht, aber der Ursprung ist unoptimierter Code, der mit einem Tool konvertiert wurde. Hintergrund dazu siehe den Artikel über Fixpunktkombinatoren: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • Der Z-Kombinator lässt sich viel einfacher als Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)) schreiben und auch in SKI kürzer ausdrücken

  • Es freut mich zu sehen, dass Johannes mit Tree Calculus experimentiert und Möglichkeiten explizit zeigt, die in meinem Buch GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf nur implizit vorhanden waren
    Endlich gibt es einen typisierten Tree Calculus, und deshalb habe ich angefangen, auf GitHub.com/barry-jay-personal zu bloggen

    • Hier ist der funktionierende Link zum Buch: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Man muss rechts den Download-Button finden
    • Ich interessiere mich sehr für das Paper „Typed Program Analysis Without Encodings“, konnte es online aber nicht finden. Ich würde gern wissen, wo ich suchen sollte

  • Ich habe mir das eine ganze Weile angesehen und ein paar Dinge erkannt. Das könnte besonders Leuten helfen, die mit dem Lambda-Kalkül oder formaler Semantik einigermaßen vertraut sind, einen Einstieg zu finden
    Um zu verstehen, was Small-Step-Semantik bedeutet, musste ich bis zur OCaml-Implementierung hinuntergehen, weil die grundlegende Baumstruktur nicht gut zu erkennen war. Bei den vier Reduktionsformeln der Definition sieht man, was worauf angewendet wird, wenn man bei den ersten drei Termen Klammern setzt. Auch rechts scheinen Klammern zu fehlen
    Zum Beispiel sollte man es eher so lesen: (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
    Außerdem fehlen in der Tabelle Fälle, die offenbar „selbstverständlich“ aus der Assoziativität der Syntax folgen; wenn man t a -> (t a), (t a) b -> (t a b) ergänzt, lässt sich die Bedeutungsreduktion sauberer auf Ausdrücke der Grammatik E E anwenden
    Der Kern ist: So wie man im Lambda-Kalkül Lambdas bündelt, um eine von zwei Optionen „auswählen“ zu lassen, ist dieser Tree Calculus so gebaut, dass er je nachdem, ob ein gegebener Knoten ein Blatt, ein Stamm oder eine Verzweigung ist, drei Auswahlmöglichkeiten hat. Das ist der Kern der Regeln 3a, 3b und 3c, und die übrigen Funktionen des Systems bauen auf dieser dreifachen Verzweigung auf

    • Diese Erklärung hätte auf der ersten Seite stehen sollen
      Dadurch wirkt es zwar wie ein interessantes Kalkül, aber ob es sich besser als SKI oder Lambda-Kalkül für De-Kompilierung, Serialisierung und Kompilierung eignet, ist eine andere Frage. De-Kompilierung ist schwierig, Serialisierung ist einfach, und Kompilierung ist einigermaßen einfach

  • In Python kann man Leaf als leere Liste, Stem als Liste mit einem einzelnen Element und Fork als Liste mit zwei Elementen darstellen und apply entsprechend dem OCaml-Code der Spezifikation implementieren.
    Wenn man false, true und not als Bäume definiert, funktionieren not false -> true und not true -> false.

    • In Racket oder Scheme lässt sich dieselbe Idee ebenfalls verwenden.
      Leaf kann null, Stem list und Fork cons sein; mit apply t-not t-false und apply t-not t-true lässt sich dasselbe Ergebnis überprüfen.