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