λПролог
| Парадигма | Логическое программирование |
|---|---|
| Разработано | Дейл Миллер и Гопалан Надатур |
| Впервые появился | 1987 [ 1 ] |
| Дисциплина набора текста | строго типизированный |
| Лицензия | Стандартная общественная лицензия GNU v3 |
| Веб-сайт | www |
| Основные реализации | |
| Тейюс, ELPI | |
| Под влиянием | |
| Пролог | |
| Под влиянием | |
| Могила | |
λProlog , также называемый лямбда-прологом , — это язык логического программирования, включающий полиморфную типизацию , модульное программирование и программирование высшего порядка . Эти расширения Пролога высшего порядка, основаны на наследственных формулах Харропа используемых для обоснования основ λProlog. Квантификация более высокого порядка , просто типизированные λ-термины и унификация более высокого порядка дают λProlog базовую поддержку, необходимую для преобразования подхода синтаксиса λ-дерева в абстрактный синтаксис более высокого порядка , подхода к представлению синтаксиса, который отображает привязки на уровне объекта в программирование. языковые привязки. Программистам в λProlog не нужно иметь дело с именами связанных переменных: вместо этого доступны различные декларативные устройства для работы с областями связывания и их созданием экземпляров.
История
[ редактировать ]С 1986 года λProlog получил множество реализаций. По состоянию на 2023 год язык и его реализации все еще активно разрабатываются.
Средство доказательства теорем Абеллы было разработано, чтобы предоставить интерактивную среду для доказательства теорем о декларативном ядре λProlog.
См. также
[ редактировать ]- Парадокс Карри # Лямбда-исчисление - о проблемах несогласованности , вызванных объединением (пропозициональной) логики и нетипизированного лямбда-исчисления.
- Сравнение реализаций Пролога
- Синтаксис и семантика Пролога
Ссылки
[ редактировать ]- ^ «Часто задаваемые вопросы: какие реализации лямбда-пролога доступны?» . www.lix.polytechnique.fr . Проверено 16 декабря 2019 г.
Учебники и тексты
[ редактировать ]- Дейл Миллер и Гопалан Надатур написали книгу «Программирование с логикой высшего порядка» , опубликованную издательством Cambridge University Press в июне 2012 года.
- Эми Фелти написала в 1997 году учебник по лямбда-прологу и его приложениям к доказательству теорем .
- Джон Ханнан написал учебник по анализу программ на лямбда-прологе для конференции PLILP 1998 года.
- Оливье Риду написал Lambda-Prolog de A à Z... ou presque (163 страницы, на французском языке). Он доступен в форматах PostScript , PDF и html .
Внешние ссылки
[ редактировать ]- Домашняя страница λПролога
- Вступление в группу сохранения программного обеспечения.
Реализации
[ редактировать ]- Компилятор Teyjus λProlog в настоящее время является самой старой реализацией, которая до сих пор поддерживается. [ 1 ] Этот компиляторный проект возглавляют Гопалан Надатур и ряд его коллег и учеников.
- ELPI: встраиваемый интерпретатор λProlog был разработан Энрико Тасси и Клаудио Сакердоти Коэном . Он реализован на языке OCaml и доступен в Интернете . Система описана в документе , опубликованном в LPAR 2015. ELPI также доступен в виде плагина Coq Энрико Тасси : см. руководство по этому плагину.
- Доказательство Абеллы можно использовать для доказательства теорем о программах и спецификациях λProlog.
 | Эта языкам программирования, статья, посвященная является незавершенной . Вы можете помочь Википедии, расширив ее . |
- ^ Надатур, Гопалан; Дастин Митчелл (1999). Описание системы: Teyjus — компилятор и абстрактная машинная реализация лямбда-пролога . ЛНАИ. Том. 1632. стр. 287–291. дои : 10.1007/3-540-48660-7_25 . ISBN 978-3-540-66222-8 .
{{cite book}}:|journal=игнорируется ( помогите )