Leanのメタプログラミングで帰納型を組み合わせる
Modular Composition of Inductive Types Using Lean Meta-programming
この論文をやさしく読む
ひとことで言うと
一度定義した帰納型に新しい構成要素を加えにくい問題を、Leanのメタプログラミングで扱う。
何に役立つ？
定理証明や言語処理で、型と関数を部品ごとに再利用・合成する設計に役立つ。
この研究の面白いところ
帰納型と関数の合成アルゴリズム、Leanの構文拡張、三つの部分言語を合成する事例を示した。
どこまで分かった？
適用対象はLeanの型・関数定義の一部であり、事例研究でも枠組みの限界を示したと要旨にある。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
帰納型は多くのプログラミング言語と定理証明言語の基本要素である。型の値を作るコンストラクターの集合は閉じており、型を定義した後は拡張できない。この制約は、型やその値を扱う関数を定義するときの拡張性、再利用、関心事のモジュール分離を妨げる。既存部分を修正・再コンパイルせずに式言語へ新しい構文コンストラクターを追加することが、多くの言語で難しいという「式問題」に、この制約が表れる。本論文は、メタプログラミングに基づいて帰納型と関数実装を合成するアルゴリズムを提示する。さらに、そのアルゴリズムを実装した Lean 証明支援系の構文拡張を示す。この枠組みは、Lean の型定義と関数定義の一部について、モジュール単位の再利用、合成、拡張を可能にする。部品となる型と合成した型の間の意味的な部分型関係を、型理論と実装の両面から論じる。三つの部分言語の構文と意味に関する要素を一つの言語に組み合わせる事例研究で枠組みを示し、その機能と限界を明らかにする。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-21（UTC）
- 最新改訂
- 2026-09-21 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-21 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Inductive types are ubiquitous building blocks in many programming and theorem proving languages. An inductive type is a closed set of constructors from which values of the type can be created. That set cannot be extended though once a type is defined. This limits extensibility, reuse, and modular separation of concerns when defining types and functions operating over their values. This limitation is manifested in the expression problem, where extending an expression language with new syntactic constructors without having to modify or re-compile existing ones is a challenge in almost all programming languages. This paper presents inductive type and function implementation composition algorithms based on meta-programming. In addition, a set of syntactic extensions to the Lean proof assistant implementing those algorithms are presented. This framework allows for modular reuse, composition, and extension of a subset of Lean type and function definitions. In addition, semantic subtyping relations between component and composite types are discussed both at the type theoretic and implementation levels. The framework is demonstrated on a case study, involving the composition of syntactic and semantic artifacts of three sublanguages into one language. The case study highlights both the features and limitations of the composition framework.
著者のコメント
SEFM 2026 preprint
arXiv ID: 2609.25427 ／ 要約の誤りについて