Автор объясняет, что Isabelle сознательно отказалась от объектов доказательств, которые являются неотъемлемой частью обычных теорий типов. Это сделано потому, что объекты доказательств не нужны и занимают много места. Вместо этого Isabelle использует архитектуру LCF, где проверка типов осуществляется в языке реализации, а не в логике, что гарантирует легитимность шагов доказательства. Robin Milner имел это фундаментальное понимание 50 лет назад.

Лоуренс Полсон рассказывает о своем опыте работы с AUTOMATH и Martin-Löf type theory. Первоначально Isabelle была реализацией Martin-Löf type theory, которая до сих пор включена в дистрибутив как Isabelle/CTT. Однако автор переключился на более общий подход, вдохновленный AUTOMATH - "большим рестораном, который обслуживает любую кухню". В итоге Isabelle/HOL стала доминирующей, хотя де Брёйн не одобрял растущую мощь теорий типов и презирал теорию множеств.

• Обсуждение показало, что вопрос не в «плохих» зависимых типах, а в том, что они не нужны для большинства задач и не оправдывают свою сложность.
• Участники обсуждали, что отсутствие зависимых типов не мешает Isabelle/HOL доказать критически важные части математики, и что вместо этого важнее автоматизация и библиотеки.
• Сообщество отметило, что даже в языках без зависимых типов можно выразить «матрица 10×5 из float32», если размеры известны на этапе компиляции, и что это покрывает большинство практических случаев.
• Несколько участников поделились личным опытом, что попытка использовать зависимые типы в продакшене привела к тому, что команды отказались их использовать из-за кривой кривой обучения и отсутствия инструментальной поддержки.
• В итоге автор статьи подытожил, что выбор между зависимыми типами и другими системами типов часто сводится к личным предпочтениям и доступным инструментам, а не к объективным преимуществам.

Простое введение в z3

Изучение мира решателей ограничений на простых примерах.

Что такое решатели?

Решатели — это инструменты, которые принимают правила и ограничения, а затем находят решение. Они не всегда быстрее специальных алгоритмов, но гораздо гибче при изменении условий. Применяются для планирования, распределения ресурсов и других задач.

Терминология

В документации z3 много жаргона. Например, «Sort» означает тип, а «constants» — это переменные, которыми оперирует решатель. Solver работает со своим языком SMT-LIB2, а библиотеки переводят код в этот язык.

Простое уравнение

Решим уравнение x + 4 = 7. Вот код на Rust:

use z3::{Solver, ast::Int};
fn main() {
    let solver = Solver::new();
    let x = Int::new_const("x");
    solver.assert(&(x + 4).eq(&7));
    assert_eq!(solver.check(), SatResult::Sat);
    let model = solver.get_model().unwrap();
    println!("x = {}", model.eval(&x, true).unwrap());
}

Решатель находит x = 3. Это базовый пример, но он показывает принцип работы.

• Обсуждение причин некорректных ответов в задаче о сдаче (coin change) при использовании решателя Z3 без нижних границ, что приводит к минимизации до отрицательной бесконечности.
• Рекомендации ресурсов для изучения SAT/SMT-решателей, включая конкретные PDF-документы и статьи.
• Обсуждение практического применения решателей (Z3, OR-Tools, MiniZinc) для различных задач, включая игры и оптимизацию запросов.
• Сравнение и рекомендации по выбору решателей для начинающих на Python, с упоминанием Z3, OR-Tools и CPMpy.
• Трудности моделирования проблем для решателей и важность правильной постановки ограничений для избежания неинтуитивного поведения.
• Обсуждение технических особенностей интеграции решателей в языки программирования, таких как перегрузка операторов в Rust.
• Упоминание о применении решателей для доказательства теорем и поиска контрпримеров, например, к гипотезе Гольдбаха.

%PDF-1.5  
9 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

54 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

102 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

127 0 obj  
stream  
…сжатое содержимое…  
endstream  
endobj  

• Большинство участников считают, что Ферма либо ошибся, либо пошутил: за три десятилетия он не записал «элегантное» доказательство, а все последующие попытки найти простое решение провалились.
• Обсуждаемый документ — это лишь «чертеж» (blueprint) будущего формализованного доказательства Великой теоремы Ферма в системе Lean; само доказательство займёт ещё несколько лет.
• Ключевой мотивацией формализации называют повышение надёжности: компьютер сможет полностью проверить громоздкое доказательство, исключив человеческие ошибки.
• Участники обеспокоены долговечностью кода и спрашивают, как предотвратить «захват» задач бездействующими участниками и избежать дублирования работы.
• Для массового использования Lean требуются учебные материалы и «текстбы» на его основе; уже появляются книги и курсы, включая упражнения Теренса Тао.