| Laskettavien funktioiden logiikka | |
|---|---|
| Tyyppi | Lauseen todistaja |
| Kehittäjä | Robin Milner ja muut |
| Sisään kirjoitettu | ML |
| Ensimmäinen painos | 1970-luvun alku |
| Laitteistoalusta | cross-platform |
Logic for Computable Functions ( Russian Logic for Computable Functions ), (LCF) on interaktiivinen automaattinen lauseiden todistamistyökalu, jonka Robin Milner ja hänen työtoverinsa Stanfordissa ja Edinburghissa 1970-luvun alussa kehittivät Dana Scottin ehdottaman samannimisen deduktiivisen järjestelmän perusteella. . LCF-järjestelmän työskentelyn aikana kehitettiin universaali ohjelmointikieli ML . Sen käyttö järjestelmässä antoi käyttäjille mahdollisuuden kirjoittaa lauseiden todistamistaktiikoita, jotka tukevat algebrallisia tietotyyppejä, parametrista polymorfismia, abstrakteja tietotyyppejä ja poikkeuksia.
Lauseet järjestelmän kielessä esitetään termeillä, joilla on erityinen tyyppi "lause". ML-abstraktin tietotyypin mekanismi mahdollistaa lauseiden päättelyn käyttämällä "lause"-abstraktille tyypille määriteltyjen operaatioiden antamia päättelysääntöjä . Käyttäjät voivat kirjoittaa mielivaltaisen monimutkaisia ohjelmia ML-kielellä lauseiden laskemiseksi; lauseiden totuus ei kuitenkaan riipu tällaisten ohjelmien monimutkaisuudesta. Se seuraa abstraktin tietotyypin ja itse ML-kääntäjän toteutuksen oikeellisuudesta.
LCF-lähestymistapa tarjoaa todistusluotettavuuden, joka on samanlainen kuin järjestelmät, jotka luovat eksplisiittisiä vaiheittaisia lauseiden todistamismenettelyjä, mutta kaikkia todistukseen liittyviä väliobjekteja ja tietorakenteita ei tarvitse tallentaa muistiin. Näiden objektien ja tietorakenteiden pysyvyys voidaan kuitenkin helposti toteuttaa tai konfiguroida uudelleen riippuen järjestelmän ajonaikaisesta konfiguraatiosta. Näin voit yleistää ja tehdä todisteen luomisen perusmenettelystä mahdollisimman joustavan. Yleiskäyttöisen ohjelmointikielen käyttö lauseiden kehittämiseen varmistaa lähestymistavan universaalisuuden ja mahdollistaa todisteiden johtamisen suoraan missä tahansa yleisohjelmassa.
Taustalla olevan ML-kääntäjän toteutus perustuu oletettuun luottamukseen järjestelmän loogiseen ytimeen, joka on hyväksyttävä perusteettomasti oikeaksi. CakeML Compiler Project kehitti kääntäjän, jonka muodollisesti todettiin toimivan oikein. Tästä tuli osittainen ratkaisu määritettyyn ongelmaan [1] .
Lauseen todistaminen LCF-lähestymistavan puitteissa perustuu pääosin päätösmenettelyihin ja lauseiden todistamisalgoritmeihin, joiden oikeellisuus on tarkistettava huolellisesti. Oikein tapa toteuttaa nämä proseduurit LCF:ssä edellyttää, että tällaiset proseduurit päättelevät aina tulokset järjestelmän aksioomista, lemmoista ja päättelysäännöistä sen sijaan, että ne laskevat tuloksen suoraan. Mahdollisesti tehokkaampi lähestymistapa on käyttää reflektiota todisteiden luomiseen näiden menettelyjen toimivuudesta [2] .
Järjestelmästä on useita johdannaistoteutuksia, erityisesti - Cambridge LCF. Myöhemmät järjestelmät, joihin LCF on vaikuttanut, ovat valinneet alkuperäistä järjestelmää yksinkertaisempien versioiden käyttämisen. Tämä johtuu erityisesti sellaisista lauseiden todistamistyökaluista, kuten HOL , HOL Light ja Isabelle , joka tukee työskentelyä erilaisten deduktiivisten järjestelmien kanssa. Huhtikuusta 2020 lähtien Isabelle sisältää kuitenkin edelleen LCF-loogisen järjestelmän toteutuksen - Isabelle/LCF.