Logic for Computable Functions

Logic for Computable Functions
Тип Средство доказательства теорем
Разработчики Робин Милнер и др.
Написана на ML
Первый выпуск ранние 1970ые
Аппаратная платформа кросcплатформенное

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

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

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

Достоинства

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

Недостатки

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

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

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

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

Влияние

Существует целый ряд производных реализаций системы, в частности — Cambridge LCF. Более поздние системы, испытавшие влияние LCF, шли по пути использования более простых версий логики, чем в исходной системе. Это можно отнести, в частности, к таким инструментам доказательства теорем как HOL, HOL Light[англ.] и 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:10.1007/3-540-09724-4.
  • Gordon, Michael J. C. From LCF to HOL: a short history // Proof, language, and interaction. — Cambridge, MA: MIT Press, 2000. — С. 169—185. — ISBN 0-262-16188-5.
  • Loeckx, Jacques; Sieber, Kurt. The Foundations of Program Verification. — 2nd. — Vieweg+Teubner Verlag[англ.], 1987. — ISBN 978-3-322-96754-1. — doi:10.1007/978-3-322-96753-4.
  • Milner, Robin. Logic for Computable Functions: description of a machine implementation (англ.). — 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:10.1007/3-540-09526-8_11.

Примечания

  1. ↑ CakeML. Дата обращения: 2 ноября 2019. Архивировано 14 сентября 2020 года.
  2. ↑ Boyer, Robert S; Moore, J Strother. Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures (PDF) (Report). Technical Report CSL-108, SRI Projects 8527/4079. pp. 1—111. Архивировано (PDF) 2 ноября 2019. Дата обращения: 2 ноября 2019.