Rippling
From Wikipedia, the free encyclopedia
Rippling is a family of meta-level heuristics for controlling term rewriting in automated theorem proving systems. Special annotations are employed to control term rewriting. The family was developed (and continues to be developed) in the Mathematical Reasoning Group at the University of Edinburgh. Functional rippling has been implemented in the Clam and IsaPlanner [1] proof planning systems.
Contents |
[edit] History
Raymond Aubin first noticed a pattern during the rewriting of step cases in inductive proofs in his 1976 PhD thesis. He named the pattern rippling-out, in analogy to waves moving across the surface of a loch, leaving a clear reflection in their wake.
Alan Bundy later turned the idea on its head and created the static functional rippling theory that will be explained below.
[edit] Motivation
Gerhard Gentzen's original formulation of the Sequent calculus included the "Cut rule", a rule designed to allow the introduction of an arbitrary formula so long as it can be shown to be a consequence of formulas already known to be true. Whilst useful, this introduces a source of infinite branching in any backwards-directed proof. Gentzen recognised this problem and was able to show that any theorem deduced using the "Cut rule" also had an analogous proof that could be deduced without the use of the "Cut rule" (Gentzen's Cut-elimination theorem).
Unfortunately, Kreisel was able to show that Gentzen's Cut-elimination theorem does not hold in inductive theories. All but the simplest of inductive proofs require use of the "Cut rule", implying that inductive search spaces are more often than not necessarily infinite in size. [2] Specialist strategies, such as rippling, therefore need to be developed in order to control the size of inductive search spaces. Rippling is especially nice in that it can be shown to always terminate. [3]
Although rippling has applications beyond inductive proof, [4] it is the control of rewriting in inductive proofs that has become most associated with the rippling heuristic.
[edit] Basic mechanism
The rippling family is split in two: static and dynamic rippling. Both variants aim to reduce the synactic differences between two expressions. Static rippling broadly works by:
- identifying syntactic differences between two expressions
- annotating these differences with annotations
- annotating rewrite rules with similar annotations
- using the annotations to control and guide rewriting
- exhaustively applying rewrites
The dynamic rippling variant, due to Smaill and Green, works in a slightly different manner:
- finding all possible annotations of expressions at each proof step
- performing all possible rewrites at each proof step
- throwing away all rewrites that do not decrease a measure
Whereas static rippling carries around annotations, dynamic rippling calculates new annotations at each rewrite rule application. This calculation stage creates an inefficiency, but dynamic rippling is more stable than static rippling, i.e. annotations are not stable over beta-reduction in the lambda calculus. [5]
[edit] Notes
- ^ Dixon, L: "A Proof Planning Framework for Isabelle", PhD Thesis, University of Edinburgh, 2005
- ^ Bundy, A: "The Automation of Proof by Mathematical Induction", Chapter 13, Handbook of Automated Reasoning, Elsevier Science Publisher, BV, 2001
- ^ Basin, D and Walsh, T: "A Calculus for an Termination of Rippling", Journal of Automated Reasoning, 16(1-2)147-180, 1996
- ^ Bundy, A and Lombart, V: "Relational Rippling, a General Approach", IJCAI, 175-181, 1995
- ^ Smaill, A and Green, I: "Higher Order Annotated Terms for Proof Search", Theorem Proving in Higher Order Logics, 399-413, 1996
