4 ms·
To follow up: I believe the original paper introducing tactics is Milner's still excellent "The Use of Machines to Assist in Rigorous Proof" from 1984 [1]. The
by momentoftop 6y ago
To follow up: I believe the original paper introducing tactics is Milner's still excellent "The Use of Machines to Assist in Rigorous Proof" from 1984 [1].
The basic idea is that a "tactic" is a function which inputs some abstract goal and outputs a pair consisting of subgoals and a mechanism by which the solutions to those subgoals can be combined into a solution to the original goal. This is a very general notion, but it was mostly influential in Milner's style of theorem prover. To this day, most proofs in HOL systems such as HOL4 and HOL Light are just combinations of tactics.
That tactics could potentially be used in Haskell is just a reflection of the fact that Haskell's type system has a connection to propositional logic, where Milner's tactics become a mechanism by which to come up with a program (solution) matching a type (goal).
There's nothing buzzwordy about this.
[1] https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstract https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstra...
- ImprobableTruth 6y agoEdinburgh LCF already had tactics, both the book about it and the paper "A Metalanguage for Interactive Proof in LCF" from 1978 mention it and I wouldn't be surprised if there was an even earlier mention. Pretty crazy to think about how ML was devised to allow a safe working with tactics.
- momentoftop 6y agoOh wow! The paper [1] already introduces "tacticals", being functions from tactics to tactics that give you a very powerful language for composing tactics, and its examples are still very close to what you would see in things like HOL Light: (REPEAT GENTAC) THEN REPEAT (ANYCASESTAC THEN SIMPTAC). Every one of these identifiers is an ordinary ML function. "THEN" is infix. REPEAT : tactic -> tactic GENTAC : tactic ANYCASESTAC : tactic THEN : tactic -> tactic -> tactic SIMPTAC : tactic [1] http://www-public.imtbs-tsp.eu/~gibson/Teaching/CSC4504/ReadingMaterial/GordonMMNW78.pdf http://www-public.imtbs-tsp.eu/~gibson/Teaching/CSC4504/Read...