Type Checking in Lean 4

このドキュメントは、読者が Lean のカーネルをよりよく理解し、Lean を使用する際の信頼の前提を明確にし、Lean のカーネル言語用に独自の外部型チェッカを書きたい人のためのリソースとなることを目的としています。

この翻訳について

この翻訳は有志による 非公式 翻訳です。翻訳に際して分かりやすさのために表現を大きく変えた箇所があります。また、用語の訳が一般的でない・誤りを含む可能性があります。必要に応じて原文 Type Checking in Lean 4(GitHub)をご覧ください。

原文のライセンスはApache License 2.0であり、それに基づいて原文を翻訳・公開しています。

誤字脱字・内容の誤りの指摘・フォークからのPull Request・フォークによる翻訳の改変等歓迎いたします。ご指摘は当該リポジトリにてIssue・Pull Requestで受け付けております。

翻訳に際して、機械翻訳サービス DeepL翻訳を参考にしました。

バージョン情報

この翻訳は原文のcommit fb99301873182d6a6712523c78502e68d965de05 に基づいています。

Foreword

The author would like to thank:

Mario Carneiro

Leonardo de Moura

Sebastian Ullrich

Gabriel Ebner

Jonathan Protzenko

The Lean Zulip community.

Each and every contributor to Lean4, Mathlib, and the broader Lean ecosystem.

This book is dedicated to the memory of Philip Elliot Bailey (31 January, 1987 - 9 December, 2023).

カーネルとは何か？

カーネル（kernel）とは Lean の論理をソフトウェアで実装したもののことです；Lean の論理言語の要素を構築し、それらの要素の正しさをチェックするための必要最小限の機構を備えたコンピュータプログラムです。主な構成要素は以下の通りです：

アドレッシングのための名前。

宇宙レベル。

式（ラムダ式、変数など）

宣言（公理・定義・定理・帰納型など）

環境、これは名前から宣言へのマップです。

式の操作のための機能。例えば、束縛変数の置換や宇宙パラメータの置換など。

型推論・簡約・定義上の等しさ（definitional equality）など、型検査で用いられる中核的な操作。

帰納型の宣言を操作し、チェックする機能。例えば、型の再帰子（recursor、除去則）を生成したり、型のコンストラクタが型の仕様に合致しているかどうかのチェックをしたりします。

オプションのカーネル拡張、自然数や文字列リテラルへ上記の操作を実行できます。

カーネルを小さいパーツに分離し、Lean の定義を最小限のカーネル言語に翻訳することを求める目的は、証明システムの信頼性を高めることです。Lean の設計によって堅牢なメタプログラミング・豊富なエディタサポート・拡張可能な構文といった素晴らしい機能を網羅した証明支援系とユーザの対話が可能になる、一方で（証明支援系である）Lean を生産的で快適に使用できるようにする高水準の機能を実装するコードの正しさを信頼することなく、構築された証明項を検証可能な形に抽出することを可能にします。

Certified Programming with Dependent Types の 1.2.3 節にて、Adam Chlipala は de Bruijn 基準、もしくは de Bruijn 原理と呼ばれるものを定義しています。

証明支援系は、たとえ証明を探索するために複雑で拡張可能な手続きをはじめから使っている場合であっても、小さなカーネル言語で証明項を生成すれば「de Bruijn 基準」を満たす。これらのコア言語は、数学の形式的基礎（例えば ZF 集合論）の提案に見られるような複雑さを持っている。証明を信じるには、探索中のバグの可能性を無視し、探索結果に適用する（比較的小さな）証明チェック用のカーネルに頼ればよい。

Lean のカーネルは十分に小さいため、開発者は独自の実装を書くことができ、エクスポータ ¹ を使うことで独自に Lean の証明をチェックすることができます。Lean のエクスポートフォーマットには、エクスポートされた宣言に関する十分な情報が含まれているため、ユーザはオプションで実装をカーネル全体の特定のサブセットに限定することができます。例えば、推論・簡約・定義上の等しさのコア機能に興味のあるユーザは帰納的な仕様のチェック機能の実装を省略することができます。

上記のリストに加え、外部の型チェッカは Lean のエクスポートフォーマット用のパーサと、入出力用でそれぞれにプリティプリンタも必要になります。パーサとプリティプリンタはカーネルの一部ではありませんが、カーネルと興味深いやり取りをしたいのであれば重要です。

自分で型チェッカを書くことは容易なプロジェクトではありませんが、市民科学者にとっては十分達成可能な範囲です。

信頼

Lean が提供する価値の大部分は、プログラムの正しさに関する証明を含む数学的証明を構築する能力です。これに対するユーザの一般的な疑念は、Lean を信頼するには、具体的に何をどの程度信頼すればよいのかということです。

この質問に対する回答は2つの部分からなります：すなわち、Lean における証明を信頼するためにユーザがまず信頼すべきものは何かということ、そして Lean プログラムをコンパイルして得られる実行可能プログラムを信頼するためにユーザが信頼すべきものは何かということです。

この違いは具体的には、証明（プログラムに関する文を含む）とコンパイルされていないプログラムが Lean のカーネル言語で直接表現でき、カーネルの実装によってチェックされるというものです。これらは実行ファイルにコンパイルする必要はなく、そのため、この信頼はこれらをチェックするカーネルの実装に限定され、Lean のコンパイラは信頼できるコードベースの一部にはなりません。

コンパイルされた Lean プログラムの正しさを信頼するには、Lean のコンパイラを信頼する必要がありますが、コンパイラはカーネルとは別物であり、Lean のコアロジックの一部ではありません。ここで Lean の 文とプログラム を信頼することと、Lean のコンパイラが生成したプログラム を信頼することは区別されます。Lean のプログラムに関する文は証明であり、カーネルだけを信頼すればよいカテゴリに入ります。プログラムに関する証明が コンパイルされたプログラムの動作にまで及ぶこと を信頼することで、コンパイラは信頼されるコードベースに入ります。

注意：タクティクや他のメタプログラムは、たとえコンパイルされたタクティクであっても信頼される必要は 全くありません；これらは他で使用されるカーネルの項を生成するために使用される信頼されていないコードです。ある命題 P は信頼されたコードベースをカーネルを超えて拡張することなく、任意に複雑なコンパイル済みのメタプログラムを使って証明することができます。なぜならこのメタプログラムは Lean のカーネル言語で表現された証明を生成する必要があるからです。

これらの文はエクスポートされた証明に対して有効です。より ~~くどい~~ 警戒心の強い読者を満足させるために、これは例えば、エクスポータと検証器を実行するために使用されるコンピュータの OS・ハードウェアなどに対するある程度の信頼を必然的に伴います。

エクスポートされていない証明については、ユーザはさらにカーネル外の Lean の要素（エラボレータ、パーサなど）を信頼することになります。

より詳細なリスト

Lean 4 に関連する信頼について、Mario Carneiro による Lean の Zulip への投稿からより詳細に説明しましょう。

一般的に：

Lean のロジックが健全であること（原著者注：これには Nat や String のようなカーネルの拡張も含まれる）を信頼する。

プログラムの正しさを証明しなかった場合、エラボレータがあなたの入力から期待するプログラムを示す Lean の式に変換したことを信頼する。

プログラムが正しいことを証明したのであれば、そのプログラムに関する証明がチェックされていることを信頼する（これを排除するために外部のチェッカを使う）。

これらすべてを動かしているハードウェア・ファームウェア・OS ソフトウェアが壊れたり、嘘をついたりしていないことを信頼する。

（プログラムを実行する時）ハードウェア・ファームウェア・OS ソフトウェアが仕様通りに忠実にプログラムを実行し、デバッガやハードディスク上の磁石や宇宙線がプログラムの出力を乱すことがないことを信頼する。

複雑な実行ファイルについて：

コンパイラのオーバーライド（extern・implemented_by）がLean のロジックに違反しないことを信頼する（すなわち、モデルが実装と一致する）。

Lean のコンパイラ（Lean コードを C に変換）がプログラムの意味を維持することを信頼する。

C プログラムを同じ意味を持つ実行ファイルに変換する clang・LLVM を信頼する。

前半のポイントは証明とコンパイルされた実行ファイルの両方に適用され、後半のポイントは特にコンパイルされた実行ファイルに適用されます。

外部チェッカへの信頼

Lean のロジックが健全であることをとにかく信頼する。

外部チェッカの開発者が適切にプログラムを実装していることを信頼する。

実装言語のコンパイラやインタプリタを信頼する。複数の外部チェッカを実行する場合、それらをベン図の円のように考えることができます；円が交差する部分に健全性の問題がないことを信頼します。

Nat と String のカーネル拡張について、おそらく実装言語の bignum ライブラリと UTF-8 文字列型を信頼する。

外部チェッカを使用する利点は以下の通りです：

ユーザは Lean のエコシステムから切り離され、Lean のコードベースのどの部分にも依存しないものを使って結果をチェックすることができます。

外部チェッカは成熟したコンパイラやインタプリタを利用するように書くことができます。

カーネル拡張に対しては、ユーザは複数の bignum・string 実装の結果をクロスチェックできます。

エクスポート機能を使うことは、Lean のカーネル外の部分を信頼することから抜け出す唯一の方法です。したがって、エクスポートされたファイルが lean4lean のようなものによってチェックされたとしてもこれを行うことには利点があります。それゆえ Lean のメタプログラミング機能の誤用による影響を心配するユーザはエクスポート機能を使うことが推奨されます。

安全でない宣言

Lean の特異なマークとして、ユーザは unsafe とマークされた宣言を書くことができ、これによって通常であれば禁止されるようなものが許可されるようになります。例えば、Lean は次のような定義を許可しています：

  unsafe def y : Nat := y

安全でない宣言はエクスポートされず ¹、信頼される必要もなく、（ちなみに）たとえこのマークがついたものの中であったとしても証明にて使うことは許可されません。それでもこのマークによる安全でない宣言の許可は Lean ユーザにとって有益です。なぜなら、証明を生成するために使用されるもののそれ自体に対しておよびそれ自体が証明である必要がないコードを書く際に、より多くの自由をユーザに与えるからです。

このことについて aesop ライブラリは優れた実例を有しています。Aesop は自動化のフレームワークです；これはユーザが証明を生成することを補助します。このライブラリのある時点で、aesop の作者たちはシステムのある部分を表現するにあたって、ここで見られるように相互に定義された帰納型を使うことが最適だと考えました。偶然にも、この帰納型のセットは Lean の理論で宣言されている型の中に1つ無効なものがあり、Lean のカーネルでは許可されないため unsafe とマークする必要があります。

それでもこの定義を unsafe の宣言として許可することは開発者とユーザのどちらにとっても有益です。aesop の開発者は、Lean を使ってこのライブラリを書くにあたり望むままにライブラリを書くことができますが、それにあたってメタプログラミングの DSL を呼び出すことなく（そして学ぶこともなく）、またカーネルを満足させるために抜け道を使う必要もありません。aesop のユーザも aesop による 証明を aesop 自体を検証する必要なくエクスポートし検証することができます。

技術的には、安全でない宣言をエクスポートファイルに入れることを妨げることはできません（特にエクスポートファイルは信頼できるコンポーネントではないため）が、カーネルが実行するチェックによって、安全でない宣言が実際に安全でない場合には環境に追加されることを防ぐことができます。適切に実装された型チェッカは上記の aesop ライブラリを宣言したエクスポートファイルを受け取った場合にエラーを投げるでしょう。

敵対的な入力

より一般的な信頼の問題に対してしばしば付随するトピックとして、敵対的な入力に対する Lean の堅牢性が挙げられます。

正しい型チェッカは利用者が許可する公理のもとにおいて、受け取る入力を Lean の型システムのルールで制限します。利用者が許容する公理を3つの「公式の」公理（propext・Quot.sound・Classical.choice）に制限した場合、入力ファイルはどのような状況においても型チェッカが受け入れる prelude の False である証明を提供することはできないはずです。

しかし、最小の型チェッカは論理的には正しいですが、利用者を欺くように設計された Lean の宣言を提供する入力から積極的に保護することはできません。例えば、敵が深い依存関係を理解した上で再定義してレフェリーが検査しないようにしたり、ユニコードに似たものでプリティプリンタの出力を生成するようなものを導入しつつその裏で重要な定義変更をしたりできてしまいます。

「ある定理が形式的に証明されたとユーザが考える一方で、実際にはシステムが実際に行ったことが何であるかについてユーザが誤解している」というアイデアは Pollack consistency という概念で扱われており、Freek Wiedijk によるこの書籍¹ で議論されています。

このようなカーネルの最小限の機能でカバーできない攻撃に対する保護を提供するために、開発者がソフトウェアを書いたり、型チェッカを拡張したりすることは原理的に妨げるものは何もありません。しかし、Lean のユーザがその強力なカスタム構文とマクロシステムをどの程度まで受け入れているか、ここまでの話を改善することに興味を持つ人々にとっていくつかの課題が生じる可能性があります。読者におかれましては、このことを多少なりとも今後の課題として考えるべきでしょう。

Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012

エクスポートファイル

エクスポータは外部の型チェッカが利用できるように、カーネル言語を使って Lean の宣言の出力を行うプログラムのことです。出力されるエクスポートファイルは Lean のエコシステムから完全に分離されています；ファイル内のデータは完全に外部のソフトウェアでチェックすることができ、エクスポータ自体は信頼できるコンポーネントではありません。これらの宣言が開発者の意図通りにエクスポートされたかどうかを確認するためにエクスポートファイル自体を検査するのではなく、エクスポートされた宣言は外部のチェッカによってチェックされ、エクスポートファイルよりもはるかに読みやすい出力を生成するプリティプリンタによる表示をユーザは確認します。読者は Lean のエクスポートファイル用に独自の外部チェッカを書くことができます（また、推奨されます）。

公式のエクスポータは lean4export です。

現在のエクスポートファイルのフォーマットは下記に詳細を挙げます。また、エクスポートフォーマットをどのように進化させるのがベストなのかについて現在進行形の議論もあります。

(ver 0.1.2)

分かりやすくするために、複合的な要素のいくつかは、例えば (name : T) のようにここでは名前で装飾されていますが、エクスポートファイルでは単なる T の要素として表示されます。

相互の帰納とネストした帰納についてのエクスポートスキーマは次の通りです：

Inductive.inductiveNames は mutual .. end ブロック内のすべての型の名前を含みます。入れ子になった（しかし相互ではない）構成で使用される他の帰納型の名前は含まれません。
Inductive.constructorNames にはその帰納型のすべてのコンストラクタの名前が含まれ、他には何も含まれません（相互ブロック内の他の型のコンストラクタや、入れ子構造のコンストラクタは含まれません）。

注意： 独自のパーサやチェッカを書いている読者は name[0] を匿名の名前として初期化し、level[0] を宇宙レベル 0 として初期化すべきです。こうすることでこれらはエクスポータに出力されず、しかしこれらの名前とレベルの添字が 0 を占めることが期待されます。

File ::= ExportFormatVersion Item*

ExportFormatVersion ::= nat '.' nat '.' nat

Item ::= Name | Universe | Expr | RecRule | Declaration

Declaration ::= 
    | Axiom 
    | Quotient 
    | Definition 
    | Theorem 
    | Inductive 
    | Constructor 
    | Recursor

nidx, uidx, eidx, ridx ::= nat

Name ::=
  | nidx "#NS" nidx string
  | nidx "#NI" nidx nat

Universe ::=
  | uidx "#US"  uidx
  | uidx "#UM"  uidx uidx
  | uidx "#UIM" uidx uidx
  | uidx "#UP"  nidx

Expr ::=
  | eidx "#EV"  nat
  | eidx "#ES"  uidx
  | eidx "#EC"  nidx uidx*
  | eidx "#EA"  eidx eidx
  | eidx "#EL"  Info nidx eidx
  | eidx "#EP"  Info nidx eidx eidx
  | eidx "#EZ"  Info nidx eidx eidx eidx
  | eidx "#EJ"  nidx nat eidx
  | eidx "#ELN" nat
  | eidx "#ELS" (hexhex)*
  -- metadata node w/o extensions
  | eidx "#EM" mptr eidx

Info ::= "#BD" | "#BI" | "#BS" | "#BC"

Hint ::= "O" | "A" | "R" nat

RecRule ::= ridx "#RR" (ctorName : nidx) (nFields : nat) (val : eidx)

Axiom ::= "#AX" (name : nidx) (type : eidx) (uparams : uidx*)

Def ::= "#DEF" (name : nidx) (type : eidx) (value : eidx) (hint : Hint) (uparams : uidx*)
  
Theorem ::= "#THM" (name : nidx) (type : eidx) (value : eidx) (uparams: uidx*)

Quotient ::= "#QUOT" (name : nidx) (type : eidx) (uparams : uidx*)

Inductive ::= 
  "#IND"
  (name : nidx) 
  (type : eidx) 
  (isRecursive: 0 | 1)
  (isNested : 0 | 1)
  (numParams: nat) 
  (numIndices: nat)
  (numInductives: nat)
  (inductiveNames: nidx {numInductives})
  (numConstructors : nat) 
  (constructorNames : nidx {numConstructors}) 
  (uparams: uidx*)

Constructor ::= 
  "#CTOR"
  (name : nidx) 
  (type : eidx) 
  (parentInductive : nidx) 
  (constructorIndex : nat)
  (numParams : nat)
  (numFields : nat)
  (uparams: uidx*)

Recursor ::= 
  "#REC"
  (name : nidx)
  (type : eidx)
  (numInductives : nat)
  (inductiveNames: nidx {numInductives})
  (numParams : nat)
  (numIndices : nat)
  (numMotives : nat)
  (numMinors : nat)
  (numRules : nat)
  (recRules : ridx {numRules})
  (k : 1 | 0)
  (uparams : uidx*)

カーネルのコンセプト

本章では、すべての人が読むべき高レベルのロードマップから始まり、カーネルの基本部品を理解するために必要ないくつかのアイデアをカバーします。理論面にはあまり重点を置きません。この後出てくる節での考え方は前もって完全に理解しておく必要はなく、読者は気軽にさっと目を通して必要に応じて戻ってくると良いでしょう。

全体像

読者に道筋を示すために、エクスポートファイルをチェックする全手順を構成するステップを以下に挙げます：

エクスポートファイルを解析し、各プリミティブのあつまりのコンポーネントのコレクションを生成します：ここでプリミティブは名前・レベル・式と宣言のコレクションです。

パースされた宣言のコレクションは環境を表します。環境とは各宣言の名前から宣言そのものへのマッピングです；これらの宣言こそ型チェックプロセスのターゲットです。

環境内の各宣言に対してカーネルは、その宣言が環境内に既に宣言されていないこと、重複した宇宙パラメータを持たないこと、宣言の型が値ではなく実際に型であること（infer declar.ty が式 Sort <n> を返すこと）、宣言の型に自由変数がないことを要求します。

定義・定理・opaque な宣言については、定義の値の型を推論することでユーザが宣言に割り当てた型と定義上等しい式が得られることを保証します。これは証明が正しいことを保証する点において肝心なところであり、定理については「ユーザはこれが P の証明であると言っているが、その値は実際に P の有効な証明を構成しているか？」ということに対応するステップです。

帰納的な宣言・それのコンストラクタ・再帰子については、それらが適切に形成され、Lean の型理論の規則に準拠していることをチェックします（これについては後で詳しく説明します）。

エクスポートファイルに商の型のプリミティブ宣言が含まれている場合は、それらの宣言が正しい型を持っていること、そして Eq 型が存在し、適切に定義されていることを確認します（商は同値に依存するため）。

最後に、ユーザから要求された宣言をプリティプリントし、チェックした宣言がエクスポートした宣言と一致しているかどうかをユーザがチェックできるようにします。

言語の明確化

型・ソート・命題

Prop は Sort 0 を指します。

Type n は Sort (n+1) を指します。

Sort n はカーネルでの実際の表現で、常に使用することができます。

時折 Type <N> と Prop が常に Sort n に従う代わりに使われることがあるのは、Type <N> の要素には Prop の要素では観察されない重要な性質や振る舞いがあり、その逆もまたあるからです。

例：Prop の要素は定義の証明の無関係性を考慮することができますが、Type _ の要素は別でテストに合格することなく large elimination を使用することができます。

レベル・宇宙とソート

「レベル」と「宇宙」という用語は基本的には同義語です；これらは同じ種類のカーネルのオブジェクトを指します。

小さな違いとして、「宇宙パラメータ」は暗黙裡に変数・パラメータであるレベルに制限されることがあります。これは「宇宙パラメータ」が Lean の宣言をパラメータ化するレベルのあつまりを指しますが、これは識別子にしかなり得ないことから識別子に限定されます。もしこれが読者にとって意味が無くても今は気にしないでください。例として、ある Lean の宣言が def Foo.{u} .. ではじまると、これは「宇宙変数 u によってパラメータ化された定義」を意味しますが、これを def Foo.{1} .. で始めることはできません。なぜなら 1 は明示的なレベルであり、パラメータではないからです。

一方で、Sort _ はレベルを表現した式のことです。

値 vs 型

式は値にも型にもなります。おそらく読者は Nat.zero が値である一方で Nat が型であることにはなじみがあるでしょう。もし infer e != Sort _ ならば、式 e は「値レベルの式」です。もし infer(e) = Sort _ ならば、式 e は型か「型レベルの式」です。

パラメータ vs 添字

パラメータと添字の区別は帰納型を扱う際に出てきます。大雑把に言えば、宣言のコロンの前にはめ込まれた要素はパラメータで、コロンの後に来る要素は添字です：

      parameter ----v         v---- index
inductive Nat.le (n : Nat) : Nat → Prop

この違いはカーネルに無視されません。というのもパラメータは宣言内で固定されますが、添字は固定されないからです。

インスタンス化と抽象化

インスタンス化は束縛変数を適切な引数に置き換えることです。抽象化は束縛子を置換する際に、自由変数を適切な束縛変数に置き換えることです。Lean のカーネルは束縛変数には de Bruijn インデックスを使用し、自由変数には一意な識別子を使用します。

この目的において、自由変数はある「開いた」束縛子に指定されている式の中の変数のことで、これは即座に利用することができません。そのため対応する束縛変数を、残しておく束縛子に関する情報を持つ自由変数に置き換えます。

このことを示すために、あるラムダ式 (fun (x : A) => <body>) があり、これの型推論をしようとしているとしましょう。型推論は式の <body> 部分を走査する必要があり、その中には x を参照する束縛変数があるかもしれません。本体を走査する際、束縛子のステートフルなコンテキストに x を追加してステートフルなコンテキスト全体を本体に持ち込むか、一時的に x を参照するすべての束縛変数を自由変数に置き換えて追加のコンテキストを持たずに本体を走査するかのどちらかを行うことができます。

最終的に束縛子を開く前にいた場所に戻れば、抽象化によってかつて x を参照する束縛変数だったすべての自由変数を、正しい de Bruijn インデックスによって再び x を参照する新しい束縛変数に置換することができます。

自由変数の抽象化の実装

de Bruijn レベルにおいて、自由変数は「私は telescope の頂点から n 番目の束縛変数を表す自由変数である」ということを意味する数字を追跡します。

これは「telescope の底から n 番目の束縛変数」を示す数値である de Bruijn インデックスの逆です。

ここでいう上と下は式の telescope を木に見立てています：

      fun
      /  \
    a    fun
        /   \
      b      ...
              \
              fun
             /   \
            e    bvar(0)

例えば、ラムダ式 fun (a b c d e) => bvar(0) の場合、束縛変数は「下から0番目」を参照して e を参照します。

ラムダ式 fun (a b c d e) => fvar(4) では、自由変数はここでも再び e を表す de Bruijn レベルですが、今回は「telescope の上から4番目」です。

なぜ区別するのでしょうか？強い簡約を行う際に自由変数を作成するとき、いくつかの事実が利用可能です：ここで割り当てようとしている自由変数がさらに簡約することで移動してしまうかもしれないこと、開いた束縛子がそこの上にいくつあるか（ここに到達するために束縛子を訪れないといけないため）、束縛子を置き換えるためにこの式を quote・抽象化する必要があるかもしれないこと、つまり自由変数を再束縛する必要があることなどです。しかし、その時点では束縛子が下にいくつ残っているかわからないため、その変数が最終的に抽象化・quote されたときに下から何番目の変数になるかはわかりません。

一意な識別子を使用して自由変数にタグをつける実装の場合、抽象化の際に再構築される実際の telescope があれば、この問題は解決します。式と一意にタグ付けされた自由変数のリストさえあれば、リスト内の自由変数の位置が束縛子の位置を示すため、抽象化することができます。

弱い簡約と強い簡約

Lean の簡約戦略の実装詳細については別の章で説明します；本節は、特に弱い簡約と強い簡約の一般的な概念の違いを明確にするためのものです。

弱い簡約

弱い簡約とは、引数が適用されていない束縛子までで止まる簡約です。束縛子はラムダ・pi・let 式のことです。

例えば、弱い簡約によって (fun (x y : Nat) => y + x) (0 : Nat) は (fun (y : Nat) => y + 0) に簡約できますが、これ以上の簡約はできません。

「弱頭正規形への簡約」や「強い」と特に特定せずに単に簡約と言ったりする場合は、弱い簡約のことを指します。強い簡約はどこかで束縛子を開いた後に弱い簡約を適用した副産物として発生します。

強い簡約

強い簡約とは開いた束縛子のもとでの簡約を指します；対応する引数が無い束縛子（引数を適用する app ノードが無いラムダ式のようなもの）に遭遇した際、本体を走査して自由変数を作成して代入することでさらに簡約できる可能性があります。強い簡約は型推論と定義の定義上の等しさのチェックに必要です。型推論にあたっては、本体で簡約が行われた後に自由変数を正しい束縛変数に置き換える、開いた項を「再度閉じる」機能も必要です。これは単に以前と同じ束縛変数に置き換えればよいというような単純なものではありません。なぜなら束縛変数がシフトし、新しく再構築された式に対する古い de Bruijn インデックスが無効になっている可能性があるからです。

弱い簡約と同様に、強い簡約でも (fun (x y : Nat) => y + x) (0 : Nat) は (fun (y : Nat) => y + 0) に簡約され、そこで詰まることなく y を自由変数に置き換えて簡約を続行し、式は ((fVar id, y, Nat) + 0) と (fvar id, y, Nat) へと簡約できます。

自由変数の情報を どこか に残しておく限り、その情報を簡約された (fVar id, y, Nat) と組み合わせることで (fun (y : Nat) => bvar(0)) へと再作成することができます。

名前

カーネルのプリミティブ型の中でも最初のものは Name で、これはその名称の通りのもののあつまりを指します；これはアドレスのための方法を備えたカーネルの要素を提供します。

Name ::= anonymous | str Name String | num Name Nat

Name 型の要素はドット区切りの名前で表示されます。これはおそらく Lean ユーザにはなじみ深いでしょう。例えば、num (str (anonymous) "foo") 7 は foo.7 と表示されます。

実装についての注記

名前の実装では、文字が Unicode scalar である UTF-8 文字列を想定しています（言語の文字列型のこの実装に関するこれらの想定は、文字列リテラルのカーネル拡張にとっても重要です）。

名前の字句構造に関するいくつかの情報についてはこちらを参照してください。

エクスポータは匿名の名前を明示的に出力せず、インポートされた名前の0番目の要素であることを期待します。

宇宙レベル

本節では、実装の観点から宇宙レベルについて説明し、読者が Lean の宣言を型チェックする際に知っておくべきことを取り上げます。Lean の型理論における宇宙レベルの役割についてのより深い説明は TPIL4 ¹ や Mario Carneiro の論文の第二節を参照してください。

宇宙レベルの構文は以下のようになっています：

Level ::= Zero | Succ Level | Max Level Level | IMax Level Level | Param Name

読者が注意すべき Level 型の特徴は、宇宙レベルに半順序が存在すること、変数の存在（Param コンストラクタ）、そして Max と IMax の区別です。

Max は単純に左右の引数のうち大きい方を表す宇宙レベルを構築します。例えば、Max(1, 2) は 2 に単純化され、Max(u, u+1) は u+1 に単純化されます。IMax コンストラクタは左と右の引数のうち大きい方を表しますが、これは右の引数が Zero に単純 されない場合に限り 、またこの場合は IMax は 0 へと解決されます。

IMax の重要な点は、例えば forall (x y : Sort 3), Nat は Sort 4 と推論されるが、forall (x y : Sort 3), True は Prop と推論されるように型推論の処理と相互作用することにあります。

レベル上の半順序

Lean の Level 型は半順序を備えています。つまりレベルのペアに対して実行可能な「以下」の検査が存在します。以下のなかなか素晴らしい実装は Gabriel Ebner の Lean 3 チェッカである trepplein から持ってきています。カバーしなければならないケースはかなり多いですが、複雑なマッチは cases に依存しているものだけです。これは x ≤ y であるかどうかのチェックについて、パラメータ p に Zero が代入された時、および p に Succ p が代入されたときに x ≤ y が成り立つかどうか調べることで行っています。

  leq (x y : Level) (balance : Integer): bool :=
    Zero, _ if balance >= 0 => true
    _, Zero if balance < 0 => false
    Param(i), Param(j) => i == j && balance >= 0
    Param(_), Zero => false
    Zero, Param(_) => balance >= 0
    Succ(l1_), _ => leq l1_ l2 (balance - 1)
    _, Succ(l2_) => leq l1 l2_ (balance + 1)

    -- descend left
    Max(a, b), _ => (leq a l2 balance) && (leq b l2 balance)

    -- descend right
    (Param(_) | Zero), Max(a, b) => (leq l1 a balance) || (leq l1 b balance)

    -- imax
    IMax(a1, b1), IMax(a2, b2) if a1 == a2 && b1 == b2 => true
    IMax(_, p @ Param(_)), _ => cases(p)
    _, IMax(_, p @ Param(_)) => cases(p)
    IMax(a, IMax(b, c)), _ => leq Max(IMax(a, c), IMax(b, c)) l2 balance
    IMax(a, Max(b, c)), _ => leq (simplify Max(IMax(a, b), IMax(a, c))) l2 balance
    _, IMax(a, IMax(b, c)) => leq l1 Max(IMax(a, c), IMax(b, c)) balance
    _, IMax(a, Max(b, c)) => leq l1 (simplify Max(IMax(a, b), IMax(a, c))) balance


  cases l1 l2 p: bool :=
    leq (simplify $ subst l1 p zero) (simplify $ subst l2 p zero)
    ∧
    leq (simplify $ subst l1 p (Succ p)) (simplify $ subst l2 p (Succ p))

レベルの同値

Level 型では反対称律による同値が認められています。つまり、2つのレベル l1 と l2 は l1 ≤ l2 かつ l2 ≤ l1 ならば等しいです。

実装上の注記

エクスポータは Zero をエクスポートしないことに注意してください。しかし、これは Level の0番目の要素として仮定されます。

ただこう言ってはなんですが、Level の実装はパフォーマンスに大きな影響を与えないため、ここで積極的に最適化する必要はありません。

訳注：日本語訳は https://aconite-ac.github.io/theorem_proving_in_lean4_ja/dependent_type_theory.html#types-as-objects-%E9%A0%85%E3%81%A8%E3%81%97%E3%81%A6%E3%81%AE%E5%9E%8B

式

完全な構文

式の詳細については後述しますが、まずはこれが何であるかを明らかにするために、以下に文字列と nat リテラルの拡張を含む式についての完全な構文を挙げます：

Expr ::= 
  | boundVariable 
  | freeVariable 
  | const 
  | sort 
  | app 
  | lambda 
  | forall 
  | let 
  | proj 
  | literal

BinderInfo ::= Default | Implicit | InstanceImplicit | StrictImplicit

const ::= Name, Level*
sort ::= Level
app ::= Expr Expr
-- a deBruijn index
boundVariable ::= Nat
lambda ::= Name, (binderType : Expr), BinderInfo, (body : Expr)
forall ::= Name, (binderType : Expr), BinderInfo, (body : Expr)
let ::= Name, (binderType : Expr), (val : Expr) (body : Expr)
proj ::= Name Nat Expr
literal ::= natLit | stringLit

-- Arbitrary precision nat/unsigned integer
natLit ::= Nat
-- UTF-8 string
stringLit ::= String

-- fvarId can be implemented by unique names or deBruijn levels; 
-- unique names are more versatile, deBruijn levels have better
-- cache behavior
freeVariable ::= Name, Expr, BinderInfo, fvarId

これについて、いくつかの注意点があります：

nat リテラルが利用する Nat は任意精度の自然数・bignum でなければなりません。

束縛子（ラムダ・pi・let・自由変数）を持つ式では3つの引数（束縛子の名前・型・スタイル）を1つの引数 Binder として簡単にまとめることができます。ここで束縛子は Binder ::= Name BinderInfo Expr となります。他の場所で例示する疑似コードでは、読みやすさのためにそのプロパティを持っているかのように常に扱うことにします。

自由変数の識別子は、一意な識別子にすることも de Bruijn レベルにすることもできます。

Lean で使用される式の型は mdata コンストラクタというものも持っており、これはメタデータを付与した式を宣言します。このメタデータはカーネル内での式の動作には影響しないため、このコンストラクタはここでは取り扱いません。

束縛子の情報

ラムダ・pi・let・自由変数コンストラクタで構築された式は、名前・束縛子の「スタイル」・束縛子の型の形式で束縛子の情報を保持します。束縛子の名前とスタイルはプリティプリンタが使用するためだけのものであり、推論・簡約・同値チェックの中核となる処理を変更することはありません。しかし、プリティプリンタでは束縛子のスタイルがプリティプリンタのオプションに応じて出力を変更することがあります。例えば、ユーザは暗黙的または暗黙インスタンス（型クラス変数）を出力に表示したい場合もあれば、したくないこともあるでしょう。

ソート

sort は単にレベルのラッパーであり、式として使用することができます。

束縛変数

束縛変数は de Bruijn インデックスを表す自然数として実装されています。

自由変数

自由変数は束縛子が一時的に利用できない状況で、束縛変数に関する情報を伝達するために使用されます。これは自由変数について、新しい（異なる場合もある）束縛変数に入れ替えて束縛子を再構築する上で束縛変数を一時的に自由変数に置き換える代わりに、カーネルが束縛式の本体を走査し、束縛情報の構造化されたコンテキストを保持しないことを通常選択するためです。この利用できないことの説明は曖昧に聞こえるかもしれませんが、役立つように文字通りに説明すると、式は親ノードのポインタを持たない木として実装されているため、子ノードに降りてくると（特に関数の境界を超える場合）、ある式の現在地より上の要素を見失ってしまうことになってしまいます。

束縛子を再構築して開いた式を閉じる時、束縛子が変更されることで以前に有効だった de Bruijn インデックスが無効になることがあります。一意な名前か de Bruijn レベルを使用することで、あらゆる変更を補正し、再束縛された変数の新しい de Bruijn インデックスが再構築されたテレスコープに対して有効であることを保証するようにこの束縛子を再度閉じることができます（この節を参照してください ¹）

今後、実装がどのようなスキーム（一意なIDか de Bruijn レベル）を使っているかに関わらず、何らかの形で「自由変数の識別子（free variable identifier）」という用語を使うかもしれません。

`const`

const コンストラクタは、ある式が環境内の別の宣言を参照するための方法です。これは参照として行われなければなりません。

以下の例では、def plusOne が Definition 宣言を作成し、これがチェックされたのちに環境に受け入れられます。こうした宣言は式の中に直接置くことはできないため、plusOne_eq_succ の型が前の宣言 plusOne を呼び出すときは名前を指定しなければなりません。こうして Expr.const (plusOne, []) という式が作成され、カーネルがこの const 式を見つけると、plusOne という名前で参照されている宣言をこの環境で探すことができます：

def plusOne : Nat -> Nat := fun x => x + 1

theorem plusOne_eq_succ (n : Nat) : plusOne n = n.succ := rfl

const コンストラクタで作成された式は、const 式が参照する定義を検索することで、環境から取得した宣言の展開や推論に代入されるレベルのリストも保持します。例えば、const List [Level.param(x)] の型を推測するには、現在の環境で List の宣言を検索し、その型と宇宙パラメータを取得し、そして List が最初に宣言された宇宙パラメータに x を代入します。

ラムダ式、pi

lambda と pi 式（Lean では pi の代わりに forallE を使用します）は、それぞれ関数の抽象化と「全ての」束縛子（依存関数型）を意味します。

   束縛子名        本体
      |            |
fun (foo : Bar) => 0 
            |         
         束縛子の型

-- `BinderInfo` は束縛子を囲む括弧のスタイルに反映されています。

let 式

let はまさにその名前の通りのものです。let 式は束縛子ですが、BinderInfo を持たず、束縛子の情報は Default として扱われます。

   束縛子名        値
      |            |
let (foo : Bar) := 0; foo
            |          |
        束縛子の型      .... 本体

適用

app 式は関数への引数の適用を表します。適用のノードはバイナリ（2つの子、つまり1つの関数とその1つの引数のみを持つ）であるため、f x_0 x_1 .. x_N は App(App(App(f, x_0), x_1)..., x_N) として表され、以下のような木として視覚化されます：

カーネルが提供する式の操作は非常に一般的で、適用の列を畳み込んだり展開したりすることで、上の木構造から (f, [x_0, x_1, .., x_N]) を取得したり、f, [x_0, x_1, .., x_N] を上の木へと畳み込んだりすることができます。

射影

proj コンストラクタは構造体の射影を表します。再帰的でなく、コンストラクタが1つしかなく、添字を持たない帰納型は構造体になることができます。

このコンストラクタは当該の型の名前と、射影されるフィールドを示す自然数、そして射影が適用される実際の構造体を取ります。

ここでカーネルでは射影のインデックスは 0 始まりであるのに対して Lean の用語では 1 始まりであることに注意してください。Lean サイドでは 0 はそのコンストラクタのパラメータではない最初の引数に使われます。

例えば、proj Prod 0 (@Prod.mk A B a b) というカーネルの式は、パラメータ A と B をスキップした後の0番目のフィールドとして a を射影します。

proj が提供する動作は、型の再帰子を使用することで実現できますが、proj は頻繁に行われるカーネルの操作をより効率的に処理します。

リテラル

Lean のカーネルはオプションとして任意精度の Nat リテラルと String リテラルをサポートしています。必要に応じてカーネルは自然数リテラル n を Na.zero または Nat.succ m に変換したり、文字列リテラル s を String.mk List.nil や String.mk (List.cons (Char.ofNat _) ...) に変換したりすることができます。

文字列リテラルは、定義上の等しさをテストするためか、再帰子の簡約において主要な対象として現れる時に文字のリストに遅延変換されます。

自然数リテラルは文字列を同じ立ち位置（定義上の等しさと再帰子の適用の主要な対象）でサポートされていますが、カー熱は加算・乗算・指数・減算・剰余・割り算のほか、自然数リテラルに対する真偽値の同値と「以下」の比較もサポートしています。

訳注：原文では./kernel_concepts.md#implementing-free-variable-abstractionへリンクが貼られていましたがリンクが切れていたので対応するリンクに更新しています。

式の実装

カーネルを一部もしくは全部書いてみたい読者のために、式の型について特筆すべき点をいくつか挙げておくと……

データの格納

式は法外に高価な再計算を防ぐために、ある程度のデータをインラインで保持するか、どこかにキャッシュする必要があります。例えば、app x y という式を作成する場合、結果の app 式のハッシュダイジェストを計算し保存する必要があります。その際には x と y の木全体を走査して x と y のダイジェストをそれぞれ再帰的に計算するのではなく、キャッシュされた x と y のハッシュダイジェストを取得する必要があります。

おそらくインラインで保存したくなるデータはハッシュダイジェスト・式中の loose な束縛変数の数・式に自由変数があるかどうかです。後者の2つはそれぞれインスタンス化と抽象化を最適化するにあたって便利です。

app 式の「スマートなコンストラクタ」は次の例のようになるでしょう：

def mkApp x y:
  let hash := hash x.storedHash y.storedHash
  let numLooseBvars := max x.numLooseBvars y.numLooseBvars
  let hasFvars := x.hasFvars || y.hasFvars
  .app x y (cachedData := hash numLooseBVars hasFVars)

ディープコピーをしない

式は、親の式を構築するために使用する子の式をディープコピーしないように実装されるべきです。別の言い方をすれば、app x y という式を作成する場合、x と y の要素を再帰的にコピーするべきではありません。むしろポインタ・整数のインデックス・ガベージコレクションされるオブジェクトへの参照・参照カウントの対象のオブジェクトなど、なんらかの参照を取るべきです（これらの戦略のいずれでも許容可能なパフォーマンスを提供する必要があります）。式を構築するためのデフォルトの戦略にディープコピーが含まれてしまうと、自明でない環境を構築するために大量のメモリを消費しなければならなくなります。

loose な束縛変数の数の実装例

numLooseBVars e:
    match e with
    | Sort | Const | FVar | StringLit | NatLit => 0
    | Var dbjIdx => dbjIdx + 1,
    | App fun arg => max fun.numLooseBvars arg.numLooseBvars
    | Pi binder body | Lambda binder body => 
    |   max binder.numLooseBVars (body.numLooseBVars - 1)
    | Let binder val body =>
    |   max (max binder.numLooseBvars val.numLooseBvars) (body.numLooseBvars - 1)
    | Proj _ _ structure => structure.numLooseBvars

Var 式において、loose な束縛変数の数は de Bruijn インデックスに1を足した値になります。これは、その変数が loose でなくなるために必要な束縛子の数を数えているからです（+1 は de Bruijn インデックスが0始まりであるからです）。式 Var(0) の場合、その変数が loose でなくなるためには、束縛子を束縛変数の上に1つ置く必要があります。Var(3) の場合は4つ必要です：

--  3 2 1 0
fun a b c d => Var(3)

新しい束縛子（ラムダ式・pi・let式）を作るとき、本体の loose な bvar の数から1を引きます（自然数の飽和減算を使います）。なぜなら本体は1つの追加の束縛子の下に置かれるからです。

宣言

宣言は高額商品であり、最後の定義すべきな主要の要素です。

declarationInfo ::= Name, (universe params : List Level), (type : Expr)

declar ::= 
  Axiom declarationInfo
  | Definition declarationInfo (value : Expr) ReducibilityHint
  | Theorem declarationInfo (value : Expr) 
  | Opaque declarationInfo (value : Expr) 
  | Quot declarationInfo
  | InductiveType 
      declarationInfo
      is_recursive: Bool
      num_params: Nat
      num_indices: Nat
      -- この型の名前と相互ブロック内の他の型の名前
      allIndNames: Name+
      -- **この** 型のみについてのコンストラクタの名前
      -- このブロックに含まれる可能性のある相互のコンストラクタは含まない
      constructorNames: Name*
      
  | Constructor 
      declarationInfo 
      (inductiveName : Name) 
      (numParams : Nat) 
      (numFields : Nat)

  | Recursor 
        declarationInfo 
        numParams : Nat
        numIndices : Nat
        numMotives : Nat
        numMinors : Nat
        RecRule+
        isK : Bool

RecRule ::= (constructor name : Name), (number of constructor args : Nat), (val : Expr)

宣言のチェック

すべての宣言に対して、特定の宣言に特化した追加の手続きが行われる前に、以下の予備的なチェックが行われます：

宣言の declarationInfo 内の宇宙パラメータは重複してはなりません。例えば、def Foo.{u, v, u} ... という宣言は禁止されています。

宣言の型は自由変数を持ってはなりません；「完成した」宣言の変数はすべて束縛子に対応しなければなりません。

宣言の型は型でなければなりません（infer declarationInfo.type の結果は Sort でなければならない）。Lean では、def Foo : Nat.succ := .. という宣言は許可されていません；Nat.succ は値であり、型ではありません。

公理

公理に対して行われる唯一のチェックは、declarationInfo が合格することを保証するすべての宣言に対して行われるチェックです。公理が有効な宇宙パラメータと有効な型を持ち、自由変数を持たない場合、その公理は環境に受け入れられます。

商

Quot についての宣言は Quot・Quot.mk・Quot.ind・Quot.lift です。これらの宣言は Lean の理論で健全であるとされる型を持ち、環境の商についての宣言はこれらの型に正確に一致しなければなりません。これらの型は許されざるほど複雑というわけではないため、カーネルの実装にハードコードされています。

定義・定理・opaque

定義・定理・opaque は型と値の両方を持つという点で興味深いものです。これらの宣言をチェックするには、宣言の値の型を推論し、その型が declarationInfo 内で定義された型と定義上等しいことを確認します。

定理の場合、declarationInfo の型はユーザが主張する型であり、したがってユーザが証明することを主張しているもので、値はユーザによってその型の証明を提供されるものです。受け取った値の型を推論することは、その証明が実際に何を証明しているかをチェックすることに等しく、定義上の等しさのチェックはその値が証明する事柄が実際にユーザが証明しようと意図したものであることを保証します。

簡約についてのヒント

簡約のヒントには、宣言がどのように展開されるべきかという情報が含まれています。abbreviation は一般的に常に展開され、opaque は展開されず、regular N は N の値によって展開されるかどうかが決定します。regular の簡約のヒントは定義の「高さ」に対応しています。この用語はその定義自体の定義に用いられている宣言の数を指します。定義 y を参照する値を持つ定義 x の高さは　y より大きくなります。

帰納型の知られざる一生

帰納的対象

より精確には、「帰納的宣言」の全体像は型・コンストラクタのリスト・再帰子のリストからなります。宣言の型とコンストラクタはユーザが指定し、再帰子はそれらの要素から派生します。各再帰子は計算規則とも呼ばれる「再帰子規則」のリストも取得します。これはι簡約（パターンマッチの大げさな言い方）で使用される値レベルの式です。これ以降においては、「帰納型」と「帰納的宣言」はなるべく区別するようにします。

Lean のカーネルでは相互帰納的宣言をネイティブにサポートしています。この場合、（型とコンストラクタのリストの）ペアのリストが存在します。カーネルは入れ子になった帰納的宣言について、一時的に相互帰納的宣言に変換することでサポートします（これについては後述します）。

帰納型

カーネルは帰納的宣言のうち「帰納型」について、値ではなく実際に型であることを要求します（infer ty は何らかの sort <n> を生成しなければなりません）。相互帰納型では、宣言される型がすべて同じ宇宙にあり、同じパラメータを持たなければなりません。

コンストラクタ

帰納型のどのコンストラクタにおいても、カーネルによって以下のチェックが課されます：

コンストラクタの型・テレスコープは宣言されている帰納型と同じパラメータを共有する必要があります。

コンストラクタ型のテレスコープのパラメータではない要素では、束縛子の型は実際に型でなければなりません（Sort _ として推論されなければなりません）。

コンストラクタ型のテレスコープのパラメータではない要素では、その要素から推論されたソートが帰納型のソート以下であるか、もしくは帰納型が命題として宣言されていなければなりません。

コンストラクタの引数は宣言されている型の positive ではない出現を含んではなりません（この問題についてはより知りたい読者はこちらを参照してください）。

コンストラクタのテレスコープの終わりは、宣言されている型への引数の有効な適用でなければなりません。例えば、List.cons .. コンストラクタは .. -> List A で終わる必要があり、.. -> Nat で終わる List.cons .. はエラーになります。

入れ子になった帰納的対象

入れ子になった帰納的対象をチェックするのはとても手間のかかる手順です。まず相互ブロックの中の帰納型の入れ子部分を一時的に特殊化することで相互帰納型の「通常の」（入れ子になっていない）あつまりを持つようにし、特殊化された型をチェックし、それからすべての特殊化を解除してそれらの型を認可します。

次の入れ子構造 Array Sexpr を伴った S 式の定義を考えてみましょう：

inductive Sexpr
| atom (c : Char) : Sexpr
| ofArray : Array Sexpr -> Sexpr

俯瞰的に見ると、入れ子の帰納的宣言をチェックするプロセスには3つのステップがあります：

現在の型がネストされている「コンテナ型」を特殊化することによって、入れ子になった帰納的宣言を相互帰納的宣言に変換する。コンテナ型自体が他の型で定義されている場合は、それらの要素も特殊化する必要があります。上の例では、コンテナ型として Array を使用していますが、Array は List の用語によって定義されているため、Array と List の両方をコンテナ型として扱う必要があります。

相互帰納型の通常のチェックと構築の手順を行う。

特殊化された入れ子の型をもとの形に戻し（非特殊化）、復帰・非特殊化された宣言を環境に追加する。

この特殊化の例として、上記の入れ子になった帰納的対象 Sexpr は次のように変換されます：

mutual
  inductive Sexpr
    | atom : Char -> Sexpr
    | ofList : ListSexpr -> Sexpr

  inductive ListSexpr 
    | nil : ListSexpr
    | cons : Sexpr -> ListSexpr -> ListSexpr 

  inductive ArraySexpr
    | mk : ListSexpr -> ArraySexpr
end

そして、これらの型をチェックする過程で元の帰納的宣言を回復します。より明確にすると、「特殊化」といった場合、上記の新しい ListSexpr 型と ArraySexpr 型は通常の List 型のように任意の型に対して汎用的であることは対照的に、Sexpr のリストと配列としてのみ定義されているという意味で特殊化されています。

再帰子

TBD

型推論

型推論は与えられた式の型を決定するための手続きであり、Leanのカーネルのコア機能の1つです。型推論は Nat.zero が Nat 型の要素であることや、(fun (x : Char) => var(0)) が Char -> Char 型の要素であることを決定する方法です。

本節ではまず型推論のためのもっとも単純で完全な手続きを確かめ、次いでそれぞれの手続きより性能の高い、しかし少し複雑なバージョンについて確認します。

また、Lean のカーネルが型推論中に行ういくつかの付加的な正しさの主張についても見ていきます。

束縛変数

Lean の実装に従って locally nameless なアプローチを使う場合、型推論中で束縛変数に遭遇することはないでしょう。というのもすべての開いた束縛子は適切な自由変数でインスタンス化されているからです。

束縛子に遭遇した場合、本体の型を決定するために本体を走査する必要があります。束縛子の型に関する情報を保持するには主に2つのアプローチがあります；Lean が正式に採用しているものは、束縛子の型情報を保持する自由変数を作成し、インスタンス化を対応する束縛変数を自由変数に置き換えてから本体に入るというものです。これは型付けコンテキストのために個別の状態を追跡する必要がないため良い方法です。

クロージャに基づく実装では、一般的に開いた束縛子を追跡するための別の型付けコンテキストを持つことになります；束縛変数に遭遇すると、その変数の型を取得するために、型付けコンテキストにインデックスを作ることになります。

自由変数

自由変数が作られる際には、それが表す束縛子から型情報が与えられるため、型推論の結果としてその型情報を受け取ればよいです。

infer FVar id binder:
  binder.type

関数適用

infer App(f, arg):
  match (whnf $ infer f) with
  | Pi binder body => 
    assert! defEq(binder.type, infer arg)
    instantiate(body, arg)
  | _ => error

ここで追加の主張として必要なものは、arg の型が binder の型と一致することです。例えば、次の式

(fun (n : Nat) => 2 * n) 10 について、defEq(Nat, infer(10)) を主張しなければなりません。

既存の実装ではこのチェックをインラインで実行することを好んでいますが、他の場所で処理するためにこの同値の主張を保存することもできます。

ラムダ式

infer Lambda(binder, body):
  assert! infersAsSort(binder.type)
  let binderFvar := fvar(binder)
  let bodyType := infer $ instantiate(body, binderFVar)
  Pi binder (abstract bodyType binderFVar)

Pi

infer Pi binder body:
  let l := inferSortOf binder
  let r := inferSortOf $ instantiate body (fvar(binder))
  imax(l, r)

inferSortOf e:
  match (whnf (infer e)) with
  | sort level => level
  | _ => error

ソート

任意の Sort n の型は Sort (n+1) です。

infer Sort level:
  Sort (succ level)

定数

const 式は他の宣言を名前で参照するために使われ、参照される任意の他の宣言はこれより以前に宣言され、型がチェックされていなければなりません。したがって、参照される宣言の型が何であるかはすでに分かっているため、それを環境から探してくるだけで良いのです。ただし、現在の宣言の宇宙レベルを添字付けられた定義の宇宙パラメータに代入する必要があります。

infer Const name levels:
  let knownType := environment[name].type
  substituteLevels (e := knownType) (ks := knownType.uparams) (vs := levels)

Let

infer Let binder val body:
  assert! inferSortOf binder
  assert! defEq(infer(val), binder.type)
  infer (instantiate body val)

射影

ここで Proj (projIdx := 0) (structure := Prod.mk A B (a : A) (b : B)) のようなものの型を推論しようとしているとしましょう。

まず渡される構造体の型を推測することから始めます；そこから構造体の名前を取得し、構造体とコンストラクタの型を環境で調べることができます。

コンストラクタの型のテレスコープを走査し、Prod.mk のパラメータをコンストラクタ型のテレスコープに代入します。A -> B -> (a : A) -> (b : B) -> Prod A B というコンストラクタ型に着目すると、A と B を代入することで、(a : A) -> (b : B) -> Prod A B というテレスコープが残ります。

コンストラクタのテレスコープの残りの部分は構造体のフィールドを表しており、束縛子に型情報を持っているため、telescope[projIdx] を調べて束縛子の型を取ればよいです。やることはあと1つ残っています；後続の構造体のフィールドはその前の構造体のフィールドに依存することがあるため、残りのテレスコープ（各ステージの本体）を proj thisFieldIdx s でインスタンス化する必要があります。ここで s は推測する対象の射影の式中のオリジナルの構造体です。

infer Projection(projIdx, structure):
  let structType := whnf (infer structure)
  let (const structTyName levels) tyArgs := structType.unfoldApps
  let InductiveInfo := env[structTyName]
  -- This inductive should only have the one constructor since it's claiming to be a structure.
  let ConstructorInfo := env[InductiveInfo.constructorNames[0]]

  let mut constructorType := substLevels ConstructorInfo.type (newLevels := levels)

  for tyArg in tyArgs.take constructorType.numParams
    match (whnf constructorType) with
      | pi _ body => inst body tyArg
      | _ => error

  for i in [0:projIdx]
    match (whnf constructorType) with
      | pi _ body => inst body (proj i structure)
      | _ => error

  match (whnf constructorType) with
    | pi binder _=> binder.type
    | _ => error

数値リテラル

数値リテラルは Nat 宣言を参照する定数として推測されます。

infer NatLiteral _:
  Const(Nat, [])

文字列リテラル

文字列リテラルは String 宣言を参照する定数として推測されます。

infer StringLiteral _:
  Const(String, [])

定義上の等しさ

定義上の等しさは関数として実装されています。これは2つの式を受け取り、それらが Lean の理論の中で定義上等しい場合は true を、そうでない場合は false を返します。

カーネル内において定義上の等しさは重要なものですが、それは単に型チェックに必要だからです。またカーネル内部へ挑まない Lean ユーザにとっても定義上の等しさは重要な概念です。というのも定義上の等しさは Lean を書く上で比較的簡単に扱えるからです；定義上等しい a と b に対して、Lean は2つの式が等しいかどうかを判断するためにユーザからのプロンプトや追加の入力を必要としません。

定義上の等しさの処理を実装には大きく分けて2つの部分があります。まず、定義が等しいかどうかをチェックするための個別のテストです。エンドユーザの視点から定義上の等しさを理解することに興味がある読者にとっては、おそらくこれが知りたいことでしょう。

型チェッカを書くことに興味がある読者は、問題を扱いやすくするために個々のチェックが簡約やキャッシュに対してどのように組み合わされるかについても理解しておく必要があります；素朴に各チェックを実行し、それに従い簡約を行うことは受け入れがたいパフォーマンスとなってしまう可能性が高いです。

ソートの同値

2つの Sort 式が定義上等しいのは、それらが表すレベルがレベルの半順序関係の反対称律によって等しい場合です。

defEq (Sort x) (Sort y):
  x ≤ y ∧ y ≤ x

定数の同値

2つの Const 式が定義上等しいのは、名前が同一で、レベルが反対称律の下で等しい場合です。

defEq (Const n xs) (Const m ys):
  n == m ∧ forall (x, y) in (xs, ys), antisymmEq x y

  -- もし利用する `zip` がよしなにしてくれない場合は、xs と ys が同じ長さであることも主張します

束縛変数

locally nameless のような置換ベースの戦略を使用している場合（もし C++ や lean4lean の実装に従っているならあなたのことです）、束縛変数に遭遇するとエラーになります；というのも束縛変数はそれが引数を参照している場合、弱い簡約を行う中で置換されるか、pi またはラムダ式の定義上の等しさのチェックの一部として強い簡約を介して自由変数に置換されるべきです。

クロージャベースの実装では、束縛変数に対応する要素を調べ、それらが定義上等しいことを保証します。

自由変数

2つの自由変数が定義上等しいのは、同じ識別子（一意な ID か de Bruijn レベル）を持っている場合です。束縛子の型が等しいかどうかの検証は、（pi ・ラムダ式の定義上の等しさのチェックと同じように）自由変数が構築された場所で必ず行われたはずなので、今更再チェックする必要はありません。

defEqFVar (id1, _) (id2, _):
  id1 == id2

関数適用

2つの関数適用の式が定義上等しいのは、関数のコンポーネントと引数のコンポーネントが定義上等しい場合です。

defEqApp (App f a) (App g b):
  defEq f g && defEq a b

Pi

2つの Pi の式が定義上等しいのは、束縛子の型が定義上等しく、適切な自由変数を代入した後の本体の型が定義上等しい場合です。

defEq (Pi s a) (Pi t b)
  if defEq s.type t.type
  then
    let thisFvar := fvar s
    defEq (inst a thisFvar) (inst b thisFvar)
  else
    false

ラムダ式

ラムダ式では Pi と同じチェックを用います：

defEq (Lambda s a) (Lambda t b)
  if defEq s.type t.type
  then
    let thisFvar := fvar s
    defEq (inst a thisFvar) (inst b thisFvar)
  else
    false

構造的なη

Lean は2つの要素 x と y が両方ともある構造体型のインスタンスであり、一方のコンストラクタ引数と他方の射影されたフィールドを比較する以下の手順を使用してフィールドが定義上等しい場合、定義上の等しさを認めます：

defEqEtaStruct x y:
  let (yF, yArgs) := unfoldApps y
  if 
    yF is a constructor for an inductive type `T` 
    && `T` can be a struct
    && yArgs.len == T.numParams + T.numFields
    && defEq (infer x) (infer y)
  then
    forall i in 0..t.numFields, defEq Proj(i+T.numParams, x) yArgs[i+T.numParams]

    -- `T.numParams` をインデックスに追加しているのは、
    -- パラメータ以外の引き数のみをテストしたいからです。
    -- 推論される型が定義上等しいため、パラメータが defEq であることはすでに分かっています。

より一般的な例である [a, .., N] = [x, .., M] の時の合同 T.mk a .. N = T.mk x .. M は、単純に App のチェックで処理できます。

ユニットのようなものの同値

Lean では以下の条件の下にある2つの要素 x: S p_0 .. p_N と y: T p_0 .. p_M が定義上等しいとしています：

S は帰納型である
S は添字を持たない
S はただ一つのコンストラクタを持ち、それが S のパラメータ p_0 .. p_N 以外に引数を取らないこと
型 S p_0 .. p_N と T p0 .. p_M が定義上等しいこと

直観的にこの定義上の等しさは問題ないでしょう。なぜなら、これらの型の要素が伝えることのできる情報はすべて型に捕捉されており、私たちはこれらの型が定義上等しいことを要求しているからです。

η 展開

defEqEtaExpansion x y : bool :=
  match x, (whnf $ infer y) with
  | Lambda .., Pi binder _ => defEq x (App (Lambda binder (Var 0)) y)
  | _, _ => false

右辺でラムダ式が作られており、この (fun _ => $0) y は明らかに y に簡約されますが、ラムダ式の束縛子を追加することで、 x と y が残りの定義上の等しさの手続きによる一致の機会を与えます。

proof irrelevance な同値

Lean は proof irrelevance な同値を定義上のものとして扱います。例えば、Lean の定義上の等しさの手続きは 2 + 2 = 4 についての任意の2つの証明を定義上同値として扱います。

If a type T infers as Sort 0, we know it's a proof, because it is an element of Prop (remember that Prop is Sort 0).

defEqByProofIrrelevance p q :
  infer(p) == S ∧ 
  infer(q) == T ∧
  infer(S) == Sort(0) ∧
  infer(T) == Sort(0) ∧
  defEq(S, T)

p が A 型の証明で、q が B 型の証明である場合、A が B と定義上等しいなら、p と q は proof irrelevance によって定義上等しいです。

整数（整数リテラル）

2つの整数リテラルが定義上等しいのは、それらが Nat.zero に簡約できる場合か、(Nat.succ x, Nat.succ y) へと簡約できる場合で、ここで x と y は定義上等しいです。

match X, Y with
| Nat.zero, Nat.zero => true
| NatLit 0, NatLit 0 => true
| Nat.succ x, NatLit (y+1) => defEq x (NatLit y)
| NatLit (x+1), Nat.succ y => defEq (NatLit x) y
| NatLit (x+1), NatLit (y+1) => x == y
| _, _ => false

文字列リテラル

StringLit(s), App(String.mk, a)

文字列リテラル s は Const(String.mk, []) の適用によって List Char に変換されます。Lean の Char 型は Unicode スカラー値を表現するために使用されるため、その整数表現は32ビットの符号なし整数です。

例として、32ビットの符号なし整数 111 と 107 に対応する2つの文字を使った文字列リテラル「ok」は次のように変換されます。

(String.mk (((List.cons Char) (Char.ofNat.[] NatLit(111))) (((List.cons Char) (Char.ofNat NatLit(107))) (List.nil Char))))

Lazy delta 簡約

利用可能なカーネル実装は簡約のヒントを使用して遅延的に定義を展開し、物事が有望に見えるときに一致をチェックする定義上の等しさのチェックの一部として「Lazy delta 簡約」手順を実装しています。これは定義が一致するかどうかをチェックする前に両方の式を完全に簡約するよりもはるかに効率的な戦略です。

a と b という2つの式があり、a が高さ10の定義の適用で、b が高さ12の定義の適用である場合、両者を完全に展開したりやみくもにどちらか片方を展開するのではなく、Lazy delta 手順は b を展開して a に近づけようとするより効率的なルートを取ります。

Lazy delta 処理が引数への const 式の適用である2つの式を見つけ、その const 式が同じ宣言を参照している場合、その式の合同（定義上等しい引数に適用される同じ定数であるかどうか）がチェックされます。合同チェックは def_eq_args の呼び出しが効果になる可能性があるため、独自のカーネルを書く読者にとって、これは失敗をキャッシュすることはパフォーマンス上重要な最適化であることがわかります。

文法上の同値（または構造体・ポインタ上の同値）

型チェッカが2つのオブジェクトが同じコンポーネント（Name・Level・Expr のコンストラクタが該当します）から構築される場合に限り等しいことを保証する限り、2つの式が全く同じ実装されたオブジェクトを参照する場合、これらは定義上等しくなります。

簡約

簡約とは、式が定義上等しいかどうかを判定てきるように式を正規形に近づけることです。例えば、(fun x => x) Nat.zero が Nat.zero と定義上等しいと判断するためにβ簡約を行い、id List.nil が List.nil と定義上等しいと判断するためにδ簡約を行う必要があります。

Lean のカーネルにおける簡約には2つの性質がありますが、この分野を扱う基本的な教科書では触れられない恐れがあります。まず、場合によっては簡約と推論が同時に行われることがあります。とりわけ、たとえ簡約によって自由変数が生成されなくとも、これは開いた項で簡約を実行する必要があるかもしれないことを意味しています。第二に、複数の引数に適用される const 式は（ι簡約のように）簡約を行う中でそれらの引数を一緒に考慮する必要がある場合があり、簡約開始時に一連の適用を一緒に展開する必要があります。

β簡約

β簡約は関数適用についての簡約です。具体的には、次の簡約です：

(fun x => x) a    ~~>    a

β簡約の実装は app 式の引数を集め、それらが適用される式がラムダ式であるかどうかをチェックし、適切な引数を関数本体の対応する束縛変数の出現に置換するために式を手入れしなければなりません：

betaReduce e:
  betaReduceAux e.unfoldApps

betaReduceAux f args:
  match f, args with
  | lambda _ body, arg :: rest => betaReduceAux (inst body arg) rest
  | _, _ => foldApps f args

β簡約のインスタンス化（置換）コンポーネントの重要なパフォーマンス最適化は、「generalized beta reduction」と呼ばれるもので、対応するラムダ式を持つ引数を集め、それらを一度に置換する方法です。この最適化は、適用された引数を持つ n 個の連続したラムダ式に対して、n 回の走査ではなく、適切な引数を代入するための1回の走査のみを実行することを意味します。

betaReduce e:
  betaReduceAux e.unfoldApps []

betaReduceAux f remArgs argsToApply:
  match f, remArgs with
  | lambda _ body, arg :: rest => betaReduceAux body rest (arg :: argsToApply)
  | _, _ => foldApps (inst f argsToApply) remArgs

ζ簡約（`let` 式の簡約）

ζ簡約は let 式の簡約を表す大仰な名前です。具体的には、次の簡約です：

let (x : T) := y; x + 1    ~~>    (y : T) + 1

実装はシンプルであり、ほぼ次と同じです：

reduce Let _ val body:
  instantiate body val

δ簡約（定義の展開）

δ簡約は定義（と定理）を展開することを指します。δ簡約は const .. 式について、その定義の多相宇宙パラメータを現在のコンテキストに関連した値で交換した後に、参照されている定義の値で置き換えることによって行われます。

現在の環境に定義 x があり、その定義が宇宙パラメータ u* と値 v で宣言されている場合、式 Const(x, w*) を val で置き換えてδ簡約し、宇宙パラメータ u* を w* に置き換えます。

deltaReduce Const name levels:
  if environment[name] == (d : Declar) && d.val == v then
  substituteLevels (e := v) (ks := d.uparams) (vs := levels)

δ簡約された const 式に到達するために、適用された引数を簡約しなければならなかった場合、それらの引数は簡約された定義に再適用されなければなりません。

射影の簡約

proj 式は射影されるフィールドを表す自然数のインデックスと、構造体そのものを示す式を持ちます。構造体を構成する実際の式は、コンストラクタを参照する const に適用される一連の引き数でなければなりません。

ここで心に留めてもらいたいこととして、完全にエラボレートされた項に対して、コンストラクタの引数は任意のパラメータを含むため、Prod コンストラクタのインスタンスは例えば Prod.mk A B (a : A) (b : B) となります。

射影されたフィールドを示す自然数は0始まりであり、0はコンストラクタの最初の 非パラメータ 引数です。というのも射影は構造体のパラメータのアクセスに使うことができないからです。

これを念頭に置けば、コンストラクタの引数を (constructor, [arg0, .., argN]) へと手直しすれば、射影の簡約は単純に i + num_params の位置にある引数を取るだけであることが明白になるでしょう。ここで num_params はその名前の通りのもので、その構造体型のパラメータの数を表します。

reduce proj fieldIdx structure:
  let (constructorApp, args) := unfoldApps (whnf structure)
  let num_params := environment[constructorApp].num_params
  args[fieldIdx + numParams]

  -- Following our `Prod` example, constructorApp will be `Const(Prod.mk, [u, v])`
  -- args will be `[A, B, a, b]`

射影の特殊なケース：文字列リテラル

カーネルは文字列リテラルについて拡張を行っており、これによって射影の簡約で1つ、ι簡約で1つの特殊なケースが導入されます。

文字列リテラルに対する射影の簡約：なぜなら構造体の射影の式を簡約すると文字列リテラルになる可能性があるからです（Lean の String 型は List Char のフィールドを1つ持つ構造体として定義されています）。

もしその構造体が StringLit (s) に簡約される場合、これを String.mk (.. : List Char) に変換し、いつものように射影の簡約が処理されます。

整数リテラルの簡約

整数リテラル用のカーネル拡張には加算・減算・乗算・指数・除算・剰余・真偽値の同値・真偽値の以下の二項演算に加えて Nat.succ の簡約が含まれます。

簡約される式が Const(Nat.succ, []) n で n が整数リテラル n に簡約できる場合、NatLit(n'+1) に簡約されます。

もし式が Const(Nat.<binop>, []) x y へと簡約され x と y がそれぞれ整数リテラル x' と y' に簡約される場合、適切な <binop> のネイティブ版を x' と y' に適用し、結果の整数リテラルを返します。

例：

Const(Nat.succ, []) NatLit(100) ~> NatLit(100+1)

Const(Nat.add, []) NatLit(2) NatLit(3) ~> NatLit(2+3)

Const(Nat.add, []) (Const Nat.succ [], NatLit(10)) NatLit(3) ~> NatLit(11+3)

ι簡約（パターンマッチ）

ι簡約とは与えられた帰納的宣言に特有でかつそこから派生した簡約戦略を適用することです。これはまさに帰納的宣言の再帰子（または後で説明する Quot の特別な場合）の適用です。

各再帰子は「再帰子ルール」を持っており、各コンストラクタごとに1つの再帰子ルールがあります。型として表示される再帰子とは対照的に、これらの再帰子ルールはコンストラクタ T.c で作成された T 型の要素をどのように除去するかを示す値レベルの式です。例えば、Nat.rec は Nat.zero と Nat.succ それぞれに対する再帰子ルールを持ちます。

帰納的宣言 T に対して、T の再帰子が要求する要素の1つは実際の (t : T) であり、これは除去する対象です。この (t : T) 引数は「major premise」と呼ばれます。ι簡約は major premise を分解することで t の構築にあたってどのコンストラクタが使われたかを確認し、対応する再帰子ルールを環境から取得して適用することでパターンマッチを行います。

再帰子の型シグネチャは必要なパラメータ・motive・minor premiseも要求するため、例えば Nat.succ とは対照的に Nat.zero に対して簡約を実行するために再帰子の引数を変更する必要はありません。

実際には major premise を作成するために使用されたコンストラクタを公開するための初期化的な手動操作が必要になることがあります。というのもこのコンストラクタがコンストラクタを直接適用したものとして見つからないことがあるからです。例えば、NatLit(n) 式は Nat.zero か App Const(Nat.succ, []) .. のいずれかに変換する必要があります。構造体では、構造体のη展開を行う場合もあります。要素 (t : T) を T.mk t.1 .. t.N に変換することで、mk コンストラクタの適用が明らかになり、ι簡約を進めることができます（major premise を作成するために使用されたコンストラクタが分からない場合、簡約は失敗します）。

List.rec type

forall 
  {α : Type.{u}} 
  {motive : (List.{u} α) -> Sort.{u_1}}, 
  (motive (List.nil.{u} α)) -> 
  (forall (head : α) (tail : List.{u} α), (motive tail) -> (motive (List.cons.{u} α head tail))) -> (forall (t : List.{u} α), motive t)

List.nil rec rule

fun 
  (α : Type.{u}) 
  (motive : (List.{u} α) -> Sort.{u_1}) 
  (nilCase : motive (List.nil.{u} α)) 
  (consCase : forall (head : α) (tail : List.{u} α), (motive tail) -> (motive (List.cons.{u} α head tail))) => 
  nil

List.cons rec rule

fun 
  (α : Type.{u}) 
  (motive : (List.{u} α) -> Sort.{u_1}) 
  (nilCase : motive (List.nil.{u} α)) 
  (consCase : forall (head : α) (tail : List.{u} α), (motive tail) -> (motive (List.cons.{u} α head tail))) 
  (head : α) 
  (tail : List.{u} α) => 
  consCase head tail (List.rec.{u_1, u} α motive nilCase consCase tail)

k-like 簡約

「subsingleton eliminator」として知られているいくつかの帰納型では、major premise のコンストラクタが直接公開されていなくても、その型が分かっている限りι簡約を進めることができます。これは例えば major premise が自由変数として現れるような場合です。これは k-like 簡約と呼ばれ、subsingleton eliminator のすべての要素が同一であるため許容されます。

subsingleton eliminator であるためには、帰納的宣言は帰納的な命題でなければならず、また相互帰納的対象や入れ子の帰納的対象であってはならず、コンストラクタはちょうど1つでなければならず、その唯一のコンストラクタは型のパラメータだけを引数として取らなければなりません（型シグネチャで完全に捕捉されていない情報を「隠す」ことはできません）。

例えば、Eq Char 'x' 型の要素の値はこの型のすべての要素は同一であるため、その型だけで完全に決定されます。

ι簡約によって subsingleton eliminator である major premise が見つかった場合、その major premise を型コンストラクタの適用に置換することが許容されます。なぜならその自由変数としてあり得るのがこの型コンストラクタだけだからです。例えば、Eq Char 'a' 型の自由変数である major premise は明示的に構成された Eq.refl Char 'a' に置換することができます。

根本的な話として、もし k-like 簡約を探索して適用することを怠れば、subsingleton eliminator である自由変数は対応する再帰規則を特定できず、ι簡約は失敗し、成功すると期待されたある種の変換は成功しなくなるでしょう。

`Quot` の簡約；`Quot.ind` と `Quot.lift`

Quot はカーネルでハンドルするべき2つの特殊なケースを導入します。1つは Quot.ind で、もう一つは Quot.lift の場合です。

Quot.ind と Quot.lift はどちらも関数 f の引数 (a : α) への適用に対応しており、ここで a は Quot r の構成要素であり、Quot.mk .. a によって形成されます。

この簡約を実行するには、f の要素である引数と、(a : α) が見つかる Quot 要素である引数を取り出し、a に関数 f を適用する必要があります。最後に、Quot.ind や Quot.lift の呼び出しとは関係のない外部式の一部であった引数を再適用します。

これは簡約のステップにすぎないため、式全体が適切に型付けされていることを保証するために他の場所で行われる型チェックの段階に頼ります。

以下に Quot.ind と Quot.mk の型シグネチャを再作成し、テレスコープの要素を引数として見つけるべきものにマッピングしています。* が付いている要素は簡約のために必要なものです。

Quotient primitive Quot.ind.{u} : ∀ {α : Sort u} {r : α → α → Prop} 
  {β : Quot r → Prop}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q

  0  |-> {α : Sort u} 
  1  |-> {r : α → α → Prop} 
  2  |-> {β : Quot r → Prop}
  3* |-> (∀ (a : α), β (Quot.mk r a)) 
  4* |-> (q : Quot r)
  ...

Quotient primitive Quot.lift.{u, v} : {α : Sort u} →
  {r : α → α → Prop} → {β : Sort v} → (f : α → β) → 
  (∀ (a b : α), r a b → f a = f b) → Quot r → β

  0  |-> {α : Sort u}
  1  |-> {r : α → α → Prop} 
  2  |-> {β : Sort v} 
  3* |-> (f : α → β) 
  4  |-> (∀ (a b : α), r a b → f a = f b)
  5* |-> Quot r
  ...

課題と今後の展望

ファイルフォーマット

エクスポートファイルのフォーマットをJSONに移行する件について、こちらにオープンなRFCがあります。これは大きなバージョン変更になるでしょう。

整数・文字列が適切に定義されていることの確認

Nat・String・およびそれらに関連するカーネル拡張がカバーする操作のためのエクスポートファイルの宣言が、信頼されたコードにエクスポータを引き込まない方法で拡張が期待するものと一致するかどうかを判断するための特定の解決策について Lean コミュニティはまだ定まっていません。

Eq と Quot の宣言のようなアプローチ（型チェッカ内で手作業で定義し、それらが同じであることを保証する）は Nat でサポートしているバイナリ演算のための完全にエラボレートされた項が複雑であるため実行不可能です。

Pollack consistency の改善

Lean 4 はカスタム構文・マクロ・プリティプリンタの定義に非常に強力な機能を提供し、Lean 4 の内部のほとんどすべての側面がユーザによって利用可能です。Lean の設計のこれらの要素は Lean 3 の存続期間中に mathlib コミュニティから実際に寄せられたフィードバックに対する効果的な対応でした。

これらの機能は大規模な形式化作業を可能にするツールとして Lean が成功した重要な要因である一方、Lean 4 の Pollack consistency¹ が危うく、もしくは損なわれる恐れがあります。プリティプリンタでマクロと構文拡張機能を複製しなければ、型チェッカは一貫して項を認識可能な形で読んでユーザに返すことができません。しかし、これらの機能をプリティプリンタに追加するアイデアは信頼されたコードベースを拡張する点においては魅力的なものではありません。別のアプローチとしてプリティプリンタをやめて、信頼できるパーサ（通称 metamath zero）を採用する方法もありますが、Lean のパーサはカスタム構文宣言を使ってユーザ空間でその場で変更することができます。

Lean が成熟し、採用が進むにつれて Pollack consistency を犠牲にすることなく、ユーザが Lean の拡張性を活用できるような技術や手法の開発が進められるでしょう。

前方推論

既存の型チェッカは後方推論の形式を実装しています；型チェッカの戦略の別路線として、外部プログラムによって作成された前方推論の連鎖を受け入れ、チェックすることがあり、これは後方推論よりもシンプルな型チェッカとなる可能性があります。

Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012

その他の記事

Mario Carneiro による Lean の型理論

Lean 公式カーネル：https://github.com/leanprover/lean4/tree/master/src/kernel

lean4lean、Lean 4 による Lean カーネルの再実装

lean4export、Lean 4 環境のオフィシャル・推奨エクスポータ
lean4checker

Peter Dybjer による Lean で実装される帰納型に関するオリジナルの記述：P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.

Conor McBride と James McKinna の論文 I am not a number: I am a free variable は束縛・自由変数への locally nameless なアプローチを記述しています。

帰納型における positive ではない出現に関する情報、Counterexamples in Type Systems: https://counterexamples.org/strict-positivity.html?highlight=posi#positivity-strict-and-otherwise
Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012

Type Checking in Lean 4 日本語訳