		Search-engine friendly clone of the ACL2 documentation.

Soft

Soft-future-work

Some possible improvements and extensions to SOFT.

Mutual Recursion

SOFT should be extended with the ability to introduce and instantiate mutually recursive functions, perhaps via a new mutual-recursion2 macro.

Other Well-Founded Relations

Currently recursive second-order functions must use o< as their well-founded relation. This could be relaxed, perhaps even to the point of allowing second-order well-founded relations.

Other Function and Theorem Introduction Macros

Besides second-order versions of defun, defchoose, defun-sk, define2, and define-sk2, we could add support for second-order versions of defun-nx, defpun, and other function introduction events. defun-inst would generate the same macros for instances. The macros could be called defun-nx2, defpun2, etc.

Under some conditions, it would make sense for defun-inst to instantiate a partial second-order function (introduced, say, via a future defpun2 macro) to a total second-order function (i.e. a defun2 or defun), when the instantiated :domain or :gdomain restrictions are theorems.

defthm-inst could also generate instances with the same macros from second-order theorems introduced via defthm, defrule, and other theorem introduction events.

Program Mode

Currently SOFT only supports logic-mode second-order functions. Supporting program-mode functions as well may be useful.

Guards of Instances of Second-Order Functions

It would be useful to allow the default guards of instances of second-order functions (obtained by instantiating the guards of the second-order functions) to be overridden by stronger guards.

The guard theorem of a second-order function may be useful (although not sufficient in general) to verifies the guards of instances of the second-order function. A mechanism to enable the use of that theorem would be useful.

See the future work section of the Workshop paper for a more detailed discussion with examples.

Lambda Expressions

Instantiations could be extended to allow function variables to be replaces with lambda expressions, besides named functions.

Transitivity of Instantiations

Intuitively, if f is an instance of g and g is an instance of h, then f should be an instance of h. This is currently not supported by defun-inst, but probably it should be.

See the future work section of the Workshop paper for a more detailed discussion with examples.

More Constraints on Function Variables

The types of function variables are currently limited to signatures with single-value results and with no stobjs. This could be extended to allow multiple-value results and stobjs. Instantiations will have to respect these additional type structures.

Other than their types, function variables are currently unconstrained. In some cases, it may be useful to specify some logical constraints, resulting in a constrained function as in non-trivial encapsulates. Instantiations will have to respect these additional constraints.

The latter extension would overlap with some existing tools, such as instance-of-defspec and make-generic-theory. Ideally, the functionality of SOFT and those tools would be integrated.

Function variables current have guard t. It may be useful to allow guards to be specified for function variables. Instantiations will have to match these guards.

Automatic Instances

Currently, when an instantiation is applied to a term, the table of instances of second-order functions is consulted to find replacements for certain second-order functions, and the application of the instantiation fails if replacements are not found. Thus, all the needed instances must be introduced before applying the instantiation. SOFT could be extended to generate automatically the needed instances of second-order functions.

SOFT could also be extended with a macro defthm2 to prove a second-order theorem via defthm and to record the theorem in a new table, along with information about the involved second-order functions. defun-inst could be extended with the option to generate instances of the second-order theorems that involve the second-order function being instantiated. defthm2 could include the option to generate instances of the theorem that correspond to the known instances of the second-order functions that the theorem involves. These extensions would reduce the use of explicit defthm-insts.

The convention of including function variables in square brackets in the names of second-order functions and theorems, could be exploited to name the automatically generated function and theorem instances.

Default Rule Classes

Currently the default rule classes of an instance of a second-order theorem are (:rewrite), but perhaps the default should be the rule classes of the second-order theorem that is being instantiated.