付録D 意味論・仕様索引
綴りは構文早見表、規則の理由と例は以下の各章を参照してください。この索引は、本で説明している範囲の規則を探す入口です。言語の全構文や、まだ検証していない機能を網羅した仕様ではありません。
D.1 値・宣言・型
| 調べたいこと | 規則と注意点 | 詳しい説明 |
|---|---|---|
| 束縛と代入 | let と var を区別し、変更可能なセルへの代入に := を使う | 値と型 |
| 数値型 | 固定幅の整数・浮動小数点・証明で使う Nat を同じものとして扱わない | 基本型、実行時の対応 |
| 関数と分岐 | 引数と結果の型、分岐ごとの結果、残る効果を確認する | 関数と制御フロー |
| データ構造 | struct のフィールド、enum の構成子、match の各場合を区別する | struct・enum・match |
| 型パラメータ | 本の関数例は <A>、型の適用は List(A)。任意の項ジェネリクスまで使えるとは読み替えない | ジェネリクス |
| 型クラス | where Ord(A) の要求と、比較の実装と、証明で使う法則の境界を区別する | 型クラス、ソートの証明 |
| 名前と import | 相対パスでの取り込みと標準ライブラリの取り込み、pub の公開範囲を確認する | プロジェクト |
D.2 所有権・借用・効果
| 調べたいこと | 規則と注意点 | 詳しい説明 |
|---|---|---|
copy / shared / affine / linear | 複製と破棄に関する使用規則。変数が変更可能かとは別の軸 | 四つの種 |
& と &mut | 読み取りと変更の借用を区別する。値を移動する呼び出しと混同しない | 借用 |
| view の束縛 | let &x := ... の使用範囲を確認する | 借用と参照 |
perform / handle | 効果の要求と、その処理を分ける。未処理の効果は外側に残る | 代数的効果 |
! {…} | 関数の結果と別に、外に現れる効果を読む | 関数、効果 |
resume | 継続を使える回数と、その環境に含まれる値の使用規則を合わせて考える | 継続と所有権 |
| 実行の予算 | 言語の予算と、ホストの時間・メモリ制限を混同しない | 実行の上限、信頼の境界 |
D.3 命題・証明・宇宙
| 調べたいこと | 規則と注意点 | 詳しい説明 |
|---|---|---|
Prop と証明項 | 命題を型として、証明をその型を持つ項として読む | 証明の第一歩 |
Refl | 等式の両辺が定義に従う計算で一致するときに使う。任意の数学的等式を自動で証明する道具ではない | 等式 |
| 帰納法 | 各構成子の場合と帰納法の仮定を区別する | 帰納法と再帰 |
| タクティク | 証明を構築する支援と、完成した証明の検査を区別する | タクティク |
?name | 未完成の穴。候補を表示できても、埋めた後の検査成功が必要 | 証明支援 |
Type(u) / Level | 宇宙の高さを読む。自由な記号レベルの推論を前提にしない | 依存型と宇宙 |
| 公理・外部関数 | 仮定として採用した命題と外部実装は保証の境界に含まれる | 信頼の境界 |
D.4 よく混同する概念
- 型の一致と等式の証明：型検査中の定義的な一致と、命題としての等式に証明項を与えることは同じ操作ではありません。計算で一致しない等式には、書き換えや別の証明が必要になる場合があります。
- 定理と実行テスト：一般の入力に関する定理と、選んだ入力で実行したテストは別の証拠です。どちらかの成功を他方の成功と読み替えません。
- 依存型とすべての型レベル関数：値を含む命題が書けることから、あらゆる実行用関数やクラスメソッドを型の位置で利用できるとは限りません。使いたい経路ごとに小さな例で検査してください。
- 検査済みと実行可能：検査が成功したファイルでも、使うバックエンド・ホスト能力・外部関数との組合せは別に確認します。
D.5 ここにない仕様を調べる
標準 API の正確な引数や公開範囲は、使っているバージョンの tauto library FILE と tauto doc PATH で確認します。CLI の選択肢は tauto --help と対象コマンドの --help を参照します。マクロ、FFI、各バックエンドの全制約について、この索引だけを完全な仕様として使わないでください。
不明な構文を新しい推測で埋めるより、まず検証の手引きに従って小さな再現を作ります。設計提案と、配布されたバージョンで動く機能を区別して記録してください。