Логика для вычислимых функций

См. Также: Логика вычислимых функций.

Логика для вычислимых функций ( LCF ) — это интерактивное автоматизированное средство доказательства теорем , разработанное в Стэнфорде и Эдинбурге Робином Милнером и его сотрудниками в начале 1970-х годов на основе теоретической основы логики вычислимых функций , ранее предложенной Даной Скотт . Работа над системой LCF представила язык программирования общего назначения ML , позволяющий пользователям писать тактики доказательства теорем, поддерживающий алгебраические типы данных , параметрический полиморфизм , абстрактные типы данных и исключения .

Основная идея

Теоремы в системе являются терминами специального абстрактного типа данных «теорема» . Общий механизм абстрактных типов данных ML гарантирует, что теоремы выводятся с использованием только правил вывода , заданных операциями абстрактного типа теоремы. Пользователи могут писать произвольно сложные программы машинного обучения для вычисления теорем; Справедливость теорем не зависит от сложности таких программ, а следует из корректности реализации абстрактного типа данных и корректности ML-компилятора.

Преимущества

Подход LCF обеспечивает надежность, аналогичную системам, которые генерируют явные подтверждающие сертификаты, но без необходимости хранить подтверждающие объекты в памяти. Тип данных «Теорема» можно легко реализовать для дополнительного хранения объектов доказательства, в зависимости от конфигурации времени выполнения системы, поэтому он обобщает базовый подход к созданию доказательств. Решение использовать язык программирования общего назначения для разработки теорем означает, что, в зависимости от сложности написанных программ, можно использовать один и тот же язык для написания пошаговых доказательств, процедур принятия решений или средств доказательства теорем.

Недостатки

Доверенная вычислительная база

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

процедур

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

Влияния

Среди последующих реализаций — Cambridge LCF. Более поздние системы упростили логику, чтобы использовать полные функции вместо частичных, что привело к HOL , HOL Light и помощнику доказательства Изабель , который поддерживает различную логику. По состоянию на 2019 год помощник по доказательству Isabelle по-прежнему содержит реализацию логики LCF Isabelle/LCF.

Ссылки

• Гордон, Майкл Дж .; Милнер, Артур Дж.; Уодсворт, Кристофер П. (1979). Эдинбургский LCF: механизированная логика вычислений . Конспекты лекций по информатике. Том. 78. Берлин-Гейдельберг: Шпрингер. дои : 10.1007/3-540-09724-4 . ISBN  978-3-540-09724-2 . S2CID   21159098 .
• Гордон, Майкл Дж. К. (2000). «От LCF до HOL: краткая история». Доказательство, язык и взаимодействие . Кембридж, Массачусетс: MIT Press. стр. 169–185. ISBN  0-262-16188-5 . Проверено 11 октября 2007 г.
• Лёкс, Жак; Зибер, Курт (1987). Основы проверки программ (2-е изд.). Vieweg+Teubner Verlag. дои : 10.1007/978-3-322-96753-4 . ISBN  978-3-322-96754-1 .
• Милнер, Робин (май 1972 г.). Логика для вычислимых функций: описание машинной реализации (PDF) . Стэндфордский Университет.
• Милнер, Робин (1979). «Lcf: Способ проведения доказательств с помощью машины». В Бечварже, Иржи (ред.). Математические основы информатики 1979 . Конспекты лекций по информатике. Том. 74. Берлин-Гейдельберг: Шпрингер. стр. 146–159. дои : 10.1007/3-540-09526-8_11 . ISBN  978-3-540-09526-2 .