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

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

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

Достоинства

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

Недостатки

Проблема доверия к логическому ядру системы

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

Проблемы с эффективностью и сложностью процедур доказательств

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

Влияние

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

Литература

• Gordon, Michael J.; Milner, Arthur J.; Wadsworth, Christopher P. Edinburgh LCF: A Mechanised Logic of Computation (англ.) . — Berlin Heidelberg: Springer, 1979. — Vol. 78. — (Lecture Notes in Computer Science). — ISBN 978-3-540-09724-2 . — doi : .
• Gordon, Michael J. C. From LCF to HOL: a short history // . — Cambridge, MA: MIT Press , 2000. — С. 169—185. — ISBN 0-262-16188-5 .
• Loeckx, Jacques; Sieber, Kurt. The Foundations of Program Verification. — 2nd. — (англ.) ( , 1987. — ISBN 978-3-322-96754-1 . — doi : .
• Milner, Robin. (англ.) . — Stanford University, 1972.
• Milner, Robin. Lcf: A way of doing proofs with a machine // Mathematical Foundations of Computer Science 1979 (англ.) / Bečvář, Jiří. — Berlin Heidelberg: Springer, 1979. — Vol. 74. — P. 146—159. — (Lecture Notes in Computer Science). — ISBN 978-3-540-09526-2 . — doi : .

Примечания