Математические модели вычислений

Ещё немного про индуктивные типы

Типы идентичности (равенства)

Интензиональное и экстензиональное равенство

«Наблюдательная теория типов»

Гомотопическая теория типов и аксиома унивалентности

Высшие индуктивные типы

Материалы курса: https://maxxk.github.io/formal-models-2015/

«По следам наших публикаций»

  1. \(\#k\) — тип из \(k\) элементов (\(\#0, \#1, \#2\) — типы ложных высказываний, истиных высказываний, булевских значений, соответственно)

  2. Реализации λ-исчисления с зависимыми типами бывают и на C++: Lean (код, презентация, видео доклада)

Индексированные индуктивные типы

На индексированных индуктивных типах можно продемонстрировать отличия двух способов определения индуктивных типов (как набор конструкторов и как неподвижную точку функтора):

\[ \begin{array}{l} μ_{Πℕ.𝐓𝐲𝐩𝐞} Even : Πℕ.𝐓𝐲𝐩𝐞 ≡ \\ \qquad even_{zero} : Even(\mathbb{0}) \\ \qquad even_{plus2} : Π(k : ℕ).Even(k) → Even (\mathbb{S}(\mathbb{S}(\mathbb{k}))) \end{array} \]
В первом случае структура типа \(Even · 2\) от нас скрыта.

\[ \begin{array}{l} Even' : Πℕ.𝐓𝐲𝐩𝐞 ≡ λ(n : ℕ).ind_ℕ(Πℕ.𝐓𝐲𝐩𝐞, c_\mathbb{0} ≡ λℕ.\#1, \\ \qquad c_\mathbb{S} ≡ λ(k : ℕ).(step_1 : Πℕ.𝐓𝐲𝐩𝐞). λ(m : ℕ).ind_ℕ(𝐓𝐲𝐩𝐞, c_\mathbb{0} ≡ \#0, \\ \qquad \qquad c_\mathbb{S} ≡ λ(k : ℕ).(step_2 : 𝐓𝐲𝐩𝐞).step_1 · k, m), n) · n \end{array} \]

Во втором случае для каждого конкретного числа \(n\) в канонической форме тип \(Even'\) вычисляется в #0 или #1.
Для некоторых индексированных типов такое преобразование из набора конструкторов в функтор затруднено (например, для типа на следующем слайде).

Индуктивные типы и сопоставление с образцом

В современных функциональных языках программирования часто используется конструкция сопоставления с образцом (pattern matching). Подробнее о конструкции в целом, наверное, в следующем семестре, пока что пример на Haskell:

interpret term context = case term of
    Var n   -> get context n
    Abs t   -> λn -> interpret t (add context n)
    App l r -> (interpret l context) (interpret r context)

Оператор простого удаления (итерации) для индуктивным типов, определённых как набор конструкторов, естественным образом представляется в виде сопоставления с образцом (образцы = конструкторы). Пример на Coq:

Fixpoint reverse lst := match lst with
| nil => nil
| cons head tail => (reverse tail) ++ head
end.

В простом случае это синтаксический сахар. Более сложные образцы не совсем повторяют структуру удаления индуктивного типа.

Индукция и сопоставление с образцом

Для зависимого удаления (индукции) простая схема сопоставления с образцом не работает. Пример — реализация функции «предыдущее натуральное число» с полной спецификацией в Coq:

pred : forall n : nat, n > 0 -> { m : nat | n = S m } :=
fun n : nat =>
match n as n0 return (n0 > 0 -> {m : nat | n0 = S m}) with
| 0 =>
    fun _H : 0 > 0 => False_rec ...
| S n' =>
    fun _H : S n' > 0 => exist (fun m : nat => S n' = S m) n' (... n _H)
end.
И соответствующий ему терм, непосредственно использующий индукцию:
pred ≡ ind_ℕ(T = λ(n : ℕ).Π(n-gt-zero : n > 0).Σ(m : ℕ).(n = m+1),
    c0 : T(0) ≡
      λ n-gt-zero . exfalso n-gt-zero T(0, n-gt-zero),
    cS : Π(k : ℕ).T(k) → T(k+1) ≡
      λ(k : ℕ) . (tk : T(k)) . (sk_gt_zero : k+1 > 0).
        pair(k, refl(k+1))
    )

Пояснения:
T(0) ⟶ (n_gt_zero : 0 > 0). Σ(m : ℕ).(0 = m+1)
T(k+1) ⟶ Π(n_gt_zero : k+1 > 0).Σ(m : ℕ).(k+1 = k+1)

Тип идентичности (равенства)

Для произвольного типа \(A\) — индексированный индуктивный тип \(Id : ΠA.A.𝐓𝐲𝐩𝐞\)
\[Id(a, b) ≡ a = b\]
Единственный конструктор — рефлексивность: \(\mathrm{refl}_A : Π(a : A).Id(a, a)\).

Терм зависимого удаления — конвертация по равенству:
\[ J(a, b : A, ε : a =_A b, C : Π(x, y : A).(δ : x =_A y).𝐓𝐲𝐩𝐞, x : C(a, a, \mathrm{refl}_A(a))) : C(a, b, ε) \]

Пример: пусть \(P : ℕ → 𝐓𝐲𝐩𝐞\) — предикат, \(p_2 : P(2)\) — доказательство предиката для 2, \(x : ℕ\) — некоторое натуральное число и \(ε : 2 =_ℕ x\) — элемент типа идентичности.

Допустим, нужно вызвать функцию \(fun : Π(y : ℕ).P(y) → ℕ\). С помощью удаления \(ε\) это можно сделать так:
\[ fun(x, J(2, x, ε, λ(x, y : ℕ).(δ : x =_ℕ y).P(y), p_2)) \]

Далее будем использовать запись:
fun(x, p_2 : ε ⇝ P(2))
В позициях, набранных полужирным, левая часть равенства заменяется на правую.

Использование типов идентичности

  1. Покажем, что ε : 0=1 — ложное высказывание:
    helper ≡ λ (n : ℕ) . iter_ℕ(𝐓𝐲𝐩𝐞, #1, #0, n)
    0#1 : helper · 0 ⟶ #1
    ε ⇝ 0#1 : helper · 0 ⟶ #0
    (λ (ε : 0=1). ε ⇝ 0#1 : helper · 0) : Π(0=1).#0

  2. Оптимизация на уровне типов:

Равенство по определению и пропозициональное равенство

Ранее мы рассматривали понятие эквивалентности термов для проверки типизации.

Термы эквивалентны, если они за конечное число редукций могут быть приведены к одному виду (с точностью до индексов уровней универсумов, которые не должны образовывать циклов с ребром «<»).

\(Id(a, b)\) — пропозициональное равенство (утверждение о равенстве)

Для любых эквивалентных термов мы можем получить доказательство пропозиционального равенства с использованием терма \(\mathrm{refl}\): (\(Id(a, b) ⟶^* Id(a, a)\), если \(b ⟶^* a\))

Если мы имеем \(ε : 2 =_ℕ x\), то это не значит, что мы можем подставлять \(x\) вместо 2 везде (можем только с использованием \(J\)-терма)

Из пропозиционального равенства нельзя получить равенство по определению.

Интензиональное и экстензиональное равенство

Интензиональная (intensional) теория типов — типы равенства могут содержать какие-то неизвестные нам элементы, не описываемые \(\mathrm{refl}_A(c)\).

Экстензиональная (extensional) теория типов — типы равенства содержат только тривиальные элементы (любой элемент \(Id_A(a, b)\) — это \(\mathrm{refl}_A(c)\) для какого-то \(c\)).
Способы наложения такого ограничения:

  1. Ввести правило редукции (с ним получить из пропозиционального равенства — равенство по определению можно):
    \[\dfrac{ε : Id_A(x, y)}{x ⩽ y}\]
    — но тогда проверка типов становится неразрешима, т.к. алгоритм проверки должен уметь проверять, выводимо ли равенство для любых пар термов.
  2. Ввести одну из дополнительных аксиом:
    • единственность доказательств равенства (uniqueness of identity proofs) — все элементы типа идентичности равны
      \[ UIP : Π(A : 𝐓𝐲𝐩𝐞).(x, y : A).(ε, δ : x =_A y).ε =_{x =_A y} δ \]
    • аксиома \(K\) (Streicher)
      \[ Π(A : 𝐓𝐲𝐩𝐞).(x : A).(P : Π(x=_Ax).𝐓𝐲𝐩𝐞).P(\mathrm{refl}_A(x)) → Π(h : x=_Ax).P(h) \]
      Расширенный Pattern Matching в Agda тоже делает теорию экстензиональной.

Интензиональная и экстензиональная теория типов

Интензиональность vs экстензиональность — внутренняя структура vs внешние проявления

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

Есть отдельное понятие функциональной экстензиональности — аксиома экстензиональности только для функций:
\[ Π(A, B : 𝐓𝐲𝐩𝐞).(f, g : ΠA.B).(Π(a : A).f(a) =_{B(a)} g(a)).f =_{ΠA.B} g \]
— функции равны, если они дают равные ответы для любых входных данных.

Наблюдательная теория типов

Observational Type Theory; McBride, Altenkirch 2006, 2007.

Основная идея: рассматривать не равенство, а приведение типов.
[S=T〉— метод получения объектов типа S из типа T.

Определяются отдельные правила для преобразования стандартных конструкторов:
\([ΠA_1.B_1 = ΠA_2.B_2 〉\)
\([ΣA_1.B_1 = ΣA_2.B_2〉\)

Недостаток — «удаление» такого типа идентичности менее выразительно, чем \(J\).
1.Altenkirch T., McBride C. Towards observational type theory. 2006.
2.Altenkirch T., McBride C., Swierstra W. Observational Equality, Now! // Proceedings of PLPV 2007. P. 57–68.

Гомотопическая теория типов

Awodey, Voevodsky; Homotopy Type Theory: The Univalent Foundations of Mathematics, 2013.

Теория типов интерпретируется в теории высших категорий. Если рассмотреть пример топологических пространств, типы идентичности — пути между двумя точками. Правило удаления J интерпретируется как перенос вдоль пути.

Гомотопическая теория типов

Типы идентичности имеют структуру группоида (определена частичная бинарная операция, которая на своей области определения удовлетворяет определению группы).
С помощью правила J можно показать, что типы идентичности удовлетворяют определению:

  • операция — композиция (транзитивность) \(ε : a = b, δ : b = c ⟹ ε ∘ δ : a = c\)
  • нейтральные элементы — рефлексивность \(refl : a=a\)
  • обратный элемент \(ε : a = b ⟶ ε^{-1} : b = a\)
  • ассоциативность, нейтральность, обратность.

Задача 9.1* Записать термы, доказывающие перечисленные выше свойства.

Аксиома унивалентности

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

$ univalence : A ~ B → A =_{𝐓𝐲𝐩𝐞} B $

Введем следующие сокращения (по книге п. 4.2 – 4.3):
$ \mathrm{linv}(f : ΠA.B) ≡ Σ(ΠA.B).ΠA.1·(f·0) =_A 0 $
$ \mathrm{rinv}(f : ΠA.B) ≡ Σ(ΠA.B).ΠB.f·(1·0) =_B 0 $
$ \mathrm{biinv}(f : ΠA.B) ≡ Σ \mathrm{linv}(f) . \mathrm{rinv}(f) $

Положим также \(id_A : ΠA.A ≡ λA.0\).

Для типов \(𝐓𝐲𝐩𝐞\) эквивалентности высших размерностей рассматриваются следующим образом:
$ A =_{𝐓𝐲𝐩𝐞} B ⇔ Σ(ΠA.B).\mathrm{biinv}(0) $

Вычислительное содержание аксиомы унивалентности

$ plus0 ≡ λ (x : ℕ). 0+x =_{Πℕ.ℕ} λ (x : ℕ) . x + 0$

$ J(Πℕ.ℕ, λ x.0+x, λ x.x+0, ℕ, 0, plus0) \not ⟶ x$

(переписывание формулы \(0+x\) по коммутативности при данном \(x+0 → x\) не приводится к \(x\)).

Варианты решения:

  1. Интерпретация в кубических множествах (cubical sets).
    Bezem M., Coquand T., Huber S. A model of type theory in cubical sets. TYPES 2013.

  2. Расширение наблюдательной теории типов.
    Моя диссертация — раздел 2.2 :) http://istina.msu.ru/dissertations/10283583/

Высшие индуктивные типы

Можно определить типы индуктивно с конструкторами не только непосредственно элементов типа, но и элементов типа идентичности на нём.

Пример из топологии:
\(Circle = base : Circle , loop : base =_{Circle} base\)

Пример:

R : Type
doc : R
_↔_@_ : (s1 s2 : String) (i : Fin n) → (doc = doc)
indep : (i ≠ j) → (s ↔ t @ i) ◦ (u ↔ v @ j)
= (u ↔ v @ i) ◦ (s ↔ t @ j)
noop : s ↔ s @ i = refl

Задачи со звёздочкой

Решение задач должно быть представлено в виде термов разновидности исчисления конструкций (с выбранными вами обозначениями для стандартных конструкторов) с индуктивными типами, в том числе — со стандартным образом определёнными натуральными числами. Можно использовать Coq.
Задача 9.2.** Определить операцию умножения на натуральных числах и показать свойства 0 и 1 через равенство.
Пример на сложении:
plus : Π(a, b : ℕ).ℕ ≡ λ(a, b : ℕ).iterℕ(ℕ, c0 ≡ b, cS ≡ λ(c : ℕ).(res : ℕ).res+1, a)
plus_zero : Π(a : ℕ).(plus(0, a) = a) ≡ λ a. refl a, т.к. plus(0, a) ≡ iterℕ(ℕ, c0≡a, cS≡…, 0) ⟶ c0 ⟶ a
zero_plus : Π(a : ℕ).(plus(a, 0) = a) — можно показать через симметричность равенства или по индукции по a (последнее можно сделать в качестве отдельной задачи на *)

(бонусная * ) Показать коммутативность и ассоциативность сложения.

Задача 9.3*** Получить представление индуктивного типа — неподвижной точки функтора через натуральные числа и высшие индуктивные типы.