情報科学 › Claude Code の中身 › 拡張の仕組み

ツール定義の常駐コスト

命題 3.8(「拡張の仕組み」§3) ・ ✓公理まで証明済み

NN 個のツールがあり、ツール ii の定義の長さを did_i、名前の長さを mim_i(mi≤dim_i \le d_i)とする。会話の中で使うツールの集合を UU とする。

  1. 定義を前もって全部読み込む方式で、文脈に置かれるツールの記述の量は ∑i=1Ndi\sum_{i=1}^{N} d_i。
  2. 名前だけを置き、使うときに定義を読み込む方式では ∑i=1Nmi+∑i∈Udi\sum_{i=1}^{N} m_i + \sum_{i \in U} d_i。
  3. 差(1 から 2 を引いたもの)は ∑i∉U(di−mi)−∑i∈Umi\sum_{i \notin U} (d_i - m_i) - \sum_{i \in U} m_i。定義と名前の長さがどれも dd、mm で ∣U∣=u|U| = u のとき、差は (N−u)(d−m)−u m(N - u)(d - m) - u\,m で、2 のほうが小さいのは u<N (d−m)/du \lt N\,(d - m)/d のときである。
  4. 2 の方式で、定義の読み込みをメッセージ列の末尾への追記として行えば、それまでの要求は新しい要求の接頭辞のままで、既存のキャッシュのブレークポイントは命中し続ける。要求の先頭の層にあるツール定義の集合を途中で変える方式では、変えた位置より後ろのブレークポイントはすべて命中しない。

本文で読む(証明と前後の説明)→

閉包の状態

✓ 公理まで証明済み

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

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

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

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

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 1 問