λ Prolog
| Paradigm | Logisk programmering |
|---|---|
| Designad av | Dale Miller och Gopalan Nadathur |
| Dök först upp | 1987 |
| Maskinskrivningsdisciplin | starkt skrivet |
| Licens | GNU General Public License v3 |
| Hemsida | |
| Stora implementeringar | |
| Teyjus, ELPI | |
| Influerad av | |
| Prolog | |
| Influenced | |
| Makam | |
λProlog , även skrivet lambda Prolog , är ett logiskt programmeringsspråk med polymorf typning , modulär programmering och högre ordningsprogrammering . Dessa tillägg till Prolog är härledda från de högre ordningens ärftliga Harrop-formler som används för att rättfärdiga grunden för λProlog. Kvantifiering av högre ordning , enkelt skrivna λ-termer och enande av högre ordning ger λProlog de grundläggande stöden som behövs för att fånga λ-trädsyntaxmetoden till abstrakt syntax av högre ordning , en metod för att representera syntax som mappar objektnivåbindningar till programmering språkbindningar. Programmerare i λProlog behöver inte hantera bundna variabelnamn: istället finns olika deklarativa enheter tillgängliga för att hantera binderomfång och deras instansieringar.
Historia
Sedan 1986 har λProlog fått många implementeringar. Från och med 2023 utvecklas språket och dess implementeringar fortfarande aktivt.
Abella-satsbevisaren har utformats för att tillhandahålla en interaktiv miljö för att bevisa satser om den deklarativa kärnan i λProlog.
Se även
- Currys paradox#Lambdakalkyl — om inkonsekvensproblem som orsakas av att kombinera (propositionell) logik och otypad lambdakalkyl
Handledningar och texter
- Dale Miller och Gopalan Nadathur har skrivit boken Programmering med logik av högre ordning, publicerad av Cambridge University Press i juni 2012.
- Amy Felty har skrivit i en handledning från 1997 om lambda Prolog och dess tillämpningar för att bevisa teorem .
- John Hannan har skrivit en handledning om programanalys i lambda Prolog för 1998 års PLILP-konferens.
- Olivier Ridoux har skrivit Lambda-Prolog de A à Z... ou presque (163 sidor, franska). Det finns som PostScript , PDF och html .
externa länkar
- λ Prolog hemsida
- Inträde i Software Preservation Group.
Genomföranden
- Teyjus λProlog-kompilatorn är för närvarande den äldsta implementeringen som fortfarande underhålls. Detta kompilatorprojekt leds av Gopalan Nadathur och olika av hans kollegor och studenter.
- ELPI: en inbäddningsbar λProlog-tolk har utvecklats av Enrico Tassi och Claudio Sacerdoti Coen . Det är implementerat i OCaml och är tillgängligt online . Systemet beskrivs i ett papper som publicerades LPAR 2015. ELPI finns även tillgängligt som ett Coq-plugin : se Enrico Tassis handledning om detta plugin.
- Abella - provaren kan användas för att bevisa satser om λProlog-program och specifikationer.
- ^ Nadathur, Gopalan; Dustin Mitchell (1999). Systembeskrivning: Teyjus - En kompilator och abstrakt maskinbaserad implementering av lambda Prolog . Konferens om automatiskt avdrag . LNAI. Vol. 1632. s. 287–291. doi : 10.1007/3-540-48660-7_25 . ISBN 978-3-540-66222-8 .