Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
λProlog, также написанный как lambda Prolog, - это логический язык программирования, включающий полиморфный тип, модульное программирование и программирование более высокого порядка. Эти расширения Prolog получены из высокопоставленных наследственных формул Харропа, используемых для обоснования основы λProlog. Количественное определение высшего порядка, просто напечатанные термины λ и унификация высшего порядка дают λProlog основные поддержки, необходимые для захвата синтаксического подхода дерева λ к абстрактному синтаксису высшего порядка, подходу к представлению синтаксиса, который отображает связки уровня объекта с связками языка программирования. Программистам в λProlog не нужно иметь дело с именами связанных переменных: вместо этого доступны различные декларативные устройства для работы с объемом связующих и их инстанциями.
λProlog, also written lambda Prolog, is a logic programming language featuring polymorphic typing, modular programming, and higher order programming. These extensions to Prolog are derived from the higher order hereditary Harrop formulas used to justify the foundations of λProlog. Higher order quantification, simply typed λ terms, and higher order unification gives λProlog the basic supports needed to capture the λ tree syntax approach to higher order abstract syntax, an approach to representing syntax that maps object level bindings to programming language bindings. Programmers in λProlog need not deal with bound variable names: instead various declarative devices are available to deal with binder scopes and their instantiations.
История
С 1986 года λProlog получил многочисленные реализации. По состоянию на 2023 год язык и его реализации все еще активно разрабатываются. Проверка теоремы Абелла была разработана для обеспечения интерактивной среды для доказательства теорем о декларативном ядре λProlog.
Since 1986, λProlog has received numerous implementations. As of 2023, the language and its implementations are still actively being developed. The Abella theorem prover has been designed to provide an interactive environment for proving theorems about the declarative core of λProlog.
Учебные пособия и тексты
Дейл Миллер и Гопалан Надатур написали книгу "Программирование с логикой высшего порядка", опубликованную издательством Cambridge University Press в июне 2012 года. Эми Фелти написала в 1997 году учебник по lambda Prolog и его применению к доказательству теорем. Джон Ханнан написал учебник по анализу программ в lambda Prolog для конференции PLILP 1998 года. Оливье Риду написал "Ламбда Пролог" (англ.) русск. Она доступна в виде PostScript, PDF и html.
Dale Miller and Gopalan Nadathur have written the book Programming with higher order logic, published by Cambridge University Press in June 2012. Amy Felty has written in a 1997 tutorial on lambda Prolog and its Applications to Theorem Proving. John Hannan has written a tutorial on Program Analysis in lambda Prolog for the 1998 PLILP Conference. Olivier Ridoux has written Lambda Prolog de A à Z ou presque (163 pages, French). It is available as PostScript, PDF, and html.
Реализация
Компилятор Teyjus λProlog в настоящее время является самой старой реализацией, которая все еще поддерживается. Этот компиляторный проект возглавляет Гопалан Надатур и его коллеги и студенты. ELPI: встраиваемый интерпретатор λProlog был разработан Энрико Тасси и Клаудио Сасердоти Коэном. Он реализован в OCaml и доступен в Интернете. Система описана в статье, которая появилась в LPAR 2015. ELPI также доступен в качестве плагина Coq: см. Учебное пособие Энрико Тасси по этому плагину. Проверкатель Абелла может использоваться для доказательства теорем о программах и спецификациях λProlog.
The Teyjus λProlog compiler is currently the oldest implementation still being maintained. This compiler project is led by Gopalan Nadathur and various of his colleagues and students. ELPI: an Embeddable λProlog Interpreter has been developed by Enrico Tassi and Claudio Sacerdoti Coen. It is implemented in OCaml and is available online. The system is described in a paper that appeared LPAR 2015. ELPI is also available as a Coq plugin: see Enrico Tassi's tutorial on this plugin. The Abella prover can be used to prove theorems about λProlog programs and specifications.