Перейти к основному содержимому

CIC как извлечение

Статус​

[Т-набр] — детали .

Обзор​

CIC (Calculus of Inductive Constructions) — мощное зависимое теория типов, основа Coq. Разработана Coquand-Huet (1988+), расширяется для Lean 4. В Diakrisis: α_CIC.

Значение CIC​

  • Основа proof-assistants: Coq, Lean 4 (частично), Matita.
  • Вычислительная мощь: тотальное programmming + доказательство.
  • Индуктивные типы: элегантное определение структур.
  • Консистентность: доказана (Werner 1994).

α_CIC​

ν_{α_CIC} = ω + 2.

Почему ω+2​

  • ω: базовые типы + функциональные.
  • +1: зависимые типы (Π, Σ).
  • +1: вычислительные правила + индуктивные типы.
  • Итог ω+2.

Конструкция α_CIC​

  • Ob(α_CIC): типы CIC.
  • Hom(A, B): функции A → B (зависимые).
  • 2-морфизмы: definitional equalities (β, ι, δ).
  • α_math: выделенный universe (Type_0 в Coq).

Структурные инварианты​

  • Зависимые типы (Π, Σ, W).
  • Вычислительные правила (β, ι, δ-редукции).
  • Индуктивные типы.
  • Импредикативный Prop.
  • Иерархия универсумов.

Детализация​

Зависимые типы:

  • Π(x:A). B(x) — зависимые функции.
  • Σ(x:A). B(x) — зависимые пары.
  • W(x:A). B(x) — W-типы (inductive well-founded).

Вычислительные правила:

  • β: (λx.t) u ↝ t[x := u] (beta-редукция).
  • ι: case analysis for inductive types.
  • δ: definitional expansion.
  • Все редукции — strongly normalizing.

Индуктивные типы:

  • Nat: 0 | S(n).
  • List A: nil | cons(a, l).
  • Tree: leaf | node(l, r).
  • Vector A n: зависимый от n.

Импредикативный Prop:

  • Propositions как тип (пропозициональная irrelevance).
  • ∀ X : Prop, ... — квантификация по всем Prop.
  • Отличие от HoTT, где Prop — n=-1 усечение.

Иерархия универсумов:

  • Prop : Type_0.
  • Type_0 : Type_1.
  • Type_1 : Type_2.
  • ...
  • Universe cumulativity: Type_i ≤ Type_{i+1}.

Индуктивные типы = инициальные алгебры​

06.T3: CIC-индуктивный тип T соответствует инициальной F-алгебре эндо-функтора.

Пример: Nat = инициальная (0, S)-алгебра = α_Nat.

Детализация​

Индуктивный тип Nat:

  • Constructors: 0, S.
  • Functor F: F(X) = 1 + X (one point or successor).
  • Initial F-algebra: Nat с структурой (0: 1 → Nat, S: Nat → Nat).

В Diakrisis:

  • α_Nat = соответствующий объект в ⟪⟫.
  • Инициальная алгебра = неподвижная точка 𝖬_F для F-endofunctor.
  • Путь Nat — часть Trace(𝖠).

Общая теория​

Для любого полиномиального функтора F:

  • Инициальная F-algebra = μF (наименьшая неподвижная точка).
  • CIC допускает μF как inductive type.

В Diakrisis: соответствует 12.T1 (существование A_init).

Strong normalization = 𝖬-монотонность​

06.C3: CIC strong normalization = монотонность 𝖬-H (H — артикуляционная энтропия, из 27 каркас).

Strong normalization​

SN: каждая редукция CIC-term завершается в normal form за конечное число шагов.

  • Следствие: CIC — консистентна (нет ⊥ доказуемости).
  • Доказано Werner (1994), Barras et al. (1999).

Соответствие в Diakrisis​

  • 𝖬-монотонность: применение 𝖬 не увеличивает «энтропию» артикуляции.
  • H-функция: мера «сложности» артикуляции.
  • Соответствие: SN в CIC = монотонность 𝖬 в α_CIC.

Это — частная форма общего принципа: вычислительная термина — в итеративных 𝖬-свойствах.

Coq / Lean — gauge-эквивалентные реализации​

06.C4: Coq, Lean, Agda — gauge-эквивалентные реализации α_CIC.

Детализация​

  • Coq: классическая реализация CIC.
  • Lean 4: CIC + дополнения (impredicative Prop, quotients).
  • Agda: MLTT с pattern matching + HITs.

Все — в одном gauge-классе в 𝓜_Fnd при подходящих настройках.

Отличия (внутри gauge-класса)​

  • Синтаксис: Coq — классический, Lean — современный.
  • Тактики: различные стратегии доказательства.
  • Library: Coq Standard Library, Lean mathlib, Agda stdlib.

Эти отличия — gauge-trivial: структурно эквивалентны.

Verum-связь​

06.C5: Verum-формализация Diakrisis через α_CIC + УГМ-расширение.

Роль Verum​

  • Verum — специализированный прувер для УГМ.
  • На основе CIC-подобной теории типов.
  • С дополнениями для quantum-specific конструкций.

В Diakrisis​

  • α_verum — специфическая gauge-версия α_CIC.
  • Содержит УГМ-расширения: CPTP-каналы, плотностные матрицы, 7D структуры.
  • Путь Б — реализация этого.

CIC ≠ HoTT​

α_CIC и α_HoTT — параллельные ветви Trace(𝖠). Не сравнимы по ⊏_0 напрямую.

Cubical HoTT — гибрид.

Детализация различий​

СвойствоCICHoTT
Identity typeβ-reducingpath type
Унивалентностьотсутствуетаксиома
Quotient typesчерез setoidsnative (HITs)
Computationalтотальноечастично (cubical)
Universecumulativenon-cumulative

В 𝓜_Fnd​

  • [α_CIC] и [α_HoTT] — разные точки.
  • Путь между ними: через переформулировки (не прямой gauge).
  • Cubical HoTT: промежуточная точка (CIC-подобная вычислительность + HoTT-структура).

Признанные редукции​

  • Стандартная Coquand-Huet CIC.
  • Известно.

Источники​

  • Coquand-Huet (1988): Calculus of Constructions.
  • Coquand-Paulin (1990): Inductive types.
  • Werner (1994): SN proof.
  • Мартин-Лёф (1984): ITT (предок CIC).
  • Coq development team (1984+): Coq system.
  • Lean 4 (2021+): Modern CIC реализация.

Специфика α_CIC в Diakrisis​

Вычислительность​

CIC — тотально вычислима. В Diakrisis:

  • ρ(α_CIC) имеет вычислительную структуру.
  • Переводы между артикуляциями — алгоритмичны.
  • Прямо применимо к Verum.

Связь с logic programming​

  • Через Curry-Howard: types как пропозиции.
  • CIC как логика: impredicative + inductive.
  • Гибкость: можно выражать как конструктивные, так и классические теории.

Путь к HoTT​

  • MLTT + univalence = HoTT.
  • CIC + modification = Cubical HoTT.
  • Переходы — хорошо изучены.

Применение в Diakrisis​

Как основа Пути Б​

  • Verum базируется на CIC-подобной теории.
  • Все УГМ-теоремы должны быть выразимы в α_CIC-расширении.

Как reference для вычислительной математики​

  • α_CIC — идеал вычислительного основания.
  • Сравнение других оснований с α_CIC показывает их вычислительную мощь.

Ограничения​

  • CIC — уровень 5 (как и все другие).
  • Не выражает AFN-T напрямую (мета-утверждение).
  • Формализация Diakrisis в CIC — частичная (мета-уровень вне CIC).

Следующий документ​

/04-extractions/06-logics-catalog.