情報科学 › Claude Code の中身 › 拡張の仕組み
エラーを結果として返すと、ループの不変条件が保たれる
第 1 章 の模型で、あるツールの実行を MCP の tools/call で行うとする。tools/call の帰結は、(i) isError が偽の結果、(ii) isError が真の結果、(iii) プロトコルのエラー、(iv) 応答なし（時間切れ）のどれかである。クライアントが帰結を tool_result に写す規則を とする。
- が (i)・(ii) について「結果の
contentを内容とし、isErrorをエラーの印とする tool_result を 1 つ作る」と定められていれば、(i)・(ii) の帰結のもとで、tool_use と tool_result の対応の不変条件は保たれる。エラーの場合もループは続けられる。 - が (iii)・(iv) について定められていなければ、その帰結のもとで対応する tool_result が作られず、不変条件は破れる。 がすべての帰結について tool_result をちょうど 1 つ作るように定められていれば、不変条件は保たれる。
閉包の状態
✓ 公理まで証明済み
証明が使う定理を 前提 としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 5 件、定義なども含めて 7 件）。
印の意味: ✓公理まで証明済み ・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は 閉包の状況。
前提をたどる 証明が使う定理・定義（直接 2 件）
▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。
ループは対応の不変条件を保つ✓命題 3.4・エージェントループ
- データ型の実装・表現不変条件・抽象化関数定義 6.1・契約による設計
表現不変条件の帰納法✓定理 6.2・契約による設計
拒否された呼び出しもループを止めない✓命題 3.5・エージェントループ
- ループは対応の不変条件を保つ✓命題 3.4・エージェントループ（上で展開済み）
これを使っている定理
証明で明示的に参照している定理は、まだありません。