Cálculo de árboles

 (treecalcul.us)
1 puntos por GN⁺ 2024-12-11 | 1 comentarios | Compartir por WhatsApp
  • Un sistema que busca construir cómputos con una sintaxis mínima; con un solo operador △ y la aplicación aborda minimalidad, completitud de Turing, reflexión y modularidad
  • La sintaxis es E::= △ | E E; cuando △ actúa sobre tres valores se computa, y los valores son árboles binarios naturales compuestos por nodos hoja, tallo y bifurcación
  • Como K y S de la lógica combinatoria pueden expresarse dentro de Tree Calculus, tiene completitud de Turing; a diferencia del λ-calculus, puede expresar funciones recursivas en forma normal
  • Como los programas también se tratan como valores, permite introspección y reflexión mediante autoaplicación; hay un ejemplo en el que size size se evalúa a 168
  • Los subtérminos aparecen como subárboles, lo que lleva a demos como bootstrap de funciones comunes, serialización, análisis y optimización de programas, y tipado estático y dinámico

Árboles binarios naturales creados con un solo operador

  • Tree Calculus fue descubierto por Barry Jay, y el sitio enlaza su libro y blog, además de demos desarrolladas por Johannes Bader
  • Sus características clave se resumen en cuatro: minimal, Turing-complete, reflective y modular

  • Minimalidad

    • Tree Calculus tiene un único operador, △
    • La sintaxis tiene la forma E ::= △ | E E
    • Visualmente, △ es un nodo de árbol, y al aplicar E1 a E2, E2 se adjunta a la derecha de la raíz de E1
    • Los valores son árboles binarios naturales, y los nodos se llaman leaf, stem y fork
    • Demos prácticas
      • portability: permite crear intérpretes simples y seguros en varias plataformas
      • emit-json: muestra un ejemplo adecuado para generar configuraciones multiplataforma

Completitud de Turing y reflexión

  • Completitud de Turing

    • Los operadores K y S de la lógica combinatoria pueden expresarse en Tree Calculus
    • K = △ △
    • S x = △ (△ x)
    • Como la base K/S de la lógica combinatoria es completa, Tree Calculus también es Turing-complete
    • A diferencia del λ-calculus, mediante construcciones de punto fijo como orange/brown, las funciones recursivas pueden expresarse en forma normal

  • Reflexión

    • triage {l, s, f} = △ (△ l s) f realiza análisis por casos para leaf, stem y fork
    • El número natural n puede representarse como △^n △
    • La prueba de 0 se construye como triage {true, K false, K² false}
    • Como los programas también son valores, los programas intensionales pueden realizar introspección y reflexión mediante autoaplicación
    • El programa de ejemplo size calcula la cantidad de nodos de su argumento, y size size se evalúa a 168
    • Demos prácticas
      • serialize-anything: aborda la posibilidad de serializar programas
      • halting-problem: formula el problema de la detención de manera más simple
      • fusion: expresa el análisis y la optimización de programas como funciones
      • gradual-typing: ofrece un ejemplo que trata el tipado estático y el dinámico como llamadas a funciones

Modularidad y demos

  • Los subtérminos se representan como subárboles
  • El programa size en la parte superior de la página usa triage para contar nodos recursivamente
  • Demos prácticas

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-12-11
Opiniones en Hacker News

  • Tree Calculus es un tema fascinante con implicaciones que van más allá de este sitio web.
    Sin embargo, es una lástima que el sitio no mencione explícitamente al creador y autor, Prof. Barry Jay. Si quieren saber más, pueden ver el libro de Jay: https://github.com/barry-jay-personal/tree-calculus/blob/mas...

    • En la página “Specification” sí se hace referencia a su libro.
      La atribución podría ser más clara, y lo será, pero no hay ninguna intención de apropiarse del crédito. Dejé más contexto en esta respuesta: https://news.ycombinator.com/item?id=42375914
    • Apenas vi esto, lo primero que me vino a la mente fue el Bondi Language / Pattern Calculus de Barry Jay, así que parece que no estaba tan desencaminado.

  • Se ve interesante, pero la página ofrece muy poca orientación y cuesta entenderlo.
    Estaría bien tener una explicación “para principiantes”.

    • Como el cálculo SKI o su primo, el cálculo lambda, es un modelo de cómputo simple con reglas precisas para evaluar o reducir expresiones de forma mecánica: https://en.wikipedia.org/wiki/SKI_combinator_calculus
      La diferencia con el cálculo SKI es que puede introspectar la estructura de sus propios programas; por ejemplo, permite determinar si dos programas son iguales: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
      Además, a diferencia del cálculo lambda, al aplicar las reglas de reducción dadas, el programa converge a una forma normal estable y evita casos en los que podría caer en una cadena infinita de reducciones: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
      Por eso permite introspección sin tener que entrecomillar o serializar programas para pasarlos por una estructura de datos estable, y tiene cierto parecido con la homoiconicidad de Lisp.
    • La composición de la página principal es bastante extraña.
      Usa un título de una sola palabra, frases con cierto aire de buzzword y ejemplos de código animados, como el sitio de un lenguaje de programación o framework de moda, pero el texto principal es excesivamente denso y largo, con estilo académico. Y aun así, ese estilo académico no incluye suficientes detalles para entender qué está pasando.
      Estuve un buen rato parseando los párrafos, pero, pese a lo verboso, solo dice “qué cree el autor que tiene de bueno este lenguaje”, como una landing page típica de un lenguaje de programación, y no explica cómo funciona. Al final parece que hay que leer la especificación.
    • La gramática de la especificación, E ::= t | E E, puede hacer que, a primera vista, uno piense erróneamente que todas las expresiones se ven simplemente como t t t t t t t.
      En realidad hay que conservar la estructura de paréntesis, así que toman formas como (t t) (t ((t t) (t t))), y en el nivel superior y dentro de cada paréntesis siempre hay exactamente dos subexpresiones. Es decir, el espacio en blanco funciona como un operador binario.
      Como esta expresión tiene muchos paréntesis, este operador binario se considera asociativo por la izquierda. a b c se interpreta como (a b) c, y a b c d como ((a b) c) d.
      Visto así, se entiende de dónde salen los árboles. Como el único símbolo terminal es t, si eliminamos los paréntesis innecesarios, toda expresión siempre empieza con t y le siguen varias expresiones. Dibujas la primera t como un nodo y, por cada expresión que sigue, dibujas un subárbol con el mismo procedimiento.
      Las reglas semánticas de la página de especificación explican cómo “simplificar” nodos con tres o más subárboles; es decir, cómo reducir una expresión en la que a t le siguen tres o más subexpresiones.
    • Ayudaría que arriba de la página hubiera una frase de definición del estilo “Tree Calculus es [sintagma nominal] para [resumen del propósito]”.
      Es como suelen empezar los artículos de Wikipedia: “El cálculo lambda es un sistema formal para…”, “El cálculo matricial es una notación especializada para…”.
    • En resumen, es un lenguaje de programación en el que tanto los programas como los valores son árboles sin etiquetas.
      Un árbol sin etiquetas es una estructura de datos en forma de árbol cuyos nodos no tienen datos, pero donde el orden de los hijos sí importa. Tree Calculus define un conjunto de reglas para evaluar árboles sin etiquetas y obtener otros árboles sin etiquetas.
      Si aplicas las reglas repetidamente, o caes en un bucle infinito o llegas a un árbol que ya no cambia. Las reglas están diseñadas para no afectar a los árboles binarios, así que si evalúas un árbol binario, obtienes el mismo árbol y el cálculo queda terminado.
      Estas reglas están escritas en la página “Specification” en forma de semántica de pasos pequeños, común en la teoría de lenguajes de programación.
      Lo que se afirma es que las reglas de evaluación son Turing completas, de modo que pueden expresar cualquier cómputo, y que la evaluación es asintóticamente óptima, por lo que un programa de cualquier lenguaje podría ejecutarse en Tree Calculus con una sobrecarga casi constante. A primera vista no parece una afirmación absurda, pero no queda claro qué tan importante es en la práctica.
      Su uso podría resultar interesante para algunos investigadores de teoría de lenguajes de programación, y quizá sirva para simplificar demostraciones en teoría de la computación. Si este tipo de cosas te interesa, recomendaría aprender primero el cálculo lambda, que es más simple, más conocido y más útil que Tree Calculus.

  • En la página de inicio aparecen “Democratizing Functions” y “Democratizing Metatheory”, y sea lo que sea que quieran decir, da mucho la sensación de que abusan de la palabra democratizing

    • Este uso es bastante común
      La segunda definición de Britannica también es “hacer que algo esté disponible para todos, hacer que todos puedan entenderlo”: https://www.britannica.com/dictionary/democratize
    • De acuerdo. También vale la pena ver “What democratize really means”: https://intage.us/articles/words/democratize/
      “El lenguaje está moldeado por la cultura, y tú también eres parte de esa cultura. No hace falta renunciar a la responsabilidad. Hay opciones”

  • Hice mis propios diagramas para intentar entender “a ojo” la lógica de las reglas de reducción de Tree Calculus: https://latypoff.com/tree-calculus-visualized/
    Puede ser útil para personas que piensan visualmente

    • Ayuda muchísimo. En especial me gusta el texto, escrito con mucho cuidado
      Eso sí, parece haber un error en la segunda imagen, “Stem with a single leaf child”. La línea que baja del triángulo va hacia un cuadrado, pero parece que ese cuadrado debería ser un círculo
    • Está buenísimo. Si esto se convirtiera en algo animable, quedaría muy bien en la página Specification del sitio web

  • Me pregunto si quienes recomendaron esto de verdad entendieron qué es antes de recomendarlo

    • A mis ojos parece otra implementación más del cálculo lambda, y también decepciona que la página web no explique por qué es interesante
    • Lo recomendé porque pensé que podría generar una discusión interesante
    • Lo recomendé esperando que alguien lo explicara

  • ¿Alguien puede explicar por qué esto no es simplemente Lisp o Forth con otra sintaxis?
    No lo digo para criticarlo ni para descartarlo superficialmente; de verdad quiero entender

    • Lisp se basa en el cálculo lambda, y el cálculo lambda en sí no tiene herramientas para modificar programas escritos dentro de sí mismo
      Como esta capacidad es útil, a los lenguajes de la familia Lisp se les han ido agregando cosas como macros, con distintas formas de implementación. Incluso eval, común en la familia Lisp, no forma parte del cálculo lambda. En el cálculo lambda solo hay abstracción, aplicación y variables; no hay entorno
      Si la noción de reflexión está bien definida y Tree Calculus es reflexivo, definitivamente no es solo Lisp con otra sintaxis, y mucho menos Forth
      No soy experto, así que tómalo con mucho escepticismo. En la práctica puede parecer un Lisp lento, pero en teoría es distinto del cálculo lambda y podría servir como base para implementar de forma más simple algo parecido a un Lisp lento
    • Si no tiene paréntesis obligatorios ni sensibilidad a la indentación, para mi gusto eso ya es una gran ventaja
      Otros gustos también son totalmente válidos, claro, pero es una pena que la homoiconicidad esté encerrada casi siempre dentro de dialectos de Lisp

  • Tomé el combinador Z de SKI, lo convertí a Tree Calculus pasando por un ejemplo en cálculo lambda y lo imprimí como árbol
    No lo probé, pero el original es código no optimizado convertido con una herramienta. Para el contexto relacionado, ver el artículo sobre combinadores de punto fijo: https://en.wikipedia.org/wiki/Fixed-point_combinator

    • El combinador Z puede escribirse de forma mucho más simple como Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v)), y también puede expresarse de forma más corta en SKI

  • Me alegra ver que Johannes está experimentando con Tree Calculus y mostrando explícitamente posibilidades que en mi libro GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf solo estaban implícitas
    Por fin existe un Tree Calculus con tipos, y por eso empecé a escribir un blog en GitHub.com/barry-jay-personal

  • Estuve mirando esto un buen rato y me di cuenta de algunas cosas. En particular, puede ayudar a encontrar un punto de apoyo a quienes ya estén algo familiarizados con el cálculo lambda o con la semántica formal
    Tuve que bajar hasta la implementación en OCaml para entender qué significaba la semántica de pasos pequeños, porque la estructura básica de los árboles no se veía bien. En las cuatro fórmulas de reducción de la definición, si se ponen paréntesis en los tres primeros términos se ve qué se aplica a qué. A la derecha también parece faltar algún paréntesis
    Por ejemplo, conviene verlo 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
    Además, en la tabla faltan casos que al parecer se consideran derivados “obviamente” de la asociatividad de la sintaxis; si se agregan como t a -> (t a), (t a) b -> (t a b), se puede aplicar la reducción semántica de forma más limpia a expresiones de la gramática E E
    La idea central es que, así como en el cálculo lambda se empaqueta una lambda para hacer que “elija” una de dos opciones, este Tree Calculus está construido para hacer tres elecciones según si un nodo dado es una hoja, un tallo o una rama. Ese es el núcleo de las reglas 3a, 3b y 3c, y el resto de las funciones del sistema se apoya sobre esa elección de tres vías

    • Esta explicación debería haber estado en la primera página
      Gracias a eso sí parece un cálculo interesante, pero otra cosa es si resulta más adecuado que SKI o el cálculo lambda para descompilar, serializar o compilar. Descompilar es difícil, serializar es fácil y compilar es relativamente fácil

  • En Python, se puede implementar Leaf como una lista vacía, Stem como una lista de un solo elemento y Fork como una lista de dos elementos, e implementar apply de acuerdo con el código OCaml de la especificación.
    Si se definen false, true y not como árboles, funcionan not false -> true y not true -> false.

    • En Racket o Scheme también se puede usar la misma idea.
      Leaf puede ser null, Stem puede ser list y Fork puede ser cons; se pueden comprobar los mismos resultados con apply t-not t-false y apply t-not t-true.