文書のためのコア計算体系 (2024)
本論文では、文書の構造と操作を形式的にモデル化するためのコア計算体系「λ-doc」を提案する。この体系は、文書を第一級の値として扱い、文書の合成、変換、クエリ操作を型安全に実行できる。ラムダ計算を拡張したこの体系は、文書処理言語の理論的基盤を提供する。
背景メモ
- 文書（HTMLやMarkdown、LaTeXなど）を統一的に扱うための「型システム」を、計算理論の枠組み（ラムダ計算）で初めて定式化した学術論文。著者はマイケル・B・ゲイル（MIT）。
- 通常、プログラミング言語は「関数」や「数値」の型を厳密に定義するが、「文書」は単なる文字列 or 木構造として雑に扱われがちで、構造や埋め込み（画像・脚注・参照など）を正確に表現する型理論が存在しなかった。
- この論文は DOCALC という最小限の核計算体系を提案。文書部品（テキスト、画像、グループ化）とそれらを合成する演算子を定義し、各操作が「型安全」であることを証明可能にした。
- 意義は、Webブラウザや組版エンジン（例：ブラウザのレンダリング、LaTeX処理系）の内部ロジックを数学的に検証可能にし、バグのない文書処理や次世代の文書言語設計への基礎を与える点。
- プログラミング言語理論と文書処理という、従来あまり交わらなかった領域を架橋する仕事として、PLDI（プログラミング言語デザイン・実装のトップ会議）2024で発表された。