/-! # 第1章：型・項・定義・計算 `2 + 3` は自然数の加算として読めます。これに対して `2 + true` では、数を足す演算の場所に 真偽値が置かれています。どちらも記号として紙に書けますが、同じ計算規則で扱えるわけではありません。 記号の書き方と使い方を規則で定めた言語を**形式言語**（formal language）と呼びます。形式言語を 学ぶ第一歩は、記号を暗記することではなく、「この書き方は何として使えるか」を見分けることです。 式を型によって分類する形式言語の理論を**型理論**（type theory）と呼びます。本章では、まず一般の 型理論で**式**、**型**、**項**を順に定義し、型理論でいう**判断**という語へ到達します。次に、 その区別がLeanの表示とコマンドにどう現れるかを確かめ、型検査、評価、定義という三つの操作へ進みます。 ## 書けることと、受理されることは異なる ある形式言語の規則に従って組み立てた記号のまとまりを**式**（expression）と呼びます。ここでは `2`、`true`、`2 + 3`、`2 + true` を候補となる式として考えます。ただし、言語の構文規則だけで 作れることと、その式へ計算上の役割を与えられることは別です。ここで**構文規則**とは、記号をどの順で 組み合わせれば候補となる式を作れるかを定める規則です。 式を「自然数として使える」「真偽値として使える」というように分類するものを**型**（type）と 呼びます。型は、どのように値を作り、どの操作へ渡せるかを定めます。型を値の集合とみなす解釈は 有用ですが、本書ではまだ定義に採用しません。まずは、許される構成と使用を定める分類として読みます。 ## 型を持つという主張 式 $e$ が型 $A$ に分類されることを $$ e : A $$ と書き、「$e$ は型 $A$ を持つ」と読みます。型理論では、規則に照らして成立するか否かを問う文を **判断**（judgment）と呼びます。上の文は、とくに**型付け判断**です。判断は計算される値ではなく、 式が体系の規則に適合することについての主張です。 型付け判断 $e : A$ が成立する式 $e$ を、型 $A$ の**項**（term）と呼びます。したがって本章では、 「式」を分類前の候補まで含む広い語として使い、「項」を型とともに認められた式に限って使います。 ```text 式 e ── 型付け規則を満たす ──→ 判断 e : A が成立 ──→ e は A の項 ``` `2 + true` は候補となる式として書けても、自然数の加算について型付け判断を導けません。この説明は 型を持つ形式言語に共通します。Leanでは、この分類を `#check` によって直接観察できます。 ## 規則から判断を導く 型付け判断は、例を眺めて真偽を推測する文ではありません。どの判断からどの判断へ進めるかを**推論規則** （inference rule）で定めます。自然数と真偽値を持つ簡単な言語なら、数値と加算の規則を次のように書けます。 $$ \frac{}{n : \mathsf{Nat}} \qquad \frac{m : \mathsf{Nat} \qquad n : \mathsf{Nat}} {m+n : \mathsf{Nat}} $$ 横線の上は前提、下は結論です。最初の規則には前提がなく、数値リテラルを自然数の項として導入します。 第二の規則は、二つの前提をともに導けたときだけ和を自然数の項と認めます。したがって $$ \frac{\dfrac{}{2 : \mathsf{Nat}} \qquad \dfrac{}{3 : \mathsf{Nat}}} {2+3 : \mathsf{Nat}} $$ という導出を作れます。`true` に得られるのは $\mathsf{Bool}$ という別の型です。第二の規則が要求する 右前提 $\mathsf{Nat}$ を満たさないため、同じ規則から $2+\mathit{true} : \mathsf{Nat}$ は導けません。 この失敗は「結果が未定」という計算上の失敗ではなく、計算を始めるための型付け判断が成立しないことです。 -/ namespace FormalLab.Foundation.TermsAndTypes /-! ## Leanで型を観察する -/ #check 2 #check true #check Nat /-! Leanの `#check` は、式を精緻化して型検査し、得られた型を表示する観察コマンドです。 ```text 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` という名前を与えます。 -/ def two : Nat := 2 /-- 自然数 `n` を受け取り、`n + n` を返す定義です。 -/ def double (n : Nat) : Nat := n + n /-! Leanの宣言を左から読むと、各部分の役割が分かります。空白の幅に意味を持たせず、構文と役割を 対応させると次のようになります。 | 構文 | 役割 | この宣言で表すもの | |---|---|---| | `double` | 名前 | 定義した関数を後から参照する名前 | | `(n : Nat)` | 入力 | 自然数型 `Nat` の引数 `n` | | `: Nat` | 出力型 | 関数が返す値の型 | | `:= n + n` | 本体 | 入力から出力を計算する式 | -/ /-! ## 仮定の下で型を調べる 一般の型理論では、ある式を調べる間だけ変数の型を仮定できます。自然数 `n` を仮定して `n + n` を調べるには、仮定を左に添えて次のように書きます。 $$ n : \mathsf{Nat} \vdash n+n : \mathsf{Nat}. $$ 記号 `⊢` の左には利用できる仮定、右にはその仮定から確かめる判断を置きます。仮定が増えたときは、 その列をギリシア文字 $\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 Nat #check two #check double #check double two -- 計算を観察する。`double two` は定義を展開すると `2 + 2` になる。 #eval double two /-! ## 検査と計算は別の問いに答える `#check double two` の答えは `Nat` です。これは結果がどの規則で使えるかを教えます。 `#eval double two` の答えは `4` です。これは閉じた計算を実行した結果を教えます。 型が分かっても値はまだ分からず、値を計算できても一般の法則を証明したことにはなりません。 ## 入力した式が検査されるまで Leanは数値リテラルや省略された引数を含む入力を、そのまま最終検査へ渡しません。 **elaborator**（精緻化器）が省略を補って 核となる項を作り、**kernel**（核）がその項の型を小さな規則集合で再検査します。`#check` の表示は、 この処理を通った結果の観察です。 `#reduce` は定義展開などkernelの簡約に近い形を観察し、`#eval` は実行系を使って値を 計算します。初学段階では、前者を「定義が何へ展開されるか」、後者を「プログラムの結果は 何か」と読むとよいでしょう。elaboratorとkernelはLean固有の構成要素であり、一般の型理論でいう 型・項・判断の定義そのものではありません。 -/ #reduce double two /-! ## 定義が導入するもの `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のエラー文を貼るだけでなく、各情報を型付け判断へ翻訳した説明を添えます。 修正後の二定義が型検査を通り、元の不成立との差を一つの対応表で示せれば完了です。 -/ end FormalLab.Foundation.TermsAndTypes