驗證器相關性與獨立性幻覺：Jensen 下界、有效偵測器數，與「一致無資訊、分歧有資訊」的單邊效力

/**
 * 驗證器相關性與獨立性幻覺。
 * 型別層：禁止把同一語料來源的兩個驗證器宣告為獨立。
 * 執行層：以難度變數模型計算共同失效機率，對比獨立假設下的估計。
 * 執行：node s6.ts        型別檢查：tsc --strict --noEmit s6.ts
 */

// ---- 型別層：來源以判別聯集標定，獨立性必須由不同來源證成 ----
type Corpus = "web-corpus" | "code-corpus" | "human-reviewer" | "symbolic-engine";

type Verifier<C extends Corpus> = {
  readonly id: string;
  readonly corpus: C;
  readonly missRate: number; // 單獨作用時的漏檢率
};

/** 獨立性憑證：只能由兩個來源不同的驗證器產生。 */
type IndependencePair<A extends Corpus, B extends Corpus> = {
  readonly left: Verifier<A>;
  readonly right: Verifier<B>;
  readonly justification: string;
};

/**
 * B 被限制為 Exclude<Corpus, A>：傳入同來源的兩個驗證器是型別錯誤，
 * 而不是一個可以在程式碼審查中被忽略的約定。
 */
function assumeIndependent<A extends Corpus, B extends Exclude<Corpus, A>>(
  left: Verifier<A>,
  right: Verifier<B>,
  justification: string,
): IndependencePair<A, B> {
  return { left, right, justification };
}

// ---- 執行層：Eckhardt-Lee 難度變數模型 ----

/** 輸入空間上的「難度」分佈：theta = 單一驗證器在該類輸入上漏檢的機率。 */
type DifficultyProfile = ReadonlyArray<{ readonly theta: number; readonly weight: number }>;

function expectation(profile: DifficultyProfile, f: (t: number) => number): number {
  const total = profile.reduce((s, p) => s + p.weight, 0);
  return profile.reduce((s, p) => s + (p.weight / total) * f(p.theta), 0);
}

/** 真實的共同漏檢率：E[theta^n]，對難度分佈取期望後才做 n 次方。 */
function jointMissRate(profile: DifficultyProfile, n: number): number {
  return expectation(profile, (t) => Math.pow(t, n));
}

/** 獨立假設下的估計：(E[theta])^n，先取期望再做 n 次方。 */
function independentAssumption(profile: DifficultyProfile, n: number): number {
  return Math.pow(expectation(profile, (t) => t), n);
}

/** 等相關近似下的有效偵測器數。rho = 0 時等於 n；rho = 1 時恆為 1。 */
function effectiveVerifiers(n: number, rho: number): number {
  return n / (1 + (n - 1) * rho);
}

/** 一致 / 分歧的單邊效力：回傳兩種觀察各自的似然比。 */
function agreementLikelihoodRatios(rho: number, baseAccuracy: number, underspecRate: number) {
  // 高相關下，兩個驗證器在「作者對」與「作者錯」時都傾向一致 —— 一致無資訊。
  const agreeGivenCorrect = baseAccuracy + (1 - baseAccuracy) * rho;
  const agreeGivenWrong = baseAccuracy * rho + (1 - baseAccuracy) * rho + (1 - rho) * 0.5;
  // 分歧則主要由「這裡從來沒有人決定過」驅動。
  const disagreeGivenUnderspec = underspecRate;
  const disagreeGivenSpecified = (1 - rho) * (1 - baseAccuracy);
  return {
    agreement: agreeGivenCorrect / agreeGivenWrong,
    disagreement: disagreeGivenUnderspec / Math.max(disagreeGivenSpecified, 1e-9),
  };
}

function assert(cond: boolean, msg: string): void {
  if (!cond) {
    console.error("不變式違反：" + msg);
    process.exit(1);
  }
}

// ---- 情境一：架構判斷。偵測任務與生成任務高度相關，難度分佈極度分散。 ----
const architectural: DifficultyProfile = [
  { theta: 0.05, weight: 0.55 }, // 容易的情形，幾乎都抓得到
  { theta: 0.55, weight: 0.30 },
  { theta: 0.95, weight: 0.15 }, // 「所有人一起錯」的那一類輸入
];

// ---- 情境二：局部機械缺陷。偵測與生成是不同任務，難度分佈集中。 ----
const mechanical: DifficultyProfile = [
  { theta: 0.19, weight: 0.50 },
  { theta: 0.20, weight: 0.35 },
  { theta: 0.21, weight: 0.15 },
];

function main(): void {
  // 1. Jensen 不等式：E[theta^n] >= (E[theta])^n，等號僅在 theta 退化為常數時成立。
  for (const n of [2, 3, 5]) {
    const real = jointMissRate(architectural, n);
    const naive = independentAssumption(architectural, n);
    assert(real > naive, `n=${n} 時真實共同漏檢率必須嚴格大於獨立假設估計`);
  }

  console.log("情境一：架構判斷（偵測與生成高度相關）");
  console.log(
    `${"審查者數 n".padEnd(12)}${"真實共同漏檢".padStart(16)}${"獨立假設估計".padStart(16)}${"低估倍數".padStart(12)}`,
  );
  let prevFactor = 0;
  for (const n of [1, 2, 3, 5, 8]) {
    const real = jointMissRate(architectural, n);
    const naive = independentAssumption(architectural, n);
    const factor = real / naive;
    console.log(
      `${String(n).padEnd(12)}${real.toFixed(6).padStart(16)}${naive.toFixed(6).padStart(16)}${factor.toFixed(2).padStart(12)}`,
    );
    if (n > 1) assert(factor > prevFactor, `低估倍數應隨 n 遞增（n=${n}）`);
    prevFactor = n === 1 ? factor : Math.max(prevFactor, factor);
  }

  // 2. 集中難度分佈（機械缺陷）下，獨立假設幾乎成立。
  const mechReal = jointMissRate(mechanical, 5);
  const mechNaive = independentAssumption(mechanical, 5);
  assert(mechReal / mechNaive < 1.05, "難度分佈集中時，獨立假設的低估幅度應很小");
  console.log(
    `\n情境二：局部機械缺陷 n=5 → 真實 ${mechReal.toExponential(3)}，` +
      `獨立假設 ${mechNaive.toExponential(3)}，低估倍數 ${(mechReal / mechNaive).toFixed(3)}`,
  );

  // 3. 有效偵測器數：相關係數把 n 個審查者壓縮成 n_eff 個。
  console.log(`\n${"rho".padEnd(8)}${"n=2".padStart(10)}${"n=5".padStart(10)}${"n=10".padStart(10)}${"n→∞ 上界".padStart(12)}`);
  for (const rho of [0.0, 0.1, 0.3, 0.6, 0.9]) {
    const bound = rho > 0 ? 1 / rho : Infinity;
    console.log(
      `${rho.toFixed(1).padEnd(8)}${effectiveVerifiers(2, rho).toFixed(2).padStart(10)}` +
        `${effectiveVerifiers(5, rho).toFixed(2).padStart(10)}${effectiveVerifiers(10, rho).toFixed(2).padStart(10)}` +
        `${(rho > 0 ? bound.toFixed(2) : "∞").padStart(12)}`,
    );
    if (rho > 0) {
      assert(effectiveVerifiers(10, rho) < 10, `rho=${rho} 時有效偵測器數必須小於 n`);
      assert(effectiveVerifiers(1000, rho) < bound + 1e-6, `rho=${rho} 時 n_eff 不得超過 1/rho 上界`);
    }
  }
  assert(Math.abs(effectiveVerifiers(5, 0) - 5) < 1e-12, "rho=0 時 n_eff 應等於 n");

  // 4. 單邊效力：一致無資訊，分歧有資訊。
  const lr = agreementLikelihoodRatios(0.85, 0.8, 0.6);
  assert(Math.abs(lr.agreement - 1) < 0.25, `高相關下「一致」的似然比應接近 1，實得 ${lr.agreement.toFixed(3)}`);
  assert(lr.disagreement > 5, `「分歧」的似然比應顯著大於 1，實得 ${lr.disagreement.toFixed(3)}`);
  console.log(
    `\n單邊效力（rho=0.85）：一致的似然比 ${lr.agreement.toFixed(3)}（接近 1，無資訊）；` +
      `分歧的似然比 ${lr.disagreement.toFixed(2)}（指示欠指定）`,
  );

  // 5. 型別層：獨立性宣告必須由不同來源證成。
  const webModel: Verifier<"web-corpus"> = { id: "reviewer-A", corpus: "web-corpus", missRate: 0.3 };
  const codeModel: Verifier<"code-corpus"> = { id: "reviewer-B", corpus: "code-corpus", missRate: 0.3 };
  const symbolic: Verifier<"symbolic-engine"> = { id: "type-checker", corpus: "symbolic-engine", missRate: 0.4 };

  const pair1 = assumeIndependent(webModel, symbolic, "符號引擎不依賴語料統計，盲區來源不同");
  const pair2 = assumeIndependent(webModel, codeModel, "語料部分重疊，獨立性僅為部分成立");
  // 注意：「兩端來源必須不同」這條不變式不需要執行期檢查——型別系統已經證清它。
  // 寫成 pair1.left.corpus !== pair1.right.corpus 反而會被 tsc 以
  //   TS2367: This comparison appears to be unintentional because the types
  //           '"web-corpus"' and '"symbolic-engine"' have no overlap
  // 指出該比較恆為真。不變式被移到型別層之後，執行期的防衛程式碼就成了多餘。
  assert(pair1.justification.length > 0 && pair2.justification.length > 0, "獨立性宣告必須附理由");
  console.log(`\n已證成的獨立性配對：${pair1.left.id} × ${pair1.right.id}；${pair2.left.id} × ${pair2.right.id}`);

  // 下一行無法通過型別檢查，因為兩端來源相同：
  //   const bad = assumeIndependent(webModel, { id: "reviewer-C", corpus: "web-corpus", missRate: 0.3 }, "同語料");
  //   ^ TS2322: Type '"web-corpus"' is not assignable to type
  //             '"code-corpus" | "human-reviewer" | "symbolic-engine"'

  console.log("\n自驗證通過：Jensen 下界、低估倍數遞增、n_eff 上界、單邊效力與獨立性型別約束斷言全部成立。");
}

main();