Tau-system
Make a rule for the ACL2 ``type checker''
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.
The documentation below is written as though the tau system is in auto
mode! To ensure 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 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
reasoning (using 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 by default,
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.
Subtopics
- Introduction-to-the-tau-system
- A decision procedure for runtime types
- Set-tau-auto-mode
- Turn on or off automatic (``greedy'') generation of :tau-system
rules
- Bounders
- Intervals, bounder functions, and bounder correctness
- In-tau-intervalp
- Boolean membership in a tau interval
- Make-tau-interval
- Make a tau interval
- Time-tracker-tau
- Messages about expensive use of the tau-system
- Tau-intervalp
- Boolean recognizer for tau intervals
- Tau-status
- Query or set tau system status
- Tau-data
- To see what tau knows about a function symbol
- Tau-interval-lo-rel
- Access the lower bound relation of a tau interval
- Tau-interval-hi-rel
- Access the upper bound relation of a tau interval
- Tau-interval-hi
- Access the upper bound of a tau interval
- Tau-interval-lo
- Access the lower bound of a tau interval
- Tau-interval-dom
- Access the domain of a tau interval
- Tau-database
- To see the tau database as a (very large) object
