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
*fn a1...an**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.

*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

(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-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 `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,
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 `executable-counterpart``executable-counterpart`

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`.

*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

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 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 `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 `set-tau-auto-mode`.

To prevent tau reasoning from being used, disable the `executable-counterpart` of

(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

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.

- Future-work-related-to-the-tau-system
- Some tau system problems that we hope someone will address
- Dealing-with-tau-problems
- Some advice on dealing with problems caused by the tau system
- Regenerate-tau-database
- Regenerate the tau database relative to the current enabled theory