LCF: програма, що перевіряє доведення про обчислення
У травні 1972 року Робін Мілнер описав у мемо Стенфордського проєкту штучного інтелекту LCF — програму, що перевіряє формальні доведення в логіці обчислюваних функцій, яку Дана Скотт запропонував в Оксфорді восени 1969 року. Людина ставить мету й розбиває її на підцілі, а машина веде доведення й перевіряє кожен крок.
Чому це важливо
Доведення стало діалогом: людина вирішує, куди йти, машина гарантує, що кожен крок правильний. У единбурзькій версії цей діалог отримав власну мову, ML; Гордон, учасник проєкту, пише, що нащадки LCF утворили цілий напрям машинних міркувань.
Мемо описує логіку Скотта в нотації типізованого лямбда-числення і машинну реалізацію перевірки доведень для неї; серед команд — окрема група для постановки мети й роботи з підцілями в діалозі. Роботу підтримали NASA і ARPA. Чисел мемо не наводить. Про единбурзьку LCF запис спирається не на книжку 1979 року, яку прочитати не вдалося, а на ретроспективу її учасника Майка Гордона: близько 1973 року Мілнер перейшов до Единбурга; щоб теорему можна було отримати лише доведенням, теореми зробили значеннями абстрактного типу, чиї операції — правила виведення; для цього Мілнер разом із Моррісом і Ньюї спроєктував строго типізовану мову ML (Meta Language), а стратегії пошуку доведення стали функціями, які Мілнер назвав тактиками. Чого запис не стверджує: дат і змісту книжки 1979 року понад те, що каже Гордон.