Типы и Логика

Это текстовая версия видео-лекции с нашего канала.

Теория типов

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

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

Теории типов изначально возникли как альтернатива теории множеств из-за некоторых противоречивых ситуаций, которые появляются в наивной теории множеств при рассмотрении некоторых определений множеств.

Парадокс Рассела

Наиболее важным примером является парадокс Рассела рассматривающий множество всех множеств, которые не содержат самих себя

R = { x | x ∉ x }

Ясно, что это множество содержит само себя тогда и только тогда, когда оно не содержит само себя, что является противоречием.

Эта проблема в математике классически решается аксиоматизацией теории множеств(система Цермело — Френкеля или система фон Неймана — Бернайса — Гёделя) либо ограничивающей создание множеств из произвольных элементов либо вводя дополнительную сущность “класс” как замену множеству множеств, но эта проблема может быть решена и с помощью теории типов благодаря классификации объектов.

Вселенные типов

Как я уже говорил в системе типов Agda и во многих других решается с помощью иерархии типов

U, U₁, U₂ ...

и Uᵢ : Uᵢ₊₁ для любого i. Таким образом у нас не существует типа “универсума” содержащего все типы, сущности которая и приводит к противоречиям, но мы можем рассуждать в терминах “вселенных” рассматривая элементы на различных уровнях

Соответствие Карри — Ховарда

Соответствие Карри — Ховарда это наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями.

Названо оно так в честь Хаскелла Карри и Уильяма Ховарда, которые как раз и заметили, что построение конструктивных доказательств схожи с описанием вычислений, а высказывания конструктивной логики схожи с типами вычисляемых выражений.

Аксиомы интуиционистской логики

В рамках данной лекции я хочу показать выполнение аксиом интуиционисткой логики. Интуиционисткая логика отличается от классической отсутствием аксиомы исключённого третьего и таким образом все доказательства являются конструктивными, т.е., например, для доказательства существования какого-либо объекта нужно его предоставить или сконструировать, в отличии от классической логики в которой можно обосновать существование объекта показав, что его не может не существовать.

Для начала объявим единичный тип, это тип в котором есть всего один элемент tt и по соответствию Карри-Ховарда он эквивалентен true.

data ⊤ : Set where --\top
  tt : ⊤

так же объявим пустой тип, который так же называется дном, как тип без конструкторов

data ⊥ : Set where --\bot

и определим для него элиминатор позволяющий выводить любое утверждение из пустого типа

⊥-elim : {A : Set} → ⊥ → A
⊥-elim = λ () --\lambda или \Gl

() позволяет сказать Agda, что данная ситуация является невозможной т.е. не существует элемента для которой её можно вызвать.

Импликации ⇒ в Agda соответствует функциональный тип →. Покажем, что это в точности одно и то же:

implies₁ : ⊤ → ⊤
implies₁ x = x

implies₂ : ⊥ → ⊥
implies₂ x = x

implies₃ : ⊥ → ⊤
implies₃ x = ⊥-elim x

implies₄ : ⊤ → ⊥
implies₄ x = ?

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

Ещё несколько примеров для функционального типа как импликации:

proof₁ : {A : Set} → A → A
proof₁ a = a

что можно прочитать как “из А следует А” или “из существования терма типа А следует существование терма типа А”. А вот “из А следует B” ложное утверждение терм такого такого типа мы составить не можем:

!proof : {A B : Set} → A → B
!proof = ?

Так же можем доказать, что из А следует то, что из B следует B.

proof₂ : {A B : Set} → A → (B → B)
proof₂ _ = λ x → x

и

proof₃ : {P Q R : Set} → (P → Q → R) → (P → Q) → P → R
proof₃ f g x = (f x)(g x)

Теперь можем показать, что выполняется первая и вторая аксиомы интуиционисткого искчисления высказываний.

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)

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

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

data _×_ (A : Set) (B : Set) : Set where --\x
    <_,_> : A → B → (A × B)

и теперь уже можем показать выполнение следующих трёх аксиом:

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

для следующих аксиом нужна дизьюнкция, поэтому сначала нужно определить тип суммы

data _∣_ (A B : Set) : Set where
   Left : A → A ∣ B
   Right : A → A ∣ 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

введём отрицание

¬ : Set → Set -- for ¬ type \neg
¬ A = A → ⊥

и последние две аксиомы интуиционисткого исчисления высказываний

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)

Так же можем показать выполнение двух аксиом расширяющих систему до интуиционисткого исчисления предикатов:

axiom₁₁ : {A : Set}{P : A → Set}((a : A) → P a) → (a₁ : A) → P a₁
axiom₁₁ f = f

где 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

Фактически тип зависимой суммы это пара в которой тип второго элемента зависит от значения первого. Ну и квантор существования это в точности Сигма тип т.к. для его конструирования нам нужно предоставить как предикат так и хотя бы один элемент для которого этот предикат истинен.

Необходимо обратить внимание, что может возникнуть путаница т.к. тип зависимой суммы является обобщением типа произведения, а тип зависимого произведения является обобщением типа суммы. Почему так получается я расскажу когда будем более подробно обсуждать Пи и Сигма типы.

Ну и последняя аксиома это просто определение квантора существования:

axiom₁₂ : (A : Set) → (P : A → Set) → Set
axiom₁₂ = ∃

Упражнения

В качестве упражнений предлгаю:

1. Реализовать логическую операцию эквивалентности

 _⇔_ : Set → Set → Set --\<=>

2. Доказать коммутативность операторов произведения и суммы типов

×-comm : {P Q : Set} → (P × Q) ⇔ (Q × P)
∣-comm : {P Q : Set} → (P ∣ Q) ⇔ (Q ∣ P)

3. Доказать ассоциативность операция произведения типов

×-assoc : { P Q R : Set } → ((P × Q) × R) ⇔ (P × (Q × R))

4. Показать, что сигма тип является обобщением типа произведения