STEP: 1524 / Test: 29/29 PASS / Lean 4: 5 theorem zero sorry / Type: STEP 1493 情報科学 3rd tool (47 defer 全体 15 番目)
★ Halting UNDECIDABLE → SELF⟲ diagnostic tool 化: STEP 1493 情報科学 arc 核 identity (complexity_undecidable_gives_self) の operational 実装。 bounded execution 内で fixpoint / cycle / divergence 診断。
❶ Bounded execution + fixpoint / cycle detection: initial state + step function → maxSteps 内で 診断。 Halting problem 一般解 は 計算不能 (Turing 1936、 non-goal 明記)。
❂ SELF⟲ 二重: fixpoint (next = current) と cycle (state repeats in history) の 両 case で SELF verdict = 自己参照 loop の 二形態。
❸ Generic type State: number / string / object 全対応、 JSON.stringify equality (custom equals も 対応)。
| Condition | Verdict | Reason |
|---|---|---|
| isHalted(state) = true | TRUE | halted_normally |
| next = current (fixpoint) | SELF ★ | fixpoint_reached |
| state repeats in history | SELF ★ | cycle_detected_undecidable |
| monotone divergent (20+ increases + large) | INFINITY | divergent_growth |
| maxSteps exceeded | NEITHER | undecidable_within_budget |
| invalid input | NEITHER | invalid_input |
// Countdown → TRUE (halted)
haltingDiagnosticLens({
initial: 5,
step: (n) => n - 1,
isHalted: (n) => n <= 0,
maxSteps: 20,
});
// { verdict: 'TRUE', reason: 'halted_normally', stepsExecuted: 5 }
// Identity → SELF (fixpoint)
haltingDiagnosticLens({ initial: 42, step: (n) => n });
// { verdict: 'SELF', reason: 'fixpoint_reached', cycleLength: 1 }
// Cycle 0→1→2→0 → SELF ★
haltingDiagnosticLens({ initial: 0, step: (n) => (n+1) % 3 });
// { verdict: 'SELF', reason: 'cycle_detected_undecidable', cycleLength: 3 }
// Doubling → INFINITY (divergent)
haltingDiagnosticLens({
initial: 1,
step: (n) => n * 2,
stateToNumber: (n) => n,
});
// { verdict: 'INFINITY', reason: 'divergent_growth' }
// Collatz small budget → NEITHER (undecidable within budget)
haltingDiagnosticLens({
initial: 27,
step: (n) => n % 2 === 0 ? n / 2 : 3 * n + 1,
isHalted: (n) => n === 1,
maxSteps: 5, // 27 needs 111 steps
});
// { verdict: 'NEITHER', reason: 'undecidable_within_budget' }
halt_halted_gives_true : halted → TRUE halt_fixpoint_gives_self : fixpoint → SELF ★ halt_cycle_gives_self : cycle → SELF ★ halt_divergent_gives_infinity : divergent → INFINITY halt_budget_gives_neither : budget exceeded → NEITHER
❶ Non-goal: Halting problem 一般解 は 計算不能 (Turing 1936 diagonal argument)、 本 tool は bounded steps 内の 診断のみ。
❂ divergent heuristic (20 consecutive increases + value > 1e6) は 保守的、 false positive/negative あり。
❸ cycle detection は O(n²) (history 全 scan)、 大 history では 遅い、 Brent's algorithm 未 embed。
❹ 「世界初」 なし = Turing 1936 既知 D-FUMT₈ mapping。 novelty = SELF⟲ 二形態 (fixpoint + cycle) の 明示区別。
❺ 累計 defer 34 → 33。