Математическая логика
Субструктурные логики
Rust гарантирует memory safety без garbage collector - за счёт линейных типов, встроенных прямо в систему типов. Это не просто практический трюк: это теорема Жирара 1987 года, воплощённая в промышленном языке.
- **Rust ownership:** система владения = аффинные типы; borrow checker = proof checker в separation logic
- **Facebook Infer:** статический анализатор на separation logic, находит null dereferences и memory leaks в prod-коде Meta/Amazon
- **Квантовые вычисления:** линейная логика моделирует квантовые схемы (нет клонирования квантовых состояний - no-cloning theorem)
Предварительные знания
Структурные правила и их отсутствие
Rust использует линейную логику: каждое значение потребляется ровно 1 раз (нет ослабления, нет сжатия) - borrow checker это 250 000 строк реализации. Классическая и интуиционистская логика неявно используют три **структурных правила** секвенциального исчисления: ослабление (weakening), сжатие (contraction) и перестановку (exchange). Субструктурные логики отбрасывают некоторые из них, получая логику с принципиально иными свойствами.
Без ослабления: нельзя «игнорировать» гипотезы - каждая должна быть использована. Без сжатия: нельзя «копировать» гипотезы - каждая используется ровно один раз. Это моделирует ресурсы: деньги, время, физические объекты.
В аффинной логике запрещено сжатие, но разрешено ослабление. Что это означает для гипотез?
Линейная логика Жирара
Линейная логика (Жирар, 1987) - логика **ресурсов**: каждая формула - это ресурс, который потребляется при использовании. «1 → булочка» можно использовать только один раз. Жирар также показал, что классическая логика вкладывается в линейную через модальности!
В линейной логике есть два вида конъюнкции: A ⊗ B (tensor - оба ресурса одновременно) и A & B (with - выбор одного из двух). Аналогично два вида дизъюнкции: A ⅋ B (par) и A ⊕ B (plus). Это отражает разные способы «разделения» ресурсов.
В чём разница между A ⊗ B (tensor) и A & B (with) в линейной логике?
Логика отделения (Separation Logic)
Логика отделения (Reynolds, O'Hearn, 2000) - расширение логики Хоара для рассуждений о **разделённой памяти**. Ключевой оператор «разделяющая конъюнкция» P * Q означает «P и Q истинны для непересекающихся участков памяти».
Главная мощь separation logic - Frame Rule: {P} C {Q} ⟹ {P*R} C {Q*R}. Если программа C корректна при предусловии P, то добавление несвязанного состояния R не влияет. Это позволяет рассуждать о частях памяти локально.
Что гарантирует оператор * (разделяющая конъюнкция) в P * Q?
Линейные типы в Rust
Система владения Rust - это **аффинные типы** в действии. Каждое значение имеет ровно одного владельца. Перемещение (move) потребляет значение. Заимствование (&, &mut) - ограниченное временное использование. Это линейная логика, компилируемая в машинный код без GC.
Borrow checker Rust формально эквивалентен проверке доказательств в аффинной системе типов. Время жизни (lifetime 'a) - это регионы в separation logic. RustBelt (2018) - формальная верификация Rust в Coq/Iris.
Почему система типов Rust называется «аффинной», а не «линейной»?
Ключевые идеи
- **Структурные правила** - W (ослабление), C (сжатие), E (перестановка); субструктурные логики отбрасывают часть из них
- **Линейная логика** - нет W и C; каждый ресурс используется ровно раз; два вида ∧ (tensor ⊗, with &) и два вида ∨
- **Separation Logic** - разделяющая конъюнкция P*Q: P и Q для непересекающейся памяти; Frame Rule; основа Infer
- **Rust = аффинные типы** - move semantics потребляет значение; borrow checker формально эквивалентен separation logic
Связанные темы
Субструктурные логики связывают теоретическую логику и системное программирование:
- Естественный вывод — Структурные правила появляются в секвенциальном исчислении Генцена; их отсутствие = субструктурность
- Теория типов (CHI) — Линейные типы = CHI для линейной логики; программы = доказательства, ресурсы = формулы
- Верификация в AI — Separation logic применяется для верификации нейросетевого кода и безопасных систем
Вопросы для размышления
- В Haskell функции чистые и ссылки на данные можно копировать свободно - какую «логику» реализует система типов Haskell? Нужна ли ей линейность?
- Квантовая механика запрещает копирование квантовых состояний (no-cloning theorem) - как линейная логика моделирует квантовые вычисления?
- Rust решил проблему memory safety через типы. Какие ещё проблемы можно решить, встроив логику в систему типов?