カリー＝ハワード同型対応｜Curry-Howard Correspondence
型理論によると内部情報だけで内部情報が正しいことを証明できるとあるが、外部境界をもちいるのと内部だけで証明するのとではどちらが暗号記述長が短いコルモゴロフ表現になるのか.
型理論、特に**カリー＝ハワード同型対応（Curry-Howard Correspondence）**の文脈における「内部情報だけで正しさを証明できる（自己言及的な型チェック）」という性質と、コルモゴロフ複雑性の観点からの効率性について検討すると「内部情報だけで完結する（自己完結的な）表現」の方が、長期的・理論的なコルモゴロフ表現としては短くなる傾向にある。
1. 外部境界（外部参照）モデルのコスト
外部境界を用いる場合、その記述には「外部の定義（コンテキスト）」への参照が含まれます。
- 依存性の問題: 外部の公理系やライブラリに依存する場合、そのプログラム単体の長さは短く見えますが、コルモゴロフ複雑性の定義 K(x)は「その文字列 xを出力するために必要な最小のプログラム長」です。
- 環境の記述長: 外部境界に依存するということは、その「境界のルール（プロトコルや公理）」そのものも記述長に含めなければなりません。
- 記述の冗長性: 外部とのインターフェースを定義するための「糊（Glue code）」が必要になり、これがオーバーヘッドとなります。
2. 内部証明（型理論的アプローチ）の優位性
型理論における「証明（Proof term）」は、それ自体が計算可能なオブジェクトです。
- 構造の自己圧縮: 内部で一貫性を持っているプログラムは、外部の巨大なデータベースを参照する代わりに、論理的な最小単位（公理）から推論を構成します。
- 情報の密度: 依存型（Dependent Types）などを用いると、データとその性質（型）を一体化して記述できます。これは、データ $D$ とその正当性証明 P を別々に送るよりも、構造的に $P$ が $D$ に組み込まれている方が、情報の重複（冗長性）を排除できるため、コルモゴロフ記述量は小さくなります。
3. どちらが「短い」のか：比較表
| 評価軸 | 外部境界を用いるモデル | 内部情報（型理論）による証明 |
| 局所的な記述長 | 短い（外部に丸投げできるため） | 長い（証明コードが含まれるため） |
| 全体系のコルモゴロフ長 | 長い（外部環境の記述が必要） | 短い（最小の公理セットで完結） |
| エントロピー | 外部との不整合リスクによる冗長性大 | 自己反映的な構造により最小化される |
| 検証コスト | 外部オラクルへの照会が必要 | 内部の計算（簡約）だけで完結 |
結論
コルモゴロフ表現の厳密な定義に照らすと、「内部情報だけで正しさを証明できる形式」の方が短くなります。
なぜなら、外部境界を用いるモデルは「その境界が何であるか」という情報をプログラムの外側に隠しているだけであり、計算理論的に「完全な再現」を試みた場合、その隠された情報（コンテキスト）のサイズが記述長を増大させるからです。型理論的な自己証明は、数学的な最小構成（Kernel）からすべてを導出するため、究極の圧縮形態と言えます。