Войти
Логика для вычислимых функций (LCF ) - интерактивное автоматическое средство доказательства теорем, разработанное в Стэнфорде и Эдинбурге Робином Милнером и соавторами. в начале 1970-х годов, на основе теоретических основ логики вычислимых функций, ранее предложенных Даной Скотт. В ходе работы над системой LCF был представлен универсальный язык программирования ML, позволяющий пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.
Теоремы в системе являются терминами специальной «теоремы» абстрактного типа данных. Общий механизм абстрактных типов данных ML гарантирует, что теоремы выводятся с использованием только правил вывода, заданных операциями абстрактного типа теорем. Пользователи могут писать произвольно сложные программы машинного обучения для вычисления теорем; справедливость теорем не зависит от сложности таких программ, но следует из обоснованности реализации абстрактного типа данных и корректности компилятора ML.
Подход LCF обеспечивает такую же надежность, что и системы, которые генерируют явные сертификаты подтверждения, но без необходимости хранить объекты доказательства в памяти. Тип данных «теорема» может быть легко реализован для факультативного хранения объектов доказательства, в зависимости от конфигурации системы во время выполнения, поэтому он обобщает базовый подход создания доказательств. Проектное решение использовать язык программирования общего назначения для разработки теорем означает, что, в зависимости от сложности написанных программ, можно использовать тот же язык для написания пошаговых доказательств, процедур принятия решений или средств доказательства теорем.
Реализация базового компилятора машинного обучения добавляет к базе доверенных вычислений. Работа над CakeML привела к появлению официально проверенного компилятора ML, что частично сняло эти опасения.
Доказательство теорем часто выигрывает от процедур принятия решений и алгоритмов доказательства теорем, правильность которых была тщательно проанализирована. Простой способ реализации этих процедур в подходе LCF требует, чтобы такие процедуры всегда выводили результаты из аксиом, лемм и правил вывода системы, в отличие от прямого вычисления результата. Потенциально более эффективный подход - использовать отражение, чтобы доказать, что функция, работающая с формулами, всегда дает правильный результат.
Среди последующих реализаций - Cambridge LCF. Более поздние системы упростили логику, чтобы использовать общие функции вместо частичных, что привело к HOL, HOL Light и Isabelle proof assistant, которые поддерживают различные логики. По состоянию на 2019 год помощник по доказательству Изабель все еще содержит реализацию логики LCF, Isabelle / LCF.
