Математическая логика

Теория категорий и логика

SQL-запросы, монады в Haskell и денотационная семантика языков программирования - это всё частные случаи категорной логики и топосов Гротендика. Curry-Howard-Lambek трёхсторонний изоморфизм объединяет логику, теорию типов и теорию категорий в одном языке.

  • Базы данных: SQL как исчисление реляционных алгебр - топос категории отношений
  • Haskell: монады из категорной логики, fp-ts - 3M загрузок/месяц
  • Программные языки: денотационная семантика через декартово замкнутые категории
  • Quine Labs: категорные методы для верификации распределённых систем
  • Microsoft Research: Quantomatic - категорные диаграммы для квантовых вычислений
  • Формальная лингвистика: категорные грамматики для анализа естественного языка

Топос-теория Гротендика объединяет три науки в один язык: алгебраическую геометрию (пучки), логику (внутренняя логика топоса) и теорию типов (через CCC). Денотационная семантика Haskell, монады, SQL-запросы - всё это частные случаи категорной логики. Одна идея, тысячи применений.

**О чём этот урок на самом деле:** теория категорий - это язык структур. Вместо того чтобы изучать каждую математическую структуру отдельно, категории дают единый словарь. CCC = STLC = IPC - три способа сказать одно. Топос = «вселенная математики» с выбираемой логикой.

Curry-Howard-Lambek: тройной изоморфизм

Ламбек (1969) добавил третью вершину к изоморфизму Карри-Говарда: декартово замкнутые категории. Теперь одна математическая структура описывается тремя языками: **типы = объекты, программы = морфизмы, экспоненциал B^A = тип функций A→B**. Денотационная семантика - это перевод программ в морфизмы CCC.

Топосы: примеры и их логика

Монады как алгебраические эффекты

Могги (1991) показал: вычислительные эффекты (исключения, состояние, ввод-вывод) моделируются монадами в категориях. Монада T = (T, η, μ) где η:Id→T (return), μ:T²→T (join). Законы монады = диаграммная коммутативность. Haskell IO - это монада в CCC, не специальная синтаксическая конструкция.

**Теория категорий и логика в индустрии** От математики до production-систем • **Haskell / GHC** (CCC на практике): GHC Core - System F, интерпретируемый в CCC. Монады = монады в категориях. Free monad = свободная алгебра. • **Scala / Cats** (Функториальное программирование): Cats/Scalaz реализуют категорные абстракции: Functor, Applicative, Monad, Traverse. Типы классов = структуры в категориях. • **Functorial Data (FQL)** (Базы данных как функторы): Спивак и Wisnesky. SQL-like язык, где схема = категория, данные = функтор. Математически гарантированные миграции без JOIN-аномалий. • **Lean 4 / Mathlib** (HoTT-основания математики): Mathlib формализует категории, функторы, топосы. Верификация геометрии Гротендика - активная область.

Декартово замкнутые категории = просто типизированное лямбда-исчисление

Гротендик разработал топос-теорию в 1960-х, объединив логику и геометрию. Lean 4 и Coq используют топосную семантику для верификации математических теорем - в 2023 году Lean проверил доказательство теоремы Гая о сферах за 3 секунды. В каждом топосе своя логика: геометрия диктует, что считается «истинным».

Теория типовТеория категорийЛогика (IPC)
Тип AОбъект AПропозиция A
Функция f:A→BМорфизм f:A→BДоказательство A→B
Тип функций A→BЭкспоненциал B^AИмпликация A→B
Произведение A×BДекартово произведениеКонъюнкция A∧B
Сумма A+BКопроизведениеДизъюнкция A∨B
Единичный тип 1Терминальный объект ⊤Истина ⊤
Пустой тип 0Инициальный объект ⊥Ложь ⊥

Что соответствует типу A→B в изоморфизме Curry-Howard-Lambek?

CHL унифицирует три языка: тип A→B = морфизм в CCC = импликация в логике. Экспоненциальный объект B^A в CCC - это тип функций A→B в STLC.

Топосы: математические вселенные с внутренней логикой

Гротендик ввёл топосы в 1960-х для алгебраической геометрии. Лоувер и Тирни (1969) показали: каждый топос имеет **внутреннюю логику** - интуиционистскую логику высшего порядка. Объект истинности Ω в топосе Sh(X) пучков на топологическом пространстве X - это множество открытых подмножеств X. Истина «в точке» = истина «в окрестности точки».

Почему внутренняя логика любого топоса интуиционистская? Потому что Ω не обязан быть {⊤,⊥}. В Sh(X) двойное отрицание ¬¬U - это внутренность замыкания U, что не совпадает с U для открытых множеств. **¬¬U ≠ U в общем случае** - это именно отсутствие LEM.

Почему внутренняя логика любого топоса интуиционистская, а не классическая?

В Sh(X) объект истинности Ω - открытые подмножества X. Для U∈Ω: ¬¬U = Int(Closure(U)) ≠ U в общем случае, что ломает закон двойного отрицания и LEM.

Алгебры Хейтинга и внутренний язык

Решётка открытых множеств топологического пространства образует **алгебру Хейтинга** - алгебраическую модель интуиционистской логики. Булева алгебра - частный случай, где ¬¬a=a. Это делает топологию и логику двумя описаниями одного объекта: открытое множество = истинная пропозиция.

Какое условие превращает алгебру Хейтинга в булеву алгебру?

Булева алгебра = алгебра Хейтинга + ¬¬a = a. Пример: Open(ℝ) - хейтингова, но не булева, так как ¬¬(ℝ\{0}) = ℝ ≠ ℝ\{0}.

Применения: базы данных, семантика, HoTT

Категорная логика - не только теория. **Functorial Data Migration** (Спивак, 2010): схема базы данных - малая категория C, экземпляр БД - функтор C→Set, запрос - натуральное преобразование. Миграция между схемами = функтор между категориями. Это SQL без JOIN-ов, но с математической гарантией корректности.

**HoTT в Agda**: типы как пространства, Id(a,b) как пространство путей. **Денотационная семантика**: значение программы = морфизм в подходящей CCC. Haskell компилируется через GHC Core - язык, близкий к System F, который напрямую интерпретируется как морфизмы в CCC. Монады Haskell - это монады в категории.

**Grothendieck toposes** используются в алгебраической геометрии для доказательства гипотез Вейля (Делинь, 1974, медаль Филдса). Etale topos кривой над конечным полем кодирует счёт точек над расширениями поля. Логика топоса = геометрическая информация о кривой.

В теоретико-категорной модели реляционной БД что играет роль объектов категории?

Схема БД = малая категория: объекты = таблицы, морфизмы = внешние ключи (FK). Функтор в Set сопоставляет каждой таблице набор строк - это экземпляр БД.

Терм: (λx:A. t) a редуцируется к t[a/x] Категорно: λx:A. t = транспонирование f̃ : 1 → B^A (через eval : B^A × A → B) применение a:A = морфизм a : 1 → A (λx. t) a = eval ∘ (f̃ × id_A) ∘ ⟨id_1, a⟩ Beta-редукция = законы о eval и transpose в CCC: eval ∘ (transpose(f) × id) = f

ТопосОбъект истинности ΩЛогика
Set{⊤,⊥} = 2Классическая (булева)
Sh(X) пучки на XОткрытые подмножества XИнтуиционистская (непрерывная)
G-SetПодгруппы GИнтуиционистская
[C,Set] пресвязкиСимеvy идеалы CИнтуиционистская
Топос ГротендикаПучок покрытийГеометрическая логика

Упражнения

  1. Что такое изоморфизм Curry-Howard-Lambek и чем он отличается от Curry-Howard? — CH: типы=пропозиции, программы=доказательства; CHL добавляет: типы=объекты в CCC, программы=морфизмы; Экспоненциал B^A = тип функций A→B = импликация A→B; Единый формализм для логики, типов и категорий
  2. Почему внутренняя логика топоса Sh(X) интуиционистская? Покажите на примере ¬¬U ≠ U. — Ω = Open(X) - открытые подмножества X; ¬U = Int(X\U) - внутренность дополнения; ¬¬U = Int(Closure(U)) ≠ U для U=X\{p}; LEM нарушен: U∨¬U ≠ X в общем топосе

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

  • CCC = STLC = IPC (Curry-Howard-Lambek): объекты=типы=пропозиции, морфизмы=программы=доказательства
  • Экспоненциал B^A: морфизмы C×A→B биективны с C→B^A - это тип функций A→B
  • Топос = CCC + субобъектный классификатор Ω; Sh(X): Ω = Open(X), логика непрерывна
  • Алгебра Хейтинга: ¬a = a→0; булева = хейтинга + ¬¬a=a; Open(ℝ) - хейтинга, не булева
  • Монады (Могги): вычислительные эффекты = монады в CCC; State, IO, Maybe - категорные объекты
  • Функторная семантика БД: схема = категория, данные = функтор, запросы = натуральные преобразования

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

Категорная логика - перекрёсток алгебры, геометрии, логики и CS

  • Теория типов (CHI, MLTT) — CCC = STLC; MLTT = локально декартово замкнутые категории; HoTT объединяет всё
  • Конструктивная математика — Топосная семантика = конструктивная логика; аксиома унивалентности HoTT реализована в Agda/Lean
  • Интуиционистская логика — Алгебры Хейтинга = семантика ИЛ; любой топос порождает ИЛ через внутренний язык

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

  • plt-07-algebraic-types
Теория категорий и логика

0

1

Войти