126 Chapter 7 Higher-Order Functions
allPos extracts the contents of s to a set and applies the test x>0 to each element
returning true if all elements are greater than 0.
7.6 Function Inclusion and Composition
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)).
image and filter are exceptionally useful for manipulating sequences. Using
Using image, filter, and
image, defining word functions from bit functions is a simple matter of applying
functions to all bits in a sequence. Two functions that perfor m xor and (and) of
one bit across an entire word are:
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
The two definitions represent two different approaches. The wordXor function
defines an internal helper function that applies xor to the bit input to wordXor
and the single input bit x. This function is then applied to each element of the input
bitvector. This approach is similar to that used in languages such as Scheme, where
currying is not directly supported. The wordAnd function uses currying to define
a new function from the binary operation + and the input bit b. This new unary
function is applied to each element of the input vector adding the b value w ith each
element. filter is equally useful for extracting values from a sequence or perform-
ing searches without resorting to primitive recursion. The following definition is for
a function that determines if there are exactly two elements in a bitvector with a
value 1:
twoOnes(b::bitvector)::boolean is
#(filter(<(x::bit)::boolean is x=1>,b))==2
Finally, we can define a parity checking function using reduce over bitvectors:
evenParity(b::bitvector)::boolean is %(reduce xor 0b)
The evenParity function starts with 0 and applies xor to the accumulated value and
the current bit. As each 1 is visited, the accumulated value toggles. The % operation is
used to convert the resulting bit to a boolean value.
7.6 Function Inclusion and Composition 127
7.6.1 Function Inclusion
The function ty pe former <(d::D)::R> defines the set of functions mapping D
to R. This set is in all ways a Rosetta t ype 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 =< f2
d2=<d1 and forall(x::d1 | f1(x) == f2(x))
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). Explor ing 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:
f1 =< f2
d2 =< d1 and r1 =< r2
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:
f1 =< f2
d2 =< d1 and forall(x::d1 | f1(x) in r2)
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:
f1 =< f2
d1 =< d2 and ran(f1) =< r2
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

Get System Level Design with Rosetta now with O’Reilly online learning.

O’Reilly members experience live online training, plus books, videos, and digital content from 200+ publishers.