第1章：型・項・定義・計算#

2 + 3 は自然数の加算として読めます。これに対して 2 + true では、数を足す演算の場所に 真偽値が置かれています。どちらも記号として紙に書けますが、同じ計算規則で扱えるわけではありません。 記号の書き方と使い方を規則で定めた言語を形式言語（formal language）と呼びます。形式言語を 学ぶ第一歩は、記号を暗記することではなく、「この書き方は何として使えるか」を見分けることです。

式を型によって分類する形式言語の理論を型理論（type theory）と呼びます。本章では、まず一般の 型理論で式、型、項を順に定義し、型理論でいう判断という語へ到達します。次に、 その区別がLeanの表示とコマンドにどう現れるかを確かめ、型検査、評価、定義という三つの操作へ進みます。

書けることと、受理されることは異なる#

ある形式言語の規則に従って組み立てた記号のまとまりを式（expression）と呼びます。ここでは 2、true、2 + 3、2 + true を候補となる式として考えます。ただし、言語の構文規則だけで 作れることと、その式へ計算上の役割を与えられることは別です。ここで構文規則とは、記号をどの順で 組み合わせれば候補となる式を作れるかを定める規則です。

式を「自然数として使える」「真偽値として使える」というように分類するものを型（type）と 呼びます。型は、どのように値を作り、どの操作へ渡せるかを定めます。型を値の集合とみなす解釈は 有用ですが、本書ではまだ定義に採用しません。まずは、許される構成と使用を定める分類として読みます。

型を持つという主張#

式 $e$ が型 $A$ に分類されることを

と書き、「$e$ は型 $A$ を持つ」と読みます。型理論では、規則に照らして成立するか否かを問う文を 判断（judgment）と呼びます。上の文は、とくに型付け判断です。判断は計算される値ではなく、 式が体系の規則に適合することについての主張です。

型付け判断 $e : A$ が成立する式 $e$ を、型 $A$ の項（term）と呼びます。したがって本章では、 「式」を分類前の候補まで含む広い語として使い、「項」を型とともに認められた式に限って使います。

式 e  ── 型付け規則を満たす ──→  判断 e : A が成立  ──→  e は A の項

2 + true は候補となる式として書けても、自然数の加算について型付け判断を導けません。この説明は 型を持つ形式言語に共通します。Leanでは、この分類を #check によって直接観察できます。

規則から判断を導く#

型付け判断は、例を眺めて真偽を推測する文ではありません。どの判断からどの判断へ進めるかを推論規則 （inference rule）で定めます。自然数と真偽値を持つ簡単な言語なら、数値と加算の規則を次のように書けます。

横線の上は前提、下は結論です。最初の規則には前提がなく、数値リテラルを自然数の項として導入します。 第二の規則は、二つの前提をともに導けたときだけ和を自然数の項と認めます。したがって

という導出を作れます。true に得られるのは $\mathsf{Bool}$ という別の型です。第二の規則が要求する 右前提 $\mathsf{Nat}$ を満たさないため、同じ規則から $2+\mathit{true} : \mathsf{Nat}$ は導けません。 この失敗は「結果が未定」という計算上の失敗ではなく、計算を始めるための型付け判断が成立しないことです。

Leanで型を観察する#

Leanの #check は、式を精緻化して型検査し、得られた型を表示する観察コマンドです。

2         : Nat
Bool.true : Bool
Nat       : Type

右側はLeanが求めた型です。左側は精緻化後の式なので、true の省略された名前空間が そのまま再表示されるとは限りません。型付け判断 $e : A$ は型についての一つの主張であり、Leanで #check e を実行すると、検査結果が同じコロン記法で表示されます。

最初の #check 2 では期待する型を指定していないため、Leanは単独の数詞を既定の自然数として解釈します。 型を明記して検査させる書き方は、次の def 宣言で導入します。

Nat : Type は、自然数型 Nat 自身もLeanの中で分類されることを表します。Type の階層は 「宇宙階層と宇宙多相」で扱うため、ここでは「型を分類する型」とだけ読みます。

Leanで名前を定義する#

Leanでは、受理された式に def で名前を与えられます。次の二つの宣言では、コロンの右に期待する 型を明記し、右辺が本当にその型を持つかを検査させます。

Nat 型の項 2 に two という名前を与えます。

自然数 n を受け取り、n + n を返す定義です。

Leanの宣言を左から読むと、各部分の役割が分かります。空白の幅に意味を持たせず、構文と役割を 対応させると次のようになります。

仮定の下で型を調べる#

一般の型理論では、ある式を調べる間だけ変数の型を仮定できます。自然数 n を仮定して n + n を調べるには、仮定を左に添えて次のように書きます。

記号 ⊢ の左には利用できる仮定、右にはその仮定から確かめる判断を置きます。仮定が増えたときは、 その列をギリシア文字 $\Gamma$ で略し、一般に $\Gamma \vdash e : A$ と書きます。ここで初めて文脈 （context）が必要になります。外から仮定を必要としない式を閉じた式と呼び、その型だけを示すときは 左側を省略して単に $e : A$ と書きます。

型付け判断とLeanの宣言を対応させる#

Leanの double では、引数宣言 (n : Nat) が数式中の文脈 $n : \mathsf{Nat}$ に、本体 n + n と 出力型 Nat が右側の判断 $n+n : \mathsf{Nat}$ に対応します。一般の文脈付き判断をLeanが def という同じ構文で表しているわけではなく、関数定義を検査する過程で同じ型情報を使っています。

two は引数を持たない名前付きの項、double は自然数を受け取る項です。型を先に予想してから #check の出力と比べてください。

検査と計算は別の問いに答える#

#check double two の答えは Nat です。これは結果がどの規則で使えるかを教えます。 #eval double two の答えは 4 です。これは閉じた計算を実行した結果を教えます。 型が分かっても値はまだ分からず、値を計算できても一般の法則を証明したことにはなりません。

入力した式が検査されるまで#

Leanは数値リテラルや省略された引数を含む入力を、そのまま最終検査へ渡しません。 elaborator（精緻化器）が省略を補って 核となる項を作り、kernel（核）がその項の型を小さな規則集合で再検査します。#check の表示は、 この処理を通った結果の観察です。

#reduce は定義展開などkernelの簡約に近い形を観察し、#eval は実行系を使って値を 計算します。初学段階では、前者を「定義が何へ展開されるか」、後者を「プログラムの結果は 何か」と読むとよいでしょう。elaboratorとkernelはLean固有の構成要素であり、一般の型理論でいう 型・項・判断の定義そのものではありません。

定義が導入するもの#

def は、証明なしで受け入れる新しい前提、すなわち公理を追加する命令ではありません。 右辺を持つ名前を導入し、その名前は必要に応じて本体へ展開できます。したがって two を使うことは、本質的には 2 を使う ことです。名前は計算内容を変えず、後続の説明と再利用の単位を作ります。

一方、同じ型を持つ項が同じ値とは限りません。2 : Nat と 3 : Nat はどちらも型検査を 通りますが、型が等しいことは項が等しいことを意味しません。型は「どの値か」ではなく、 「どの種類の構成・使用が許されるか」を制約します。

型・項・計算を同一視しない#

#eval double two が 4 を返すことと、一般に二つの式が等しいと証明することは 同じではありません。定義を展開するだけで同じ形になることと、二つの式が等しいという証拠を 構成することの違いは、「等式・代入・外延性・一意存在」で厳密に定義します。

要点#

型理論の基本的な主張は、孤立した式ではなく $e : A$ という型付け判断です。推論規則は前提から 判断を導く方法を定め、導出の有無が受理と拒否を分けます。#check は判断の型側を、 #eval は計算可能な項の値を観察し、def は型検査済みの本体へ名前を与えます。この三操作を 区別できれば、後の章で「命題を型、証明を項として扱う」準備ができます。

研究史と文献案内#

本章の「型」は、歴史上の単一の体系からそのまま採った概念ではありません。Russellの1908年の 分岐型理論 [RUS08] は、論理的逆理を避ける階層を組織しました。Churchの1940年の単純型理論 [CHU40] は、ラムダ項と型の規則を結びつけました。両者は目的にも構文にも違いがあり、Leanの型理論の旧版として 並べることはできません。

判断と規則を証明論から学ぶには [GLT89]、プログラミング言語の静的意味論として学ぶには [TAPL02; PFPL16] が次の文献です。とくに [PFPL16] は、構文的対象を定めてから判断と規則へ進むため、 本章で用いた「書ける式」と「成立する型付け判断」の区別を一般化できます。現行Leanのelaboratorと kernelについては [LEAN-REF] を参照します。

問題#

型判断の構造を復元する#

Nat : Type と two : Nat を、単なるコロン記法の例ではなく、異なる二つの型判断として分解してください。 式、項、型、判断の四語をそれぞれ定義してください。体系の中で分類される対象を指す語と、 規則の成立について述べる文を指す語を明記します。

続いて $\Gamma \vdash e : A$ に、仮定 n : Nat の下で調べる式 n + 1 を代入し、文脈 $\Gamma$ を完全に 書いてください。解答は、判断の左右を項同士の等式と誤解せず、何が仮定で何が結論かを説明できれば完了です。

最後に、本章の加算規則を使って $2+3 : \mathsf{Nat}$ の導出木を何も見ずに再構成します。葉、横線、 結論がそれぞれ何を表すかを説明し、右辺を true に替えると、どの前提を作れなくなるかを指してください。

型検査と評価を別の実験として設計する#

triple (n : Nat) : Nat を定義し、#check triple 4 と #eval triple 4 の出力をLeanに渡す前に書いてください。 それぞれのコマンドが検査する入力、返す結果、答えない問いを三列の表にします。さらに 2 : Nat と 3 : Nat を用い、型が一致しても値の同一性は従わないことを示します。

最後に、型検査に成功するが計算結果をこの章の知識だけでは予測しにくい式と、型検査の前に拒否される式を一つずつ作ります。 両者の差を「検査」と「評価」の語だけに頼らず、入出力を指して説明してください。

拒否される定義を判断の不成立として診断する#

def bad : Nat := true について、期待型、本体から推論される型、成立させたい判断を順に書いてください。 その上で、宣言型を Bool に変える修正と、本体を自然数に変える修正が、どの判断を成立させるかを比較します。

診断にはLeanのエラー文を貼るだけでなく、各情報を型付け判断へ翻訳した説明を添えます。 修正後の二定義が型検査を通り、元の不成立との差を一つの対応表で示せれば完了です。