Материалы курса: https://maxxk.github.io/formal-models-2015/
Нужно определиться со временем (и аудиторией) зачётов и подать их в учебную часть.
Я надеюсь, мы справимся за 2 раза (а то и за один), но нужно поставить все 3.
Слушатели не из 510 группы, которые хотят сдать спецкурс:
Контексты — список типов переменных (записывается как \(x : A, y : B\), обозначается греческими буквами \(Γ\))
Термы:
Элемент типа \(A+B\) — это или элемент типа \(A\) или элемент типа \(B\).
Элемент типа \(A × B\) — это пара из элемента типа \(A\) и элемента типа \(B\)
Luo, 1989. Extended Calculus of Constructions
Элемент типа \(Σ(x : A).B(x)\) — это пара из элемента \(a\) типа \(A\) и элемента \(b_a\) типа \(B(a)\).
| Логика | Исчисление конструкций |
|---|---|
| «и» A ∧ B | ΣA.B |
| «или» A ∨ B | A + B |
| A → B | ΠA.B |
| «не» A | #0 или ΠC.A.C |
| ∀a.P(a) | Π(a : A).P(a) |
| ∃a.P(a) | Σ(a : A).P(a) |
«Конструктивность» логики — все доказательства представляют собой эффективные вычисления, все правила вывода тоже возвращают вычисление. Например, оператор \(π_1\) для зависимой суммы/квантора существования вернёт тот самый \(x\), для которого верно \(P(x)\).
Разновидности исчисления конструкций, правила вывода которых задаются с помощью суждения типизации «x : A» называют теориями типов.
Есть понятие теорий подтипов, в которых вводится понятие отношения вложения типов \(X <: Y\) и правило включения \(\dfrac{Γ ⊦ x : X, \qquad X <: Y}{Γ ⊦ x : Y}\), но у них есть сложности с нормализацией.
\(\mathbf{Type}\) — универсум («тип всех типов»), в общем случаи такие конструкции опасны, т.к. позволяют определить парадоксы.
Самое опасное — это рекурсивное включение универсумов, которое мы дали в первом правиле редукции сегодняшней лекции: \(\mathbf{Type} : \mathbf{Type}\). Оно делает противоречивым даже System F\({}_ω\) — полиморфное λ-исчисление с конструкторами типов.
2^S ≡ Pow ≡ λ (S : Type). Π S . Type
Univ ≡ Π (X : Type). (Π (Π 2^{2^X} . X). 2^{2^X})
PPUniv ≡ 2^{2^Univ}
τ ≡ λ (t : PPUniv) (X : Type) (f : Π 2^{2^X} . X ) (p : 2^X ) .
t · (λ (x : Univ) . (p (f ((x X) f))))
σ ≡ λ (s : Univ) . ((s · Univ) (λ (t : PPUniv) . τ · t))
Δ ≡ λ (y : Univ) . (Π (Π (p : (Pow Univ)). (σ y p) (p (τ (σ y)))) #0)
Ω ≡ (τ · (λ (p : 2^Univ)) · (Π (x : Univ). (σ · x · p) · (p · x)))
False ≡ (λ (O : (Π (p : 2^Univ) (Π (x : Univ) . (σ · x · p) · (p · x)) (p · Ω) )).
(((O Δ) (λ (x : Univ) (t : σ x Δ) (u : (Π (p : (Pow Univ)). (σ y p) (p (τ (σ y))))).
(u · (λ (y : Univ)) (p (τ (σ y)))))))
· (λ (p : 2^Univ) . (O (λ (y : Univ) . p (τ (σ y)))))
· (λ (p : 2^Univ). (v : (Π (x : Univ). (σ x p) (p x))).
(v · Ω) · (λ (x : Univ) . (v · (τ (σ x))))))
False : #0Для того, чтобы избежать таких парадоксов, рассматривают не один универсум \(\mathbf{Type} : \mathbf{Type}\), а их набор \(\mathbf{Type}_i\), где \(i\) — какой-то набор индексов с заданным строгим порядком \(<\) (обычно используется что-то вроде решётки, чтобы у любой пары индексов был максимальный \(\max\), нестрого больший \(i, j ⩽ \max(i,j))\).
Тогда правило типизации универсума преобразуется к следующему виду: \(\dfrac{i < j}{\mathbf{Type}_i : \mathbf{Type}_j}\),
А правила типизации зависимой суммы и произведения — к виду:
$ \dfrac{Γ ⊦ A : \mathbf{Type}_i \qquad Γ, x : A ⊦ B(x) : \mathbf{Type}_j}{Γ ⊦ Π(x : A).B(x) : \mathbf{Type}_k, [i, j ⩽ k]} $
При проверке типов индексы строятся в виде ориентированного графа, рёбра которого помечены \(<\) и \(⩽\), а потом, например, алгоритмом Тарьяна, определяется, можно ли получить на основе этого графа требуемый порядок (можно, если нет ориентированного цикла с одним из рёбер, помеченных \(<\))
http://wiki.portal.chalmers.se/agda/pmwiki.php
http://proofweb.cs.ru.nl/
Proof Assistant, выбрать Coq, Guest Login
Задача 7.1* Определить \(π_{1,2}\) через \(\mathrm{split}\).
Задача 7.2** Реализовать сортировку списка натуральных чисел в Coq.
Задача 7.3** Сформулировать одну из «больших» теорем математических курсов (мат. анализ, алгебра и т.п.) в Coq