Русская Википедия:Logic for Computable Functions
Logic for Computable Functions (Шаблон:Lang-ru), (LCF) — инструмент для интерактивного автоматического доказательства теорем, разработанный Робином Милнером и его сотрудниками в Стэнфорде и Эдинбурге в начале 1970-х годов на базе одноимённой дедуктивной системы, предложенной Даной Скоттом. В ходе работы над системой LCF был разработан универсальный язык программирования ML. Его применение в системе позволило пользователям писать тактики доказательства теорем, поддерживающие алгебраические типы данных, параметрический полиморфизм, абстрактные типы данных и исключения.
Основная идея
Теоремы в языке системы представляются термами, имеющими специальный тип «теорема». Механизм абстрактных типов данных ML обеспечивает вывод теорем с использованием правил вывода, заданных операциями, которые определены для абстрактного типа «теорема». Пользователи могут писать на ML произвольно сложные программы, для вычисления теорем; истинность теорем, при этом, не зависит от сложности таких программ. Она следует из корректности реализации абстрактного типа данных и самого компилятора ML.
Достоинства
Подход LCF обеспечивает надежность доказательства, аналогичную надежности системам, которые генерируют явные пошаговые процедуры подтверждения истиности теорем, но необходимость сохранять все промежуточные объекты и структуры данных, относящиеся к доказательству в памяти, при этом, отсутствует. Сохранение этих объектов и структур данных, тем не менее, может быть легко реализовано или перенастроено в зависимости от конфигурации системы во время выполнения программы. Это позволяет обобщить и сделать максимально гибкой базовую процедуру генерации доказательства. Использование языка программирования общего назначения для разработки теорем обеспечивает универсальность подхода и позволяет использовать вывод доказательств непосредственно в любой программе общего назначения.
Недостатки
Проблема доверия к логическому ядру системы
Реализация базового компилятора ML опирается на постулируемое доверие к логическому ядру системы, которое приходится принимать в качестве корректного без обоснований. В проекте компилятора CakeML был разработан компилятор, корректность работы которого была формально верифицированна. Это стало частичным решением указанной проблемы[1].
Проблемы с эффективностью и сложностью процедур доказательств
Доказательство теорем в рамках подхода LCF, в основном, опирается на процедуры принятия решений и алгоритмы доказательства теорем, корректность которых нуждается в тщательной проверке. Наиболее правильный стиль реализации этих процедур в LCF требует, чтобы такие процедуры всегда выводили результаты из аксиом, лемм и правил вывода системы, а не вычисляли результат непосредственно. Потенциально более эффективный подход состоит в том, чтобы использовать рефлексию, для того, чтобы сгенерировать доказательство того, что эти процедуры работают корректно[2] .
Влияние
Существует целый ряд производных реализаций системы, в частности — Cambridge LCF. Более поздние системы, испытавшие влияние LCF, шли по пути использования более простых версий логики, чем в исходной системе. Это можно отнести, в частности, к таким инструментам доказательства теорем как HOL, Шаблон:Iw и Isabelle, поддерживающей работы с различными дедуктивными системами. Впрочем, по состоянию на апрель 2020 Isabelle по-прежнему включает в себя вариант реализации логической системы LCF — Isabelle/LCF.
Литература
Примечания
