情報科学 › Claude Code の中身 › エージェントループ

拒否された呼び出しもループを止めない

命題 3.5（「エージェントループ」§3）・ ✓公理まで証明済み

定義 3.1 の 1 段の 4 で、ある $j$ について $g(n_j, x_j) = \mathrm{refuse}$ だったとする。このとき次が成り立つ。

$j$ 番目の呼び出しは環境を変えない（ $e^{(j)} = e^{(j-1)}$ ）。
次の状態のメッセージ列 $h \cdot a \cdot b$ は $\mathrm{Inv}$ を満たし、ループは停止せずに次の段へ進める。
一方、拒否された呼び出しの tool_result ブロックを $b$ から省く方式では、 $h \cdot a \cdot b$ は (P2) を満たさない。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 4 件、定義なども含めて 6 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

前提をたどる証明が使う定理・定義（直接 1 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

ループは対応の不変条件を保つ✓命題 3.4・エージェントループ
- データ型の実装・表現不変条件・抽象化関数定義 6.1・契約による設計
- 表現不変条件の帰納法✓定理 6.2・契約による設計
  - 数学的帰納法の原理✓定理 3.2・証明の技術
    背理法の正当性✓命題 6.2・証明の技術
    整列性公理 3.1・証明の技術

これを使っている定理証明で参照している 1 件

エラーを結果として返すと、ループの不変条件が保たれる✓命題 3.7・拡張の仕組み

関連するノック 1 問

Claude Code の中身第 2 問