FUTURE-WORK-RELATED-TO-THE-TAU-SYSTEM.html -- ACL2 Version 6.1

FUTURE-WORK-RELATED-TO-THE-TAU-SYSTEM

some tau system problems that we hope someone will address

Major Section:  INTRODUCTION-TO-THE-TAU-SYSTEM

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 defun so that input-output relationships phrased in tau terms are proved as :tau-system rules immediately after functions are introduced:

We have, for example, experimented with a book defining a macro that allows the definition of the function ap (append) accompanied by a signature rule. Subsequent defsig events can add other signatures in the same notation.

(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 fn as a formula requires significantly more typing by the user:

(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 ap above rather obviously has the signature

(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 x) is known to satisfy P and (f x) is known to satisfy R when its argument satisfies S:

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

then if the user asserts that (f (g x)) ``ought'' to have tau R, one plausible suggestion is the simple tau rule that (P x) implies (S x). Such assistance -- while still confronting an undecidable problem -- might be easier to implement within the tau framework than more generally in ACL2. (Many users have wanted such an assistant to suggest lemmas for the rewriter.)