Типы и Логика

Дата: May 1, 2020 Автор: BeiZero
Tags: agda, соответствие Карри-Ховарда

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

Теория типов

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

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

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

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

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

R = { x | x ∉ x }

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

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

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

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

U, U₁, U₂ ...

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

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

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

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

Логические системы Языки программирования
Высказывание Тип
Доказательство высказывания P Терм (выражение) типа P
Утверждение P доказуемо Тип P обитаем
Импликация P ⇒ Q Функциональный тип P → Q
Конъюнкция P ∧ Q Тип произведения (пары) P × Q
Дизъюнкция P ∨ Q Тип суммы (размеченного объединения) P + Q
Истинная формула Единичный тип
Ложная формула Пустой тип
Квантор всеобщности ∀ Тип зависимого произведения (Π-тип)
Квантор существования ∃ Тип зависимой суммы (Σ-тип)

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

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

Для начала объявим единичный тип, это тип в котором есть всего один элемент 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 --\<=>
  1. Доказать коммутативность операторов произведения и суммы типов
×-comm : {P Q : Set}  (P × Q)(Q × P)
∣-comm : {P Q : Set}  (P ∣ Q)(Q ∣ P)
  1. Доказать ассоциативность операция произведения типов
×-assoc : { P Q R : Set }  ((P × Q) × R)(P × (Q × R))
  1. Показать, что сигма тип является обобщением типа произведения