Глава 5. Типобезопасность как fuel-финитизация

Ещё одно лицо финитизации

После дискриминанта (15.4) — ещё один положительный, разрешимый инструмент той же границы: типизированная оценка. Цепь редукций программы потенциально бесконечна, и вопрос «оборвётся ли она?» в общем виде есть role-limit (15.3). Наша система не пытается его решить — она финитизирует: горючее обрезает бег до конечной глубины (P4), а типобезопасность гарантирует, что этот конечный бег никогда не застрянет неожиданно (допустим лишь явно выделенный благонамеренный тупик). Коротко:

типобезопасность — это финитизация цепи редукций горючим: бесконечное сворачивается в конечный прогон, а типы держат его осмысленным.

Сам результат типобезопасности (сохранение$+$прогресс) стандартен; наш угол — читать горючее как P4-финитизацию, а всю главу — как положительное зеркало дискриминанта.

Выражения, типы, шаг

Язык задан тремя вещами. Выражения — индуктивные термы (константы, пары, $\lambda$, применение, системные конструкции). Типы — роль, которую выражению позволено играть (типовое суждение $\Gamma ⊢e:T$). Шаг — малошаговое отношение редукции $e\to e^{\prime }$: именно ПОРЯДОК шагов (L5) превращает терм в вычисление, а его итерация — в цепь $e\to e_1\to e_2\to \dots$¹

В терминах E/R/R это снова знакомая триада: выражения — элементы, шаг — правило (L5), тип — роль (L4). Вопрос главы — когда бег по правилу безопасен и как сделать его конечным.

Сохранение типов и прогресс

Типобезопасность стоит на двух половинах. Сохранение (subject reduction): тип не теряется при шаге — если $\Gamma ⊢e:T$ и $e\to e^{\prime }$, то $\Gamma ⊢e^{\prime }:T$. Прогресс: хорошо типизированное замкнутое выражение либо уже значение, либо может шагнуть — застрять «неожиданно» оно не может (единственные тупики благонамеренны, выделены отдельным предикатом). Вместе:

$$\text{хорошо типизировано}⟹\text{бег не упирается в неожиданный тупик.}$$

Это и есть «well-typed programs don’t get stuck», машинно.²

Горючее финитизирует редукцию

Сохранение и прогресс говорят о каждом шаге. Но цепь шагов может быть сколь угодно длинной — и здесь вступает горючее (fuel). eval_fuel $n$ применяет шаг не более $n$ раз:

$$‘eva{l}_{f}uel‘0e=e,‘eva{l}_{f}uel‘(n+1)e=\{\begin{array}{ll}e,& e\text{ — значение},\\ ‘eva{l}_{f}uel‘n(\text{шаг }e),& \text{иначе.}\end{array}$$

Это та же P4-развёртка, что run $n$ для остановки (15.1): бесконечная цепь — role-limit, а eval_fuel $n$ — её конечное приближение. И две половины §15.5.3 переносятся на бег с горючим: тип сохраняется вдоль всего прогона, а безопасная оценка звучна — хорошо типизированная программа в пределах бюджета даёт значение либо честный частичный результат с progress-статусом, но никогда не выходит за доказанную типовую дисциплину и не застревает неожиданно.³

Имя P4_evaluation_terminates говорит само за себя: завершаемость здесь — не свойство программы (его-то диагональ и запрещает решать тотально), а свойство процесса с горючим. Мы не решаем halting — мы его обходим финитизацией.

Зеркало дискриминанта

Типобезопасность — тот же положительный ход, что дискриминант (15.4): свести role-limit-вопрос к терминирующей процедуре. Дискриминант сводит «спектр рационален?» к тесту полного квадрата; горючее вместе с типобезопасностью заменяет вопрос «оборвётся ли бесконечная редукция?» на конечную процедуру: проверить тип, выполнить $n$ шагов, получить тип-сохраняющий результат с progress-статусом. Оба рисуют Element-границу одним терминирующим критерием; оба — на положительной стороне пары диагональ $\oplus$ дискриминант. Аналогия точна с оговоркой: дискриминант решает свойство на заданном классе; горючее$+$типобезопасность не решает остановку, а сертифицирует каждый конечный прогон.

Важно, чего глава не утверждает. Диагональ (15.3) запрещает тотальный решатель завершаемости, и типовая система его не обходит как теорему — она финитизирует вокруг него: горючее делает всякий бег конечным (P4), а типы делают конечный бег осмысленным. Это и есть честный смысл «вычисление есть граница финитизации»: там, где тотального ответа нет, есть конечная процедура с гарантией.

Разбор E/R/R и что глава подготовила

Правила (L5). Малошаговый шаг $e\to e^{\prime }$ конституирует вычисление; eval_fuel $n$ — его P4-развёртка на конечную глубину; сохранение$+$прогресс — правило, делающее бег безопасным.

Роли (L4). Тип — роль, которую выражению позволено играть; проверка типов — роль-критерий (разрешимый); «значение / благонамеренный тупик / шаг» — статусы прогресса.

{

Элементы (L1$+$P4). Конкретные выражения, прогоны eval_fuel $n$, значения. Не элемент: бесконечная завершённая цепь редукций — role-limit, финитизируемый горючим.}

Компонент	Что фиксирует	E/R/R-категория
шаг $e\to e^{\prime }$; eval_fuel $n$; сохранение$+$прогресс	конституцию и безопасность бега	Правило (L5)
тип как роль; проверка типов; статусы прогресса	роли и критерий	Роль (L4)
выражения; прогоны eval_fuel $n$; значения	конечно-актуальные носители	Элемент (L1$+$P4)

Диагностика P4. Горючее — явная финитизация: бесконечная цепь $\to$ конечный прогон; типобезопасность — гарантия, что финитизация осмысленна (не застрянет, не парадоксальна). Это положительная сторона границы: разрешимое$=$финитизируемое.

Что глава подготовила. Типизированная оценка предъявлена как ещё одно лицо положительной стороны: сохранение$+$прогресс$+$горючее$=$безопасный конечный прогон; всё машинно и 0-аксиомно (результат стандартен, наш угол — P4-финитизация). Дальше — глава 15.6: сложность как цена — когда вычисление возможно и безопасно, остаётся его стоимость; а финал 15.7 сведёт обе master-структуры воедино: диагональ $\oplus$ дискриминант — одна граница финитизации.

---

---

Часть: Часть XV. Вычисления и граница финитизации · Том: «Математика»

Понятия: Парадокс

Навигация: ← Глава 4. Один дискриминант: редукционный атлас и разрешимая сторона · Глава 6. Сложность как цена финитизации →

Footnotes

1. Машинно проверено, 0 аксиом: src/Expressions.v (тип Expr, типовое суждение), src/Reduction.v (отношение step, его детерминированность step_deterministic, и multi_step). ↩

2. Машинно проверено, 0 аксиом: src/SubjectReduction.subject_reduction (сохранение типа при шаге); src/Progress.progress (значение или шаг) с is_benign_stuck (благонамеренные тупики) и no_unexpected_stuck. ↩

3. Машинно проверено, 0 аксиом: src/Reduction.v — eval_fuel, eval_fuel_terminates; src/SubjectReduction.eval_fuel_preservation (сохранение вдоль прогона); src/TypeSafety.v — type_safety и P4_ evaluation_ terminates (бег с горючим завершается через eval_fuel_terminates — P4); safety_ implies_ no_paradox в текущем файле — мостовая формулировка сохранения типа при eval_fuel (отдельный предикат «нет парадокса» не вводится); src/Evaluator.v — safe_eval / safe_eval_sound и сквозной verified_pipeline (типизация$+$оценка). ↩