2. エラボレーションとコンパイル（Elaboration and Compilation）

大まかに言うと、Lean のソースファイルに対する処理は以下のステージに分類されます：

パース: パーサは文字のシーケンスを Syntax 型の構文木に変換します。Lean のパーサは拡張可能であるため、 Syntax 型は非常に一般的です。

マクロ展開: マクロは構文糖衣をより基本的な構文に置き換える変換です。マクロ展開の入力と出力のどちらも Syntax 型を持ちます。

エラボレーション: エラボレーション（elaboration）とは、Lean のユーザ向けの構文をコア型理論に変換するプロセスです。このコア理論はよりシンプルであり、信頼されたカーネルを非常に小さくすることができます。エラボレーションはさらに、Lean の対話的機能に使用される証明状態や式の型などのメタデータを生成し、サイドテーブルに格納します。

カーネルによるチェック: Lean の信頼されたカーネルはエラボレータの出力が型理論の規則に従っているかどうかをチェックします。

コンパイル: コンパイラはエラボレートされた Lean のコードを実行可能な実行ファイルへと変換します。

The Lean Pipeline

実際には、上記の段階は厳密に次々と行われるわけではありません。Lean は1つのコマンド（command、トップレベルの宣言）をパースし、ついでエラボレートし、必要なカーネルのチェックを実行します。マクロ展開はエラボレーションの一部です；構文の一部を翻訳する前に、エラボレータはまず一番外側のレイヤに存在するマクロを展開します。マクロ構文はより深いレイヤに残っているかもしれませんが、その後でエラボレータがそれらのレイヤに到達した時に展開されます。エラボレーションには複数の種類が存在します：コマンドエラボレーションは各トップレベルのコマンドの作用（例えば帰納型の宣言・定義の保存・式の評価）を実装し、項エラボレーションは多くのコマンドで出現する項（例えばシグネチャ内の型・定義の右辺・評価される式）の構築を担当します。タクティクの実行は、項エラボレーションの特殊化です。

あるコマンドがエラボレートされると、Lean の状態は変化します。新しい定義や型が将来の使用のために保存されたり、構文が拡張されたり、明示的な修飾なしに参照できる名前の集合が変更されるかもしれません。次のコマンドはこの更新された状態で解析され、エラボレートされます。

2.1. パース（Parsing）🔗

Lean のパーサは再帰下降パーサであり、Pratt パーサ (Pratt, 1973)Vaughan Pratt, 1973. “Top down operator precedence”. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. に基づく動的テーブルを使用して、演算子の優先順位と結合性を解決します。文法が曖昧でない場合、パーサはバックトラックする必要がありません；曖昧な文法の場合、パックラットパースで使用されるものと同様のメモ化テーブルによって指数関数的な爆発を避けます。Lean のパーサは非常に拡張性が高いです：ユーザはどのコマンドでも新しい構文を定義でき、その構文は次のコマンドで使用できるようになります。現在の section scope で開いている名前空間も、どのパース規則を使用するかに影響します。なぜなら、パーサの拡張機能は指定した名前空間が開いているときにのみ有効になるように設定できるからです。

曖昧な表現に遭遇した場合、最長一致のパースが選択されます。一意に最長一致が無い場合、一致するパースの両方が choice node の構文木に保存され、後でエラボレータによって解決されます。パーサが失敗した場合、 Syntax.missing ノードを返し、エラーの回復を可能にします。

成功した場合、パーサは元のソースファイルを再構築するのに十分な情報を保存します。成功しなかったパースは、パース出来なかったファイルの領域に関する情報を見逃す可能性があります。 SourceInfo レコード型はソースの位置と周囲の空白を含む、構文の一部分のソースに関する情報を記録します。 SourceInfo フィールドに基づいて、 Syntax がソースファイルに対して以下の3つの関係を持つことができます：

SourceInfo.original は、構文の値がパーサによって直接生成されたことを示します。
SourceInfo.synthetic は、構文の値がマクロ展開などによってプログラム的に生成されたことを示します。そうであるにも関わらず、統合的な構文は標準（canonical）とマークされることがあります。これによって Lean のユーザインタフェースはこの構文をあたかもユーザが書いたかのように扱います。統合的な構文には元のファイル位置が注釈されますが、先頭や末尾の空白は含まれません。
SourceInfo.none は、ファイルとの関係がないことを示します。

パーサは、現在において言語の一部となっている予約語を追跡する字句テーブルを保持します。新しい構文を定義したり、名前空間を開いたりすると、以前は有効だった識別子がキーワードになることがあります。

Lean の文法では、各生成物に名前が付けられています。この生成物の名前は種（kind）と呼ばれています。これらの構文の種は重要です。なぜならエラボレータのテーブルで構文の解釈を検索するために使用されるキーだからです。

構文拡張については専用の章で詳しく説明されています。

2.2. マクロ展開とエラボレーション（Macro Expansion and Elaboration）🔗

コマンドをパースした後、次のステップはそれをエラボレートすることです。 エラボレーション （elaboration）の正確な意味は何をエラボレートするかによって異なります：コマンドのエラボレートは Lean の状態変化に作用し、項のエラボレートによって Lean のコア型理論の項が生成されます。コマンドと項エラボレーションのどちらも再帰的となり得ます。これはどちらも Lean.Parser.Command.in : commandin のようなコマンドコンビネータや、項が他の項を含むことがあるためです。

コマンドエラボレーションと項エラボレーションは異なる能力を持ちます。コマンドエラボレーションは環境に副作用を与える可能性があり、 IO で任意の計算を実行するアクセス権を持っています。Lean の環境は名前から定義への通常のマッピングに加え、環境拡張（environment extension）で定義される追加データを含んでいます；環境拡張は simp 補題・カスタムのプリティプリンタ・コンパイラの中間表現などの内部を含む、Lean コードに関する他のほとんどの情報を追跡するために使用されます。コマンドエラボレーションはまた、コンパイラの情報出力・警告・およびエラー内容を含むメッセージログ・メタデータをもとの構文に関連付ける情報木のセット（証明状態の表示・識別子の補完・ドキュメントの表示などの対話的な機能に使用されます）・蓄積されたデバッグトレース・開いた section scope ・マクロ展開に関連するいくつかの内部状態を維持します。項エラボレーションは開いたスコープを除くこれらすべてのフィールドを変更することができます。さらに、Lean の簡潔で親しみやすい構文からコア言語で完全に明示的な項を作成するために必要な単一化・型クラスインスタンス合成・型チェックを含むすべての機構にアクセスすることができます。

項とコマンドエラボレーションのどちらも最初のステップはマクロ展開です。構文の種とマクロの実装を対応付けるテーブルが存在し、マクロの実装はマクロ構文を新しい構文に変換するモナド関数です。マクロは同じテーブルに保存され、項・コマンド・タクティク・および Lean のその他のマクロ拡張可能な部分に対して同じモナドで実行されます。マクロによって拡張された構文それ自体がマクロである場合、その構文は再び拡張されます。このプロセスはマクロではない構文がせいせいされるか、最大反復回数に達するまで繰り返されます。最大反復回数に到達した場合、Lean はエラーを出力します。一般的なマクロは構文の外側のレイヤを処理し、いくつかの部分項はそのままにします。つまり、マクロ展開が完了しても、トップレベル以下の構文にはマクロ呼び出しが残っている可能性があります。新しいマクロをマクロテーブルに追加することができます。新しいマクロの定義についてはマクロの節で詳しく説明されます。

マクロ展開の後、項とコマンドエラボレータのどちらも、構文の種をエラボレータの手続きにマップするテーブルを参照します。項エラボレータは、構文とオプションで期待される型を、前述の非常に強力なモナドを使用するコア言語の式にマッピングします。コマンドエラボレータは構文を受け入れ、値を返しませんが、グローバルのコマンド状態に対してモナドの副作用を持つかもしれません。項とコマンドエラボレータのどちらも IO にアクセスできますが、副作用を実行するのは一般的ではありません；例外は外部ツールやソルバとのやり取りを含みます。

エラボレータのテーブルは、項とコマンドの両方に新しい構文を使用することができるように拡張することができます。Lean にエラボレータを追加する方法についてはエラボレータの節を参照してください。コマンドや項がさらなるコマンドや項を含む場合、ネストされた構文に対して適切なエラボレータを再帰的に呼び出します。このエラボレータはテーブルからエラボレータを呼び出す前にマクロを展開します。マクロ展開は構文の与えられた「レイヤ」のエラボレーションの前に行われますが、マクロ展開とエラボレーションは一般的に交互に実行されます。

2.2.1. 情報木（Info Trees）

Lean のコードと対話する場合、単に依存関係としてインポートする場合よりもはるかに多くの情報が必要になります。例えば、Lean の対話型環境は、選択した式の型を表示したり、証明のすべての中間状態をステップごとに眺めていったり、ドキュメントを表示したり、束縛変数のすべての出現をハイライトしたりするために使用できます。Lean を対話的に使用するために必要な情報はエラボレーション中において 情報木 （info tree）と呼ばれるサイドテーブルに格納されます。

情報木はユーザのオリジナルの構文にメタデータを関連付けます。その木構造は構文の木構造に密接に対応していますが、構文木のあるノードにはそれについて異なる側面を文書化する多くの対応する情報木があるかもしれません。このメタデータには、Lean のコア言語におけるエラボレータの出力・ある時点でアクティブな証明状態・対話的な識別子補完のための提案等その他多くのものが含まれます。またこのメタデータは任意に拡張可能です；コンストラクタ Info.ofCustomInfo は Dynamic 型を受け付けます。これを使用して、カスタムコードアクションやその他のユーザインタフェース拡張で使用する情報を追加することができます。

2.3. カーネル（The Kernel）

Lean が信頼する カーネル （kernel）はコア型理論のための型チェッカの小さく堅牢な実装です。カーネルには構文的停止チェッカは含まれず、単一化も行いません；停止性はすべての再帰関数をプリミティブ再帰子の使用にエラボレートすることで保証され、単一化はエラボレータによってすでに実行されていることが期待されます。コマンドと項エラボレータによって新しい帰納型や定義が環境に追加される前に、エラボレータによって潜在的なバグを防ぐために、それらはカーネルによってチェックされなければなりません。

Lean のカーネルは C++ で書かれています。また独立した再実装として Rust と Lean によるものもあり、Lean プロジェクトは可能な限り多くの実装を用意して、互いにクロスチェックできるようにすることを望んでいます。

カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です：

完全な依存型
相互に帰納的であったり、他の帰納型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型
impredicative ・定義上証明と irrelevant な命題の拡張的宇宙
predicative なデータの宇宙の非蓄積な階層

定義上の計算規則を伴った商型（Quotient type）

命題上の関数外延性関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。
関数と積についての定義上のη等価性
宇宙多相定義
一貫性： False 型の公理にとらわれない閉項は存在しません

この理論は最先端の研究数学を表現するのに十分豊かでありながら、小規模で効率的な実装が可能なほどシンプルです。明示的な証明項が存在することで、独立した証明チェッカを実装することが可能であり、信頼性が高まります。詳しくは Carneiro (2019)Mario Carneiro, 2019. The Type Theory of Lean. Masters thesis, Carnegie Mellon University と Ullrich (2023)Sebastian Ullrich, 2023. An Extensible Theorem Proving Frontend. Dr. Ing. dissertation, Karlsruhe Institute of Technology で説明されています。

Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、impredicativity・計算する商型・定義上の証明の irrelevance・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。

2.4. エラボレーションの結果（Elaboration Results）

Lean のコア型理論には、パターンマッチや再帰定義は含まれていません。その代わりに、場合分けと原始再帰の両方を実装するために使用できる低レベルの再帰子を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。

再帰子への翻訳には2つのフェーズが発生します：項エラボレーションの間、パターンマッチの使用はコード中で発生する特定の場合分けを実装する補助関数の出現に置き換えられます。これらの補助関数はそれ自体が再帰子を使用して定義されますが、再帰子が実際に再帰的な動作を実装する機能は使用しません。再帰子は再帰子とエラボレーションの節で記述する casesOn 構成を使います。このように、項エラボレータはパターンマッチが場合分けを実装する特別な関数の使用に置き換えられたコア言語による項を返しますが、これらの項には定義されている関数の再帰的な出現が含まれる可能性があります。Lean の出力に補助的なパターンマッチ関数を表示するには、オプション pp.match を false に設定します。

option

pp.match

Default value: true

(pretty printer) disable/enable 'match' notation

こうしてエラボレートされた定義はコンパイラとカーネルに送られます。コンパイラは再帰が残っているバージョンを受け取りますが、カーネルに送られたバージョンは、明示的な再帰を再帰子の使用に置き換える2つ目の変換を受けます。この区別には3つの理由があります：

コンパイラは partial 関数をコンパイルすることができますが、カーネルは推論のためにこれを不透明な定数として扱います。
コンパイラは unsafe 関数もコンパイルすることができますが、これはカーネルでは完全に無視されます。
再帰子への翻訳は、特に遅延か正格についてプログラマに期待されたコストモデルを保存する必要はありません。しかし、コンパイルされたコードは予測可能な性能を持たなければなりません。コンパイラは中間表現を環境拡張に保存します。

構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は整礎再帰（well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの基準が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、eq_unfold は関数を直接定義に関連付け、eq_def は暗黙のパラメータをインスタンス化した後の定義に関連付け、 N 個の補題 eq_N はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。

等式の補題

定義 thirdOfFive に対して：

def thirdOfFive : List α → Option α
  | [_, _, x, _, _] => some x
  | _ => none

thirdOfFive をその定義に関連付ける等式の補題が生成されます。

thirdOfFive.eq_unfold は引数が与えられていないもとの定義に展開できることを示します：

thirdOfFive.eq_unfold.{u_1} :
  @thirdOfFive.{u_1} = fun {α : Type u_1} x =>
    match x with
    | [head, head_1, x, head_2, head_3] => some x
    | x => none

thirdOfFive.eq_def は引数に適用されたときにその定義を一致することを示します：

thirdOfFive.eq_def.{u_1} {α : Type u_1} :
  ∀ (x : List α),
    thirdOfFive x =
      match x with
      | [head, head_1, x, head_2, head_3] => some x
      | x => none

thirdOfFive.eq_1 はその最初の定義された等式が成り立つことを示しています：

thirdOfFive.eq_1.{u} {α : Type u}
    (head head_1 x head_2 head_3 : α) :
  thirdOfFive [head, head_1, x, head_2, head_3] = some x

thirdOfFive.eq_2 は二番目に定義された等式が成り立つことを示しています：

thirdOfFive.eq_2.{u_1} {α : Type u_1} :
  ∀ (x : List α),
    (∀ (head head_1 x_1 head_2 head_3 : α),
      x = [head, head_1, x_1, head_2, head_3] → False) →
    thirdOfFive x = none

最後の補題 thirdOfFive.eq_2 は最初の分岐がマッチしなかった（つまりリストがちょうど5つの要素を持たない）という前提を含んでいます。

再帰的な等式の補題

定義 everyOther に対して：

def everyOther : List α → List α
  | [] => []
  | [x] => [x]
  | x :: _ :: xs => x :: everyOther xs

everyOther' の再帰子ベースの実装をもとの再帰定義に関連付ける等式の補題が生成されます。

everyOther.eq_unfold は引数の無い everyOther がその展開と等しいことを示します：

everyOther.eq_unfold.{u} :
  @everyOther.{u} = fun {α} x =>
    match x with
    | [] => []
    | [x] => [x]
    | x :: head :: xs => x :: everyOther xs

everyOther.eq_def は everyOther が引数に適用されたとき、その定義と等しいことを示します：

everyOther.eq_def.{u} {α : Type u} :
  ∀ (x : List α),
    everyOther x =
      match x with
      | [] => []
      | [x] => [x]
      | x :: head :: xs => x :: everyOther xs

everyOther.eq_1 はその最初のパターンを説明します：

everyOther.eq_1.{u} {α : Type u} : everyOther [] = ([] : List α)

everyOther.eq_2 は二番目のパターンを説明します：

everyOther.eq_2.{u} {α : Type u} (x : α) : everyOther [x] = [x]

everyOther.eq_3 は最後のパターンを説明します：

everyOther.eq_3.{u} {α : Type u} (x_1 head : α) (xs : List α) :
  everyOther (x_1 :: head :: xs) = x_1 :: everyOther xs

パターンが重複しないため、これらの等式の補題には先行するパターンと一致しないという仮定は必要ありません。

モジュールをエラボレートした後、カーネルで環境に対する各追加をチェックし、モジュールがグローバル環境（拡張を含む）に加えた変更を .olean ファイルにシリアライズします。これらのファイルでは、Lean の項と値はメモリにあるものと同じように表演されます；そのため、ファイルを直接メモリマップすることができます。Lean が環境に追加するすべてのコードパスでは、新しい型や定義が最初にカーネルによってチェックされます。しかし、Lean は非常にオープンで柔軟なシステムです。不完全に書かれたメタプログラムがチェックされていない値を環境に追加するために抜け穴をくぐってしまう可能性から守るために、別のツール lean4lean を使って .olean ファイル内の環境全体がカーネルを満たしているかどうかを検証することができます。

.olean ファイルに加えて、エラボレータは言語サーバが使用するインデックスである .ilean ファイルを生成します。このファイルには定義のソース位置など、モジュールを完全にロードせずに対話的に作業するために必要な情報が含まれています。.ilean ファイルの内容は実装の詳細であり、どのリリースでも変更される可能性があります。

最後に、環境拡張に格納された関数の中間表現を C コードに変換するためにコンパイラが起動されます。Lean モジュールごとに C ファイルが生成され、バンドルされている C コンパイラを使ってネイティブコードにコンパイルされます。ビルド構成で precompileModules オプションが設定されている場合、このネイティブコードは動的にロードされ、Lean によって呼び出されます。ほとんどのワークロードでは、コンパイルのオーバーヘッドはインタプリタを使用しないことで節約できる時間よりも大きいですが、一部のワークロードではタクティク・言語拡張・Lean の他の拡張をプリコンパイルすることで劇的に高速化できます。

2.5. 初期化（Initialization）

起動する前に、エラボレータは正しく初期化されなければなりません。コンパイラの初期状態を正しく構築するために、Lean 自身は実行しなければならない初期化（initialization）コードを含んでいます；このコードはモジュールのロード前とエラボレータの起動前に実行されます。さらに、各依存関係は環境拡張をセットアップするために初期化コードを提供することもあります。内部的には、各環境拡張は配列に一意のインデックスが割り当てられ、この配列のサイズは登録された環境拡張の数に等しいため、環境を正確に割り当てるために拡張の数は既知でなければなりません。

Lean 自身の組み込み初期化を実行した後、モジュールのヘッダが解析され、依存関係の .olean ファイルがメモリにロードされます。依存関係の環境の合併を含む「事前環境」が構築されます。次に、依存関係によって指定されたすべての初期化コードがインタプリタで実行されます。この時点で、環境拡張の数がわかっているため、事前環境を正しいサイズの拡張配列を持つ環境構造体に再割り当てすることができます。

syntax

Lean.Parser.Command.initialize : commandinitialize ブロックはモジュールの初期化にコードを追加します。 Lean.Parser.Command.initialize : commandinitialize ブロックの内容は、 IO モナドの Lean.Parser.Term.do : termdo ブロックの内容として扱われます。

時には、初期化は副作用によって内部データ構造を拡張することだけを必要とします。その場合、内容は IO Unit 型を持つことが期待されます：

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. initialize
        doSeqItem*

初期化は、環境拡張によってバックアップされた属性などの内部状態への参照を含む値を構築するためにも使用できます。この形式の Lean.Parser.Command.initialize : commandinitialize では、初期化は IO モナドで指定された型を返す必要があります。

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. initialize ident : term ←
        doSeqItem*

syntax

Lean の内部では、初期化中に実行しなければならないコードも定義されています。しかし、Lean はブートストラップコンパイラであるため、Lean 自身の一部として定義された初期化には特別な注意が必要であり、Lean 自身の初期化は 任意の モジュールを先にインポートやロードする前に実行しなければなりません。これらの初期化は Lean.Parser.Command.initialize : commandbuiltin_initialize を使って指定し、これはコンパイラの実装外では使うべきではありません。

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. builtin_initialize
        doSeqItem*

command ::= ...
    | `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions. builtin_initialize ident : term ←
        doSeqItem*