The core of Rosetta’s built-in higher-order functions includes functions for extracting the domain, range, and return type from a function definition. Described in Table 7.1, dom, ran, and ret provide capabilities for extracting domain, range, and return type from a function, respectively. The dom function accepts a function as its only argument and returns the domain of that function. For unary functions such as inc, this is simply a process of returning the type associated with the input parameter. If inc is defined in the traditional fashion:

  inc(x::natural)::natural is x+1;

the domain of inc is found by using the dom function:

   dom(inc) == natural;

ret is the return type of the function. Using inc again as an example, the return type is found by evaluating ret on the function:

  ret(inc) == natural;

Like the domain function, the return type function is realized by simply examining the function definition.

The ran function accepts a single, arbitrary function as its only argument and returns the actual range of the function. Unlike the return type function, the range function evaluates to the function’s range by assembling the results of applying the function to each element of its domain type. Determining the range of inc is achieved by evaluating inc on every value of its domain. Thus, the range of inc is the natural numbers without zero. Formally:

  ran(inc) == {x::dom(inc) | inc(x)} == posint;

where posint is the name of the type containing all natural values except 0. It is known that for any function, the range must be contained in the return type:

  forall(f::function | ran(f) =< ret(f));

The domain and range functions present a greater challenge when dealing with functions of arity other than 1. It is possible to define a function with no arguments, often called a nullary function. During function evaluation, nullary functions are always reduced to expressions by removing the function former. Specifically:

     <* ()::T is e *> == e

This is perfectly legal, as the purpose of the function former brackets is to define the scope of function parameters. With no parameters, there is no need to define scope. The domain of all nullary functions is the empty type containing no values. The range of a nullary function is the result of evaluating its associated expression. Thus:

    dom(()::natural is <* 3+2 *>) == {}
    ran(()::natural is <* 3+2 *>) == {5}

Using these identities, one can define evaluation of a fully instantiated function as taking its range after instantiating and removing parameters. If all arguments to a function are known, then the range of that instantiated function is the same as evaluating the function.

   image(f,d);

    image(f,dom(f))

    ran(f)

The domain of functions with more than one parameter is defined as the type of the first parameter. This follows directly from the curried semantics, where every function can be reduced to a unary function. The range of functions with more than one parameter is defined as the type of the function resulting from curried evaluation with respect to the first parameter. Finally, the return type is the type syntactically specified as the return type of the function.

Given a find function that determines if a value is in a sequence of values:

   find(x::natural,y::sequence(natural))::boolean is
     if y/=null then
        if x=y(0) then true
           else find(x,(y sub [1,..#y-1]))
        end if
        else false
   end if;

domain, range, and return type are defined as:

   dom(find) == natural
   ran(find) == <*(y::sequence(natural))::boolean*>
   ret(find) == boolean

The domain is the type of the first parameter and the return type is the type associated with the function. If this function were partially evaluated specifying only the first parameter, the resulting function type would be a mapping from an array of naturals to a boolean value. Thus, the range of the find function is the function type specified in the previous definition.

   <*(x::S)::ret(f) is f(x)*>

   image(f,S) == ran(<*(x::S)::ret(f) is f(x)*>)

The functions dom, ran, and ret are defined to return elements of a function definition. Thus, it is natural to call these functions using functions as parameters. When thinking about image and mapping functions, Iminimum, maximum, and quantifier functions, the common practice is to start with a set of items and perform a specified operation on that set. Mapping functions apply a transformation to each element of a set, minimum and maximum return the appropriate value from a set, and quantifiers check to see if a property holds for all or some values from a set. Although each of these properties can be expressed using a higher-order function, it can become difficult to read and understand.

Rosetta introduces a standard notation to allow a more natural expression of higher-order properties involved in quantification associated with sets. The following notation is equivalent to finding the minimum value generated by inc in the earlier example:

   min(x::natural | x+1)

Using this notation, the domain and value expression of the function are separated in a manner consistent with traditional notations. The interpretation of this notation is to take all elements of natural, apply the expression x+1, and return the minimum resulting value. The mapping from this notation back to the higher-order function is a simple syntactic manipulation. If S is a set and e is an expression defined over elements of S, then the following relationship is always true:

  min (x::S | e)  min(<*(x::S)::T is e*>)

Here the elements of the set are pulled out and used as a type in the function former. The notation:

   min(x ::natural | x)

specifies the minimum value in the set of natural numbers.

What makes this notation powerful is that natural can be replaced by any set and Rosetta forms the higher-order function. If the collection can be identified and the expression defined, the preceding notation can be used to accomplish the higher-order specification task. If additional single-parameter higher-order functions are defined, the same notation applies. Semantically, the notation adds nothing, but it significantly enhances the readability of specifications.

The primary functions used to define quantifiers are the minimum and maximum functions (Table 7.3). Each of these functions takes as its single argument an arbitrary function, finds the range of that function, and returns the minimum or maximum value in the range, respectively. In other words, the minimum function returns the smallest value a function can produce, while the maximum produces the largest.

The min function takes a function and evaluates that function on every possible domain value and selects the minimum value. This can be viewed as taking the function’s range and returning the minimum of the range values. A simple function example is the identity function:

  id(x::natural)::natural is x;

This function is equal to its single natural number argument. Applying the min function returns its smallest possible value, or, in this case, the smallest possible natural number:

   1. min (id)
   2.   == min (<*(x::natural)::natural is x*>)
   3.   == 0

The domain of the argument function is the type natural. The range of the argument function is the expression applied to each element of the domain — specifically, the natural numbers. The min function then returns the minimum value associated with natural or 0.

Similarly, the min function can be applied to inc where the expression associated with the function is x+1. Specifically:

   1. min (inc)
   2.   == min (<*(x::natural)::natural is x+1*>)
   3.   == 1

The max function is defined similarly and operates in the same manner, except it returns the maximum value associated with a function’s domain, rather than the minimum value.

The concept of a quantifier from traditional logic allows specifiers to make statements about sets of items. The universal quantifier, called forall, allows the specifier to claim that a property is true for every element of a collection. Similarly, the existential quantifier, called exists, allows the specifier to claim that a property is true for at least one element of a collection. Although mysterious in many languages, Rosetta quantifiers are simply higher-order functions defined over predicates. In essence, we will take the range of a collection and use that range to determine if a quantifier holds. If the range of a predicate does not contain false, the predicate is true for all elements of its range. Similarly, if the range of a predicate contains the true value, there exists a value from the range for which the predicate holds.

Unfortunately, quantifiers and comprehension operators can be somewhat mysterious in their application and definition. In Rosetta, these operators are simply higher-order functions whose definitions do not differ substantially from simple minimum and maximum functions. Quantifier and comprehension functions and the other predefined higher order functions have the same form. The former can be instantiated with functions as their single argument:

    forall(<*(x::S)::T is P(x)*>)
    exists(<*(x::S)::T is P(x)*>)
    sel(<*(x::S)::T is P(x)*>)

or using the equivalent, more readable mathematical notation:

    forall(x::S | P(x))
    exists(x::S | P(x))
    sel(x::S | P(x))

where S is a set or type, T is a type, and P(x) is a boolean expression defined over x. The forall and exists functions determine if P holds for all or some of the values in S, respectively. The sel function selects elements of S for which P holds.

Consider the following application of forall to determine if a particular set contains only values greater than zero:

   forall(x::{1,2,3,5} | x>0)

Applying the expression x>0 to each element of the input collection, the resulting set becomes:

   {true,true,true,true}

Thus, the expression is true for each element of the input collection, meaning that the result of applying forall is also true. Assuming the input set is {1,2,3,0} demonstrates the opposite effect. Here, the result of applying the expression to each element of the collection is:

   {true,true,true,false}

Because one value is false, the forall expression evaluates to false.

Rosetta interprets the original definition by forming a function argument to forall. In this case, the function has the following form:

  forall(<*(x::{1,2,3,5})::boolean is x>0 *>)

Here, the domain of the argument function is the set {1,2,3,5} and the result expression x>0. To determine the range of the argument function, x>0 is applied to each element of domain collection giving the result presented previously. The exists function works identically, but is true when at least one of the evaluation results is true, rather than all. For example:

  exists(x::{1,2,3,-1} | x>0)

is true because the result of applying the expression is {true, true, true, false}and one element of the input collection is greater than 0. In contrast:

  exists(x::{1,2,3,0} | x<0)

produces {false, false, false, false}. None of the input collection is less than 0 and the exists function evaluates to false.

  p(x::integer)::boolean is p>5;

  forall(x::image(p,S) | x)
  exists(x::image(p,S) | x)

   forall(x::S | p(x))
   exists(x::S | p(x))

The sel function provides a mechanism for selecting from a set values that satisfy a property, and returns them as a set. In traditional logic, the selection function is referred to as comprehension and is used as a primary method along with extension for constructing sets. Consider the following example, where sel is used to filter out all elements of a set that are not greater than 0:

   sel(x::{1,2,3,0} | x>0)

In this case, the result of evaluating the sel function is the set {1,2,3}, or the subset of the input set that is greater than zero. Like the previous higher-order functions, this form of the sel function creates a function from the input arguments and operates on the range of that function. For this example, the equivalent form using a function argument is:

   sel(<* (x::{1,2,3,0})::boolean is x>0 *>)

  true > false

   exists(x::1,2,3,-1 | x>0) == max (x::1,2,3,-1 | x>0)
   forall(x::1,2,3,-1 | x>0) == min (x::1,2,3,-1 | x>0)

   filter(p,S) = sel (x::S | p(x))

   natural::subtype(integer) is sel (x::integer | x >= 0)

There are two fundamental types of higher-order functions that are useful with respect to sequences. The first includes functions that simply treat the contents of a sequence as a set. Recall from Chapter 5 that a contents function is defined that extracts the contents of a sequence as a set. Given a sequence S, its contents can be extracted as a set using the prefix operation ~S. Thus, it is possible to apply any of the higher-order set functions to sequences. For example, given a sequence S and a boolean expression P, the set of objects from S satisfying P is defined as:

   {sel(x::~S | P(x))}

The contents operator extracts the elements of S as a set and the higher-order sel function performs the comprehension. Table 7.3 shows how each of the defined higher-order functions for sets can be applied to sequences using the extraction function. Like the previous expression, this function evaluates to the subset of items from S that satisfy P(x).

The second kind of higher-order function treats sequences as sequences generating new sequences from old sequences. Table 7.4 shows the definitions of these sequence functions. Rather than using the set-based higher-order functions, these operations are defined on sequences directly. The two built-in special operations on sequences are image and filter. The image function takes a sequence and an arbitrary function and applies that function to each element in the sequence. To increment the contents of a sequence and maintain the result as a sequence, the map function is applied as:

   image(inc,[1,2,3]) == [2,3,4];

Similarly, the filter function takes a sequence and removes elements that do not satisfy a predicate. Assuming that the predicate lt3 exists that is true if its argument is less than three, filtering a sequence for values less than three is achieved by:

   filter(lt3,[3,1,2,4]) == [1,2];

Anonymous functions and let forms are particularly useful in conjunction with the image and filter operations. It is unlikely that the lt3 function just used will ever exist in any library. Using anonymous functions, the filtering operation can be implemented as:

  filter(<*(x::natural)::boolean is x <3*>,[3,1,2,4]);

The use of filter is identical in this example, except that the filtering predicate is defined locally and is discarded after the function is simplified and resolved. If a filtering or image function is used repeatedly, the let form is useful for defining a local function:

   let filterFn:: <*(x::natural)::boolean*> be
         <*(x::natural)::boolean is x<3*>
     filter(filterFn,[3,1,2,4])
   end let;

Again the function is identical, but the local function filterFn is defined in the let form and is used in the filtering activity. Like the anonymous function defined previously, filterFn is discarded following the closing of the let form’s scope. It should be noted that using the let form for local function definition in this way can be somewhat cumbersome. If filterFn is used repeatedly within the let form, or allowing the function to have a name increases readability, then the extra syntax is worthwhile.

   allPos(s: sequence(integer))::boolean is
      forall (y::(~S) | x>0)

Two operations on functions support comparison operations and composition of multiple functions into a single function. Function inclusion defines several relations that define when one function is, in effect, a sub-function of another. Specifically, we will define f=<g, f<g, and f=g for any two functions. Function composition defines new functions by composing existing functions. The operation (f. g) is defined to represent the function equivalent to the application of g then f to its argument. Specifically, we will define the composition operation so that (f. g)(x)==f(g(x)).

   wordXor(b::bit; w::bitvector)::bitvector is
     let helper ::<* (x::bit)::bit *> is
        <* (x::bit)::bit is b xor x *>

   wordAnd(b::bit; w::bitvector)::bitvector is image (__*__(b)) w

   twoOnes(b::bitvector)::boolean is
      #(filter(<*(x::bit)::boolean is x=1*>,b))==2

   evenParity(b::bitvector)::boolean is %(reduce xor 0 b)

Function Inclusion

The function type former <*(d::D)::R*> defines the set of functions mapping D to R. This set is in all ways a Rosetta type and can be manipulated as a set. Thus, operations such as subset and proper subset are defined over functions. Subset applied to functions is referred to as a function inclusion operation. Function containment, f1=<f2, holds when one function is fully contained in another function or function type. Assuming f1(x::d1)::r1 and f2(x::d2)::r2:

f1 is contained in f2 if and only if the domain of f2 is a subset of the domain of f1 and for every element of f2’s domain, f1(x) is equal to f2(x). Exploring function inclusion’s several cases reveals where it applies.

The simplest case is when r1 and r2 are specified as sets, where the parameter x is not involved in the definition. Examining the function inclusion law, the universal quantifier falls out and the following relationship results:

In this case, f1 is included in f2 when (i) dom(f2) is contained in its domain and (ii) its range is contained in ran(f2).

A second case occurs when r1 is an expression and r2 is a set. Instantiating the function inclusion law results in the following statement:

r2 is a constant value independent of x. Therefore, the law requires that applying expression r1 to actual parameter x results in an element of r2. This is equivalent to the previous result and can be simplified to:

As an example, consider the increment function defined over natural numbers. It should hold that:

   inc ::<*(x::natural)::natural*>

Instantiating the function inclusion law gives:

   1. inc ::<*(x::natural)::natural*>
   2.   == natural =< dom(inc) and
           forall (x::natural | inc(x) in natural)
   3.   == natural =< natural and
           forall (x::natural | x+1 in natural)
   4.   == true and true

Thus, inc is of type <*(x::natural)::natural*>. It is interesting to note that this is exactly the relationship that must be checked for every definition of the form:

  f(x::Td)::Td is e;

as it indicates that the actual function is of the same type as the specified signature.

The final case defines when one constant function is included in another constant function. In this case, both d1 and d2 are expressions and the most general expression of the function inclusion law must be applied.

First, consider determining if the increment function is included in itself. Clearly, this should be the case and the function inclusion law supports the assertion:

   1. inc =< inc
   2.   == dom(inc) =< dom(inc) and
           forall (x::natural | inc(x) = inc(x))
   3.   == natural =< natural and forall (x::natural | x+1 = x+1)
   4.   == true and true

This holds because for any Rosetta item, i=i holds by definition. Consider the case of determining if increment is contained in identity over natural numbers. In this case, the law should not hold:

   1. inc =< id
   2.   == <*(x::natural)::natural is x+1*> =<
               <*(x::natural)::natural is x* >;
   3.   == dom(id) =< dom(inc) and
            forall (x::natural | inc(x) = id(x))
   4.   == natural =< natural and 
           forall (x::natural | x+1 = x)
   5.   == true and false

false is obtained from the second expression by the counter example provided by x=0 as 0+1 /= 0.

When f1(d::d1) is e1, the following relationship holds:

   f1 =< <*(x::d2)::r2*> ==
           d2=<d1 and forall (n::d2 | f1(n) =< r2*>)

or

   f1 ::<*(x::d2)::r2*> == d1=<d2 and ran(r1) =< r2

The function containment law gives the criteria by which one function may be said to be included within a function type. Each function type defines a set of functions consisting of all those functions included in it. This means that any function can be used as a type, or set, and all the containment laws for sets apply to them. This is particularly useful when using a function that returns a set rather than a single value. Consider the function <*(n::natural)::natural*>. This function defines the set of all functions that take a natural number as an argument and return a natural number. Rosetta allows the user to ask if a given function is contained in that set and is a member of that type. For example, consider:

   succ(n::natural)::natural is n+1;

We wish to determine:

  1. succ(n::natural)::natural is n+1 ::
       succ(n::natural)::natural;
  2.   == (natural=<natural) and
           forall (n::natural | succ(n) in natural)
  3.   == true and forall (n::natural | (n+1) in natural)
  4.   == true and true
  5.   == true

Assuming that f(x::df)::rf and g(x::dg)::rg, the operations defined in Table 7.5 are defined over two functions. Functional equivalence checks to determine if every application of f and g to elements from the union of their domains results in the same value. Specifically, f(x) = g(x) for every x in either domain. Function inequality is defined as the negation of function equality.

Table 7.5. Function equivalence and inclusion properties

Operation	Format	Definition
Equal and not equal	f=g, f/=g	f=<g and f>=g, -(f=<g) or -(f>=g)
Ordering relationships	f>=g, f>g, f=<g, f<g	g=<f, g=<f andf/=g, f=<g, f=<g and f/=g
Composition	f. g	f(g(x))

  (f. g)(x)  f(g(x))

  ret(g) =< dom(f)

  inc(x::integer)::integer is x+1;

  plus2 ::<*(x::integer)::integer*> is (inc. inc);

  inc(x::natural)::natural  is x+1;

  plus2 ::<*(x::natural)::posint*> is (inc. inc);