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

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

*induction depth*, which describes how
many times we allow induction goals to lead to further induction goals. For
example,

(defun f (x) (if (endp x) 0 (1+ (f (cdr x)))))

Now consider the case where

If

There is one caveat to what was just said: if

(defun half (x) (if (zp x) 0 (1+ (half (- x 2)))))

Clearly this is terminating. If we choose a measure of

If

Levels of the hierarchy of the form

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.