| Logica pentru funcții calculabile | |
|---|---|
| Tip de | Demonstrator de teoreme |
| Dezvoltator | Robin Milner și alții |
| Scris in | ML |
| Prima editie | începutul anilor 1970 |
| Platformă hardware | multiplatformă |
Logic for Computable Functions ( Logica rusă pentru funcții calculabile ), (LCF) este un instrument automat interactiv de demonstrare a teoremei dezvoltat de Robin Milner și asociații săi la Stanford și Edinburgh la începutul anilor 1970 pe baza sistemului deductiv cu același nume propus de Dana Scott . În cursul lucrărilor la sistemul LCF, a fost dezvoltat un limbaj de programare universal ML . Utilizarea sa în sistem a permis utilizatorilor să scrie tactici de demonstrare a teoremelor care acceptă tipuri de date algebrice, polimorfism parametric, tipuri de date abstracte și excepții.
Teoremele în limbajul sistemului sunt reprezentate prin termeni care au un tip special „teoremă”. Mecanismul tipului de date abstracte ML prevede inferența teoremelor folosind regulile de inferență date de operațiile care sunt definite pentru tipul abstract „teoremă”. Utilizatorii pot scrie programe arbitrar complexe în ML pentru a calcula teoreme; adevărul teoremelor nu depinde însă de complexitatea unor astfel de programe. Rezultă din corectitudinea implementării tipului de date abstracte și a compilatorului ML însuși.
Abordarea LCF oferă o fiabilitate a dovezii similară cu sistemele care generează proceduri explicite de demonstrare a teoremei pas cu pas, dar nu este nevoie să stocați în memorie toate obiectele intermediare și structurile de date legate de demonstrație. Persistența acestor obiecte și structuri de date, totuși, poate fi ușor implementată sau reconfigurată în funcție de configurația sistemului în timpul rulării. Acest lucru vă permite să generalizați și să faceți procedura de bază pentru generarea unei dovezi cât mai flexibile posibil. Utilizarea unui limbaj de programare cu scop general pentru dezvoltarea teoremelor asigură universalitatea abordării și vă permite să utilizați derivarea demonstrațiilor direct în orice program de uz general.
Implementarea compilatorului ML subiacent se bazează pe o încredere postulată în nucleul logic al sistemului, care trebuie acceptată ca corectă fără justificare. Proiectul CakeML Compiler a dezvoltat un compilator care a fost verificat oficial pentru a funcționa corect. Aceasta a devenit o soluție parțială a problemei specificate [1] .
Demonstrarea teoremei în cadrul abordării LCF se bazează în principal pe proceduri de decizie și algoritmi de demonstrare a teoremei, a căror corectitudine trebuie verificată cu atenție. Cel mai corect stil de implementare a acestor proceduri în LCF necesită ca astfel de proceduri să deducă întotdeauna rezultate din axiomele, lemele și regulile de inferență ale sistemului, mai degrabă decât să calculeze rezultatul direct. O abordare potențial mai eficientă este utilizarea reflecției pentru a genera dovada că aceste proceduri funcționează corect [2] .
Există o serie de implementări derivate ale sistemului, în special - Cambridge LCF. Sistemele ulterioare influențate de LCF au luat calea utilizării versiunilor mai simple ale logicii decât sistemul original. Acest lucru poate fi atribuit, în special, unor instrumente de demonstrare a teoremei precum HOL , HOL Light și Isabelle , care acceptă lucrul cu diferite sisteme deductive. Cu toate acestea, din aprilie 2020, Isabelle include încă o implementare a sistemului logic LCF - Isabelle/LCF.