TAU-SYSTEM

make a rule for the ACL2 ``type checker'' 
Major Section:  RULE-CLASSES

This documentation topic describes the syntactic form of ``tau-system'' rules; these rules extend ACL2's ``type checker.'' For an introduction to the tau system, see introduction-to-the-tau-system.

There happens to be a function named tau-system, defined as the identity function. Its only role is to provide the rune (:EXECUTABLE-COUNTERPART TAU-SYSTEM), which is used to enable and disable the tau system. Otherwise the function tau-system has no purpose and we recommend that you avoid using it so you are free to enable and disable the tau system.

When in the default (``greedy'') mode (see set-tau-auto-mode), every defun and every :corollary (see :rule-classes) of every defthm stored as a rule of any :rule-class is inspected to determine if it is of one of the forms below. Rules of these forms are added to the tau database, even if they are not labeled as :tau-system rules, e.g., a :rewrite rule might contribute to the tau database! To add a rule to the tau database without adding any other kind of rule, tag it with :rule-classes :tau-system. If a theorem has :rule-classes nil, it is not considered for the tau database.

General Forms:
Boolean:
(booleanp (p v))

Eval:
(p 'const) or
(p *const*)

Simple:
(implies (p v) (q v))

Conjunctive:
(implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.

Signature Form 1:
(implies (and (p1 x1) (p2 x2) ...)
         (q (fn x1 x2 ...)))

Signature Form 2:
(implies (and (p1 x1) (p2 x2) ...)
         (q (mv-nth 'n (fn x1 x2 ...))))

Bounder Form 1 (or Form 2):
(implies (and (tau-intervalp i1)
              ...
              (or (equal (tau-interval-dom i1) 'dom1-1)
                  ...)
              ...
              (in-tau-intervalp x1 i1)
              ...)
         (and (tau-intervalp (bounder-fn i1 ...))
              (in-tau-intervalp target
                                (bounder-fn i1 ...))))

where target is
(fn x1 ... y1 ...)             in Form 1, and
(mv-nth 'n (fn x1 ... y1 ...)) in Form 2 

Big Switch:
(equal (fn . formals) body)

MV-NTH Synonym:
(equal (nth-alt x y) (mv-nth x y)) or
(equal (mv-nth x y) (nth-alt x y))
The symbols p, q, p1, etc., denote monadic (one-argument) Boolean-valued function symbols, or equalities in which one argument is constant, arithmetic comparisons in which one argument is a rational or integer constant, or the logical negations of such terms. By ``equalities'' we allow EQUAL, EQ, EQL, and =. By ``arithmetic comparison'' we mean <, <=, >=, or >. Any of these tau predicates may appear negated.

The notation (p v) above might stand for any one of: 

(INTEGERP X)
(EQUAL V 'MONDAY)
(<= I 16)
(NOT (EQUAL X 'SUNDAY))

The different rule forms above affect different aspects of the tau system. We discuss each form in more detail below.

Some Related Topics

The documentation below is written as though the tau system is in auto mode! To insure that the only rules added to the tau system are those explicitly assigned to :rule-class :tau-system, you should use set-tau-auto-mode to select manual mode.

General Form: Boolean:
(booleanp (p v))
Here p must be a function symbol and v must be a variable. Such a :tau-system rule adds p to the list of tau predicates. If p was recognized as Boolean when it was defined, there is no need to state this rule. This form is needed if you define a monadic Boolean function in such a way that the system does not recognize that it is Boolean.

General Form: Eval:
(p 'const) or
(p *const*)

Here p must be a function symbol. In addition, recall that these general tau predicate forms may appear negated. So the form above includes such theorems as (NOT (GOOD-STATEP *INITIAL-STATE*)). A theorem of this form thus records whether a named predicate is true or false on the given constant.

Generally, when the tau system must determine whether an enabled tau predicate is true or false on a constant, it simply evaluates the predicate on the constant. This can be impossible or very inefficient if p is not defined but constrained, or if p is defined in a hard-to-compute way (e.g., (defun p (x) (evenp (ack x x))) where ack is the Ackermann function), or perhaps if the constant is very large. By proving a :tau-system rule of Eval form, you cause the tau system to note the value of the predicate on the constant and henceforth to look it up instead of evaluating the definition.

A difficulty, however, is determining that a slow down is due to the evaluation of tau predicates and not some other reason. The first step is determining that tau is slowing the proof down. See time-tracker-tau for an explanation of TIME-TRACKER-NOTEs output during some proofs involving tau reasoning. These notes can alert you to the fact that significant amounts of time are being spent in the tau system. Time-tracker-tau gives some ways of determining whether tau predicate evaluation is involved. (If worse comes to worst, consider the following hack: In the ACL2 source file tau.lisp, immediately after the definition of the system function ev-fncall-w-tau-recog, there is a comment which contains some raw Lisp code that can be used to investigate whether tau's use of evaluation on constants is causing a problem.) However, once a recognizer and the constants on which it is being evaluated are identified, the tau system can be sped up by proving Eval rules to pre-compute and store the values of the recognizer on those constants. Alternatively, at the possible loss of some completeness in the tau system, the executable counterpart of the recognizer can be disabled.

General Form: Simple:
(implies (p v) (q v))
Here v must be a variable symbol. This rule builds-in the information that anything satisfying p must also satisfy q, i.e., the ``type'' q includes the ``type'' p. Recall that the forms may be negated. Most of the time, p and q will be predicate symbols but it is possible they will be equalities- or inequalities-with-constants. Examples of Simple rules include the following, which are in fact built-in:

(implies (natp x) (integerp x))
(implies (integerp x) (rationalp x))
(implies (integerp x) (not (true-listp x)))
(implies (natp x) (not (< x 0)))
(implies (symbol-alistp x) (alistp x))
Because the tau system records the transitive closure of the Simple rules, any time a term is known to satisfy natp it is also known to satisfy integerp and rationalp, and known not to satisfy true-listp, and known to be non-negative.

General Form: Conjunctive:
(implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.
The pi and q may be any tau predicates or their negations, v must be a variable symbol, and i must exceed 1 or else this is a Simple rule. An obvious operational interpretation of this rule is that if an object is known to satisfy all of the pi, then it is known to satisfy q. However, the actual interpretation is more general. For example, if an object is known to satisfy all but one of the pi and is known not to satisfy q, then the object is known not to satisfy the ``missing'' pi.

For example, the following Conjunctive rule allows tau to conclude that if weekday D is not MON, TUE, THU or FRI, then it is WED: 

(implies (and (weekdayp d)
              (not (eq d 'MON))
              (not (eq d 'TUE))
              (not (eq d 'WED))
              (not (eq d 'THU)))
         (eq d 'FRI))
The tau database is not closed under conjunctive rules; they are applied dynamically.

General Form: Signature Form 1:
(implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp)
         (q (fn x1 x2 ... xn)))
The pi and q may be any tau predicates or their negations, fn must be a function symbol of arity n, the xi must be distinct variable symbols and dep-hyp may be any term, provided it is not of the (pi xi) shape and the only the variables in it are the xi.

The Signature form actually allows multiple tau predicates to be applied to each variable, e.g., x1 might be required to be both an INTEGERP and EVENP. The Signature form allows there to be multiple hypotheses classified as dep-hyps, i.e., not fitting any of the previous shapes, and they are implicitly just conjoined. The name ``dep-hyp'' is an abbreviation of ``dependent hypothesis'' and stems from the fact they often express relations between several of the function's inputs rather than type-like constraints on individual inputs.

A Signature rule informs tau that the function fn returns an object satisfying q provided that the arguments satisfy the respective pi and provided that dep-hyp occurs in the current context. Note: to be precise, dependent hypotheses are relieved only by applying ACL2's most primitive form of reasoning, type-set. In particular, tau reasoning is not used to establish dependent hypotheses. The presence of a dep-hyp in a signature rule may severely restrict its applicability. We discuss this after showing a few mundane examples.

An example Signature rule is 

(implies (and (integer-listp x)
              (integer-listp y))
         (integer-listp (append x y)))
Of course, a function may have multiple signatures: 
(implies (and (symbol-listp x)
              (symbol-listp y))
         (symbol-listp (append x y)))
Here is a Signature rule for the function pairlis$: 
(implies (and (symbol-listp x)
              (integer-listp y))
         (symbol-alistp (pairlis$ x y)))
The tau system can consequently check this theorem by composing the last two rules shown and exploiting Simple rule stating that symbol-alists are also alists: 
(thm (implies (and (symbol-listp a)
                   (symbol-listp b)
                   (integer-listp y))
              (alistp (pairlis$ (append a b) y))))
Since a and b are known to be lists of symbols and a signature for append is that it preserves that predicate, the first argument to the pairlis$ expression is known to be a list of symbols. This means the Signature rule for pairlis$ tells us the result is a symbol-alistp, but the previously mentioned Simple rule, (implies (symbol-alistp x) (alistp x)), tells us the result is also an alistp.

When a Signature rule has an dep-hyp, that hypothesis is not an expression in the tau system. Tau is not used to check that hypothesis. Instead, tau uses the more primitive type-set mechanism of ACL2. Here is an example of a Signature rule with a dep-hyp: 

(implies (and (natp n)
              (integer-listp a)
              (< n (len a)))
         (integerp (nth n a)))

Note that the last hypothesis is a dependent hypothesis: it is not a tau predicate but a relationship between n and a. It is relieved by type-set. If one is trying to compute the signature of an (nth n a) expression in a context in which (< n (len a)) is explicitly assumed, then this mechanism would establish the dependent hypothesis. But one can easily imagine an almost identical context where, say (< n (len (rev a))) is explicitly assumed. In that context, the Signature rule would not be fired because type-set cannot establish (< n (len a)) from (< n (len (rev a))), even though it would be easily proved by rewriting using the theorem (equal (len (rev a)) (len a)).

Note also that if this signature could be phrased in a way that eliminates the dependency between n and a it would be more effective. For example, here is a related Signature rule without a dependent hypothesis:

(implies (and (natp n)
              (register-filep a)
              (< n 16))
         (integerp (nth n a)))
In this theorem we require only that n be less than 16, which is a tau predicate and hence just an additional tau constraint on n.

General Form: Signature Form 2:
(implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp)

         (q (mv-nth 'n (fn x1 x2 ... xn))))
This form of signature rule is just like form 1 except that it is useful for functions that return multiple-values and allows us to ``type-check'' their individual outputs.

General Form: Bounder Forms 1 and 2:
(implies (and (tau-intervalp i1)
              ...
              (or (equal (tau-interval-dom i1) 'dom1-1)
                  ...)
              ...
              (in-tau-intervalp x1 i1)
              ...)
         (and (tau-intervalp (bounder-fn i1 ...))
              (in-tau-intervalp target
                                (bounder-fn i1 ...))))
where target is either (fn x1 ... y1 ...) in Form 1 or (mv-nth 'n (fn x1 ... y1 ...)) in Form 2.

This form is for advanced users only and the schema given above is just a reminder of the general shape. A ``bounder'' for a given function symbol, fn, is a function symbol bounder-fn that computes an interval containing (fn x1 ... y1 ...) (or its nth component in the case of Form 2 rules) from the intervals containing certain of the arguments of fn. The correctness theorem for a bounder function informs the tau system that bounds for fn are computed by bounder-fn and sets up the correspondence between the relevant arguments, xi, of fn and the intervals containing those arguments, ii to which bounder-fn is applied. When the tau system computes the tau for a call of fn, it computes the tau of the relevant arguments and applies the bounder to the intervals of those tau. This provides a domain and upper and/or lower bounds for the value of the term. The tau system then further augments that with signature rules. See bounders for details on intervals, bounders, and bounder correctness theorems.

General Form: Big Switch:
(equal (fn . formals) body)
In the Big Switch form, fn must be a function symbol, formals must be a list of distinct variable symbols, and body must be a ``big switch'' term, i.e., one that case splits on tau predicates about a single variable and produces a term not involving that variable. An example of a Big Switch rule is 
(equal (conditional-type x y)
       (if (consp x)
           (consp y)
           (integerp y)))
The idea is that the tau system can treat calls of conditional-type as a tau-predicate after determining the tau of an argument.

Since equality-to-constants are tau predicates, a more common example of a Big Switch rule is 

(equal (dtypep x expr)
       (case x
             (STMT (stmt-typep expr))
             (EXPR (expr-typep expr))
             (MODULE (module-typep expr))
             (otherwise nil)))
This is because (case x (STMT ...) ...) macroexpands in ACL2 to (if (eql x 'STMT) ... ...) and (eql x 'STMT) is a tau predicate about x.

Big Switch rules are recognized when a function is defined (if tau is in automatic mode). They generally do not have to be proved explicitly, though they might be when mutual recursion is involved. Only the first detected Big Switch rule about a function fn is recognized.

General Form: MV-NTH Synonym:
(equal (nth-alt x y) (mv-nth x y)) or
(equal (mv-nth x y) (nth-alt x y))
Rules of this form just tell the tau system that the user-defined function nth-alt is synonymous with the ACL2 primitive function mv-nth. Because ACL2's rewriter gives special handling to mv-nth, users sometimes define their own versions of that function so they can disable them and control rewriting better. By revealing to the tau system that such a synonym has been introduced you allow Signature rules of Form 2 to be used.