付録C 用語集と学習チェックリスト
読んだだけで終わらせないために。
C.1 小さな用語集
| 用語 | 簡単な意味 |
|---|---|
| 命題（proposition） | 真であることを証明したい主張 |
| 証明項（proof term） | 命題に対応する型の値 |
| カーネル | 証明項が型に合うかを検査する、小さな核 |
| 依存型 | 値に依存して、具体的な形が変わる型 |
| 構造帰納法 | データの構成子に沿って、一般の場合を証明する方法 |
| 型クラス | 型が持つ操作と（必要なら）法則のまとまり |
| 所有権（ownership） | 値の使用・複製・破棄に関する管理 |
| 借用（borrow） | 所有権を移さずに、一時的にアクセスすること |
| 代数的効果 | 計算が要求する操作を、ハンドラに分離する仕組み |
| 継続（continuation） | 中断した地点から先の、「残りの計算」 |
| multi-shot | 同じ継続を複数回再開できること |
| effect row | 関数が外側に残す効果の集合 |
| 全域性（totality） | 定義域のすべての入力に結果を与える性質 |
| 信頼の境界 | 形式証明だけでは確認できず、外部的に信頼する対象 |
C.2 自分で確認しよう
読み終えたら、次の質問に口頭で答えてみてください。
letとvarは、所有権の観点と、変更できるかどうかの観点で、どう違うか。Option(i64)とOption<i64>のうち、Tauto で型の適用に使うのはどちらか。affineとlinearでは、資源を使う回数がどう違うか。performとhandleは、何を分担しているか。resume ωは、なぜ所有権の静的な検査と関係するか。(2: Nat) + 2 = 4にReflが使えるのはなぜか。- 帰納法と、有限個のテストケースの違いは何か。
- 「カーネルで証明したこと」と、「ネイティブの実行系を信頼したこと」を区別できるか。
ここまで説明できれば、Tauto の基本の構文と、証明を中心に置いたソフトウェア開発の最初の考え方が身についています。次は、自分の小さな関数に一つの不変条件を与えて、その証明がどの行のコードに対応しているかを、追えるようにしてみてください。