1. What is the LCF paradigm?
The LCF paradigm is a method of implementing a tool to support formal reasoning in some logic.
LCF stands both for Logic for Computable Functions (which is the name of a logic devised by Dana Scott) and for a proof tool implemented originally at the University of Edinburgh to support reasoning in the logic. There may be differing views about which features of that tool are essential ingredients of the paradigm, here I take a minimal position so that the LCF paradigm encompasses a broad collection of possible tools. 4. Functional MetaLanguage For the original LCF implementation a new functional language (called ML) was designed and implemented to serve as a metalanguage. ML was used to implement the abstract data type which guarantees the correctness of the theorems computed. ML was also made available both to the LCF system developers and to end-users to program techniques for automatically constructing proofs. 6. Use of Higher Order Functions The LCF paradigm encourages the use of higher level functions in a wide variety of ways creating a proof development environment with powerful abstract high level functionality which can be adapted to the needs of various problems or domains. Tactics and derived inference rules are among the simpler kinds of higher order function employed. |
2. Proof as Computation
The first element of the LCF paradigm is to treat a proof as a computation which computes new theorems from previously established theorems.
The key feature of the paradigm is that it permits a powerful programming language to be used in programming inferences in a way which ensures that the inferences thus programmed are guaranteed sound.
The technique for guaranteeing soundness is the use of an abstract data type.
3. Logic as Abstract DataType A Logic is represented in the LCF paradigm by an abstract data type of theorems. The abstract data type has constructors for the type of theorems which correspond precisely to the axioms and inference rules in the chosen logic, with the effect that every computation of a value of type theorem corresponds to a proof of a result in the logic. 5. Tactics The original LCF system and its descendents also have Tactics, which are one way of organising the search for a proof of some conjecture. Tactics accept a conjecture (called a "goal") and compute a number of (hopefully) simpler conjectures from which the original conjecture can be derived, together with a function which is capable of performing the required derivation if supplied with theorems corresponding to the conjectures. Tactics are just one of many ways in which the search for proofs in an LCF-like proof system can be organised and may not be considered an essential feature of the LCF paradigm. |