Ccg
A powerful automated termination prover for ACL2
In order to see how the CCG analysis works, consider the following
definition of Ackermann's function from exercise 6.15 in the ACL2
textbook:
(defun ack (x y)
(if (zp x)
1
(if (zp y)
(if (equal x 1) 2 (+ x 2))
(ack (ack (1- x) y) (1- y)))))
ACL2 cannot automatically prove the termination of ack using its
measure-based termination proof. In order to admit the function, the user
must supply a measure. An example measure is (make-ord 1 (1+ (acl2s-size
y)) (acl2s-size x)), which is equivalent to the ordinal w * (1+
(acl2s-size y)) + (acl2s-size x), where w is the first infinite
ordinal.
The CCG analysis, on the other hand, automatically proves termination as
follows. Note that there are two recursive calls. These calls, along with
their rulers (i.e. the conditions under which the recursive call is reached)
are called calling contexts, or sometimes just contexts (for
more on rulers, see ruler-extenders). For ack, these are:
1. (ack (1- x) y) with ruler ((not (zp x)) (not (zp y))).
2. (ack (ack (1- x) y) (1- y)) with ruler ((not (zp x)) (not (zp y))).
These calling contexts are used to build a calling context graph
(CCG), from which our analysis derives its name. This graph has an edge
from context c1 to context c2 when it is possible that execution can
move from context c1 to context c2 in one ``step'' (i.e. without
visiting any other contexts). For our example, we get the complete graph, with
edges from each context to both contexts.
The analysis next attempts to guess calling context measures (CCMs),
or just measures, for each function. These are similar to ACL2
measures, in that they are ACL2 terms that must provably be able to evaluate
to an ordinal value (unlike ACL2 measures, CCG currently ignores the current
well-founded relation setting). However, functions may have multiple CCMs,
instead of one, like ACL2, and the CCG analysis has some more sophisticated
heuristics for guessing appropriate measures. However, there is a mechanism
for supplying measures to the CCG analysis if you need to see ccg-xargs. In our example, the CCG analysis will guess the measures
(acl2s-size x), (acl2s-size y), and (+ (acl2s-size x) (acl2s-size
y)). This last one turns out to be unimportant for the termination
proof. However, note that the first two of these measures are components of
the ordinal measure that we gave ACL2 to prove termination earlier. As one
might guess, these are important for the success of our CCG analysis.
Like ACL2's measure analysis, we are concerned with what happens to these
values when a recursive call is made. However, we are concerned not just with
decreasing measures, but also non-increasing measures. Thus, we construct
Calling Context Measure Functions (CCMFs), which tell us how one
measure compares to another across recursive calls.
In our example, note that when the recursive call of the context 1 is made,
the new value of (acl2s-size x) is less than the original value of
(acl2s-size x). More formally, we can prove the following:
(implies (and (not (zp x))
(not (zp y)))
(o< (acl2s-size (1- x))
(acl2s-size x)))
For those of you that are familiar with measure-based termination proofs in
ACL2, this should look familiar, as it has the same structure as such a
termination proof. However, we also note the following trivial
observation:
(implies (and (not (zp x))
(not (zp y)))
(o<= (acl2s-size y)
(acl2s-size y)))
That is, y stays the same across this recursive call. For the other
context, we similarly note that (acl2s-size y) is decreasing. However, we
can say nothing about the value of (acl2s-size x). The CCG algorithm does
this analysis using queries to the theorem prover that are carefully
restricted to limit prover time.
Finally, the CCG analysis uses this local information to do a global
analysis of what happens to values. This analysis asks the question, for every
infinite path through our CCG, c_1, c_2, c_3, ..., is there a
natural number N such that there is an infinite sequence of measures
m_N, m_(N+1), m_(N+2), ... such that each m_i is a measure
for the context c_i (i.e. a measure for the function containing ci),
we have proven that the m_(i+1) is never larger than m_i, and for
infinitely many i, it is the case that we have proven that m_i is
always larger than m_(i+). That's a bit of a mouthful, but what we are
essentially saying is that, for every possible infinite sequence of recursions
it is the case that after some finite number of steps, we can start picking
out measures such that they never increase and infinitely often they
decrease. Since these measures return ordinal values, we then know that there
can be no infinite recursions, and we are done.
For our example, consider two kinds of infinite paths through our CCG:
those that visit context 2 infinitely often, and those that don't. In the
first case, we know that (acl2s-size y) is never increasing, since a
visit to context 1 does not change the value of y, and a visit to context
2 decreases the value of (acl2s-size y). Furthermore, since we visit
context 2 infinitely often, we know that (acl2s-size y) is infinitely
decreasing along this path. Therefore, we have met the criteria for proving no
such path is a valid computation. In the case in which we do not visit context
2 infinitely often, there must be a value N such that we do not visit
context 2 any more after the Nth context in the path. After this, we must
only visit context 1, which always decreases the value of (acl2s-size
x). Therefore, no such path can be a valid computation. Since all infinite
paths through our CCG either visit context 2 infinitely often or not, we have
proven termination. This analysis of the local data in the global context is
done automatically by a decision procedure.
That is a brief overview of the CCG analysis. Note that, can it prove many
functions terminating that ACL2 cannot. It also does so using simpler
measures. In the ack example, we did not require any infinite ordinal
measures to prove termination using CCG. Intuitively, CCG is in a way putting
together the measures for you so you don't have to think about the ordinal
structure. Thus, even when the CCG analysis to prove termination, it is often
easier to give it multiple simple measures and allow it to put together the
global termination argument than to give ACL2 the entire measure so it can
prove that it decreases every single step.
To find out more about interacting and controlling the CCG analysis, see
the topics included in this section.
Subtopics
- Set-ccg-hierarchy
- Set the default hierarchy of techniques for CCG-based termination
analysis.
- Ccg-xargs
- Giving hints to CCG analysis via See xargs
- Set-termination-method
- Set the default means of proving termination.
- Set-ccg-time-limit
- Set a global time limit for CCG-based termination proofs.
- Set-ccg-inhibit-output-lst
- Control output during CCG termination analysis
- Set-ccg-print-proofs
- Controls whether proof attempts are printed during CCG analysis
- Get-termination-method
- Returns the current default termination method.
- Get-ccg-time-limit
- Returns the current default ccg-time-limit setting.
- Get-ccg-print-proofs
- Returns the setting that controls whether proof attempts are printed during
CCG analysis
- Get-ccg-inhibit-output-lst
- Returns the list of ``kinds'' of output that will be inhibited during CCG
analysis
