type_theory

Luna-Flow/type_theory は Luna Flow の記号処理パッケージの意味的基盤である：変数を持つすべての AST が共有する、名前、束縛、捕獲回避代入、書き換えの単一の定義に加えて、型なしλ計算と単純型付きλ計算の参照実装を、スモールステップ簡約と評価による正規化の両方で提供する。このマニュアルは MoonBit 0.10 上のバージョン 0.2.0 を説明する。

パッケージ

各パッケージには API リファレンス（何を呼び出せるか）、チュートリアル（どう使うか）、設計ノート（その背後にある数学と判断）がある。各パッケージの pkg.generated.mbti ファイルが公開名の正式な一覧である。

パッケージ	内容	ページ
`core`	名前、新しい名前、文脈、テレスコープ、有限リネーミング	API · チュートリアル · 設計
`syntax`	汎用の名前付き `Term[T]`、自由変数、α同値、オープンな `BindingSyntax` トレイト	API · チュートリアル · 設計
`substitution`	`Term[T]` および任意の `BindingSyntax` AST 上の同時捕獲回避代入	API · チュートリアル · 設計
`rewrite`	規則名とパス付きの単一書き換えステップ、上限付き正規化、トレース	API · チュートリアル · 設計
`eval`	名前付き戦略：正規順序、適用順序、弱頭部	API · チュートリアル · 設計
`debruijn`	De Bruijn 項、変換、スコープ検査、シフト、名前なし β	API · チュートリアル · 設計
`utlc/lambda`	型なしλ計算：β、η、正規順序の正規化	API · チュートリアル · 設計
`utlc/nbe`	燃料で制限された型なしの評価による正規化	API · チュートリアル · 設計
`stlc`	単純型付きλ計算：双方向型検査、η 長形式の型付き NbE	API · チュートリアル · 設計
`adapter`	下流の `BindingSyntax` 実装のための契約テスト（公開 API なし）	API · チュートリアル · 設計

パッケージは層を成しており、各パッケージはその上にあるものだけに依存する：

core
 └─ syntax
     ├─ substitution
     ├─ rewrite ── eval
     │    └─ debruijn ── utlc/nbe
     └─ utlc/lambda (substitution, eval)
          └─ stlc (debruijn, utlc/lambda)

ガイド意味論のアーキテクチャでは、各層がどのように組み合わさるか、および 3 つの正規化器がどう関係するかを説明する。

読み進め方

ライブラリを初めて使う場合。 syntax チュートリアルから始め、次に substitution と rewrite に進む。この 3 つで束縛子を含む項を安全に操作するには十分である。

独自の AST を適合させる場合。 adapter チュートリアルを読む。そこでは小さな式言語に対して BindingSyntax を実装し、その上で汎用代入と書き換えを用いる。次に、実装が満たすべき法則について adapter の設計を読む。

λ計算を扱う場合。 utlc/lambda、eval、debruijn、utlc/nbe、stlc をこの順に読む。

コントリビュータとレビュアー。 設計ページを読むこと：各操作を数学的に定義し、その法則を導出し、各パッケージが意図的に行わないことを明記している。正しさのチェックリストは監査済みの不変条件と既知の問題を記録しており、代入、α同値、シフト、β のインスタンス化、quote、燃料の計上に対する変更ではこれを更新しなければならない。

インストール

moon add Luna-Flow/type_theory@0.2.0

次に、必要なパッケージを moon.pkg でインポートする。例：

import {
  "Luna-Flow/type_theory/core",
  "Luna-Flow/type_theory/syntax",
  "Luna-Flow/type_theory/substitution",
}

このライブラリは Luna Flow への依存を持たない。moonbitlang/quickcheck はテストでのみ使われる。

ツールチェーン

コードには MoonBit moonc 0.10 以降が必要であり、すべてのターゲット（wasm-gc、wasm、js、native）でビルドできる。リポジトリのルートでチェックを実行する：

moon check --target all
./run_test.sh
moon info

利用先

luna-poly や floating などの下流の Luna Flow リポジトリはこれらのパッケージの上に構築されている。その方法はそれぞれのマニュアルで説明されている。