Definductor
Create an induction scheme for a loop$-recursive function
Definductor is a utility provided as part of the community
book projects/apply/top, which should be included in any session dealing
with apply$, loop$, or loop$-recursion.
(Definductor fn) attempts to create an induction scheme appropriate for
the previously defined loop$-recursive function fn and prove an
:induction rule so that certain calls of fn suggest that
induction.
Warning: Definductor currently handles a very small class of
loop$-recursive functions and may produce unhelpful error messages when
given a function name outside of that class! We hope to improve it and this
documentation as we all get more experience with loop$s and
loop$-recursion.
Examples:
(definductor copy-nat-tree)
(definductor copy-nat-tree
:measure (my-measure x)
:hints (("Goal" :use ...)))
General Form:
(definductor name &key measure well-founded-relation ruler-extenders hints)
where name is the name of a previously admitted loop$-recursive
function satisfying the restrictions listed below. When successful it
defines a function named name-INDUCTOR that suggests an induction scheme
that is supposedly appropriate for name, admits it with a silent proof
of its measure theorems, and then proves an :induction rule to
associate that scheme with calls of name. When omitted, the optional
keyword arguments measure, well-founded-relation, and
ruler-extenders default to the measure, well-founded relation, and
ruler-extender settings used in the admittance of name. The keyword
argument hints defaults to nil. Note that an appropriate choice of
ruler-extenders can improve some induction schemes. See induction-coarse-v-fine-grained.
Restrictions
The given function, name, must satisfy the following restrictions.
Note: Because we anticipate this utility being further developed in the
near future this list may not correspond to the latest implementation!
- Name must be a symbol naming a previously admitted loop$-recursive
function.
- Every recursive loop$ in the body of name -- that is, every
loop$ that calls name recursively in the when, until, or
body clauses of the loop$ -- must have as its target(s) distinct
measured variables or cdr-nests around such variables.
- Every recursive loop$ must use IN-iteration, not ON- or
FROM/TO/BY-iteration.
While definductor can handle loop$ containing multiple AS
clauses (with targets as described above), it cannot handle loop$ such
as
(loop$ for v in (target x) ...)
(loop$ for v on x ...)
(loop$ for i from 1 to max ...)
To see the inductor function generated, type :pe name-INDUCTOR. To
see examples of the use of definductor inspect the book
projects/apply/definductor-tests.lisp. To see the definition of
definductor, see projects/apply/definductor.lisp.
Suggestions for improvements are welcome! We know of many, including
allowing the user to specify a different name for the inductor function,
improving the error messages, printing out the generated defun in the
event of failure to admit it, and trying to expand the class of
loop$-recursive functions that can be successfully handled. We have not
yet even looked at inductions for ON loop$s and FROM/TO/BY
loop$s, so that might be easy. Induction for loop$s over arbitrary
target expressions may be infeasible! We just need more examples of
loop$-recursive functions and successful (hand-written) induction hints
for them.
