ツリー計算
(treecalcul.us)- 最小限の文法で計算を構成しようとする体系で、1つの演算子 △ と適用だけで最小性・チューリング完全性・反映性・モジュール性をすべて扱う
- 文法は
E::= △ | E Eで、△ が3つの値に作用するときに計算され、値は葉・茎・分岐ノードからなる自然な二分木である - 組合せ論理の K と S を Tree Calculus の中で表現できるためチューリング完全性を持ち、λ-calculus と異なり再帰関数を正規形で表現できる
- プログラムも値として扱われるため、自己適用による イントロスペクション と反映が可能で、
size sizeが 168 に評価される例がある - 部分項が部分木として現れるため、共通機能のブートストラップ、シリアライズ、プログラム解析・最適化、静的・動的タイピングといったデモにつながる
1つの演算子で作る自然な二分木
- Tree Calculus は Barry Jay が発見したもので、サイトには彼の書籍とブログ、Johannes Bader が開発したデモへのリンクがある
- 中核的な特性は minimal、Turing-complete、reflective、modular の4つに整理されている
-
最小性
- Tree Calculus には1つの演算子 △ しかない
- 文法は
E ::= △ | E Eという形である - 視覚的には △ はツリーノードで、
E1をE2に適用するとE2がE1のルート右側に付く - 値は自然な二分木で、ノードは leaf、stem、fork と呼ばれる
- 実用デモ
- portability: 複数のプラットフォームで単純かつ安全なインタプリタを作れる
- emit-json: クロスプラットフォームな設定生成に適した例を示す
チューリング完全性と反映
-
チューリング完全性
- 組合せ論理の K と S 演算子を Tree Calculus で表現できる
K = △ △S x = △ (△ x)- 組合せ論理の K/S 基盤が完全であるため、Tree Calculus も チューリング完全 である
- λ-calculus と異なり、orange/brown のような不動点構成によって再帰関数を 正規形 で表現できる
-
反映性
triage {l, s, f} = △ (△ l s) fは leaf、stem、fork に対する場合分けを行う- 自然数
nは△^n △で表現できる - 0 テストは
triage {true, K false, K² false}で構成される - プログラムも値であるため、intensional プログラムは自己適用によってイントロスペクションと反映を行える
- 例のプログラム
sizeは引数のノード数を数え、size sizeは 168 に評価される - 実用デモ
- serialize-anything: プログラムのシリアライズ可能性を扱う
- halting-problem: 停止問題をより単純に定式化する
- fusion: プログラム解析・最適化を関数として表現する
- gradual-typing: 静的タイピングと動的タイピングを関数呼び出しとして扱う例を示す
モジュール性とデモ
- 部分項は 部分木 として表現される
- ページ上部の
sizeプログラムはtriageを使ってノードを再帰的に数える - 実用デモ
- bootstrap-basics: 共通機能を容易にブートストラップできる
- size-of-meaningful-programs: 強力なプログラムが必ずしも大きな木である必要はないことを示す
1件のコメント
Hacker News のコメント
Tree Calculus は、このウェブサイトの枠を超えた含意を持つ素晴らしいテーマ
ただし、ウェブサイトが創始者であり著者でもある Prof. Barry Jay を明示していないのは残念。もっと知りたければ Jay の本を見るとよい: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
出典表示はもっと明確にできるし、そうする予定だが、功績を横取りする意図はまったくない。背景はこの返信にもう少し書いてある: https://news.ycombinator.com/item?id=42375914
かっこよく見えるが、このページは案内が少なすぎて理解しにくい
「初心者向け」の説明のようなものがあるとよい
SKI 計算と違う点は、自分のプログラム構造を内省できること、たとえば 2 つのプログラムが同じかどうかを判断できること: https://github.com/barry-jay-personal/tree-calculus/blob/mas...
またラムダ計算と違い、与えられた簡約規則を適用するとプログラムが安定した 正規形へ収束し、無限の簡約列に陥りうるケースを避けられる: https://treecalcul.us/specification/, https://sci-hub.se/https://dl.acm.org/doi/abs/10.1016/j.tcs....
そのため、プログラムをクォートしたりシリアライズして安定したデータ構造へ迂回したりしなくても内省が可能で、Lisp の 同図像性に似た面がある
流行のプログラミング言語やフレームワークのウェブサイトのように、一語のタイトル、少し buzzword っぽい文句、動くコード例を使っているのに、本文は過度に密で長い学術調の文章になっている。ところが、その学術調の文章だけで何が起きているのか理解できるだけの詳細はない
しばらく段落を解析してみたが、冗長であるにもかかわらず、普通のプログラミング言語のランディングページのように「著者がこの言語の何を良いと思っているか」だけを語っており、動作の仕組みは説明していない。結局、仕様を見る必要がありそう
E ::= t | E Eは、初見だとすべての式が単にt t t t t t tのように見えると誤解しやすい実際には括弧構造を保つ必要があるので、
(t t) (t ((t t) (t t)))のような形になり、最上位と各括弧の中には常に正確に 2 つの部分式がある。つまり空白文字が二項演算子のように働くこの式は括弧が多いので、この二項演算子を 左結合 とみなす。
a b cは(a b) c、a b c dは((a b) c) dと解釈されるこう見ると、木がどこから出てくるのかが見える。終端記号が
t1 つだけなので、不要な括弧を取り除くと、すべての式は常にtで始まり、その後に複数の式が続く。最初のtをノードとして描き、続く各式について同じ手順で部分木を描けばよい仕様ページの意味規則は、部分木が 3 つ以上あるノードを「単純化」する方法、つまり
tの後に部分式が 3 つ以上付いた式を簡約する方法を述べているWikipedia の記事が通常「ラムダ計算は … のための形式体系である」「行列計算は … のための特殊な記法である」のように始まる、という感じ
ラベルなし木とは、ノードにデータを持たない木構造のデータ構造で、子の順序は存在する。Tree Calculus はラベルなし木を評価して別のラベルなし木を得る規則集合を定義している
規則を繰り返し適用すると、無限ループに陥るか、もう変化しない木に到達する。規則は二分木には影響しないよう設計されているため、二分木を評価すると同じ木が返り、計算が終了した状態になる
これらの規則は「Specification」ページに、プログラミング言語理論でよく使われる 小ステップ意味論 の形で書かれている
主張されているのは、評価規則が チューリング完全 なのでどんな計算も表現でき、評価が漸近的に最適なので、どんな言語のプログラムも Tree Calculus 上でほぼ定数オーバーヘッドで実行できるということ。初見では筋の通らない主張ではないが、実際にどれほど重要なのかは明確ではない
用途としては、一部のプログラミング言語理論の研究者には興味深く、計算理論の証明を単純化するのに使えるかもしれない。こういうものに興味があるなら、Tree Calculus よりも単純で、よく知られていて有用な ラムダ計算 を先に学ぶことを勧める
ホームページに “Democratizing Functions”、“Democratizing Metatheory” とあるが、意味が何であれ democratizing という言葉を乱用している印象が強い
Britannica の2番目の定義も「何かを誰でも利用できるようにする、誰でも理解できるようにする」という意味: https://www.britannica.com/dictionary/democratize
「言語は文化によって形作られ、あなたもその文化の一部だ。責任を放棄する必要はない。選択肢はある」
Tree Calculus の簡約規則の論理を「感覚」で理解しようとして、自分で図を作った: https://latypoff.com/tree-calculus-visualized/
視覚的に考える人には役立つかもしれない
ただし2番目の図 “Stem with a single leaf child” には誤りがありそう。三角形から下りる線が四角形につながっているが、その四角形は円であるべきだと思う
これを推薦した人たちが、本当に何なのか理解したうえで推薦したのか気になる
これが構文だけ違う Lisp や Forth ではない理由を説明してもらえるだろうか？
批判したり浅く切り捨てたりしたいわけではなく、本当に理解したい
この機能は有用なので、Lisp 系言語にはマクロのようなものが追加されてきたし、実装方法もさまざま。Lisp 系でよく見られる
evalでさえラムダ計算の一部ではない。ラムダ計算には抽象化、適用、変数だけがあり、環境はないリフレクションの概念がきちんと定義されていて Tree Calculus がリフレクティブなら、構文だけ違う Lisp では確実になく、Forth ならなおさら違う
専門家ではないので、大いに割り引いて聞いてほしい。実務的には遅い Lisp のように見えるかもしれないが、理論的にはラムダ計算とは異なり、遅い Lisp のようなものをより単純に実装する基盤として使える
他の好みも当然ありだが、ホモイコニシティがほとんど Lisp 方言の中に閉じ込められているのは残念
SKI の Z コンビネータを、ラムダ計算の例を経由して Tree Calculus に変換し、ツリーとして出力してみた
テストはしていないが、元はツールで変換した未最適化コード。関連する背景は固定点コンビネータの文書を参照: https://en.wikipedia.org/wiki/Fixed-point_combinator
Z = \f. (\x. f (\v. x x v)) (\x. f (\v. x x v))という形でもっと単純に書けるし、SKI でもより短く表現できるJohannes が Tree Calculus を試して、私の本 GitHub.com/barry-jay-personal/tree-calculus/tree_book.pdf では暗黙的にしか示されていなかった可能性を明示的に示しているのを見るのはうれしい
ついに型付き Tree Calculus ができたので、GitHub.com/barry-jay-personal でブログを書き始めた
右側のダウンロードボタンを探せばよい
これをしばらく眺めていて、いくつか気づいた点がある。特に ラムダ計算 や形式意味論にある程度なじみのある人が足がかりを得るのに役立つかもしれない
小ステップ意味論が何を意味するのか理解するために OCaml 実装まで降りる必要があったが、それは基本的な木構造がよく見えなかったため。定義の4つの要素の簡約式では、最初の3項に括弧を付けてみると、何が何に適用されているのかが見える。右辺も括弧が足りないように見える
例えば
(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のように見るほうがよいまた、表には構文の結合性から「当然」出てくると見なしているらしい場合が抜けているが、
t a -> (t a)、(t a) b -> (t a b)のように追加しておくと、E E構文の式に意味論的な簡約をよりきれいに適用できる要点は、ラムダ計算でラムダを束ねて2つの選択肢のどちらかを「選ばせる」ようにするのと同じように、この Tree Calculus は与えられたノードが葉、幹、枝のどれかに応じて 3つの選択を行うように作られているという点。規則 3a、3b、3c の核心はこれで、システムの残りの機能はこの3分岐の選択の上に積み上がっている
おかげで面白い計算体系には見えるが、SKI やラムダ計算よりも逆変換、シリアライズ、コンパイルに適しているかどうかは別問題。逆変換は難しく、シリアライズは簡単で、コンパイルはそこそこ簡単なほう
Python では、Leafを空リスト、Stemを単一要素のリスト、Forkを2要素のリストとして置き、
applyを仕様の OCaml コードに合わせて実装できるfalse、true、notを木として定義すると、not false -> true、not true -> falseが動作するLeafはnull、Stemはlist、Forkはconsとして置けばよく、apply t-not t-falseとapply t-not t-trueで同じ結果を確認できる