Топосы и логика

Типы в Rust - это логические утверждения. Компилятор - это proof checker. Каждая программа, прошедшая компиляцию - это математическое доказательство. Соответствие Карри-Говарда-Ламбека - одна из самых удивительных связей в математике.

• Coq и Agda: программирование = доказательство теорем
• Rust borrow checker: проверка утверждений о времени жизни
• Isabelle/HOL: формальная верификация критического ПО
• Lean 4: математические теоремы как программы на ML-языке

Subobject Classifier: категориальная истина

**Subobject classifier** Ω - объект, представляющий «истину» в категории. В Set: Ω = {true, false}. Для каждого подобъекта A ⊆ B существует характеристическая функция χ_A: B → Ω.

**Интуиционистская логика:** В общих топосах Ω - не булева решётка, а решётка Гейтинга. Это означает, что закон исключённого третьего (P ∨ ¬P) не выполняется! Геометрические топосы (пучки на топологических пространствах) - ключевой пример.

Топос: категория с геометрией и логикой

**Топос** - категория, обладающая всеми конечными пределами, экспоненциальными объектами и subobject classifier Ω. Топосы - «обобщённые множества», в которых можно заниматься математикой.

**Hask не является настоящим топосом:** Из-за нестрогости (⊥ = undefined) и seq категория Hask нарушает некоторые законы. Agda и Coq дают настоящие топосы. Тем не менее, интуиция из теории топосов полезна для Haskell.

Соответствие Карри-Говарда-Ламбека

**Соответствие Карри-Говарда-Ламбека** - глубокая трёхсторонняя связь: Логика ↔ Типы ↔ Категории. Каждое доказательство = программа = морфизм.

**Coq и Agda:** В этих языках типы - это буквально математические утверждения. Написать программу типа A = доказать теорему A. Весь компилятор - это proof checker. Это прямое практическое воплощение соответствия Карри-Говарда.

Ключевые идеи

• Subobject classifier Ω: объект, представляющий истину (= Bool в Set)
• Топос: категория с пределами, экспоненциалами и Ω - обобщённые множества
• В топосе Set логика булева; в общих топосах - интуиционистская
• Карри-Говард-Ламбек: Тип = Утверждение, Программа = Доказательство, Категория = Логика
• Either = ∨, Pair = ∧, функция = ⊃ в языках с зависимыми типами

Связанные темы

Топосы объединяют геометрию, логику и типы.

• Пределы и сопряжения — Аксиомы топоса включают конечные пределы
• Монады — State monad = топосный подход к состоянию

Вопросы для размышления

• Почему в интуиционистской логике нельзя доказать ¬¬P ⊃ P без дополнительных аксиом?
• Как тип Vec n a (вектор длины n) в Agda/Idris соответствует утверждению в логике?
• Что означает высказывание «программирование - это прикладная теория доказательств»?

Связанные уроки

• ml-08
• ml-11