Expr

Lean.Expr は Lean の 抽象構文木(abstract syntax tree) を表すデータ型です。

具象構文木である Syntax から Expr を得る操作のことを エラボレート(elaborate) と呼び、それを行う関数のことを エラボレータ(elaborator) と呼びます。

Syntax と Expr の違い

具象構文木である Syntax との違いを理解するために、具体的な例で比較してみましょう。

import Lean
import Qq


open Qq Lean Parser

/-- 排中律という命題に対応する `Expr` -/
def excludeMiddleExpr : Q(Prop) := q(∀ p : Prop, p ∨ ¬ p)

/- info: "forall (p : Prop), Or p (Not p)" -/
#eval toString excludeMiddleExpr

/-- `s : String` をパースして `Syntax` の項を得る。`cat` は構文カテゴリ。-/
def parse (cat : Name) (s : String) : MetaM Syntax := do
  ofExcept <| runParserCategory (← getEnv) cat s

/-
info: (Term.forall "∀" [`p] [(Term.typeSpec ":" (Term.prop "Prop"))] "," («term_∨_» `p "∨" («term¬_» "¬" `p)))
-/
#eval show MetaM Unit from do
  let stx ← parse `term "∀ p : Prop, p ∨ ¬ p"
  IO.println stx

Repr の出力を比較すると極めて長くなるので ToString の出力を比較しましたが、このように Syntax の方には抽象度の低いコードの情報が含まれています。

定義

Expr は Lean のソースコードの中で次のように定義されています。

open Lean

inductive Expr where
  /-- 束縛変数 -/
  | bvar (deBruijnIndex : Nat)

  /-- 自由変数 -/
  | fvar (fvarId : FVarId)

  /-- メタ変数 -/
  | mvar (mvarId : MVarId)

  /-- 型の宇宙レベルを表す。 -/
  | sort (u : Level)

  /--
  （宇宙多相的な）定数であり、モジュール内で以前に定義されたか、
  import されたモジュールによって定義されたもの。
  -/
  | const (declName : Name) (us : List Level)

  /-- 関数適用 -/
  | app (fn : Expr) (arg : Expr)

  /-- ラムダ抽象(無名関数) -/
  | lam (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)

  /-- 依存関数型 `(a : α) → β` -/
  | forallE (binderName : Name) (binderType : Expr) (body : Expr) (binderInfo : BinderInfo)

  /-- let 式 -/
  | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)

  /-- 自然数リテラルと文字列リテラル。 -/
  | lit : Literal → Expr

  /-- メタデータ（注釈） -/
  | mdata (data : MData) (expr : Expr)

  /-- 射影式(projection expression) -/
  | proj (typeName : Name) (idx : Nat) (struct : Expr)

bvar: 束縛変数

Expr.bvar は 束縛変数(bound variable) を表します。つまり、式の中で let や fun や ∀ などで束縛された変数のことです。deBrujinIndex パラメータは ド・ブラウンインデックス を表します。

たとえば、具体的な式では次のようになります。

open Qq in

/-
info: Lean.Expr.forallE `x (Lean.Expr.const `Nat [])
  ((((Lean.Expr.const `Eq [Lean.Level.zero.succ]).app (Lean.Expr.const `Nat [])).app (Lean.Expr.bvar 0)).app
    (Lean.Expr.bvar 0))
  Lean.BinderInfo.default
-/
#eval q(∀ x : Nat, x = x)

fvar: 自由変数

Expr.fvar は 自由変数(free variable) を表します。つまり、式の中で束縛されていない変数のことです。fvarId パラメータは自由変数の識別子です。

たとえば、証明において各時点で得られている仮定は自由変数であり Expr.fvar で表されます。

open Lean Elab Tactic in

/-- 現在の証明の状態を表示するタクティク -/
elab "my_trace_state" : tactic => do
  -- 現在のローカルコンテキストを取得する
  let ctx ← getLCtx

  for (decl : LocalDecl) in ctx do
    let fvar := Expr.fvar decl.fvarId
    let type := decl.type
    logInfo m!"{fvar} : {type}"

/-
info: _example : ∀ (n : Nat), n > 5 → ∃ n, n > 5
---
info: n : Nat
---
info: hn : n > 5
-/
example (n : Nat) (hn : n > 5) : ∃ n, n > 5 := by
  my_trace_state
  exists n

mvar: メタ変数

Expr.mvar はメタ変数を表します。メタ変数は、式におけるプレースホルダや穴だと考えることができます。つまり、後で具体的な値で埋めることが期待される変数です。

メタ変数の典型的な例は、証明における「現時点で示すべきゴール」です。

open Lean Elab Tactic in

elab "show_goal" : tactic => do
  -- 現在のゴールを取得する
  let goal ← getMainGoal
  let goalExpr := Expr.mvar goal
  -- ゴールの式を表示する
  logInfo m!"{goalExpr}: {goal}"

set_option pp.mvars false in

/- info: ?_: ⊢ True -/
example : True := by
  show_goal
  trivial

sort: 宇宙レベル

Expr.sort は型の宇宙レベルを表します。

universe u

open Lean Expr Qq

/- info: sort Level.zero -/
#eval q(Prop)

/- info: sort Level.zero -/
#eval q(Sort 0)

/- info: sort Level.zero.succ -/
#eval q(Type 0)

const: 定数

Expr.const は定数や関数を表します。

open Lean Qq Expr

/- info: const `Nat [] -/
#eval q(Nat)

/- info: const `Nat.zero [] -/
#eval q(Nat.zero)

/- info: const `Nat.succ [] -/
#eval q(Nat.succ)

/- info: const `List.map [Level.zero, Level.zero] -/
#eval q(@List.map.{0, 0})

app: 関数適用

Expr.app は関数適用を表します。たとえば f と e に対応する Expr がそれぞれ ⟦f⟧ と ⟦e⟧ であるとき、f e に対応する Expr の項は Expr.app ⟦f⟧ ⟦e⟧ です。

open Lean Expr Qq

/- info: (const `Nat.succ []).app (const `Nat.zero []) -/
#eval q(Nat.succ Nat.zero)

lam: ラムダ抽象

Expr.lam はラムダ抽象を表します。つまり、無名関数を表します。

open Lean Expr Qq

/- info: lam `x (const `Nat []) (bvar 0) BinderInfo.default -/
#eval q(fun (x : Nat) => x)

引数について説明しておきます。

binderName は束縛変数の名前を表します。下の例では x です。
binderType は束縛変数の型を表します。下の例では Nat です。
body は関数の返り値を表します。下の例では Expr.bvar 0 で、これは束縛変数 x を参照しています。
binderInfo は束縛変数の情報を表します。明示的な引数なのか、暗黙の引数なのかといった情報を持ちます。

open Lean Expr Qq Level

/- info: "fun (x : Nat) => x" -/
#eval show String from
  let expr := Expr.lam
    (binderName := `x)
    (binderType := q(Nat))
    (body := Expr.bvar 0)
    (binderInfo := .default)
  toString expr

/-
info: lam `α (sort zero.succ)
  (lam `x (bvar 0) ((((const `Eq [zero.succ]).app (bvar 1)).app (bvar 0)).app (bvar 0)) BinderInfo.default)
  BinderInfo.implicit
-/
#eval q(fun {α : Type} (x : α) => x = x)

forallE: 依存関数型

Expr.forallE は依存関数型または全称量化を表現します。

open Lean Expr Qq Level

/-
info: forallE `P (sort zero) (forallE Name.anonymous (bvar 0) (bvar 1) BinderInfo.default) BinderInfo.default
-/
#eval q(∀ (P : Prop), P → P)

/-
info: forallE `n (const `Nat []) (((const `Vector [zero]).app (const `Nat [])).app (bvar 0)) BinderInfo.default
-/
#eval q((n : Nat) → Vector Nat n)

letE: let 式

Expr.letE は let 式を表します。let 式は、変数を束縛してその値を後続の式で使用するために使われます。

open Lean Expr Qq

/-
info: letE `x (const `Nat [])
  ((((const `OfNat.ofNat [Level.zero]).app (const `Nat [])).app (lit (Literal.natVal 0))).app
    ((const `instOfNatNat []).app (lit (Literal.natVal 0))))
  (bvar 0) false
-/
#eval q(let x : Nat := 0; x)

lit: 自然数リテラルと文字列リテラル

Expr.lit は自然数リテラルや文字列リテラルを表します。

open Lean Expr Qq

/- info: lit (Literal.strVal "Lean is nice!") -/
#eval q("Lean is nice!")

Lean by Example