| Logik för beräkningsbara funktioner | |
|---|---|
| Sorts | Satsbevisare |
| Utvecklaren | Robin Milner och andra |
| Skrivet i | ML |
| Första upplagan | tidigt 1970-tal |
| Hårdvaruplattform | plattformsoberoende |
Logic for Computable Functions ( Rysk Logik för beräkningsbara funktioner ), (LCF) är ett interaktivt verktyg för automatisk satsbevisande utvecklat av Robin Milner och hans medarbetare i Stanford och Edinburgh i början av 1970-talet baserat på det deduktiva systemet med samma namn som föreslagits av Dana Scott . Under arbetet med LCF-systemet utvecklades ett universellt programmeringsspråk ML . Dess användning i systemet gjorde det möjligt för användare att skriva teorembevisande taktik som stöder algebraiska datatyper, parametrisk polymorfism, abstrakta datatyper och undantag.
Satser i systemets språk representeras av termer som har en speciell typ "sats". Mekanismen för ML-abstraktdatatyp tillhandahåller slutledning av satser med användning av slutledningsreglerna som ges av operationerna som definieras för den abstrakta typen "sats". Användare kan skriva godtyckligt komplexa program i ML för att beräkna satser; satsernas sanning beror dock inte på komplexiteten hos sådana program. Det följer av korrektheten i implementeringen av den abstrakta datatypen och själva ML-kompilatorn.
LCF-metoden ger bevistillförlitlighet liknande system som genererar explicita steg-för-steg-satsbevisande procedurer, men det finns inget behov av att lagra alla mellanliggande objekt och datastrukturer relaterade till beviset i minnet. Beständigheten hos dessa objekt och datastrukturer kan dock enkelt implementeras eller omkonfigureras beroende på konfigurationen av systemet vid körning. Detta gör att du kan generalisera och göra den grundläggande proceduren för att skapa ett bevis så flexibel som möjligt. Användningen av ett allmänt programmeringsspråk för att utveckla teorem säkerställer tillvägagångssättets universalitet och låter dig använda härledning av bevis direkt i alla allmänna program.
Implementeringen av den underliggande ML-kompilatorn bygger på ett postulerat förtroende för systemets logiska kärna, vilket måste accepteras som korrekt utan motivering. CakeML Compiler Project utvecklade en kompilator som formellt verifierades att fungera korrekt. Detta blev en dellösning på det angivna problemet [1] .
Satsbevisande inom ramen för LCF-metoden bygger huvudsakligen på beslutsprocedurer och satsbevisande algoritmer, vars korrekthet måste kontrolleras noggrant. Den mest korrekta stilen för att implementera dessa procedurer i LCF kräver att sådana procedurer alltid härleder resultat från systemets axiom, lemman och slutledningsregler, snarare än att beräkna resultatet direkt. Ett potentiellt mer effektivt tillvägagångssätt är att använda reflektion för att generera bevis på att dessa procedurer fungerar korrekt [2] .
Det finns ett antal derivatimplementeringar av systemet, i synnerhet - Cambridge LCF. Senare system påverkade av LCF har tagit vägen att använda enklare versioner av logiken än det ursprungliga systemet. Detta kan i synnerhet tillskrivas sådana teorembevisande verktyg som HOL , HOL Light och Isabelle , som stödjer arbete med olika deduktiva system. Men från och med april 2020 inkluderar Isabelle fortfarande en implementering av det logiska LCF-systemet - Isabelle/LCF.