LCF: Автоматический доказыватель теорем 1970-х годов.
Logic for Computable Functions
LCF: интерактивный автоматический доказатель теорем 1970-х. Основан на логике вычислимых функций, ввёл язык ML для тактик доказательства и абстрактных типов данных.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Автоматизированный теоремопроверщик 1970-х годов. Логика для вычислимых функций (LCF) — это интерактивный автоматизированный теоремопроверщик, разработанный в Стэнфорде и Эдинбурге Робином Мильнером и его коллегами в начале 1970-х годов, основанный на теоретических принципах логики вычислимых функций, ранее предложенных Даной Скоттом. Работа над системой LCF представила язык программирования общего назначения ML, позволяющий пользователям создавать тактики доказательства теорем и поддерживающий алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и обработку исключений.
1970s automated theorem prover
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general purpose programming language ML to allow users to write theorem proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
Основная идея
Теоремы в системе являются элементами специального абстрактного типа данных "теорема". Общий механизм абстрактных типов данных ML гарантирует, что теоремы выводятся исключительно с использованием правил вывода, заданных операциями этого абстрактного типа. Пользователи могут создавать произвольно сложные программы на ML для вычисления теорем; истинность теорем не зависит от сложности этих программ, а вытекает из корректности реализации абстрактного типа данных и правильности работы ML-компилятора.
Theorems in the system are terms of a special "theorem" abstract data type. The general mechanism of abstract data types of ML ensures that theorems are derived using only the inference rules given by the operations of the theorem abstract type. Users can write arbitrarily complex ML programs to compute theorems; the validity of theorems does not depend on the complexity of such programs, but follows from the soundness of the abstract data type implementation and the correctness of the ML compiler.
Преимущества
Подход LCF обеспечивает сопоставимую степень доверия к системам, генерирующим явные сертификаты доказательств, но без необходимости хранить объекты доказательств в памяти. Тип данных "Теорема" может быть легко реализован с возможностью опционального хранения объектов доказательств, в зависимости от конфигурации времени выполнения системы, что делает его обобщением базового подхода к генерации доказательств. Решение использовать язык программирования общего назначения для разработки теорем означает, что в зависимости от сложности написанных программ, на том же языке можно разрабатывать пошаговые доказательства, процедуры принятия решений или автоматические доказатели теорем.
The LCF approach provides similar trustworthiness to systems that generate explicit proof certificates but without the need to store proof objects in memory. The Theorem data type can be easily implemented to optionally store proof objects, depending on the system's run time configuration, so it generalizes the basic proof generation approach. The design decision to use a general purpose programming language for developing theorems means that, depending on the complexity of programs written, it is possible to use the same language to write step by step proofs, decision procedures, or theorem provers.
Доверенная вычислительная база
Реализация базового ML-компилятора расширяет доверенную вычислительную базу. Работа над CakeML привела к созданию формально верифицированного ML-компилятора, что ослабляет некоторые из этих опасений.
The implementation of the underlying ML compiler adds to the trusted computing base. Work on CakeML resulted in a formally verified ML compiler, alleviating some these concerns.
Эффективность и сложность процедур доказывания
Доказательство теорем часто выигрывает от использования процедур принятия решений и алгоритмов доказательства теорем, корректность которых была тщательно проанализирована. Прямой способ реализации этих процедур в рамках подхода LCF требует, чтобы они всегда выводили результаты из аксиом, лемм и правил вывода системы, а не вычисляли результат напрямую. Потенциально более эффективным подходом является использование рефлексии для доказательства того, что функция, оперирующая формулами, всегда выдает верный результат.
Theorem proving often benefits from decision procedures and theorem proving algorithms, whose correctness has been extensively analyzed. A straightforward way of implementing these procedures in an LCF approach requires such procedures to always derive outcomes from the axioms, lemmas, and inference rules of the system, as opposed to directly computing the outcome. A potentially more efficient approach is to use reflection to prove that a function operating on formulas always gives correct result.
Влияния
Среди последующих реализаций — Cambridge LCF. Более поздние системы упростили логику, перейдя к использованию полных вместо частичных функций, что привело к созданию HOL, HOL Light и системы автоматизированного доказательства Isabelle, поддерживающей различные логики. По состоянию на 2019 год система Isabelle по-прежнему содержит реализацию логики LCF, Isabelle/LCF.
Among subsequent implementations is Cambridge LCF. Later systems simplified the logic to use total instead of partial functions, leading to HOL, HOL Light, and the Isabelle proof assistant that supports various logics. As of 2019, the Isabelle proof assistant still contains an implementation of an LCF logic, Isabelle/LCF.