Set-ccg-hierarchy
Set the default hierarchy of techniques for CCG-based termination
analysis.
(set-ccg-hierarchy ((:built-in-clauses :equal t)
(:measure (:induction-depth 1))
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t)
((:induction-depth 1) :EQUAL nil)
((:induction-depth 1) :ALL nil)
((:induction-depth 1) :SOME nil)
((:induction-depth 1) :NONE nil)))
:set-ccg-hierarchy ((:built-in-clauses :equal t)
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t))
General Form:
(set-ccg-hierarchy v)
where v is :CCG-ONLY, :CCG-ONLY-CPN, :HYBRID,
:HYBRID-CPN, or a non-empty list of hierarchy levels, which either have
the form (pt ccm-cs cpn) or the form (:measure pt), where pt is
either :built-in-clauses or (:induction-depth n) for some natural
number n, ccm-cs is one of :EQUAL, :ALL, :SOME, or
:NONE, and cpn is t or nil.
Each level of the hierarchy describes techniques used to prove
termination. Termination proofs performed after admitting this event will use
the specified techniques in the order in which they are listed.
Basically, the CCG analysis as described and illustrated at a high level in
the documentation for ccg can potentially be very expensive. In order
to make the analysis as efficient as possible, we use less expensive (and less
powerful) techniques first, and resort to more powerful and expensive
techniques only when these fail.
There are three ways of varying the CCG analysis, which are represented by
each of the three elements in a hierarchy level (levels of the form
(:measure pt) will be explained later).
Pt tells the CCG analysis how to limit proof attempts. The idea behind
this is that ACL2 is designed to prove statements that the user thinks are
true. It therefore does everything it can to prove the conjecture. As ACL2
useres already know, this can lead to very long, or even non-terminating proof
attempts. The CCG analysis, on the other hand, sends multiple queries to the
theorem prover that may or may not be true, in order to improve the accuracy
of the analysis. It is therefore necessary to reign in ACL2's proof attempts
to keep them from taking too long. Of course, the trade-off is that, the more
we limit ACL2's prover, the less powerful it becomes.
Pt can be :built-in-clauses, which tells ACL2 to use only built-in-clauses analysis. This is a very fast, and surprisingly powerful
proof technique. For example, the definition of Ackermann's function given in
the documentation for ccg is solved using only this proof
technique.
Pt can also be of the form (:induction-depth n), where n is
a natural number. This uses the full theorem prover, but limits it in two
ways. First, it stops proof attempts if ACL2 has been working on a subgoal
with no case splitting or induction for 20 steps (that is, at a goal of the
form 1.5'20'). It also limits the induction depth, which describes how
many times we allow induction goals to lead to further induction goals. For
example, (:induction-depth 0) allows no induction, while
(:induction-depth 1) allows goals of the form *1 or *2, but
stops if it creates a goal such as *1.1 or *2.1.
Ccm-cs limits which CCMs are compared using the theorem
prover. Consider again the ack example in the documentation for ccg. All we needed was to compare the value of (acl2s-size x) before and
after the recursive call and the value of (acl2s-size y) before and after
the recursive call. We would learn nothing, and waste time with the theorem
prover if we compared (acl2s-size x) to (acl2s-size y). However,
other times, it is important to compare CCMs with each other, for example,
when arguments are permuted, or we are dealing with a mutual recursion.
Ccm-cs can be one of :EQUAL, :ALL, :SOME, or
:NONE. These limit which CCMs we compare based on the variables they
mention. Let c be a recursive call in the body of function f that
calls function g. Let m1 be a CCM for f and m2 be a CCM
for g. Let v1 be the formals mentioned in m1 and v2 be the
formals mentioned in m2' where m2' is derived from m2 by
substituting the formals of g with the actuals of c. For example,
consider following function:
(defun f (x)
(if (endp x)
0
(1+ (f (cdr x)))))
Now consider the case where m1 and m2 are both the measure
(acl2s-size x). Then if we look at the recursive call (f (cdr x)) in
the body of f, then m2' is the result of replacing x with
(cdr x) in m2, i.e., (acl2s-size (cdr x)).
If ccm-cs is :EQUAL we will compare m1 to m2 if v1
and v2 are equal. If value is :ALL we will compare m1 to
m2' if v2 is a subset of v1. If value is :SOME we
will compare m1 to m2' if v1 and v2 intersect. If
value is :NONE we will compare m1 to m2 no matter
what.
There is one caveat to what was just said: if m1 and m2 are
syntactically equal, then regardless of the value of ccm-cs we will
construct a CCMF that will indicate that (o>= m1 m2).
Cpn tells us how much ruler information we will use to compare CCMs.
Unlike ACL2's measure-based termination analysis, CCG has the ability to use
the rulers from both the current recursive call the next recursive call when
constructing the CCMFs. That is, instead of asking ``What happens when I make
recursive call A?'', we can ask, ``What happens when execution moves from
recursive call A to recursive call B?''. Using this information potentially
strengthens the termination analysis. For a brief example, consider the
following code:
(defun half (x)
(if (zp x)
0
(1+ (half (- x 2)))))
Clearly this is terminating. If we choose a measure of (nfix x) we
know that if x is a positive integer, (nfix (- x 2)) is less than
(nfix x). But consider the measure (acl2s-size x). The strange thing
here is that if x is 1, then (acl2s-size (- x 2)) is (acl2s-size
-1), which is 1, i.e. the acl2s-size of x. So, the fact that we
know that x is a positive integer is not enough to show that this measure
decreases. But notice that if x is 1, we will recur just one more
time. So, if we consider what happens when we move from the recursive call
back to itself. In this case we know (and (not (zp x)) (not (zp (- x
2)))). Under these conditions, it is trivial for ACL2 to prove that
(acl2s-size (- x 2)) is always less than (acl2s-size x).
However, this can make the CCG analysis much more expensive, since information
about how values change from step to step are done on a per-edge, rather than
a per-node basis in the CCG (where the nodes are the recursive calls and the
edges indicate that execution can move from one call to another in one
step). Thus, calculating CCMFs (how values change across recursive calls) on a
per-edge basis rather than a per-node basis can require n^2 instead of n
prover queries.
If cpn is t, we will use only the ruler of the current recursive
call to compute our CCMFs. If it is nil, we will use the much more
expensive technique of using the rulers of the current and next call.
Levels of the hierarchy of the form (:measure pt) specify that the CCG
analysis is to be set aside for a step, and the traditional measure-based
termination proof is to be attempted. Here, pt has the same meaning as it
does in a CCG hierarchy level. That is, it limits the measure proof in order
to avoid prohibitively long termination analyses.
The user may specify their own hierarchy in the form given above. The main
restriction is that no level may be subsumed by an earlier level. That is, it
should be the case at each level of the hierarchy, that it is possible to
discover new information about the CCG that could help lead to a termination
proof.
In addition to constructing his or her own CCG hierarchy, the user may use
several preset hierarchies:
:CCG-ONLY
((:built-in-clauses :equal t)
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t)
((:induction-depth 1) :EQUAL nil)
((:induction-depth 1) :ALL nil)
((:induction-depth 1) :SOME nil)
((:induction-depth 1) :NONE nil))
:CCG-ONLY-CPN
((:built-in-clauses :equal t)
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t))
:HYBRID
((:built-in-clauses :equal t)
(:measure (:induction-depth 1))
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t)
((:induction-depth 1) :EQUAL nil)
((:induction-depth 1) :ALL nil)
((:induction-depth 1) :SOME nil)
((:induction-depth 1) :NONE nil))
:HYBRID-CPN
((:built-in-clauses :equal t)
(:measure (:induction-depth 1))
((:induction-depth 0) :EQUAL t)
((:induction-depth 1) :EQUAL t)
((:induction-depth 1) :ALL t)
((:induction-depth 1) :SOME t)
((:induction-depth 1) :NONE t))
The default hierarchy for CCG termination analysis is :CCG-ONLY.
