INTRODUCTION-TO-THE-TAU-SYSTEM

a decision procedure for runtime types 
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.

Some Related Topics

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 a relationship between one tau and another (e.g., that (P x) implies (Q x)), 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.