The name LCF architecture (or LCF-style) refers to an "architecture" for any kind of software that implements logic, e.g. a theorem prover or a proof assistant.
The central idea of the LCF architecture is to only allow the construction of theorems through constructors of an abstract data type.
As such, the LCF architecture only allows correct theorems to be proven. It often also conveniently forgets the proof object at every step, so as to reduce memory usage.
Here is a description of the LCF style found in [Gordon 2000]:
[...] he had the idea that instead of saving whole proofs, the system should just remember the results of proofs, namely theorems. The steps of a proof would be performed but not recorded, like a mathematics lecturer using a small blackboard who rubs out earlier parts of proofs to make space for later ones. To ensure that theorems could only be created by proof, Milner had the brilliant idea of using an abstract data type whose predefined values were instances of axioms and whose operations were inference rules. Strict typechecking then ensured that the only values that could be created were those that could be obtained from axioms by applying a sequence of inference rules – namely theorems.
The following example comes from the slides of a 2001 talk by John Harrison.
Here is an ML module for basic equational theories:
module type Birkhoff =
sig type thm
val axiom : formula -> thm
val inst : (string, term) func -> thm -> thm
val refl : term -> thm
val sym : thm -> thm
val trans : thm -> thm -> thm
val cong : string -> thm list -> thm
val dest_thm : thm -> formula list * formula
end;;
The signature introduces a data type thm of theorems, and a number of operations that correspond to basic inference rules. Unlike later indexed representations of logical theories, there is no guarantee that e.g. trans : thm -> thm -> thm will only be applied to theorems whose RHS and LHS correspondingly match up (e.g. and ).
However, this will be guaraded for by the kernel (or core) implementation of this ADT. For example:
module Proven : Birkhoff =
struct
type thm = formula list * formula
let axiom p =
match p with
Atom("=", [s; t]) -> ([p], p)
| _ -> failwith "axiom: not an equation"
let inst i (asm, p) = (asm, formsubst i p)
let refl t = ([], Atom("=",[t;t]))
let sym (asm, Atom("=",[s;t])) = (asm, Atom("=",[t;s]))
let trans
(asm1, Atom("=",[s;t]))
(asm2, Atom("=",[t’;u])) =
if t’ = t then (union asm1 asm2,Atom("=", [s; u]))
else failwith "trans: theorems don’t match up"
let cong f ths =
let asms,eqs =
unzip(map (
fun (asm, Atom("=",[s; t])) -> asm,(s,t)
) ths)
in
let ls,rs = unzip eqs in
(unions asms,Atom("=", [Fn(f, ls); Fn(f, rs)]))
let dest_thm th = th
end;;
This implementation represents thm by a pair of a list of formulas (the assumptions) and a single formula (the conclusion).
In the case of trans, this implementation dynamically checks that the sides of the two equations match up. If they do not, it fails by throwing an exception. But if they do, it collects the assumptions that were used to prove the two equations, and returns the final theorem , forgetting the two equations and that were used to prove it.
Thus, this implementation allows one to (hopefully) only derive correct theorems, without storing their entire proof.
The term originates from Edinburgh LCF, which introduced multiple technical innovations, including the first programming language of the ML family.
However, the most distinctive of these is the ADT representation of theorems, and this is what is commonly meant by referring to the LCF style.
Gordon, Mike. 2000. ‘From LCF to HOL: A Short History’. In Proof, Language, and Interaction: Essays in Honour of Robin Milner, edited by Gordon Plotkin, Colin P. Stirling, and Mads Tofte. https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf.
@incollection{gordon_2000,
title = {From {LCF} to {HOL}: a short history},
url = {https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf},
booktitle = {Proof, {Language}, and {Interaction}: {Essays} in {Honour} of {Robin} {Milner}},
author = {Gordon, Mike},
editor = {Plotkin, Gordon and Stirling, Colin P. and Tofte, Mads},
year = {2000}
}