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

foldl-nat
foldl-es-nat
foldr-nat
foldr-es-nat
least-nat
least-nat returns a sum: Nat-or-Error
Boolean
foldl-boolean
foldl-es-boolean
exists-nat
forall-nat
String
The spec is in string-ho.re
exists-string
forall-string
image-string


Other Higher Order functions
ARRAY
The spec is in array.re
reduce-iter-l
reduce-iter-r
reduce
exists
forall
image
ARRAY-HO
The spec is in array.re
foldl-iter
foldr-iter
foldl
foldr
LIST
The spec is in list.re
reduce
exists
forall
map
filter
LIST-HO
The spec is in list.re
foldl
foldr

SpecWeb Index Specs