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

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

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

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

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

(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,

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,

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

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

To find out more about interacting and controlling the CCG analysis, see the topics included in this section.

- 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