PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:25Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:LCF and the tactic idea}}		{{DISPLAYTITLE:LCF and the tactic idea}}
			{{Lean theorem prover map}}
	LCF was a proof checker built by Robin Milner, first at Stanford in 1972 and then, in a new design, at Edinburgh. Two ideas from the Edinburgh design run through many proof assistants since: a protected type of theorems, so that only the rules of the logic can produce one, and tactics, programs that reduce a goal to simpler goals. To make tactics programmable, Milner and his colleagues designed a programming language, ML. This page follows those ideas from 1972 to Lean.		LCF was a proof checker built by Robin Milner, first at Stanford in 1972 and then, in a new design, at Edinburgh. Two ideas from the Edinburgh design run through many proof assistants since: a protected type of theorems, so that only the rules of the logic can produce one, and tactics, programs that reduce a goal to simpler goals. To make tactics programmable, Milner and his colleagues designed a programming language, ML. This page follows those ideas from 1972 to Lean.

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:12Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:LCF and the tactic idea}}
LCF was a proof checker built by Robin Milner, first at Stanford in 1972 and then, in a new design, at Edinburgh. Two ideas from the Edinburgh design run through many proof assistants since: a protected type of theorems, so that only the rules of the logic can produce one, and tactics, programs that reduce a goal to simpler goals. To make tactics programmable, Milner and his colleagues designed a programming language, ML. This page follows those ideas from 1972 to Lean.

== Stanford LCF ==

"LCF" stands for Logic for Computable Functions, Milner's name for a logic Dana Scott devised in 1969 for reasoning about recursively defined functions; Scott's manuscript was not published until 1993.<ref name="gordon2000">Mike Gordon, "From LCF to HOL: a short history", in G. Plotkin, C. Stirling and M. Tofte (eds.), ''Proof, Language, and Interaction: Essays in Honour of Robin Milner'', MIT Press, 2000. Author's copy: https://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf</ref> Milner built the first checker for it at Stanford in 1972, with Whitfield Diffie, Richard Weyhrauch and Malcolm Newey. His report of that year describes it as an interactive program for generating formal proofs about computable functions, helped by a subgoaling facility and a simplifier.<ref name="gordon2000" /><ref name="milner1972">Robin Milner, ''Logic for Computable Functions: Description of a Machine Implementation'', Stanford Artificial Intelligence Memo AIM-169, Computer Science Report STAN-CS-72-288, Stanford University, May 1972. http://i.stanford.edu/pub/cstr/reports/cs/tr/72/288/CS-TR-72-288.pdf</ref>

A user stated a goal and split it into subgoals with a fixed set of commands, such as induction, until the simplifier could finish each one. Gordon names two limits of the system. The proofs it stored filled the available memory, and its fixed set of proof commands could not easily be extended.<ref name="gordon2000" />

== Edinburgh LCF and the type of theorems ==

Around 1973 Milner moved to Edinburgh and began a successor, Edinburgh LCF, first with Lockwood Morris and Malcolm Newey, and from 1975 with Christopher Wadsworth and Mike Gordon.<ref name="gordon2000" />

The answer to the first limit was to keep theorems and discard proofs. To keep that safe, Milner made '''theorem''' an abstract data type. Its only given values were instances of the axioms, and its only operations were the rules of inference. A program could hold a value of type theorem only if it had obtained it from axioms by applying rules, so type checking alone guaranteed that every such value was a theorem of the logic.<ref name="gordon2000" /> The steps of a proof were carried out but not recorded. The guarantee lies in the programming language, not in a stored proof that someone else could check later.

== ML, tactics and tacticals ==

The answer to the second limit was a programming language in which users could write their own proof procedures. Milner, with Morris and Newey, designed '''ML''', the "Meta Language", strictly typed so that the abstract type of theorems could not be circumvented.<ref name="gordon2000" /> It was described at the 1978 Symposium on Principles of Programming Languages.<ref name="popl1978">M. Gordon, R. Milner, L. Morris, M. Newey and C. Wadsworth, "A metalanguage for interactive proof in LCF", in ''Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '78)'', ACM, 1978, pp. 119–130. doi:10.1145/512760.512773</ref> Milner's account of ML's polymorphic type inference appeared the same year.<ref name="milner1978">Robin Milner, "A theory of type polymorphism in programming", ''Journal of Computer and System Sciences'' 17 (3), 1978, pp. 348–375. doi:10.1016/0022-0000(78)90014-4</ref>

In ML a strategy for reducing a goal to subgoals is a function, which Milner called a '''tactic'''. Operations that combine strategies, taking tactics as arguments and returning tactics, are higher-order functions, which he called '''tacticals'''. Since a tactic may be applied to a goal it cannot handle, ML was given exceptions, so that a failing tactic could signal failure and another be tried. Gordon records that the needs of theorem proving shaped the first ML in detail.<ref name="gordon2000" />

The work was written up as ''Edinburgh LCF'' by Gordon, Milner and Wadsworth in 1979.<ref name="lcf1979">Michael J. Gordon, Robin Milner and Christopher P. Wadsworth, ''Edinburgh LCF: A Mechanised Logic of Computation'', Lecture Notes in Computer Science 78, Springer, 1979. doi:10.1007/3-540-09724-4</ref> In 1991 Milner received the ACM Turing Award; the citation names LCF, "probably the first theoretically based yet practical tool for machine-assisted proof construction", and ML among his achievements.<ref name="turing1991">Announcement of the 1991 ACM Turing Award to Robin Milner, with the short citation, forwarded to the TYPES mailing list, 1 November 1991. https://www.engineering.upenn.edu/~sweirich/types/archive/1991/msg00062.html</ref>

== Descendants ==

'''Cambridge LCF.''' In the early 1980s Lawrence Paulson at Cambridge and Gérard Huet in France reworked the system together. Huet improved and extended ML, and his group went on to develop Caml. Paulson's version, Cambridge LCF, was completed around 1985 and described in his 1987 book ''Logic and Computation''.<ref name="gordon2000" />

'''HOL.''' Gordon adapted Cambridge LCF to classical higher-order logic for verifying hardware. HOL kept LCF's syntax, its abstract type of theorems and its tactics, but read types as ordinary sets. A stable version, HOL88, appeared in about 1988. Reimplementations followed: HOL90, in Standard ML, by Konrad Slind, and HOL Light, in Caml Light, by John Harrison and Konrad Slind.<ref name="gordon2000" /> In 2017 Ebner and colleagues noted that HOL4 and HOL Light still work in the original LCF manner, with the user interacting directly in ML.<ref name="ebner2017">Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad and Leonardo de Moura, "A metaprogramming framework for formal verification", ''Proceedings of the ACM on Programming Languages'' 1 (ICFP), article 34, 2017. doi:10.1145/3110278. Author's copy: https://lean-lang.org/papers/tactic.pdf</ref>

'''Isabelle.''' Paulson then built Isabelle, a generic prover in which the rules of many logics are stated declaratively in a common metalogic and combined by higher-order unification.<ref name="gordon2000" /><ref name="paulson1989">Lawrence C. Paulson, "The foundation of a generic theorem prover", ''Journal of Automated Reasoning'' 5 (3), 1989, pp. 363–397. doi:10.1007/BF00248324. Preprint: https://arxiv.org/abs/cs/9301105</ref> Gordon notes that Isabelle keeps Milner's key idea, the abstract type of theorems, and lifts it to the metalogic.<ref name="gordon2000" />

'''Type theories.''' The LCF method, with ML as its metalanguage, was also applied to logics quite unlike Scott's. Gordon lists Nuprl, a proof system for Martin-Löf type theory, and one for the Calculus of Constructions among the LCF-style systems.<ref name="gordon2000" /> Those are the subjects of [[Lean theorem prover/History/Martin-Löf type theory|Martin-Löf type theory]] and [[Lean theorem prover/History/The Calculus of Constructions|The Calculus of Constructions]].

== The line to Lean ==

Lean took the tactic idea and changed where the guarantee lies. In Lean, as in Automath, a proof is a term of the type that states the theorem. Tactics are instructions that describe how to construct such a term, and they support writing a proof incrementally, one step at a time.<ref name="tpil">Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, ''Theorem Proving in Lean 4'', chapter "Tactics". https://lean-lang.org/theorem_proving_in_lean4/tactics.html</ref> The first description of Lean, in 2015, presents tactics as one way, beside writing terms directly, of constructing proof terms, as in Coq, HOL Light, Isabelle and PVS, and describes Lean's small trusted kernel and proof terms that can be checked independently.<ref name="lean2015">Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, "The Lean Theorem Prover (system description)", in ''Automated Deduction – CADE-25'', Lecture Notes in Computer Science 9195, Springer, 2015, pp. 378–388. doi:10.1007/978-3-319-21401-6_26. Author's copy: https://lean-lang.org/papers/system.pdf</ref> In LCF a faulty tactic is stopped by the type discipline of ML; in Lean whatever term a tactic produces must still pass Lean's kernel. The two arrangements are compared at [[Lean theorem prover/Explainers/What has to be trusted|What has to be trusted]].

Lean also took the metalanguage idea, but made the metalanguage Lean itself. The 2017 paper on Lean 3's metaprogramming framework recalls that ML was designed as the metalanguage for LCF, and describes tactics written in Lean, in the same files and with the same library as the mathematics they serve.<ref name="ebner2017" /> Lean 4 goes further: it is implemented largely in Lean, and users can extend its parser, elaborator and tactics in Lean.<ref name="lean4">Leonardo de Moura and Sebastian Ullrich, "The Lean 4 Theorem Prover and Programming Language (System Description)", in ''Automated Deduction – CADE 28'', Lecture Notes in Computer Science 12699, Springer, 2021, pp. 625–635. doi:10.1007/978-3-030-79876-5_37. Author's copy: https://lean-lang.org/papers/lean4.pdf</ref> How tactics work in Lean today is described at [[Lean theorem prover/Explainers/Tactics|Tactics]] and [[Lean theorem prover/System/The tactic framework|The tactic framework]].

<blockquote>
Provenance: Gordon's 2000 history, the Lean papers of 2015, 2017 and 2021 and the tactics chapter of ''Theorem Proving in Lean 4'' were read for this page. Milner's 1972 report was read in its opening pages only. Milner's 1978 paper was read in its opening pages, and Paulson's 1989 paper in its preprint (abstract and history). The 1978 POPL paper and the 1979 book were not opened; their details come from Gordon's reference list and the publishers' records. The account of Stanford and Edinburgh LCF follows Gordon, a participant from 1975.
</blockquote>

== Next ==

[[Lean theorem prover/History/Martin-Löf type theory|Martin-Löf type theory]]

== References ==
<references />

Lean theorem prover/History/LCF and the tactic idea - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source