Кратко

  • В Edinburgh LCF тактика предлагала подцели и возвращала функцию validation. Результат становился теоремой лишь тогда, когда эта функция собирала теоремы подцелей через защищённые примитивные правила.
  • Абстрактный тип thm сокращал объём кода с прямыми полномочиями создавать теоремы. Он не доказывал непротиворечивость логики, верность спецификации или безошибочность компилятора, среды выполнения и оборудования.
  • История коллективна: исходную логику предложил Dana Scott, Stanford LCF появился раньше, а Michael Gordon, Christopher Wadsworth, Lockwood Morris, Malcolm Newey и другие исследователи участвовали в создании Edinburgh LCF и ML.

Поиск заканчивается раньше, чем принятие

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

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

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

Тактики от этого не стали безошибочными. Они могли зациклиться, выбрать неудачные подцели, вызвать исключение или вернуть неверную validation. Архитектурная гарантия была уже: ошибка вне интерфейса не давала запасного конструктора. Она обычно приводила к отсутствию нужной теоремы.

От Stanford LCF к Edinburgh LCF — работа команды

В 1972 году Robin Milner описал реализованный проверяющий механизм для Logic for Computable Functions, предложенной Dana Scott. Опыт Stanford LCF показал перспективу машинной поддержки и практические трудности длинных доказательств. После перехода Robin Milner в Edinburgh в 1973 году работа сосредоточилась на программируемой среде.

Каноническая книга 1979 года подписана Michael J. C. Gordon, Robin Milner и Christopher P. Wadsworth. В статье 1978 года о метаязыке также указаны Lockwood Morris и Malcolm Newey. Исторические обзоры Larry Paulson и Michael Gordon связывают Stanford LCF с Edinburgh LCF, Cambridge LCF, HOL и Isabelle. Центральная идея Robin Milner не превращает коллективную работу в единоличную.

ML первоначально означал Meta Language и служил для программирования доказательных процедур. Полиморфная система типов затем стала самостоятельным результатом. В работе 1978 года Robin Milner сформулировал семантическую и синтаксическую soundness и описал алгоритм вывода типов, уже применявшийся в Edinburgh LCF. Премия A. M. Turing Award 1991 года отметила LCF, ML и CCS, но не отменяла распределённого авторства.

Правила вывода работали вперёд: из существующих теорем к новой. Тактики работали назад: от цели к подцелям. Validation соединяла направления. Tacticals задавали последовательность, повторение и выбор тактик; они расширяли управление поиском, но не список примитивных истин.

Что даёт абстрактный тип

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

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

Однако «малое ядро» не означает отсутствие доверия. Примитивные правила должны быть корректны для выбранной логики. Реализация ML, компилятор и среда должны сохранять абстракцию. Небезопасные возможности и аппаратные ошибки могут её разрушить. Парсер или средство отображения способно показать пользователю не тот терм, который хранится. Доверенная база сужается, но не исчезает.

Soundness ядра также не равна непротиворечивости логики. Утверждение, что значение создано только определёнными функциями, описывает происхождение; оно не доказывает независимо валидность каждой функции. И теорема о модели не подтверждает, что модель верно отражает реальную систему или человеческое намерение. Безупречное ядро может безупречно ответить на неправильно поставленный формальный вопрос.

Validation как отсроченное обязательство

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

Когда tacticals составляют поиск из нескольких тактик, они составляют и validation. Управляющий слой может стать большим, но цепь принятия всё равно возвращается к примитивным операциям. Журнал, сценарий и зелёный статус показывают активность; они не обладают полномочием принятого объекта.

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

Источники и границы вывода

Это исторический и архитектурный анализ, а не аудит современного prover и не измерение размера ядра. Связь с минимальным общим правилом, доступным локальной проверке и открытым будущим методам, является редакционной интерпретацией принципа минимальной исходной спецификации Lu Heng; она не приписывается Robin Milner как институциональная позиция.