カーネルとは何か？

カーネル（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 のエクスポートフォーマット 用のパーサと、入出力用でそれぞれにプリティプリンタも必要になります。パーサとプリティプリンタはカーネルの一部ではありませんが、カーネルと興味深いやり取りをしたいのであれば重要です。