λПролог

λProlog , также называемый лямбда-прологом , — это язык логического программирования , включающий полиморфную типизацию , модульное программирование и программирование высшего порядка . Эти расширения Пролога основаны на наследственных формулах Харропа высшего порядка , используемых для обоснования основ λProlog. Квантификация высшего порядка , просто типизированные λ-термины и унификация высшего порядка дают λProlog базовую поддержку, необходимую для преобразования синтаксического подхода λ-дерева в абстрактный синтаксис высшего порядка , подхода к представлению синтаксиса, который отображает привязки на уровне объекта в программирование. языковые привязки. Программистам в λProlog не нужно иметь дело с именами связанных переменных: вместо этого доступны различные декларативные устройства для работы с областями связывания и их созданием экземпляров.

История

С 1986 года λProlog получил множество реализаций. По состоянию на 2023 год язык и его реализации все еще активно разрабатываются.

Средство доказательства теорем Абеллы было разработано, чтобы предоставить интерактивную среду для доказательства теорем о декларативном ядре λProlog.

Смотрите также

• Парадокс Карри # Лямбда-исчисление - о проблемах несогласованности , вызванных объединением (пропозициональной) логики и нетипизированного лямбда-исчисления.

Рекомендации

1. «Часто задаваемые вопросы: какие реализации лямбда-пролога доступны?» 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.

1. Надатур, Гопалан; Дастин Митчелл (1999). Описание системы: Teyjus — компилятор и абстрактная машинная реализация лямбда-пролога . ЛНАИ. Том. 1632. стр. 287–291. дои : 10.1007/3-540-48660-7_25. ISBN 978-3-540-66222-8. {{cite book}}: |journal=игнорируется ( помощь )