式

式（Expr 型の項）はLeanプログラムの抽象構文木です。つまり、Leanで記述される各項には対応する Expr があります。例えば、関数適用 f e は式 Expr.app ⟦f⟧ ⟦e⟧ で表現されます。ここで ⟦f⟧ は f の表現であり、⟦e⟧ は e の表現です。同様に、Nat という項は Expr.const `Nat [] という式で表されます。（バッククォートと空リストについては後述します。）

Leanのタクティクブロックの最終的な目的は証明したい定理の証明となる項を生成することです。つまり、タクティクの目的は正しい型（の一部）の Expr を生成することです。したがって、メタプログラミングの多くは式を操作することに帰着します：新しい項を構成したり、既存の項を分解したりします。

タクティクブロックが終了すると、Expr はカーネルに送られます。カーネルはこの項がきちんと型付けされているか、定理が主張する型を本当に持っているかをチェックします。結果として、タクティクのバグは致命的なものにはなりません：もしミスがあっても、最終的にはカーネルがそれをキャッチしてくれます。しかし、多くのLeanの内部関数も式がきちんと型付けされていることを仮定しているため、式がカーネルに到達する前にLeanがクラッシュする可能性があります。これを避けるためにLeanは式の操作を支援する多くの関数を提供しています。この章と次の章では最も重要なものを調査します。

Expr の型について実際のものを見てみましょう：

import Lean

namespace Playground

inductive Expr where
  | bvar    : Nat → Expr                              -- bound variables
  | fvar    : FVarId → Expr                           -- free variables
  | mvar    : MVarId → Expr                           -- meta variables
  | sort    : Level → Expr                            -- Sort
  | const   : Name → List Level → Expr                -- constants
  | app     : Expr → Expr → Expr                      -- application
  | lam     : Name → Expr → Expr → BinderInfo → Expr  -- lambda abstraction
  | forallE : Name → Expr → Expr → BinderInfo → Expr  -- (dependent) arrow
  | letE    : Name → Expr → Expr → Expr → Bool → Expr -- let expressions
  -- less essential constructors:
  | lit     : Literal → Expr                          -- literals
  | mdata   : MData → Expr → Expr                     -- metadata
  | proj    : Name → Nat → Expr → Expr                -- projection

end Playground

それぞれのコンストラクタは何をするのでしょうか？

bvar は 束縛変数 （bound variable）です。例えば、fun x => x + 2 や ∑ x, x² などにおいての x です。これはある変数について、それの上に束縛子（binder）がいる場合のその式中での変数の出現を表します。なぜ引数は Nat なのでしょうか？これはde Bruijnインデックスと呼ばれるもので、後で説明します。束縛変数の型はその束縛子を見ればわかります。というのも束縛子は常にその変数の型の情報を持っているからです。
fvar は 自由変数 （free variable）です。これは束縛子で束縛されていない変数のことです。自由変数 x について、それを見ても型が何であるか知ることができないことに注意してください。型を知るには x とその型の宣言を含むコンテキストが必要です。自由変数にはIDがあり、これはその変数を LocalContext のどこを探せばよいかを教えてくれます。Lean 3では、自由変数は「ローカル変数」または「ローカル」と呼ばれていました。
mvar は メタ変数 （metavariable）です。これについては後ほど詳しく説明しますが、プレースホルダや、後で埋める必要のある表現のための「穴」と考えてもらえれば良いです。
sort は Type u や Prop などで使われます。
const はLeanの記述中でそこまでに定義済みの定数です。
app は関数適用です。複数の引数の場合は 部分適用 （partial application）を用います：f x y ↝ app (app f x) y。
lam n t b はラムダ式（fun ($n : $t) => $b）です。引数 b は本体（body）と呼ばれます。束縛する変数の型を指定する必要がある点に注意してください。
forallE n t b は依存矢印式（($n : $t) → $b）です。これはΠ型、もしくはΠ式とも呼ばれ、しばしば ∀ $n : $t, $b と書かれます。依存しない矢印 α → β は β が a に依存しない (a : α) → β の特殊な場合であることに注意してください。forallE の末尾の E は forall キーワードと区別するためのものです。
letE n t v b は let束縛子 （let binder）です（let ($n : $t) := $v in $b）。
lit は リテラル （literal）で、これは 4 や "hello world" などの数値や文字列のリテラルです。リテラルはパフォーマンスを向上させることに役立ちます：式 (10000 : Nat) を Nat.succ $ ... $ Nat.succ Nat.zero のように表現したくはありません。
mdata は式の性質を変えることなく、式に役立つかもしれない追加の情報を保存するためだけのものです。
proj は射影を表します。p : α × β のような構造体があるとすると、射影 π₁ p を app π₁ p として格納するのではなく、proj Prod 0 p と表現します。これは効率化のためです。

おそらく読者は明らかに対応する Expr を持たない多くのLeanプログラムを書くことができることに気付いているでしょう。例えば、match 文や do ブロック、by ブロックはどうすればいいのでしょうか？これらの構文やその他多くの構文はまず式に変換する必要があります。Leanにおいてこの（実質的な）タスクを実行する部分はエラボレータと呼ばれ、それ用の章で説明します。この構成の利点は、いったん Expr への変換が終われば、比較的単純な構造で作業ができることです。（欠点は Expr から高レベルのLeanプログラムに戻るのが難しいことです。）

エラボレータはまた、読者がLeanのプログラムで省略した暗黙の引数や型クラスのインスタンス引数も埋めます。このように Expr レベルでは暗黙的であろうとなかろうと、定数は常にすべての引数に適用されます。これは祝福（というのもソースコードでは明確でなかった多くの情報を得ることができるからです）であり、また呪い（Expr を組み立てる時に暗黙の引数やインスタンス引数を自分で指定しなければならないからです）でもあります。

De Bruijn インデックス

次のラムダ式 (λ f x => f x x) (λ x y => x + y) 5 を考えてみると、変数 x が衝突しているため、これを簡約する際には細心の注意を払う必要があります。

変数名の衝突を避けるために、Expr では de Bruijnインデックス と呼ばれる巧妙な技法を使用します。de Bruijnインデックスにおいて、lam や forallE で束縛された各変数は #n という数値に変換されます。この数字は、この変数を束縛している束縛子を見つけるために Expr ツリーの何番目の束縛子を探せばよいかを示しています。そのため、上記の例は次のようになります（簡潔にするために型引数にはワイルドカード _ を入れています）：app (app (lam `f _ (lam `x _ (app (app #1 #0) #0))) (lam `x _ (lam `y _ (app (app plus #1) #0)))) five。これでβ簡約を実行する際に変数名を変更する必要がなくなります。また、束縛された式を含む2つの Expr が等しいかどうかも簡単にチェックできます。これが bvar のシグネチャが Name → Expr ではなく Nat → Expr である理由です。

もしde Bruijnインデックスがそこまでに定義された束縛子の数よりも大きすぎる場合、loose bvar と言います；そうでない場合は 束縛されている と言います。例えば、式 lam `x _ (app #0 #1) では、bvar #0 は先行する束縛子によって束縛され、#1 はlooseです。Leanがすべてのde Bruijnインデックスを bvar （「束縛変数」）と呼んでいる事実は重要な不変性を示しています：いくつかの低レベルな関数以外では、Leanはすべての式がlooseな bvar を含まないことを期待しています。一方でlooseな bvar を導入したい場合は、直ちに fvar （「自由変数」）に変換します。この具体的な方法については次の章で説明します。

式の中にlooseな bvar が無い場合、その式は 閉じている （closed）と言います。looseな bvar のインスタンスをすべて Expr に置き換えるプロセスは インスタンス化 （instantiation）と呼びます。その逆は 抽象化 （abstraction）と呼ばれます。

もし読者が変数にまつわる標準的な用語に慣れているならLeanの用語は混乱するかもしれないので、ここで対応を挙げます：Leanでの「bvar」は通常単に「変数」と呼ばれます；「loose」は通常「自由」と呼ばれます；「fvar」は「ローカルな仮定」と呼ばれることがあります。

宇宙レベル

いくつかの式は Lean.Level 型で表される宇宙レベルを含みます。宇宙レベルは自然数であり、宇宙パラメータ（universe 宣言で導入されます）、宇宙メタ変数、または2つの宇宙の最大値となります。これらは2種類の式の表現に関連します。

まず、ソートは Expr.sort u で表現されます。ここで u は Level です。Prop は sort Level.zero です；Type は sort (Level.succ Level.zero) です。

次に、宇宙多相な定数は宇宙引数を持ちます。宇宙多相な定数とは宇宙パラメータを持つ型のことです。例えば、pp.universe オプションによる整形表示が示すように、List.map 関数は宇宙多相です：

set_option pp.universes true in
#check @List.map

List.map の接尾辞 .{u_1,u_2} は List.map が2つの宇宙引数 u_1 と u_2 を持つことを意味します。List の後の接尾辞 .{u_1} （これ自体が宇宙多相な定数）は List が宇宙引数 u_1 に適用されることを意味し、.{u_2} についても同様です。

実は、宇宙多相な定数を使うときは必ず正しい宇宙引数に適用しなければなりません。この適用は Expr.const の List Level 引数で表現されます。通常のLeanコードを書くとき、Leanは自動的に宇宙を推論するため、あまり考える必要はありません。しかし、自力で Expr を構築する際には、それぞれの宇宙多相な定数を正しい宇宙引数に適用するように注意しなければなりません。

式の構築

定数

もっとも単純な式は定数です。これにあたってはコンストラクタ const を使い、名前と宇宙レベルのリストを与えます。ここでのほとんどの例では宇宙多相ではない定数のみを使用しており、この場合リストは空になります。

また2つのバッククォートで名前を記述する第二の形式も示します。これは名前が実際に定義された定数を指しているかどうかをチェックするもので、タイプミスを避けるにあたって便利です。

open Lean

def z' := Expr.const `Nat.zero []
#eval z' -- Lean.Expr.const `Nat.zero []

def z := Expr.const ``Nat.zero []
#eval z -- Lean.Expr.const `Nat.zero []

また、バッククォート2つバージョンは与えられた名前を解決し、完全に修飾します。このメカニズムを説明するために、さらに2つの例を挙げましょう。1つ目の式 z₁ は安全ではありません：もし Nat 名前空間が開かれていないコンテキストで使用すると Leanは環境に zero という定数が無いと文句を言います。対照的に、2番目の式 z₂ は完全修飾名 Nat.zero を含んでおり、この問題はありません。

open Nat

def z₁ := Expr.const `zero []
#eval z₁ -- Lean.Expr.const `zero []

def z₂ := Expr.const ``zero []
#eval z₂ -- Lean.Expr.const `Nat.zero []

関数適用

次に考える式の話題は関数適用です。これらは app コンストラクタを使って構築することができ、第1引数には関数の式を、第2引数には引数の式を指定します。

ここでは2つの例を挙げます。ひとつは単純に定数を別の定数に適用したものです。もう一つは式を自然数の関数として与える再帰的定義です。

def one := Expr.app (.const ``Nat.succ []) z
#eval one
-- Lean.Expr.app (Lean.Expr.const `Nat.succ []) (Lean.Expr.const `Nat.zero [])

def natExpr: Nat → Expr
| 0     => z
| n + 1 => .app (.const ``Nat.succ []) (natExpr n)

次では、複数の引数を持つ適用を可能にする mkAppN を用いています。

def sumExpr : Nat → Nat → Expr
| n, m => mkAppN (.const ``Nat.add []) #[natExpr n, natExpr m]

お気づきかもしれませんが、最後の2つの関数については #eval の出力を示しませんでした。これは結果の式が大きくなりすぎて意味を理解するのが難しいからです。

ラムダ抽象

次にコンストラクタ lam を使って、任意の自然数を受け取って Nat.zero を返す単純な関数を作成します。引数の BinderInfo.default は x が（暗黙の引数や型クラスの引数ではなく）明示的な引数であることを表しています。

def constZero : Expr :=
  .lam `x (.const ``Nat []) (.const ``Nat.zero []) BinderInfo.default

#eval constZero
-- Lean.Expr.lam `x (Lean.Expr.const `Nat []) (Lean.Expr.const `Nat.zero [])
--   (Lean.BinderInfo.default)

宇宙レベルに絡んだより込み入った例として、以下の Expr は　List.map (λ x => Nat.add x 1) [] を表します（多少読みやすくするためにいくつかの定義に分割しています）：

def nat : Expr := .const ``Nat []

def addOne : Expr :=
  .lam `x nat
    (mkAppN (.const ``Nat.add []) #[.bvar 0, mkNatLit 1])
    BinderInfo.default

def mapAddOneNil : Expr :=
  mkAppN (.const ``List.map [levelZero, levelZero])
    #[nat, nat, addOne, .app (.const ``List.nil [levelZero]) nat]

ちょっとした技法を使えば（詳しくはエラボレーションの章で）、この Expr をLeanの項にして、より簡単に検査できるようにすることができます。

elab "mapAddOneNil" : term => return mapAddOneNil

#check mapAddOneNil
-- List.map (fun x => Nat.add x 1) [] : List Nat

set_option pp.universes true in
set_option pp.explicit true in
#check mapAddOneNil
-- @List.map.{0, 0} Nat Nat (fun x => x.add 1) (@List.nil.{0} Nat) : List.{0} Nat

#reduce mapAddOneNil
-- []

次の章では、MetaM モナドを探求します。このモナドは多くのほかのモナドの中において、より大きな式をより便利に構築・分解できるようにします。

演習問題

式 1 + 2 を Expr.app で作ってください。
式 1 + 2 を Lean.mkAppN で作ってください。
式 fun x => 1 + x を作ってください
[de Bruijn インデックス] 式 fun a, fun b, fun c, (b * a) + c を作ってください。
式 fun x y => x + y を作ってください。
式 fun x, String.append "hello, " x を作ってください。
式 ∀ x : Prop, x ∧ x を作ってください。
式 Nat → String を作ってください。
式 fun (p : Prop) => (λ hP : p => hP) を作ってください。
[宇宙レベル] 式 Type 6 を作ってください。

Metaprogramming in Lean 4 日本語訳