1970 жылдарғы автоматты теореманы дәлелдеу жүйесі (LCF)
Logic for Computable Functions
LCF – 1970-жылдарғы автоматты теореманы дәлелдеуші. ML тілін енгізіп, есептеу функциялары логикасын дамытты. Дәлелдеу тактикасы, абстрактілі дерек түрлері.
Логика есептеу функциялары (LCF) – Робин Милнер және оның әріптестері 1970-жылдардың басында Стэнфорд пен Эдинбургте Дана Скотт бұрын ұсынған есептеу функцияларының логикасының теориялық негізінде әзірлеген интерактивті автоматтандырылған теореманы дәлелдеуші. LCF жүйесіндегі жұмыс пайдаланушыларға теореманы дәлелдеу тактикасын жазуға мүмкіндік беретін, алгебралық деректер түрлерін, параметрлік полиморфизмді, абстрактілі деректер түрлерін және қателіктерді қолдайтын ML бағдарламалау тілін енгізді.
Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general purpose programming language ML to allow users to write theorem proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.
Негізгі идея
Жүйедегі теоремалар – арнайы "теорема" абстрактілі дерек типінің мүшелері болып табылады. ML абстрактілі дерек типтерінің жалпы механизмі теоремалардың теорема абстрактілі типінің операцияларымен берілген логикалық қорытынды ережелерін ғана қолдану арқылы туындатынын қамтамасыз етеді. Пайдаланушылар теоремаларды есептеу үшін кез келген күрделі ML бағдарламаларын жаза алады; теоремалардың дұрыстығы мұндай бағдарламалардың күрделілігіне емес, абстрактілі дерек типінің дұрыс іске асырылуына және ML компиляторының дұрыстығына байланысты.
Theorems in the system are terms of a special "theorem" abstract data type. The general mechanism of abstract data types of ML ensures that theorems are derived using only the inference rules given by the operations of the theorem abstract type. Users can write arbitrarily complex ML programs to compute theorems; the validity of theorems does not depend on the complexity of such programs, but follows from the soundness of the abstract data type implementation and the correctness of the ML compiler.
Артықшылықтар
LCF әдісі нақты дәлелдеу сертификаттарын жасайтын жүйелерге ұқсас сенімділікті қамтамасыз етеді, бірақ дәлелдеу нысандарын жадта сақтау қажеттілігін жояды. Теорема дерек типін жүйенің жұмыс уақытына байланысты дәлелдеу нысандарын қалау бойынша сақтау үшін оңай жүзеге асыруға болады, сондықтан ол негізгі дәлелдеу жасау әдісін кеңейтеді. Теоремаларды жасау үшін мақсатына арналған бағдарламалау тілін пайдалану туралы шешім, жазылған бағдарламалардың күрделілігіне қарай, дәл сол тілді қадамдық дәлелдемелерді, шешім қабылдау процедураларын немесе теореманы дәлелдейтін құралдарды жазу үшін қолдануға мүмкіндік береді.
The LCF approach provides similar trustworthiness to systems that generate explicit proof certificates but without the need to store proof objects in memory. The Theorem data type can be easily implemented to optionally store proof objects, depending on the system's run time configuration, so it generalizes the basic proof generation approach. The design decision to use a general purpose programming language for developing theorems means that, depending on the complexity of programs written, it is possible to use the same language to write step by step proofs, decision procedures, or theorem provers.
Сенімді есептеу базасы
ML компиляторының енгізілуі сенімді есептеу базасын кеңейтеді. CakeML жобасы нәтижесінде ресми түрде тексерілген ML компиляторы жасалды, бұл аталған алаңдаушылықтардың бір бөлігін азайтуға мүмкіндік берді.
The implementation of the underlying ML compiler adds to the trusted computing base. Work on CakeML resulted in a formally verified ML compiler, alleviating some these concerns.
Дәлелдік рәсімдердің тиімділігі мен күрделілігі
Теоремаларды дәлелдеу жиі шешімдерді қабылдау процедуралары мен теоремаларды дәлелдеу алгоритмдерінен пайда көреді, олардың дұрыстығы жан-жақты талданған. LCF тәсілінде осы процедураларды іске асырудың тікелей жолы – осы процедуралардың нәтижелерді жүйенің аксиомаларынан, леммаларынан және логикалық қорытынды шығару ережелерінен алуын талап етеді, нәтижені тікелей есептеуден гөрі. Ықтимал тиімдірек тәсіл – формулалармен жұмыс істейтін функцияның әрқашан дұрыс нәтиже беретінін дәлелдеу үшін рефлексияны қолдану болып табылады.
Theorem proving often benefits from decision procedures and theorem proving algorithms, whose correctness has been extensively analyzed. A straightforward way of implementing these procedures in an LCF approach requires such procedures to always derive outcomes from the axioms, lemmas, and inference rules of the system, as opposed to directly computing the outcome. A potentially more efficient approach is to use reflection to prove that a function operating on formulas always gives correct result.
Әсерлер
Кейінгі енгізілімдердің бірі – Кембридж LCF. Келесі жүйелер логиканы қарапайымдастырып, толық функцияларды, жартылай функциялардың орнына пайдаланды, нәтижесінде HOL, HOL Light және түрлі логикаларды қолдайтын Isabelle дәлелдеу құралы пайда болды. 2019 жылғы мәліметтер бойынша, Isabelle дәлелдеу құралында LCF логикасының енгізілімі әлі де сақталып, Isabelle/LCF ретінде қолданылады.
Among subsequent implementations is Cambridge LCF. Later systems simplified the logic to use total instead of partial functions, leading to HOL, HOL Light, and the Isabelle proof assistant that supports various logics. As of 2019, the Isabelle proof assistant still contains an implementation of an LCF logic, Isabelle/LCF.