Some tau system problems that we hope someone will address

The tau system is inexpressive compared to modern polymorphic type systems — something that may be unavoidable in an untyped first-order language. However, we believe its effectiveness could be greatly increased by the development of some additional tools. We also believe that most of these tools could be provided by ACL2 users creating certified community books that exploit the basic tools already provided. It is likely the initial attempts to create such books will show the inadequacy of some of the current algorithms and data structures in the tau system and might point the way to improvements.

As implementors of ACL2 our preference is to support the improvement of the core algorithms and data structures and provide customizable hooks allowing users to exploit them by developing effective and convenient interfaces. However, we want the further elaboration and optimization of the tau system to be based on user experience not just speculation.

Some tools we *think* might help are listed below. We invite
volunteers and further suggestions.

*A tau-centric signature notation* for use in function definitions,
exploited by a macro replacing

We have, for example, experimented with a book defining a macro that allows
the definition of the function

(defsig ap (true-listp * true-listp ==> true-listp) (x y) (if (consp x) (cons (car x) (ap (cdr x) y)) y)) (defsig ap (integer-listp * integer-listp ==> integer-listp))

This experimental book provides succinct syntax for all tau signatures. For example, that book parses the signature

(NATP (/= 3 5 7) (< 16) * TRUE-LISTP ==> BOOLEANP * INTEGER-LISTP * NATP)

to be the signature of a function with two inputs and three outputs. The first input must be a natural number, different from 3, 5, and 7, and less than 16. The second input must be a true list. The first output is a boolean, the second a list of integers, and the third a natural.

To express this signature for function

(IMPLIES (AND (NATP X) (NOT (EQUAL X 3)) (NOT (EQUAL X 5)) (NOT (EQUAL X 7)) (< X 16) (TRUE-LISTP Y)) (AND (BOOLEANP (MV-NTH 0 (FN X Y))) (INTEGER-LISP (MV-NTH 1 (FN X Y))) (NATP (MV-NTH 2 (FN X Y)))))

We suspect that the provision of some succinct tau-centric notation (not necessarily the one above) for signatures at definition-time will mean users get more benefit from the tau system.

*Some tau inference mechanisms*: This phrase suggests two different
improvements. One is to implement a mechanism that adds or completes
signatures for function definitions by exploiting knowledge of commonly used
recursive schemas and the signatures of the subroutines in the body. For
example, the definition of

(integer-listp * integer-listp ==> integer-listp)

and many others just based on the two recursive schemas that (a) collect certain elements from lists and (b) check that all elements have a certain property.

The other ``tau inference'' improvement is to implement a mechanism for
inferring relations between user-defined Booleans, perhaps by exploiting
example generation, testing, and knowledge of recursive schemas. For example,
it is fairly obvious that `symbol-alistp` implies `alistp`.
Making the user state these relations invites omissions that render the tau
system very unpredictable.

*A tau assistant*: It would be useful to have a way to find out what
tau rules are missing. Given a term that the user believes should
``obviously'' have some tau (``type'') what rules might be added to make the
tau algorithm compute that expected tau? For example, if

g : T ==> P f : S ==> R

then if the user asserts that