概要

この章では、パース・エラボレーション・評価など、Leanのコンパイルプロセスに関わる主なステップの概要を説明します。導入で言及したように、Leanのメタプログラミングはこのプロセスの核心に踏み込むことになります。まず基本的なオブジェクトである Expr と Syntax を探求し、それらが何を意味するかを学び、片方をもう一方に（そして反対方向に！）どのように変えることができるかを明らかにします。

次の章では、その詳細を学びます。本書を読み進めながら、時々この章に立ち返り、すべてがどのように組み合わさっているかを思い出すとよいでしょう。

コンパイラにアクセスする

Leanでのメタプログラミングは、パース、構文解析、変換、コード生成といったコンパイルのステップと深く関連しています。

Lean4はLeanの定理証明器をLean自体で再実装したものです。新しいコンパイラはCコードを生成し、ユーザはLeanで効率的な証明自動化を実装し、それを効率的なCコードにコンパイルしてプラグインとしてロードすることができます。Lean4では、Leanパッケージをインポートするだけで、Leanの実装に使用されるすべての内部データ構造にアクセスできます。

Leonardo de Moura, Sebastian Ullrich (The Lean 4 Theorem Prover and Programming Language)

Leanのコンパイルプロセスは以下の図にまとめることができます：

まず、Leanのコード自体である文字列から始まります。それから Syntax オブジェクトになり、次に Expr オブジェクトになります。最終的にそれを実行します。

そのため、コンパイラはLeanのコード文字列、例えば "let a := 2" を見て次のような処理を展開します：

  1. 関連する構文ルールの適用 ("let a := 2" ➤ Syntax)

    構文解析のステップにおいて、Leanはコードの文字列を宣言された 構文ルール （syntax rules）のどれかにマッチさせ、その文字列を Syntax オブジェクトにしようとします。構文ルール と聞くと仰々しいですが基本的には正規表現です。ある 構文ルール の正規表現にマッチするLean文字列を書くと、そのルールは後続のステップの処理に使用されます。

  2. すべてのマクロの繰り返し適用 (Syntax ➤ Syntax)

    エラボレーションのステップでは、各 マクロ （macro）は既存の Syntax オブジェクトを新しい Syntax オブジェクトに単純に変換します。そして新しい Syntax は適用する マクロ が無くなるまで同じように処理が行われます（ステップ1と2を繰り返します）。

  3. elabの単発適用 (Syntax ➤ Expr)

    いよいよ構文に意味を吹き込む時です。Leanは name 引数によって適切な 構文ルール にマッチする elab を見つけます（構文ルール と マクロ、elabs はすべてこの引数を持っており、必ずマッチしなければなりません）。新しく見つかった elab は特定の Expr オブジェクトを返します。これでエラボレーションのステップは完了です。

この式（Expr）は評価ステップにおいて実行可能なコードに変換されます。このステップはLeanのコンパイラがよしなに処理してくれるため、指定をする必要はありません。

エラボレーションとデラボレーション

エラボレーション（elaboration）はLeanにおいて多重な意味を持つ用語です。例えば、「エラボレーション」という言葉について、「部分的に指定された式を受け取り、暗黙にされたものを推測する」 を意図した次のような用法に出会うことでしょう：

Leanが処理するために λ x y z, f (x + y) z のような式を入力する場合、あなたは情報を暗黙的なものとしています。例えば、x・y・z の型は文脈から推測しなければならず、+ という表記はオーバーロードされたものかもしれず、そして f に対して暗黙的に埋めなければならない引数があるかもしれません。

この 「部分的に指定された式を受け取り、暗黙にされたものを推測する」 プロセスは エラボレーション （elaboration）として知られています。Leanの エラボレーション アルゴリズムは強力ですが、同時に捉えがたく複雑です。依存型理論のシステムで作業するには、エラボレータ （elaborator）がどのような種類の情報を確実に推論できるかということを知っておくことに加え、エラボレータが失敗した時に出力されるエラーメッセージへの対応方法を知っておくことが必要です。そのためには、Leanの エラボレータ がどのように動作するかということへの一般的な考え方を知っておくと便利です。

Leanが式をパースするとき、まず前処理フェーズに入ります。最初に、Leanは暗黙の引数のための「穴」（hole）を挿入します。項tが Π {x : A}, P x という方を持つ場合、tは利用箇所すべてで @t _ に置き換えられます。次に穴（前のステップで挿入されたもの、またはユーザが明示的に記述したもの）はメタ変数 ?M1・?M2・?M3・... によってインスタンス化されます。オーバーロードされた各記法は選択肢のリスト、つまり取りうる解釈に関連付けられています。同様に、Leanは適用 s t に対して、推論されるtの型を s の引数の型と一致させるために型の強制を挿入する必要がある箇所を検出しようとします。これらも選択するポイントになります。あるエラボレーションの結果、型の強制が不要になる可能性がある場合、リスト上の選択肢の1つが恒等になります。

(Theorem Proving in Lean 2)

一方で、本書では Syntax オブジェクトを Expr オブジェクトに変換するプロセスとしてエラボレーションを定義しました。

これらの定義は相互に排他的なものではありません。エラボレーションとは、確かに Syntax から Expr への変換のことですが、ただこの変換を行うためには、暗黙の引数を推論したり、メタ変数をインスタンス化したり、ユニフィケーションを行ったり、識別子を解決したりなどなど、多くの技法が必要になります。そしてこれらのアクション自体もエラボレーションそのものとして言及されます；これは「部屋の電気を消したかどうかをチェックする」（メタ変数のインスタンス化）を「学校に行く」（エラボレーション）と呼ぶことができるのと同じです。

Leanにはエラボレーションと反対のプロセスも存在し、これは名実ともにデラボレーション（delaboration）と呼ばれます。デラボレーションにおいては、Expr が Syntax オブジェクトに変換されます；そしてフォーマッタがそれを Format オブジェクトに変換し、これがLeanのinfoviewに表示されます。画面に何かログが表示されたり、#check にカーソルを合わせて出力が表示されたりするのはすべてデラボレータ（delaborator）の仕事です。

本書全体を通して、エラボレータについての言及を目にすることでしょう；そして「付録：整形した出力」章では、デラボレータについて読むことができます。

3つの必須コマンドとその糖衣構文

さて、Leanのソースコードを呼んでいると、 パース/エラボレーション/評価 のプロセスを指定するための11(+?)種のコマンドを見るでしょう：

上記の画像では notation・prefix・infix・postfix がありますが、これらはすべて macro と同じように syntax と @[macro xxx] def ourMacro を組み合わせたものです。これらのコマンドは macro と異なり、特定の形式の構文のみを定義することができます。

これらのコマンドはすべてLean自体やMathlibのソースコードで多用されるため覚えておく価値は十分にあります。しかし、これらのほとんどは糖衣構文であり、以下の3つの低レベルコマンドの動作を学んでおくことでその動作を理解することができます：syntax （構文ルール）・@[macro xxx] def ourMacro （マクロ）・@[command_elab xxx] def ourElab （elab）。

より具体的な例として、#help コマンドを実装しようとしているとします。そうすると、構文ルール・マクロ・elab を次のように書くことができます：

この図は一行ずつ読むことを想定していません。macro_rules と elab を併用しても何ら問題ありません。しかし、3つの低レベルコマンドを使って #help コマンド（最初の行）を指定したとしましょう。これによって、#help "#explode" もしくは #h "#explode" と書くことができます。どちらのコマンドも #explode コマンドのかなり簡素なドキュメントとして "Displays proof in a Fitch table" を出力します。

もし #h "#explode" と書くと、Leanは syntax (name := shortcut_h) ➤ @[macro shortcut_h] def helpMacro ➤ syntax (name := default_h) ➤ @[command_elab default_h] def helpElab というルートをたどります。もし #help "#explode" と書くと、Leanは syntax (name := default_h) ➤ @[command_elab default_h] def helpElab というルートをたどります。

構文ルール・マクロ・elab のマッチングは name 引数を介して行われることに注意してください。もし macro_rules や他の糖衣構文を使った場合、Leanは自力で適切な name 引数を見つけるでしょう。

コマンド以外のものを定義する場合、: command の代わりに : term や : tactic などの構文カテゴリを書くことができます。elab関数は #help の実装に使用した CommandElab だけでなく TermElab と Tactic など、さまざまな型を使用することができます：

  • TermElab は Syntax → Option Expr → TermElabM Expr の省略形で、elab関数は Expr オブジェクトを返すことが期待されます。
  • CommandElab は Syntax → CommandElabM Unit の省略形で、何も返さないべきです。
  • Tactic は Syntax → TacticM Unit の省略形で、何も返さないべきです。

これはLeanの項・コマンド・タクティクに対する直観的な理解に対応しています。項は実行時に特定の値を返し、コマンドは環境を変更したり何かを出力したりし、タクティクは証明の状態を変更します。

実行順序：構文ルール・マクロ・elab

これら3つの重要なコマンドの実行の流れについては、これまであちこちで匂わせてきましたが、ここで明確にしましょう。実行順序は次のような疑似的なテンプレートに従います：syntax (macro; syntax)* elab 。

以下の例を考えてみましょう。

import Lean
open Lean Elab Command

syntax (name := xxx) "red" : command
syntax (name := yyy) "green" : command
syntax (name := zzz) "blue" : command

@[macro xxx] def redMacro : Macro := λ stx =>
  match stx with
  | _ => `(green)

@[macro yyy] def greenMacro : Macro := λ stx =>
  match stx with
  | _ => `(blue)

@[command_elab zzz] def blueElab : CommandElab := λ stx =>
  Lean.logInfo "finally, blue!"

red -- finally, blue!

この処理は以下のように動きます：

  • 適切な syntax ルールにマッチ（ここでは name := xxx）➤ @[macro xxx] を適用 ➤

  • 適切な syntax ルールにマッチ（ここでは name := yyy）➤ @[macro yyy] を適用 ➤

  • 適切な syntax ルールにマッチ（ここでは name := zzz）➤ zzz に適用されるマクロが見つからず、したがって @[command_elab zzz] を適用します。🎉。

糖衣構文（elab や macro 等）の挙動はこれらの第一原理から理解することができます。

Syntax/Expr/実行コード間の手動変換

Leanでは syntax・macro・elab を使うことで前述の パース/エラボレーション/評価 のステップを自動的に実行してくれますが、しかしタクティクを書く際にはこれらの変換を頻繁に手動で行う必要が出るでしょう。この場合、以下の関数を使うことができます：

Syntax を Expr に変換する関数はすべて「elaboration」の略である「elab」で始まることに注意してください；また、Expr （もしくは Syntax）を実際のコードに変換する関数はすべて「evaluation」の略である「eval」から始まります。

代入の意味：マクロ vs エラボレーション？

原則として、elab 関数でできることは（ほとんど？）すべて macro でできます。ただ単に elab の本体にあるものを macro の中に構文として書くだけで良いです。ただし、この経験則を使うのは macro 使う方が変換が単純でエイリアスの設定が本当に初歩的であるときだけにすべきです。Henrik Böving に曰く：「型や制御フローが絡んでしまうとマクロはもはや妥当ではないでしょう」 (Zulip thread)。

従って、糖衣構文・記法・ショートカットを作るには macro を使い、プログラミングのロジックを含むコードを書き出す場合には、たとえ macro で実装できうるものだとしても elab を使いましょう。

追加のコメント

最後に、これからの章を読むにあたって、いくつかの事柄を明らかにしておきましょう。

メッセージの表示

#assertType の例ではコマンドに何かしら表示させるために logInfo を使いました。これの代わりにデバッグを素早く行いたい場合は dbg_trace を使うことができます。

しかし、以下に見るように両者の振る舞いは少し異なります：

elab "traces" : tactic => do
  let array := List.replicate 2 (List.range 3)
  Lean.logInfo m!"logInfo: {array}"
  dbg_trace f!"dbg_trace: {array}"

example : True := by -- `example` is underlined in blue, outputting:
                     -- dbg_trace: [[0, 1, 2], [0, 1, 2]]
  traces -- now `traces` is underlined in blue, outputting
         -- logInfo: [[0, 1, 2], [0, 1, 2]]
  trivial

型の正しさ

メタレベルで定義されるオブジェクトは定理証明において最も興味があるものではないため、型が正しいことを証明するのは時として退屈になりすぎることがあります。例えば、ある式をたどる再帰関数がwell-foundedであることの証明に関心はありません。そのため、関数が終了すると確信が持てるのなら partial キーワードを使うことができます。最悪のケースでは関数がループにはまり、Leanサーバがvscodeでクラッシュしてしまいますが、カーネルに実装されている基本的な型理論の健全性は影響を受けません。