Logic for Computable Functions: Difference between revisions

Revision as of 16:28, 30 June 2017

Latest revision as of 18:48, 19 March 2025

(22 intermediate revisions by 17 users not shown)

Line 1:

{{Short description|1970s automated theorem prover}}

{{see also|Logic of Computable Functions}}

'''Logic for Computable Functions''' ('''LCF''') is an interactive [[automated theorem prover]] developed at the[[Stanford universitiesUniversity|Stanford]] ofand [[University of Edinburgh|Edinburgh]] by [[Robin Milner]] and collaborators in early 1970s, based on the theoretical foundation of [[StanfordLogic Universityof Computable Functions|Stanfordlogic of computable functions]] previously proposed by [[RobinDana MilnerScott]]. andWork otherson in 1972.the LCF system introduced the general-purpose [[programming language]] [[ML (programming language)|ML]] to allow users to write theorem-proving tactics., Theorems in the system are terms of a special "theorem"supporting [[abstractalgebraic data type]]. The ML type system ensures that theorems are derived using only thes, [[inferenceparametric rulepolymorphism]]s, given[[abstract bydata thetypes]], operationsand of[[Exception the abstract typehandling|exceptions]].

== Basic idea ==

Successors include [[HOL (proof assistant)|HOL]] (Higher Order Logic) and [[Isabelle (proof assistant)|Isabelle]].

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 rule]]s 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.

== References ==

== Advantages ==

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.

== Disadvantages ==

=== Trusted computing base ===

The implementation of the underlying ML compiler adds to the [[trusted computing base]]. Work on CakeML<ref name="cakeml">{{cite web |title=CakeML |url=https://cakeml.org/ |access-date=2 November 2019}}</ref> resulted in a formally verified ML compiler, alleviating some of these concerns.

=== Efficiency and complexity of proof procedures ===

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.<ref>{{cite report |last1=Boyer |first1=Robert S |last2=Moore |first2=J Strother |title=Metafunctions: Proving Them Correct and Using Them Efficiently as New Proof Procedures |publisher=Technical Report CSL-108, SRI Projects 8527/4079 |pages=1–111 |url=https://apps.dtic.mil/dtic/tr/fulltext/u2/a094385.pdf |archive-url=https://web.archive.org/web/20191102152631/https://apps.dtic.mil/dtic/tr/fulltext/u2/a094385.pdf |url-status=live |archive-date=November 2, 2019 |access-date=2 November 2019}}</ref>

== Influences ==

Among subsequent implementations is Cambridge LCF. Later systems simplified the logic to use total instead of partial functions, leading to [[HOL (proof assistant)|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.

== Notes ==

{{Reflist}}

== References ==

{{Refbegin}}

* {{cite book

| last1 = Gordon

| first1 = Michael J.

| author1link author1-link= Michael J. C. Gordon

| last2 = Milner

| first2 = Arthur J.

| last3 = Wadsworth

| first3 = Christopher P.

| date = 1979

| title = Edinburgh LCF: A Mechanised Logic of Computation

| doi = 10.1007/3-540-09724-4

| series = Lecture Notes in Computer Science

| url = http://dx.doi.org/10.1007/3-540-09724-4

| volume = 78

| ___location =

| publisher = Springer |___location=Berlin Heidelberg

| series = Lecture Notes in Computer Science

| isbn = 978-3-540-09724-2 }}|s2cid=21159098

| volume = 78

}}

| publisher = Springer Berlin Heidelberg

| isbn = 978-3-540-09724-2 }}

* {{cite web

| last = Gordon

| first = Michael J. C.

| year = 1996

| title = From LCF to HOL: a short history

| url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html

| accessdate = 2007-10-11 }}

* {{cite book

| last = Gordon

| last1 = Loeckx

| first = Michael J. C.

| first1 = Jacques

| title chapter= From LCF to HOL: a short history

| last2 = Sieber

| url = http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html

| first2 = Kurt

|title=Proof, language, and interaction

| date = 1987

|pages=169–185

| title = The Foundations of Program Verification

|publisher=MIT Press

| doi = 10.1007/978-3-322-96753-4

| ___location=Cambridge, =Massachusetts

|date=2000

| edition = 2nd

|isbn=0-262-16188-5

| publisher = Vieweg+Teubner Verlag

| accessdate access-date= 2007-10-11 }}

| isbn = 978-3-322-96754-1 }}

* {{cite webbook

| last1 = Loeckx

| first1 = Jacques

| last2 = Sieber

| first2 = Kurt

| date = 1987

| title = The Foundations of Program Verification

| doi = 10.1007/978-3-322-96753-4

| edition = 2nd

| publisher = Vieweg+Teubner Verlag

| isbn = 978-3-322-96754-1 }}

* {{cite manual

|last=Milner |first=Robin |author -link=Robin Milner, Robin

| title = Logic for Computable Functions: description of a machine implementation.

| publisher = Stanford University

| date = May 1972

| url = httphttps://wwwapps.dtic.mil/dtic/tr/fulltextsti/u2pdfs/785072AD0785072.pdf }}

* {{cite book

| last = Milner

| first =Robin |author-link=Robin Milner

| editor = Bečvář, Jiří

| date = 1979

| title = Mathematical Foundations of Computer Science 1979

| chapter = Lcf: A way of doing proofs with a machine

| pages = 146–159

| doi = 10.1007/3-540-09526-8_11

| series = Lecture Notes in Computer Science

| url = http://dx.doi.org/10.1007/3-540-09526-8_11

| volume = 74

| series = Lecture Notes in Computer Science

| publisher = Springer |___location=Berlin Heidelberg

| volume = 74

| isbn = 978-3-540-09526-2}}

| publisher = Springer Berlin Heidelberg

| isbn = 978-3-540-09526-2

| access-date = 16 February 2016 }}

{{Refend}}

{{Mathlogic-stubML programming}}

[[Category:Logic in computer science]]

[[Category:Proof assistants]]

{{Mathlogic-stub}}