Arithmetical Hierarchy

Программист пишет статический анализатор: 'эта программа не утекает память'. Математик спрашивает: 'это утверждение доказуемо в Peano Arithmetic?' Оба наталкиваются на арифметическую иерархию. Уровни Sigma_n и Pi_n структурируют все неразрешимые задачи: HP на первом, тотальность на втором, истинность арифметики - выше всех конечных уровней. Понимание этой иерархии объясняет что принципиально недоступно программам, теоремам и анализаторам.

• **Rust type checker** - разрешает Pi_2-подобный вопрос о lifetime'ах через консервативное приближение; отклоняет некоторые валидные программы именно для того чтобы оставаться в Sigma_1 (полуразрешимо, завершается)
• **Coq theorem prover** - пользователь направляет доказательство вручную для обхода неразрешимых частей; иерархия объясняет где нужна ручная работа vs автоматика
• **Model checkers (SPIN, TLA+)** - проверяют Pi_1-свойства (всегда выполняется условие) на конечных моделях; бесконечные системы требуют абстракцию - выход за Sigma_1 неизбежен

Sigma_n классы

Задача 'M останавливается на w' (HP) описывается: существует t такое что M останавливается за t шагов. Один квантор существования -> Sigma_1. Задача 'M останавливается на ВСЕХ входах': для всех w, существует t такое что M останавливается на w за t шагов. Два кванторы (для всех, затем существует) -> Pi_2. Количество чередующихся кванторов определяет уровень иерархии.

**Sigma_n**: формула вида ∃x1 ∀x2 ∃x3 ... Q(x1,...,xn, e) где Q разрешимо, начинается с ∃, n чередований. **Пример**: Sigma_1 = RE = {A | ∃t [M_A симулирует и принимает за t шагов]}. Sigma_0 = разрешимые. Каждый Sigma_n содержится в Sigma_{n+1} строго.

Pi_n классы и дополнение

Sigma_n и Pi_n симметричны: Pi_n = дополнение Sigma_n (в смысле начального кванторa). Задача пустого языка МТ E_TM: 'для всех w, M не принимает w' - начинается с ∀, значит Pi_1. Это co-RE задача (неразрешима, не полуразрешима).

**Pi_n**: формула начинается с ∀, n чередований. Соотношения: A ∈ Sigma_n <=> complement(A) ∈ Pi_n. A ∈ Sigma_n ∩ Pi_n <=> A ∈ Delta_n (Turing-reducible к Sigma_{n-1}-complete проблеме). Delta_1 = разрешимые. Delta_2 = задачи решаемые с HP-оракулом.

Оракульные машины Тьюринга

Арифметическая иерархия может быть определена альтернативно через оракульные машины. Sigma_2 = задачи разрешимые машиной с HP-оракулом = задачи разрешимые если бы HP была разрешима. Это связывает структурную (кванторную) и вычислительную (оракульную) точки зрения.

**Оракульная МТ M^A**: обычная МТ + специальная лента для запросов к оракулу A. За один шаг: записать запрос на ленту, перейти в oracle state, оракул отвечает ∈A или ∉A. **Теорема**: Sigma_n = RE^{Sigma_{n-1}} (RE относительно Sigma_{n-1}-complete задачи). Delta_2 = {A | A <=_T HP} (Turing degree 0' - первый jump HP).

Операция Jump и степени Тьюринга

Halting Problem для оракульной машины M^A - это 'jump' множества A. Операция jump строит из любого множества A более сложное A' (A jump): задачу останова для машин с A-оракулом. Итерируя jump получаем всю арифметическую иерархию.

**Jump**: A' = {e | M_e^A останавливается на e} (A-relative halting problem). Свойства: A <_T A' (A строго легче A'); A ≡_T B => A' ≡_T B' (jump сохраняет T-степень). **Degrees**: 0 = степень разрешимых, 0' = степень HP = Delta_2 complete, 0'' = степень HP' = Sigma_2 complete, ... Иерархия: 0 < 0' < 0'' < 0''' < ...

Ключевые идеи

• **Sigma_n**: формулы с n чередующимися кванторами начиная с ∃; Sigma_1 = RE = HP; Sigma_n строго содержит Sigma_{n-1}
• **Pi_n**: начинается с ∀; Pi_1 = co-RE = E_TM; Pi_n = complement(Sigma_n)
• **Delta_n = Sigma_n ∩ Pi_n**: Delta_2 = задачи T-сводимые к HP (оракульные); Delta_1 = разрешимые
• **Jump A'**: HP для A-оракульных машин; 0 < 0' < 0'' < ... строит иерархию; 0^{(omega)} = вся арифметика первого порядка

Связанные темы

Арифметическая иерархия расширяет теорию редукций:

• Mapping Reductions — m-reduction и T-reduction - инструменты классификации задач по уровням иерархии
• Разрешимость и полуразрешимость — RE = Sigma_1 и co-RE = Pi_1 - нижние уровни иерархии

Вопросы для размышления

• Rust lifetime checker завершается для всех программ (разрешим) но отклоняет некоторые безопасные программы. Какой уровень иерархии соответствует 'идеальному' анализу владения памятью и почему Rust использует консервативное приближение?
• Model checker TLA+ проверяет свойство 'система никогда не дедлочится' для конечных моделей. Это Pi_2 свойство. При переходе к бесконечным моделям как меняется класс задачи и что использует TLA+ для обхода?
• 0^{(omega)} = все арифметические истины первого порядка. Теорема Гёделя: не все истины доказуемы в PA. Существует ли вычислительный аппарат (машина с каким оракулом) способный проверять все истины первого порядка?

Связанные уроки

• fl-01-intro