情報科学 › Claude Code の中身 › 文脈を保つ・減らす・分ける

圧縮とキャッシュ

命題 3.9(「文脈を保つ・減らす・分ける」§3) ・ ✓公理まで証明済み

圧縮の直前の要求をトークン列 R=P CR = P\,C(PP は会話より前の層、CC は会話の層)とし、RR の末尾までがキャッシュに書かれているとする。

  1. 要約を作る要求が R IR\,I(RR の末尾に要約の指示 II を足したもの)の形なら、RR はその接頭辞で、キャッシュが有効期間内なら RR の末尾のブレークポイントに命中する。前章の模型のとおり、新しく足した部分を末尾のブレークポイントまで書き込むとすると、このときの入力コストは r ∣R∣+w ∣I∣r\,|R| + w\,|I|、有効期間が切れていれば w (∣R∣+∣I∣)w\,(|R| + |I|) である。
  2. 圧縮のあとの要求を P′ S DP'\,S\,D(SS は要約、DD は新しい追記)とする。CC と SS の最初に食い違う位置より後ろにあるブレークポイントは、どれも命中しない。P′=PP' = P なら PP の末尾までのブレークポイントは命中しうるが、P′≠PP' \ne P なら、食い違う位置より後ろはすべて命中しない。

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

閉包の状態

✓ 公理まで証明済み

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

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

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

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

これを使っている定理

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