| Logik for beregnelige funktioner | |
|---|---|
| Type | Sætningsbevis |
| Udvikler | Robin Milner og andre |
| Skrevet i | ML |
| Første udgave | begyndelsen af 1970'erne |
| Hardware platform | på tværs af platforme |
Logic for Computable Functions ( Russian Logic for computable functions ), (LCF) er et interaktivt automatisk teorembevisværktøj udviklet af Robin Milner og hans medarbejdere i Stanford og Edinburgh i begyndelsen af 1970'erne baseret på det deduktive system af samme navn foreslået af Dana Scott . I løbet af arbejdet med LCF-systemet blev et universelt programmeringssprog ML udviklet . Dets brug i systemet tillod brugere at skrive teorembevisende taktikker, der understøtter algebraiske datatyper, parametrisk polymorfi, abstrakte datatyper og undtagelser.
Sætninger i systemets sprog er repræsenteret ved udtryk, der har en speciel type "sætning". ML-abstrakte datatypemekanismen sørger for inferens af teoremer ved hjælp af inferensreglerne givet af operationerne, der er defineret for "sætning"-abstrakttypen. Brugere kan skrive vilkårligt komplekse programmer i ML for at beregne teoremer; sandheden af teoremer afhænger dog ikke af kompleksiteten af sådanne programmer. Det følger af rigtigheden af implementeringen af den abstrakte datatype og selve ML-kompileren.
LCF-tilgangen giver bevispålidelighed svarende til systemer, der genererer eksplicitte trinvise sætningsbevisprocedurer, men der er ikke behov for at gemme alle mellemliggende objekter og datastrukturer relateret til beviset i hukommelsen. Vedvarenheden af disse objekter og datastrukturer kan dog nemt implementeres eller omkonfigureres afhængigt af systemets konfiguration under kørsel. Dette giver dig mulighed for at generalisere og gøre den grundlæggende procedure for at generere et bevis så fleksibel som muligt. Brugen af et programmeringssprog til generelle formål til udvikling af teoremer sikrer universaliteten af tilgangen og giver dig mulighed for at bruge udledning af beviser direkte i ethvert program til generelle formål.
Implementeringen af den underliggende ML-compiler bygger på en postuleret tillid til den logiske kerne af systemet, som skal accepteres som korrekt uden begrundelse. CakeML Compiler Project udviklede en compiler, der formelt blev verificeret til at fungere korrekt. Dette blev en delvis løsning på det specificerede problem [1] .
Teorembevis inden for rammerne af LCF-tilgangen er hovedsageligt afhængig af beslutningsprocedurer og sætningsbevisende algoritmer, hvis rigtighed skal kontrolleres omhyggeligt. Den mest korrekte måde at implementere disse procedurer på i LCF kræver, at sådanne procedurer altid udleder resultater fra systemets aksiomer, lemmaer og inferensregler i stedet for at beregne resultatet direkte. En potentielt mere effektiv tilgang er at bruge refleksion til at generere bevis for, at disse procedurer fungerer korrekt [2] .
Der er en række afledte implementeringer af systemet, især - Cambridge LCF. Senere systemer påvirket af LCF har taget vejen til at bruge enklere versioner af logikken end det originale system. Dette kan især tilskrives sådanne teorembevisende værktøjer som HOL , HOL Light og Isabelle , som understøtter arbejde med forskellige deduktive systemer. Fra april 2020 inkluderer Isabelle dog stadig en implementering af det logiske LCF-system - Isabelle/LCF.