Higher Order Specs: Issues and Examples

Higher Order

Higher Order Specs: Concepts, Issues, and Designs

Conventions

We will say that HO operations such as foldl and reduce are simple if the signature of their primary functional argument does not require new sorts. So, for example, in LIST reduce is simple and foldl is not. The convention is that simple HO functions are put in the basic spec and non-simple HO functions are put into an extended spec whose name is the name of the basic spec with an HO suffix. For example, reduce is in LIST and foldl is in LIST-HO. Generally, the return type is used as a suffix for the operation: foldl returns a nat. The versions with `es' in their name are early stop versions: if the partial result so far satisfies the specified early stop predicate, the iteration (recursion) is stopped and the partial result is returned.

Higher Order functions on Primevals

Nat

These are range (or: segment) versions of foldl etc. The bounds of the iteration are specified as: lo ( used as the index); and a least-out-of-bounds (loob). The test is "at the top" of the iteration loop: if lo < loob then the body of the iteration is executed with lo as the index. and there is a recursive call with lo increased by one. The body of the iteration is given as a transition-fcn.

Also, there are "early-stop" versions that take an early-stop predicate of the partial result. Before each iteration (i.e., at the top) the HO control function tests to determine if the lo index is less than loob and if the early-stop predicate holds of the partial result. If either the lo index is geq the loob or the early-stop predicate holds of the partial result, then the partial result is returned (and the transition function is not applied). If both the lo index is less than the loob and the early-stop predicate does not hold, then the transition function is applied and there is another call with the new partial result and with the lo index increased by one.

The spec is in nat-ho.re