Логика для вычислимых функций ( LCF ) представляет собой интерактивный автоматизирован теорема доказывающая разработана в Стэнфорде и Эдинбурге на Робин Милнер и его сотрудниками в начале 1970 - х годов, на основе теоретического обоснования логики в вычислимых функций , ранее предложенной Дана Скотт . В ходе работы над системой LCF был представлен универсальный язык программирования ML, позволяющий пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных , параметрический полиморфизм , абстрактные типы данных и исключения..
Основная идея
Теоремы в системе являются терминами специального абстрактного типа данных «теорема» . Общий механизм абстрактных типов данных ML гарантирует, что теоремы выводятся с использованием только правил вывода, заданных операциями абстрактного типа теорем. Пользователи могут писать произвольно сложные программы машинного обучения для вычисления теорем; Справедливость теорем не зависит от сложности таких программ, а следует из обоснованности реализации абстрактного типа данных и корректности компилятора ML.
Преимущества
Подход LCF обеспечивает аналогичную надежность систем, которые генерируют явные сертификаты подтверждения, но без необходимости хранить объекты доказательства в памяти. Тип данных «теорема» может быть легко реализован для факультативного хранения объектов доказательства, в зависимости от конфигурации времени выполнения системы, поэтому он обобщает базовый подход генерации доказательств. Проектное решение об использовании универсального языка программирования для разработки теорем означает, что, в зависимости от сложности написанных программ, можно использовать тот же язык для написания пошаговых доказательств, процедур принятия решений или средств доказательства теорем.
Недостатки
Надежная вычислительная база
Реализация базового компилятора машинного обучения увеличивает надежную вычислительную базу . Работа над CakeML [1] привела к появлению официально проверенного компилятора ML, что частично сняло эти опасения.
Эффективность и сложность процедур доказательства
При доказательстве теорем часто используются процедуры принятия решений и алгоритмы доказательства теорем, правильность которых была тщательно проанализирована. Простой способ реализации этих процедур в подходе LCF требует, чтобы такие процедуры всегда выводили результаты из аксиом, лемм и правил вывода системы, а не напрямую вычисляли результат. Потенциально более эффективный подход - использовать отражение, чтобы доказать, что функция, работающая с формулами, всегда дает правильный результат. [2]
Влияния
Среди последующих реализаций - Cambridge LCF. Более поздние системы упростили логику, чтобы использовать общие функции вместо частичных, что привело к HOL , HOL Light и помощнику доказательства Изабель, который поддерживает различные логики. По состоянию на 2019 год помощник доказательства Изабель все еще содержит реализацию логики LCF, Isabelle / LCF.
Заметки
- ^ "CakeML" . Дата обращения 2 ноября 2019 .
- ^ Бойер, Роберт С; Мур, Дж. Стротер. Метафункции: их правильность и эффективное использование в качестве новых процедур доказательства (PDF) (Отчет). Технический отчет CSL-108, SRI Projects 8527/4079. С. 1–111 . Дата обращения 2 ноября 2019 .
Рекомендации
- Гордон, Майкл Дж .; Милнер, Артур Дж .; Уодсворт, Кристофер П. (1979). Эдинбург LCF: Механизированная логика вычислений . Конспект лекций по информатике. 78 . Берлин Гейдельберг: Springer. DOI : 10.1007 / 3-540-09724-4 . ISBN 978-3-540-09724-2.
- Гордон, Майкл JC (2000). «От LCF к HOL: краткая история». Доказательство, язык и взаимодействие . Кембридж, Массачусетс: MIT Press. С. 169–185. ISBN 0-262-16188-5. Проверено 11 октября 2007 .
- Loeckx, Жак; Зибер, Курт (1987). Основы проверки программ (2-е изд.). Vieweg + Teubner Verlag. DOI : 10.1007 / 978-3-322-96753-4 . ISBN 978-3-322-96754-1.
- Милнер, Робин (май 1972 г.). Логика вычислимых функций: описание машинной реализации (PDF) . Стэндфордский Университет.
- Милнер, Робин (1979). «Lcf: способ делать доказательства с помощью машины». В Бечварже, Иржи (ред.). Математические основы компьютерных наук 1979 . Конспект лекций по информатике. 74 . Берлин Гейдельберг: Springer. С. 146–159. DOI : 10.1007 / 3-540-09526-8_11 . ISBN 978-3-540-09526-2.