Major Section: ACL2 Documentation
This doc topic is the main source of information about the tau system and discusses the general idea behind the procedure and how to exploit it.
A ``Type-Checker'' for an Untyped Language
Because ACL2 is an untyped language it is impossible to type check it. All
functions are total. An n-ary function may be applied to any combination
of n ACL2 objects. The syntax of ACL2 stipulates that
(fn a1...an) is a well-formed term if fn is a function symbol
of n arguments and the ai are well-formed terms. No mention is made
of the ``types'' of terms. That is what is meant by saying ACL2 is an
untyped language.
Nevertheless, the system provides a variety of monadic Boolean function
symbols, like natp, integerp, alistp, etc., that recognize
different ``types'' of objects at runtime. Users typically define many more
such recognizers for domain-specific ``types.'' Because of the prevalence of
such ``types,'' ACL2 must frequently reason about the inclusion of one
``type'' in another. It must also reason about the consequences of functions
being defined so as to produce objects of certain ``types'' when given
arguments of certain other ``types.''
Because the word ``type'' in computer science tends to imply syntactic or semantic restrictions on functions, we avoid using that word henceforth. Instead, we just reason about monadic Boolean predicates. You may wish to think of ``tau'' as synonymous with ``type'' but without any suggestion of syntactic or semantic restrictions.
:tau-system rules
Design Philosophy
The following basic principles were kept in mind when developing tau checker and may help you exploit it.
(1) The tau system is supposed to be a lightweight, fast, and helpful decision procedure for an elementary subset of the logic focused on monadic predicates and function signatures.
(2) Most subgoals produced by the theorem prover are not in any decidable subset of the logic! Thus, decision procedures fail to prove the vast majority of the formulas they see and will be net time-sinks if tried too often no matter how fast they are.
Tau reasoning is used by the prover as part of preprocess-clause, one of
the first proof techniques the system tries. The tau system filters out
``obvious'' subgoals. The tau system is only tried when subgoals first enter
the waterfall and when they are stable under simplification.
(3) The tau system is ``benign'' in the sense that the only way it contributes to a proof is to eliminate (prove!) subgoals. It does not rewrite, simplify, or change formulas. Tau reasoning is not used by the rewriter. The tau system either eliminates a subgoal by proving it or leaves it unchanged.
(4) It is impossible to infer automatically the relations between arbitrary recursively defined predicates and functions. Thus, the tau system's knowledge of tau relationships and function signatures is gleaned from theorems stated by the user and proved by the system.
(5) Users wishing to build effective ``type-checkers'' for their models must learn how rules affect the tau system's behavior. There are two main forms of tau rules: those that reveal inclusion/exclusion relations between named tau predicates, e.g., that 16-bit naturals are also 32-bit naturals,
(implies (n16p x) (n32p x)),and signatures for all relevant functions, e.g., writing a 32-bit natural to a legal slot in a register file produces a register file:
(implies (and (natp n)
(< n 16)
(n32p val)
(register-filep regs))
(register-filep (update-nth n val regs))).
For a complete description of acceptable forms see :tau-system.(6) The tau system is ``greedy'' in its efforts to augment its database. Its
database is potentially augmented when rules of any :rule-class (see
:rule-classes) are proved. For example, if you make a
:rewrite or :type-prescription rule which expresses
relationship between tau, ACL2 will build it into the tau database. The
rule-class :tau-system can be used to add a rule to the tau
database without adding any other kind of rule.
(7) Greediness is forced into the design by benignity: the tau system may
``know'' some fact that the rewriter does not, and because tau reasoning is
not used in rewriting, that missing fact must be conveyed to the rewriter
through some other class of rule, e.g., a :rewrite or
:type-prescription or :forward-chaining rule. By making
the tau system greedy, we allow the user to program the rewriter and the tau
system simultaneously while keeping them separate. However, this means you must
keep in mind the effects of a rule on both the rewriter and the tau
system and use :tau-system rules explicitly when you want to ``talk''
just to the tau system.
(8) Tau rules are built into the database with as much preprocessing as possible (e.g., the system transitively closes inclusion/exclusion relationships at rule-storage time) so the checker can be fast.
(9) For speed, tau does not track dependencies and is not sensitive to the
enabled/disabled status (see enable and disable) of rules. Once
a fact has been built into the tau database, the only way to prevent that
fact from being used is by disabling the entire tau system, by disabling
(:executable-counterpart tau-system). If any tau reasoning is
used in a proof, the rune (:executable-counterpart tau-system)
is reported in the summary. For a complete list of all the runes in the tau
database, evaluate (global-val 'tau-runes (w state)). Any of these
associated theorems could have been used.
These design criteria are not always achieved! For example, the tau system's
``greediness'' can be turned off (see set-tau-auto-mode), the tau
database can be regenerated from scratch to ignore disabled rules (see
regenerate-tau-database), and disabling the
executable-counterpart of a tau predicate symbol will prevent the tau
system from trying to run the predicate on constants. The tau system's
benignity can be frustrating since it might ``know'' something the rewriter
does not. More problematically, the tau system is not always ``fast'' and
not always ``benign!'' The typical way tau reasoning can slow a proof down
is by evaulating expensive tau predicates on constants. The typical way tau
reasoning can hurt a previously successful proof is by proving some
subgoals (!) and thus causing the remaining subgoals to have different
clause-identifiers, thus making explicit hints no longer applicable. We
deal with such problems in dealing-with-tau-problems.
Technical Details
The tau system consists of both a database and an algorithm for using the
database. The database contains theorems that match certain schemas allowing
them to be stored in the tau database. Roughly speaking the schemas encode
``inclusion'' and ``exclusion'' relations, e.g., that natp implies
integerp and that integerp implies not consp, and they encode
``signatures'' of functions, e.g., theorems that relate the output of a
function to the input, provided only tau predicates are involved.
By ``tau predicates'' we mean the application of a monadic Boolean-valued function symbol, the equality of something to a quoted constant, an arithmetic ordering relation between something and a rational constant, or the logical negation of such a term. Here are some examples of tau predicates:
(natp i) (not (consp x)) (equal y 'MONDAY) (not (eql 23 k)) (< 8 max) (<= max 24)Synonyms for
equal include =, eq, and eql. Note that
negated equalites are also allowed. The arithmetic ordering relations that
may be used are <, <=, >=, and >. One of the
arguments to every arithmetic ordering relation must be an integer or
rational constant for the term to be treated as a tau predicate.A ``tau'' is a data object representing a set of signed (positive or negative) tau predicates whose meaning is the conjunction of the literals in the set.
When we say that a term ``has'' a given tau we mean the term satisfies all of the recognizers in that tau.
The tau algorithm is a decision procedure for the logical theory described (only) by the rules in the database. The algorithm takes a term and a list of assumptions mapping subterms (typically variable symbols) to tau, and returns the tau of the given term.
When the system is called upon to decide whether a term satisfies a given monadic predicate, it computes the tau of the term and asks whether the predicate is in that set. More generally, to determine if a term satisfies a tau, s, we compute a tau, r, for the term and ask whether s is a subset of r. To determine whether a constant, c, satisfies tau s we apply each of the literals in s to c. Evaluation might, of course, be time-consuming for complex user-defined predicates.
The tau database contains rules derived from definitions and theorems stated
by the user. See :tau-system for a description of the acceptable
forms of tau rules.
To shut off the greedy augmentation of the tau database,
see set-tau-auto-mode. This may be of use to users who wish to tightly
control the rules in the tau database. To add a rule to the tau database
without adding any other kind of rule, use the rule class
:tau-system.
There are some slight complexities in the design related to how we handle
events with both :tau-system corollaries and corollaries of other
:rule-classes, see set-tau-auto-mode.
To prevent tau reasoning from being used, disable the
:executable-counterpart of tau-system, i.e., execute
(in-theory (disable (:executable-counterpart tau-system)))or, equivalently,
(in-theory (disable (tau-system)))To prevent tau from being used in the proof of a particular subgoal, locally disable the
:executable-counterpart of tau-system with a local
:in-theory hint (see hints).The event command tau-status is a macro that can be used to toggle both
whether tau reasoning is globally enabled and whether the tau database is
augmented greedily. For example, the event
(tau-status :system nil :auto-mode nil)prevents the tau system from being used in proofs and prevents the augmentation of the tau database by rules other than those explicitly labeled
:tau-system. To see what the tau system ``knows'' about a given function symbol see tau-data. To see the entire tau database, see tau-database. To regenerate the tau database using only the runes listed in the current enabled theory, see regenerate-tau-database.
