A decision procedure for runtime types
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
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.
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
(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
(6) The tau system is ``greedy'' in its efforts to augment its database.
Its database is potentially augmented when rules of any
(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
(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,
other than executable-counterpart 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
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 evaluating 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.
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
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:
Synonyms for equal include =, eq, and eql. Note that negated equalities 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
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
There are some slight complexities in the design related to how we handle
events with both
To prevent tau reasoning from being used, disable the
(in-theory (disable (tau-system)))
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
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.