Logic for Computable Functions (LCF) is an interactive

automated theorem prover Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a m ...

developed at

Stanford Stanford University, officially Leland Stanford Junior University, is a Private university, private research university in Stanford, California. The campus occupies , among the largest in the United States, and enrolls over 17,000 students. S ...

and

Edinburgh Edinburgh ( ; gd, Dùn Èideann ) is the capital city of Scotland and one of its 32 Council areas of Scotland, council areas. Historically part of the county of Midlothian (interchangeably Edinburghshire before 1921), it is located in Lothian ...

Robin Milner Arthur John Robin Gorell Milner (13 January 1934 – 20 March 2010), known as Robin Milner or A. J. R. G. Milner, was a British computer scientist, and a Turing Award winner.

and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by

Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...

. Work on the LCF system introduced the general-purpose

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

ML to allow users to write theorem-proving tactics, supporting

algebraic data type In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types. Two common classes of algebraic types are product types (i.e., ...

parametric polymorphism In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...

abstract data types In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, p ...

, and exceptions.

Basic idea

Theorems in the system are terms of a special "theorem"

abstract data type In computer science, an abstract data type (ADT) is a mathematical model for data types. An abstract data type is defined by its behavior (semantics) from the point of view of a ''user'', of the data, specifically in terms of possible values, pos ...

. The general mechanism of abstract data types of ML ensures that theorems are derived using only the

inference rule In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...

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.

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 resulted in a formally verified ML compiler, alleviating some 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.

Influences

Among subsequent implementations is Cambridge LCF. Later systems simplified the logic to use total instead of partial functions, leading to

HOL Hol is a municipality in Viken county, Norway. Administrative history The area of Hol was separated from the municipality Ål in 1877 to become a separate municipality. In 1937 a part of neighboring Uvdal with 220 inhabitants moved to Hol munic ...

HOL Light HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations. HOL Light is ...

, 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

References

* * * * * {{Mathlogic-stub Logic in computer science Proof assistants