Типы и Логика
Это текстовая версия видео-лекции с нашего канала.
Теория типов
Теория типов – формальная система сопровождаемая классификацией элементов с помощью типов, образующих некоторую иерархию.
Типы в программировании являются применением теории типов к конструкциям языков классификацируя различные выражения по разновидностям вычисляемых ими значений.
Теории типов изначально возникли как альтернатива теории множеств из-за некоторых противоречивых ситуаций, которые появляются в наивной теории множеств при рассмотрении некоторых определений множеств.
Парадокс Рассела
Наиболее важным примером является парадокс Рассела рассматривающий множество всех множеств, которые не содержат самих себя
R = { x | x ∉ x }
Ясно, что это множество содержит само себя тогда и только тогда, когда оно не содержит само себя, что является противоречием.
Эта проблема в математике классически решается аксиоматизацией теории множеств(система Цермело — Френкеля или система фон Неймана — Бернайса — Гёделя) либо ограничивающей создание множеств из произвольных элементов либо вводя дополнительную сущность “класс” как замену множеству множеств, но эта проблема может быть решена и с помощью теории типов благодаря классификации объектов.
Вселенные типов
Как я уже говорил в системе типов Agda и во многих других решается с помощью иерархии типов
и Uᵢ : Uᵢ₊₁
для любого i
. Таким образом у нас не существует типа “универсума” содержащего все типы, сущности которая и приводит к противоречиям, но мы можем рассуждать в терминах “вселенных” рассматривая элементы на различных уровнях
Соответствие Карри — Ховарда
Соответствие Карри — Ховарда это наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.
Названо оно так в честь Хаскелла Карри и Уильяма Ховарда, которые как раз и заметили, что построение конструктивных доказательств схожи с описанием вычислений, а высказывания конструктивной логики схожи с типами вычисляемых выражений.
Логические системы | Языки программирования |
---|---|
Высказывание | Тип |
Доказательство высказывания P | Терм (выражение) типа P |
Утверждение P доказуемо | Тип P обитаем |
Импликация P ⇒ Q | Функциональный тип P → Q |
Конъюнкция P ∧ Q | Тип произведения (пары) P × Q |
Дизъюнкция P ∨ Q | Тип суммы (размеченного объединения) P + Q |
Истинная формула | Единичный тип |
Ложная формула | Пустой тип |
Квантор всеобщности ∀ | Тип зависимого произведения (Π-тип) |
Квантор существования ∃ | Тип зависимой суммы (Σ-тип) |
Аксиомы интуиционистской логики
В рамках данной лекции я хочу показать выполнение аксиом интуиционисткой логики. Интуиционисткая логика отличается от классической отсутствием аксиомы исключённого третьего и таким образом все доказательства являются конструктивными, т.е., например, для доказательства существования какого-либо объекта нужно его предоставить или сконструировать, в отличии от классической логики в которой можно обосновать существование объекта показав, что его не может не существовать.
Для начала объявим единичный тип, это тип в котором есть всего один элемент tt
и по соответствию Карри-Ховарда он эквивалентен true
.
так же объявим пустой тип, который так же называется дном, как тип без конструкторов
и определим для него элиминатор позволяющий выводить любое утверждение из пустого типа
()
позволяет сказать Agda, что данная ситуация является невозможной т.е. не существует элемента для которой её можно вызвать.
Импликации ⇒ в Agda соответствует функциональный тип →. Покажем, что это в точности одно и то же:
implies₁ : ⊤ → ⊤
implies₁ x = x
implies₂ : ⊥ → ⊥
implies₂ x = x
implies₃ : ⊥ → ⊤
implies₃ x = ⊥-elim x
implies₄ : ⊤ → ⊥
implies₄ x = ?
а вот элемент типа ⊤ → ⊥
мы уже сконструировать не можем т.к. конструктора для ⊥ нет, что соответствует ложности данного утверждения в логике.
Ещё несколько примеров для функционального типа как импликации:
что можно прочитать как “из А следует А” или “из существования терма типа А следует существование терма типа А”. А вот “из А следует B” ложное утверждение терм такого такого типа мы составить не можем:
Так же можем доказать, что из А следует то, что из B следует B.
и
Теперь можем показать, что выполняется первая и вторая аксиомы интуиционисткого искчисления высказываний.
axiom₁ : {A B : Set} → A → (B → A)
axiom₁ a = λ _ → a
axiom₂ : {A B C : Set} → (A → B) → ((B → C) → (A → C))
axiom₂ f g h = g (f h)
Здесь большие скобочки лишние т.к. стрелочка правоассоциативная, но в оригинальной формулировке аксиомы они есть, поэтому оставим так.
Следующие три аксиомы используют коньюнкцию соответственно для того, чтобы показать их выполнение нужно определить тип пары.
и теперь уже можем показать выполнение следующих трёх аксиом:
axiom₃ : {A B : Set} → A → (B → A × B)
axiom₃ a b = < a , b >
axiom₄ : {A B : Set} → (A × B) → A
axiom₄ < a , b > = a
axiom₅ : {A B : Set} → (A × B) → B
axiom₅ < a , b > = b
для следующих аксиом нужна дизьюнкция, поэтому сначала нужно определить тип суммы
и три акиомы
axiom₆ : {A B : Set} → A → A ∣ B
axiom₆ = Left
axiom₇ : {A B : Set} → B → A ∣ B
axiom₇ = Right
axiom₈ : {A B C : Set} → (A → C) → ((B → C) → (A ∣ B → C))
axiom₈ f g (Left a) = f a
axiom₈ f g (Right b) = g b
введём отрицание
и последние две аксиомы интуиционисткого исчисления высказываний
axiom₉ : {A B : Set} → (A → B) → ((A → ¬ B) → ¬ A)
axiom₉ f g h = g h (f h)
axiom₁₀ : {A B : Set} → ¬ A → (A → B)
axiom₁₀ f a = ⊥-elim (f a)
Так же можем показать выполнение двух аксиом расширяющих систему до интуиционисткого исчисления предикатов:
где P
у нас предикат, ((a : A) → P a)
– зависимая функция, которая по элементу типу A
возвращает применение к этому элементу предиката P
и т.к. если такая функция существует, то P a
для каждого a
не пуст, по свойству функционального типа, то ((a : A) → P a)
мы можем прочитать как “для любого a
выполняется P a
”, что как раз и показывается соответствие типа зависимой функции(он же тип зависимого произведения) квантору всеобщности. В итоге получается, что “Если для любого a
предикат верен, то для a₁
он так же верен”.
для следующей аксиомы нам нужен будет квантор существования, ввести его можно через сигма-тип, тип зависимой суммы:
data Σ (A : Set) (P : A → Set) : Set where
⟨_,_⟩ : (a : A) → P a → Σ A P --\< \> \Sigma
∃ : (A : Set) → (P : A → Set) → Set --\ex
∃ A P = Σ A P
Фактически тип зависимой суммы это пара в которой тип второго элемента зависит от значения первого. Ну и квантор существования это в точности Сигма тип т.к. для его конструирования нам нужно предоставить как предикат так и хотя бы один элемент для которого этот предикат истинен.
Необходимо обратить внимание, что может возникнуть путаница т.к. тип зависимой суммы является обобщением типа произведения, а тип зависимого произведения является обобщением типа суммы. Почему так получается я расскажу когда будем более подробно обсуждать Пи и Сигма типы.
Ну и последняя аксиома это просто определение квантора существования:
Упражнения
В качестве упражнений предлгаю:
- Реализовать логическую операцию эквивалентности
- Доказать коммутативность операторов произведения и суммы типов
- Доказать ассоциативность операция произведения типов
- Показать, что сигма тип является обобщением типа произведения