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

Общие понятия теории категорий

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

Правила итерации и индукции

Коиндуктивные типы

Альтернатива Тьюринг-полноте — завершимость и продуктивность

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

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

Осталось 3 занятия — 1.12, 8.12, 15.12.

Предварительный список литературы курса — на сайте

Как мы говорили ранее, \(A × B\) — это частный случай \(ΣA.B\), а $ A → B$ — частный случай \(ΠA.B\), поэтому далее будем использовать и те, и другие обозначения. Для терма приложения, если это уместно, можем использовать \(A(x, y, z)\) как \(A · x · y · z\).

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

— достаточно новая область математики, которая используется для описания абстрактных математических структур (близка к алгебраической топологии).
«наука о стрелочках»
Определение. Категория \(\mathcal{C}\) состоит из следующих частей:

  • класса (набора) объектов \(\mathrm{Ob}(\mathcal{C})\)
  • класса морфизмов (стрелок) между объектами \(\mathrm{Hom}_\mathcal{C}(a, b)\) с равенством; пример записи: стрелка \(f : a → b\) из \(a\) в \(b\)
  • оператора композиции (∘): для любых \(f : a → b\), \(g : b → c\), существует стрелка \(g ∘ f : a → c\).
    При этом оператор композиции должен обладать свойствами:
  • ассоциативность: \(h ∘ (g ∘ f) = (h ∘ g) ∘ f\)
  • существование единицы: для любого объекта \(x\) существует единичный морфизм \(1_x : x → x\), нейтральный для композиции \(1_x ∘ f = f\), \(g ∘ 1_x = g\).

С. Маклейн. Категории для работающего математика. М.:Физматлит, 2004.

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

Примеры

Самый простой пример — категория множеств \(\mathrm{Set}\), объекты которой — множества, а морфизмы — функции между множествами.
Пример посложнее — направленный граф (объекты — вершины, стрелки — рёбра и единичные стрелки-циклы у вершин).

Определения (и доказательства) в теории категорий часто используют коммутативные диаграммы — направленные графы с вершинами-объектами и рёбрами-морфизмами:

\[ \require{AMScd} \begin{CD} F(X) @>F(i)>> F(F(X)) \\ @VαVV @VVF(α)V \\ X @>>i> F(X) \end{CD} \]

«Диаграмма коммутирует» означает, что при любом выбранном начальном и конечном объекте, для всех путей композиции составляющих их морфизмов равны.

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

инициальный объект
такой объект \(I\), из которого выходят морфизмы в любой объект категории (единственные для каждого объекта — ∀X ∃! f : I → X)
терминальный (финальный) объект
такой объект \(F\), в который входят морфизмы из любого объекта категории (единственные для каждого объекта — ∀X ∃! g : X → F)

caption

caption

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

функтор

отображение между категориями \(\mathcal{C}\) и \(\mathcal{D}\), такое, что:

  • каждому объекту \(X ∈ \mathrm{Ob}(\mathcal{C})\) сопоставляется \(F(X) ∈ \mathrm{Ob}(\mathcal{D})\)
  • каждому морфизму \(f : X → Y ∈ \mathrm{Hom}(\mathcal{C})\) сопоставляется \(F(f) : F(X) → F(Y)\)
  • сохраняется идентичность и композиция морфизмов
эндофунктор
функтор из категории \(\mathcal{C}\) в себя (\(F : \mathcal{C} → \mathcal{C}\))
\(F\)-алгебра
для эндофунктора \(F\) — пара \((A, α)\), где \(A\) — объект, \(α : F(A) → A\)

\(F\)-алгебры образуют категорию с морфизмами \(f\) для \(F\)-алгебр \((A, α)\) и \((B, β)\) (гомоморфизмами):
\[ \require{AMScd} \begin{CD} F(A) @>α>> A \\ @VF(f)VV @VVfV \\ F(B) @>β>> B \end{CD} \]

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

Мотивация: хочется работать с объектами произвольного размера и задавать функции на них индуктивно по их структуре.

Примеры

Натуральные числа
тип \(ℕ\), с двумя конструкторами \(\mathbb{0}\) и \(\mathbb{S}(k : ℕ)\) (следующее за данным; \(\mathbb{S}(k) ≡ k+1\))
простое удаление (итерация): \[\mathrm{iter}_ℕ(T : 𝐓𝐲𝐩𝐞, c_\mathbb{0} : T, c_\mathbb{S} : T → T, n : ℕ) : T\]
зависимое удаление (индукция): \[\mathrm{ind}_ℕ(T : ℕ → 𝐓𝐲𝐩𝐞, c_\mathbb{0} : T(\mathbb{0}), c_\mathbb{S} : Π(n : ℕ).T(n) → T(\mathbb{S}(n)), n : ℕ) : T(n)\]

редукция:

  • \(\mathrm{ind}_ℕ(…, \mathbb{0}) ⟶ c_\mathbb{0}\)
  • \(\mathrm{ind}_ℕ(…, k+1) ⟶ c_\mathbb{S}(k, \mathrm{ind}_ℕ(..., k))\)

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

Контрпример

Не-индуктивный тип на основе натуральных чисел
тип булевых (#2) векторов заданного размера \(BVector : ℕ → 𝐓𝐲𝐩𝐞\)
определяется через итерацию:
\[ \begin{array}{l} BVector (elements : ℕ) ≡ \\ \qquad \mathrm{ind}_ℕ(𝐓𝐲𝐩𝐞, c_\mathbb{0} ≡ \#1, c_\mathbb{S} ≡ λ(n : ℕ).(v : BVector(n). \#2 × BVector(n)), elements) \end{array} \]

прототип функции, которая требует непустой вектор:
(существует \(n : ℕ\), для которого длина вектора — \(ℕ+1\))

negateVector : Π(n : ℕ).BVector(n+1) → BVector(n+1)

прототип функции, которая требует два вектора одинакового размера:

andVector : Π(n : ℕ).BVector(n) → BVector(n) → BVector(n)

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

Примеры

Список из элементов типа \(A\)
тип \(\mathrm{List}(A)\) с двумя конструкторами \(\mathrm{nil}_A\) (пустой список, \([]\)) и \(\mathrm{cons}_A(h : A, t : \mathrm{List}(A))\) (\([h, t]\))
простое удаление (reduce, fold): \[ \mathrm{iter}_\mathrm{List}(T : 𝐓𝐲𝐩𝐞, c_\mathrm{nil} : T, c_\mathrm{cons} : T → A → T, l : \mathrm{List}(A)) : T \]
Формула алгебры логики

тип \(\mathrm{Formula}\) с конструкторами:

  • var(x : Nat), const(x : #2)
  • not(x : Formula)
  • or(x, y : Formula), and(x, y : Formula)
Противоречивый индуктивный тип
тип Bad с двумя конструкторами nothing : #1 и fn : Bad → #1
противоречивый терм:
\[ ω = \mathrm{iter}_{Bad}(\#1, c_\mathrm{nothing} = 0\#1, c_\mathrm{fn} = λ(t : Bad → \#1). t · \mathrm{fn}(t), \mathrm{fn}(λ(t: Bad). 0\#1) ) \]

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

Первое определение

Рассмотрим категорию типов Исчисления Конструкций \(\mathbf{Type}\) с морфизмами — функциями между ними.

Индуктивным типом на основе эндофунктора \(F : 𝐓𝐲𝐩𝐞 → 𝐓𝐲𝐩𝐞\) назовём инициальный объект F-алгебры \(μF : 𝐓𝐲𝐩𝐞\).

Для рассмотренных примеров эндофункторы:

  • \(F_ℕ ≡ λ(N : 𝐓𝐲𝐩𝐞). 1 + N\)
  • \(F_\mathrm{List} ≡ λ(A : 𝐓𝐲𝐩𝐞). λ(L : 𝐓𝐲𝐩𝐞). 1 + A × L\)
  • \(F_\mathrm{Formula} ≡ λ(F : 𝐓𝐲𝐩𝐞). ℕ + \#2 + (F × F) + (F × F) + F\)
  • $F_{Bad} ≡ λ(B : 𝐓𝐲𝐩𝐞) . 1 + (B → 1)

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

Теоретико-категориальная семантика

Алгебра — это пара из объекта и морфизма.
Объект μF — это индуктивный тип.
Морфизм α — это набор термов введения объекта.

Инициальность — наличие гомоморфизмов к любым типам — определяет терм простого удаления. Пример на натуральных числах:
\[ \require{AMScd} \begin{CD} 1+ℕ @>α>> ℕ \\ @VF(f)VV @VVfV \\ 1+T @>β>> T \end{CD} \]
∀ T, (1 + T) → T ⇒ ℕ → T

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

«Идеальный» терм удаления выглядит следующим образом (но не исключает противоречивые термы как в примере ранее — фактически, это чуть изменённый Y-комбинатор):

Π(T : 𝐓𝐲𝐩𝐞).(step : μF → T).F(μf) → T

step — рекурсивный вызов

Термы зависимого удаления (индукции) также имеют теоретико-категориальную семантику:

  1. Fumex C., Ghani N., Johann P. Indexed induction and coinduction, fibrationally // Algebra and Coalgebra in Computer Science. Springer, 2011. P. 176–191.
  2. Ghani N. et al. Fibred Data Types // Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 2013. P. 243–252.
  3. Препринты: http://arxiv.org/find/cs/1/au:+Ghani_N/0/1/0/all/0/1

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

Второе определение

Введём понятие «строго положительного» вхождения переменной \(X\) в терм \(τ\).

  • любое вхождение в терм без зависимых произведений (τ=X × X, τ = ΣX.#2) строго положительное, если есть зависимые произведения — смотрим на структуру.
  • для \(ΠA.B\), если \(X\) не встречается в \(A\), вхождения строго положительные
  • \(ΠX.B\) — отрицательное вхождение \(X\).
  • \(ΠA.B\) — если \(X\) встречается в \(A\) в отрицательных позициях, то его вхождение в τ положительно, но не строго положительно.

Т.е. \(X\) не должен стоять «слева» от стрелки вообще (строго положительное) или в самой левой части стрелки (положительное)

Примеры строго положительных вхождений: X × X, ℕ → X, X × (ℕ → X)
Пример нестрого положительного вхождения: (X → ℕ) → ℕ
Примеры отрицательных вхождений: X → ℕ, (X × ℕ) → X, F(X) → X, (ℕ → X) → X (?)

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

Второе определение

μF — набор конструкторов — типов, в которых переменная итерации \(X\) может встречаться только в строго положительных позициях.

Строгая положительность позволяет определить терм удаления в «идеальном» виде и не получить при этом возможность парадоксов.

Можно описать в той же теоретико-категориальной семантике, но нужно использовать нетривиальное понятие полиномиальных функторов (требует определения равенства).

  1. Paulin-Mohring C. Inductive Definitions in the System Coq - Rules and Properties // TLCA ’93 Proceedings of the International Conference on Typed Lambda Calculi and Applications. Springer-Verlag London, UK, 1993. P. 328–345.

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

Определение по неподвижным точкам

Индуктивный тип — наименьшая неподвижная точка \(F^i(⟂)\).

$⊘ → F(⊘) → F(F(⊘)) → … → F^∞(⊘) $

Определение в стиле Мендлера

В явном виде подходит только для System F_ω (т.к. требует Type : Type).

μF ≡ Π(G : 𝐓𝐲𝐩𝐞).Π(X : 𝐓𝐲𝐩𝐞).Π(step : X → G).F·X → G

Сигнатура типа задаёт итерацию на нём. Без Type : Type можно ввести μF как терм для произвольного F : 𝐓𝐲𝐩𝐞 → 𝐓𝐲𝐩𝐞, но разрешить удалять только с помощью терма Мендлера.

  1. Constable R.L., Mendler N.P. Recursive Definitions in Type Theory // Logics of Programs, Conference, Brooklyn College, June 17--19, 1985, Proceedings / ed. Parikh R. 1985. Vol. 193. P. 61–78.
  2. Abel A., Matthes R., Uustalu T. Iteration and coiteration schemes for higher-order and nested datatypes // Theoretical Computer Science. 2005. Vol. 333, № 1-2. P. 3–66.
  3. Ahn K.Y., Sheard T. A hierarchy of mendler style recursion combinators // ACM SIGPLAN Notices. 2011. Vol. 46, № 9. P. 234–246.

Определение с аннотацией размера

  • вводим ординалы ord
  • рассматриваем индуктивный тип в определении наименьшей неподвижной точки; терм введения увеличивает размер ($\mathbb{S} : ℕ^{(k)} → ℕ^{(k+1)} $)
  • 1.Abel A. Towards Generic Programming with Sized Types // Mathematics of Program Construction / ed. Uustalu T. Springer Berlin Heidelberg, 2006. P. 10–28.
    2.Abel A. Implementing a normalizer using sized heterogeneous types. // J. Funct. Program. 2009. № 510996. P. 1–24.

Простые расширения

Взаимно индуктивные типы

Несколько типов \(A_1, …, A_k\), определения которых могут ссылаться друг на друга.
Пример (CPDT) — типы списков с контролируемой чётностью длины:
μ(EvenList = #1 + (ℕ × OddList)
OddList = N × EvenList)

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

(индуктивные предикаты — ΠA.𝐓𝐲𝐩𝐞 для некоторого A)
Чётность (T : Πℕ.𝐓𝐲𝐩𝐞) — в форме набора конструкторов:
\[ \begin{array}{l} μ_{Πℕ.𝐓𝐲𝐩𝐞} Even = \\ \qquad even_zero : Even(\mathbb{0}) \\ \qquad even_plus_2 : Π(k : ℕ).Even(k) → Even (\mathbb{S}(\mathbb{S}(\mathbb{k}))) \end{array} \]

Коиндуктивные типы

Коиндуктивный тип — наибольшая неподвижная точка \(F^i(\#1)\), \(νF\).

Пример

поток (потенциально бесконечная последовательность)
\(\#1, ℕ × \#1, ℕ × ℕ × \#1, …, ℕ × ℕ × … × ℕ × …\)

операции:

  • удаление — взять элемент с начала потока \(νF → F(νF)\)
  • введение — сгенерировать поток по некоторым начальным данным

Коиндуктивные типы

Теоретико-категориальная семантика — дуальна индуктивным типам. Дуализм в теории категорий — все морфизмы разворачиваются. Вместо инициального объекта в категории \(F\)-алгебр — терминальный объект в категории \(F\)-коалгебр.

В стиле Мендлера:
generate : Π(G : 𝐓𝐲𝐩𝐞).Π(X : 𝐓𝐲𝐩𝐞).Π(step : G → X).G → F(X)

На уровне программ:

  • индуктивные типы — обеспечивают завершимость (termination) структурно-рекурсивных функций
  • коиндуктивные типы — обеспечивают продуктивность (productivity) структурно-рекурсивных генераторов (следующий уровень детализации объекта может быть получен за конечное число шагов)

Нетривиальные расширения

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

Одновременно определяется индуктивный тип \(U : 𝐓𝐲𝐩𝐞\) и рекурсивная функция \(T : U → 𝐓𝐲𝐩𝐞\).

  1. Forsberg F.N., Setzer A. A finite axiomatisation of inductive-inductive definitions. 2012.
  2. Ghani N. et al. Fibred Data Types // Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 2013. P. 243–252.

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

Можно ли (и с какими ограничениями) определить индуктивные/коиндуктивные типы \(μF\), где \(F : A → A\) над произвольным типом \(A\)? Ограниченным типом \(A\)?

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

Для произвольного типа \(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, ε) $

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

Задача 8.1* Записать термы зависимого удаления и правила редукции для списка, формул алгебры логики и противоречивого типа.

Задача 8.2** С помощью термов зависимого удаления реализовать (в исчислении конструкций) интерпретатор формул, который позволяет получить из окружения переменных Env : ℕ → #2 и формулы Formula результат вычисления формулы с такими переменными

  • дополнительная * — Coq

Задача 8.3** Используя дуальность индуктивных и коиндуктивных типов, записать правило удаления коиндуктивного типа, задаваемого функтором \(F\) в стиле Мендлера.