λProlog , также называемый лямбда- прологом , представляет собой язык логического программирования с полиморфной типизацией , модульным программированием и программированием более высокого порядка . Эти расширения Prolog являются производными от наследственных формул Харропа высшего порядка, используемых для обоснования основ λProlog. Количественная оценка более высокого порядка , просто типизированные λ-термины и унификация высшего порядка дают λProlog базовую поддержку, необходимую для захвата подхода синтаксиса λ-дерева к абстрактному синтаксису более высокого порядка., подход к представлению синтаксиса, который отображает привязки объектного уровня в привязки языка программирования. Программистам в λProlog не нужно иметь дело с именами связанных переменных: вместо этого доступны различные декларативные устройства для работы с областями связывания и их экземплярами.
Парадигма | Логическое программирование |
---|---|
Разработано | Дейл Миллер и Гопалан Надатур |
Впервые появился | 1987 [1] |
Печатная дисциплина | строго типизированный |
Лицензия | Стандартная общественная лицензия GNU v3 |
Веб-сайт | www |
Основные реализации | |
Тейюс, ЭЛПИ | |
Под влиянием | |
Пролог | |
Под влиянием | |
Макам |
История
С 1986 года λProlog получил множество внедрений. По состоянию на 2013 год язык и его реализации все еще активно развиваются.
Средство доказательства теорем Абеллы было разработано для обеспечения интерактивной среды для доказательства теорем о декларативном ядре λProlog.
Смотрите также
- Парадокс Карри # Лямбда-исчисление - о проблемах несогласованности, вызванных объединением (пропозициональной) логики и нетипизированного лямбда-исчисления
Рекомендации
- ^ "FAQ: Какие реализации лямбда-пролога доступны?" . www.lix.polytechnique.fr . Проверено 16 декабря 2019 .
Учебники и тексты
- Дейл Миллер и Гопалан Надатур написали книгу « Программирование с помощью логики высшего порядка» , опубликованную издательством Cambridge University Press в июне 2012 года.
- Эми Фелти написала в 1997 году учебник по лямбда-прологу и его приложениям для доказательства теорем ([Архивировано WebCite https://www.webcitation.org/5WpO4HGEh?url=http://www.site.uottawa.ca/~afelty /dist/lprolog97.ps ]).
- Джон Ханнан написал учебное пособие по анализу программ в лямбда -прологе для конференции PLILP 1998 года.
- Оливье Риду написал Lambda-Prolog de A à Z ... ou presque (163 страницы на французском языке). Он доступен в форматах PostScript , PDF и html .
Внешние ссылки
- λProlog домашняя страница
- Запись в Группу сохранения программного обеспечения.
Реализации
- Компилятор Teyjus λProlog в настоящее время является самой старой реализацией, которая все еще поддерживается. [1] Этот проект компилятора возглавляют Гопалан Надатур и различные его коллеги и ученики.
- ELPI: встраиваемый интерпретатор λProlog был разработан Энрико Тасси и Клаудио Сакердоти Коеном . Он реализован в OCaml и доступен в Интернете . Система описана в опубликованном документе LPAR 2015.
- Программа доказательства Abella может использоваться для доказательства теорем о программах и спецификациях λProlog.
- ^ Надатур, Гопалан; Дастин Митчелл (1999). Описание системы: Teyjus - компилятор и реализация лямбда-пролога на основе абстрактной машины . Конференция по автоматическому вычету . LNAI. 1632 . С. 287–291. DOI : 10.1007 / 3-540-48660-7_25 . ISBN 978-3-540-66222-8.