 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 deﬁnes several
relations that deﬁne when one function is, in effect, a sub-function of another.
Speciﬁcally, we will deﬁne f=<g, f<g, and f=g for any two functions. Function
composition deﬁnes new functions by composing existing functions. The operation
(f.g)is deﬁned to represent the function equivalent to the application of g then
f to its argument. Speciﬁcally, we will deﬁne the composition operation so that
(f . g)(x)==f(g(x)).
image and filter are exceptionally useful for manipulating sequences. Using
EXAMPLE 7.8
Using image, filter, and
reduce
image, deﬁning 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 deﬁnitions represent two different approaches. The wordXor function
deﬁnes 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 deﬁne
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 deﬁnition 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 deﬁne 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> deﬁnes 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 deﬁned 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
def
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 speciﬁed as sets, where the parameter x
is not involved in the deﬁnition. Examining the function inclusion law, the universal
quantiﬁer falls out and the following relationship results:
f1 =< f2
def
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
def
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 simpliﬁed to:
f1 =< f2
def
d1 =< d2 and ran(f1) =< r2
As an example, consider the increment function deﬁned 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.