LCF: програма, що перевіряє доведення про обчислення
У травні 1972 року Робін Мілнер описав у мемо Стенфордського проєкту штучного інтелекту LCF — програму, що перевіряє формальні доведення в логіці обчислюваних функцій, яку Дана Скотт запропонував в Оксфорді восени 1969 року. Людина ставить мету й розбиває її на підцілі, а машина веде доведення й перевіряє кожен крок.
Чому це важливо
Доведення стало діалогом: людина вирішує, куди йти, машина гарантує, що кожен крок правильний. У единбурзькій версії цей діалог отримав власну мову, ML; Гордон, учасник проєкту, пише, що нащадки LCF утворили цілий напрям машинних міркувань.
Мемо описує логіку Скотта в нотації типізованого лямбда-числення і машинну реалізацію перевірки доведень для неї; серед команд — окрема група для постановки мети й роботи з підцілями в діалозі. Роботу підтримали NASA і ARPA. Чисел мемо не наводить. Единбурзьку LCF запис описує за самою книжкою 1979 року (Гордон, Мілнер і Водсворт, «Edinburgh LCF: A Mechanised Logic of Computation», Lecture Notes in Computer Science 78), у якій відкриті передмова й перші дві сторінки вступу, і за ретроспективою Майка Гордона. За передмовою, сталий набір команд стенфордської LCF вимагав довгих і повторюваних діалогів, тож нова система замінила його мовою програмування загального призначення ML (від metalanguage): з функціями вищого порядку, обробкою винятків і надійною поліморфною дисципліною типів. Теореми — це обчислені значення типу thm, і система типів гарантує, що кожне значення цього типу є теоремою, бо обчислити його можуть лише правила виведення. Вступ називає малі складники стратегій доведення тактиками, а операції, що їх поєднують, — тактикалами, і каже, що ML проєктували так, щоб програмувати ті й ті було легко. Система працювала на DECsystem-10. Автори пишуть, що Локвуд Морріс і Малколм Ньюї мали б бути співавторами, якби це було можливо. Гордон додає, що близько 1973 року Мілнер перейшов до Единбурга. Дати початку единбурзької роботи книжка не називає; її вступ датує стенфордську реалізацію 1971–1972 роками. Авра Кон, яка брала участь у завершальних етапах проєктування, у своїй единбурзькій дисертації 1979 року написала, що систему реалізували в 1974–1979 роках Гордон, Мілнер, Морріс, Ньюї й Водсворт. Чого запис не стверджує: нічого з розділів книжки поза передмовою й початком вступу — вони за пейволом. Передмова каже про надійну дисципліну типів; те, що теореми утворюють абстрактний тип, — формулювання Гордона.