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

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

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

https://maxxk.github.io/formal-models/

Типы идентичности

Ранее для Системы Fω было дано определение типа равенства между двумя типами:
Eq = λ (α β : *). ∀ (φ : * ⇒ *). φ α → φ β

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

Формация

Γ ⊦ X : Type Γ ⊦ a, b : X
Γ ⊦ a =_X b : Type

Введение (рефлексивность)

Γ ⊦ X : Type Γ ⊦ a : X
Γ ⊦ refl a : a =_X b

Перенос вдоль идентичности

Терм зависимого удаления типа идентичности (определение C. Paulin-Möhring)

Γ ⊦ X : Type Γ ⊦ a, b : X Γ, c : X, β : a =_X c ⊦ C : Type Γ ⊦ x : C(a, refl a) Γ ⊦ α : a =_X b
Γ ⊦ J(X, a, b, α, C, x) : C(b, α)

X — тип равных элементов

a, b — равные элементы

C — «структура» переноса.

x — исходный элемент

α — равенство, вдоль которого выполняется перенос

Есть альтернативное определение, в котором C не «привязан» к точке a (определение P. Martin-Löf):
Γ, x : X, y : X, α : x =_X y ⊦ C : Type

Тип идентичности в Coq/Agda

В системах с индексированными индуктивными типами, тип идентичности можно представить как индуктивный:

Inductive eq (A:Type) (x:A) : A -> Prop :=
    eq_refl : eq A x x.

Использовать терм удаления можно двумя способами:

в явном виде с помощью конструкции match

eq_sym = fun (A : Type) (x y : A) (H : x = y) =>
  match H in (_ = y0) return (y0 = x)
  with
  | eq_refl => eq_refl
  end.

в интерактивном режиме с помощью тактики rewrite (на следующей странице)

Пример тактики rewrite в Coq

Пример из Y. Bertot. Coq in a Hurry. https://cel.archives-ouvertes.fr/inria-00001173v5/document

Require Import Coq.Arith.Mult.

Lemma example6 : forall x y, (x + y) * (x + y) = x*x + 2*x*y + y*y.
intros x y.
SearchRewrite (_ * (_ + _)).
rewrite mult_plus_distr_l.
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_r.
rewrite plus_assoc.
rewrite <- plus_assoc with (n := x * x).
rewrite mult_comm with (n:= y) (m:=x).
pattern (x * y) at 1; rewrite <- mult_1_l.
rewrite <- mult_succ_l.
rewrite mult_assoc.
reflexivity.
Qed.

Print example6.

Структура типа идентичности

Из каких элементов могут состоять типы идентичности?

Только из рефлексивности (экстензиональная теория типов)

по определению

Γ ⊦ p : a =_X b
Γ ⊦ a ≡ b

уникальность доказательств идентичности

UIP : ∀ (A : Type) (x y : A) (p q : x =_A y) . p =_x=y q

аксиома K
сильное сопоставление с образцом
функциональная экстензиональность (более слабое свойство) — поточечное равенство функций:
∀ x, f(x) =_B g(x) → f =_A→B g

Могут быть какие-то неканонические элементы (интензиональная теория типов)
Можно вывести явную структуру (наблюдательная теория типов)

Altenkirch T., McBride C., Swierstra W. Observational Equality, Now! // Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007 / ed. Stump A., Xi H. 2007. P. 57–68.

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

— развитие интензиональной теории типов, которое устанавливает соответствие между термами теории типов и объектами теории гомотопий.

Интензиональная теория типов	Гомотопическая теория типов
тип A	топологическое пространство A
терм a	точка a
суждение a : A	a ∈ A
Π(x : A).B(x)	расслоение B → A
тип идентичности p : a =_A b	путь p : a ↦ b
α : p =_a=b q	гомотопия α : p ⇒ q

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

Понятие эквивалентных типов:

f : A → B g : B → A

f(g(y)) =_A y g(f(x)) =_A x (при условии функциональной экстензиональности)

Из идентичности следует эквивалентность:

IdEq : (A = B) → Equiv(A, B)

Аксиома унивалентности утверждает, что идентичность эквивалентна эквивалентности:

Equiv(A=B, Equiv(A, B))

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

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

h-уровни типов

— уровень, определяющий, насколько сложную структуру имеет тип идентичности для элементов данного типа.

«Утверждения» — «-1» h-уровень (все элементы-доказательства утверждений равны, пространства утверждений эквивалентны)
«Множества» — «0» h-уровень (равенство элементов множества — это утверждение, выполняется аксиома UIP)
...
«k-й» h-уровень — равенство элементов типа — это элемент типа k-1-го h-уровня.

Программирование с типами идентичности

— в некотором смысле, программирование с обобщёнными типами.

список List A с двумя конструкторами (Nil, Cons) эквивалентен вектору с известной длиной Σ(length : ℕ).Vec A length. С использованием аксиомы унивалентности можно получить реализации произвольных функций для вектора из таких реализаций для списка простым применением терма переноса вдоль идентичности.
доказуемо корректное параллельное программирование с ассоциативностью:

reduce F t₀ [t₁, t₂, t₃, t₄]

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

— типы, в которых можно задавать конструкторы не только для элементов, но и для других типов идентичности.

Система контроля версий как высший индуктивный тип

Angiuli C. et al. Homotopical patch theory // Proceedings of the 19th ACM SIGPLAN international conference on Functional programming. ACM, 2014. P. 243–256.

Теория категорий

— раздел математики, изучающий свойства и отношения между математическими объектами, не зависящие от внутренней структуры объектов.

https://maxxk.github.io/formal-models-2015/

F. William Lawvere, Stephen H. Schaunel. Conceptual Mathematics: A first introduction to categories. Cambridge University Press, 1997. 358 P.

Категория

Примеры категорий

Коммутативная диаграмма

Функтор

Инициальность и терминальность

F-алгебры

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

Дуализм

Произведение и сумма

Высшие категории и гомотопическая теория типов

Литература

Homotopy Type Theory: Univalent Foundations of Mathematics. — Princeton: Institute for Advanced Study, 2013. — 603 p. https://homotopytypetheory.org/book/
F. William Lawvere, Stephen H. Schanuel. Conceptual Mathematics: A First Introduction to Categories. Cambridge University Press — 1997. — 374 p.

Задачи

Задача 10.1 *: Построить термы, соответствующие доказательствам свойств симметричности и транзитивности равенства с использованием терма зависимого удаления типов идентичности J.
Задача 10.2 *: Построить терм IdEq, преобразующий идентичность в эквивалентность.
Задача 10.3 ***: Предложить другие возможные приложения высших индуктивных типов в программировании (требования аналогично задаче 9.1).

За «1*» принимаются решения упражнений из книги Homotopy Type Theory, начиная со второй главы.

PLAY