Thinking Functionally with Haskell (35 page)

In words,
P
holds in the limit if it holds for each approximation to the limit.

For lists there is a useful Haskell function
approx
, which produces approximations to a given list. The definition is

approx :: Integer -> [a] -> [a]

approx n []
| n>0 = []

approx n (x:xs) | n>0 = x:approx (n-1) xs

The definition of
approx
is very similar to that of
take
except that, by case exhaustion, we have
approx 0 xs = undefined
for all
xs
. For example,

approx 0 [1] = undefined

approx 1 [1] = 1:undefined

approx 2 [1] = 1:[]

The crucial property of
approx
is that

for all lists
xs
, finite, partial or infinite. The proof, an induction on
xs
, is left as an exercise.

It follows that if
approx n xs
=
approx n ys
for all natural numbers
n
, then
xs
=
ys
. Thus we can prove that
iterate f x = x:map f (iterate f x)

by showing

approx n (iterate f x) = approx n (x:map f (iterate f x))

for all natural numbers
n
. And, of course, we can use induction over the natural numbers to establish this fact. The details are left as an easy exercise.

As another example, consider the value
primes
defined in the previous section. Suppose we define
prs n = approx n primes

We would like to show that
prs n
=
p
₁
:
p
^₂
: · · ·
p
_n
:⊥, where
p
_j
is the
j
th prime. We claim that

prs n = approx n (2:([3..] \\ crs n))

crs n = mergeAll [map (p*) [p..] | p <- prs n]

Given this, it is sufficient to show that
crs n
=
c
₁
:
c
²
: · · ·
c
_m
:⊥, where
c
_j
is the
j
th composite number (so
c
₁
= 4) and
Then the proof is completed by using the fact that
which is a non-trivial result in Number Theory. Details are in the exercises.

Computable functions and recursive definitions

One can describe many functions in mathematics, but only some of them are computable. There are two properties of computable functions not shared by arbitrary functions. Firstly, a computable function
f
is
monotonic
with respect to the approximation ordering. In symbols,
x
⊑
y
⇒
f
(
x
) ⊑
f
(
y
)

for all
x
and
y
. Roughly speaking, monotonicity states that the more information you supply about the argument, the more information you get as a result. Secondly, a computable function
f
is
continuous
, which means that

for all chains of approximations
x
₀
⊑
x
₁
⊑ . . .. Roughly speaking, continuity states that there are no surprises on passing to the limit.

Continuity appears similar to chain completeness but differs in two respects. One is that the chain completeness of
P
does not imply the converse property that if
P
is false for all approximations, then
P
is false for the limit. In other words, it does not imply that ¬
P
is chain complete. Secondly,
P
is a mathematical assertion, not a Haskell function returning a boolean value.

Although we won’t prove it, every monotonic and continuous function
f
has a
least fixed point
. A fixed point of a function
f
is a value
x
such that
f
(
x
) =
x
. And
x
is a least fixed point if
x
⊑
y
for any other fixed point
y
. The least fixed point of a monotonic and continuous function
f
is given by lim
_n
→∞
x
_n
where
x
₀
=⊥ and
x
_n
+1
=
f
(
x
_n
). In functional programming, recursive definitions are interpreted as least fixed points.

Here are three examples. Consider the definition
ones = 1:ones
. This definition asserts that
ones
is a fixed point of the function
(1:)
. Haskell interprets it as the least fixed point, so
ones
= lim
_n
→∞
ones
_n
, where
ones
₀
=⊥ and
ones
_n
+1
=
1:ones
_n
. It is easy to see that
ones
_n
is the partial list consisting of
n
ones, so the limit is indeed an infinite list of ones.

Second, consider the factorial function

fact n = if n==0 then 1 else n*fact (n-1)

We can rewrite this definition in the equivalent form

fact = (\f n -> if n==0 then 1 else n*f(n-1)) fact

Again, this definition asserts that
fact
is a fixed point of a function. Here we have

fact
₀
n =
⊥

fact
₁
n = if n==0 then 1 else
⊥

fact
²
n = if n<=1 then 1 else
⊥

and so on. The value of
fact
_k
n
is the factorial of
n
if
n
is less than
k
, and ⊥ otherwise.

Finally, consider the list
primes
once again. Here we have

It is not the case that
primes
_n
=
approx n primes
. In fact,

primes
₁
=
2 :⊥

primes
²
=
2 : 3 :⊥

primes
₃
=
2 : 3 : 5 : 7 :⊥

primes
₄
=
2 : 3 : 5 : 7 : · · · : 47 :⊥

The partial list
primes
²
produces all the primes less than 4,
primes
₃
all the primes less than 9, and
primes
₄
all the primes less than 49. And so on.

Our next example of infinite lists is entertaining as well as instructive. Not only does it introduce the idea of using potentially infinite lists to model a sequence of interactions between processes, it also provides another concrete illustration of the necessity for formal analysis.

The paper–rock–scissors game is a familiar one to children, though it is known by different names in different places. The game is played by two people facing one another. Behind their backs, each player forms a hand in the shape of either a rock (a clenched fist), a piece of paper (a flat palm) or a pair of scissors (two fingers extended). At a given instant, both players bring their hidden hand forward. The winner is determined by the rule ‘paper wraps rock, rock blunts scissors, and scissors cut paper’. Thus, if player 1 produces a rock and player 2 produces a pair of scissors, then player 1 wins because rock blunts scissors. If both players produce the same object, then the game is a tie and neither wins. The game continues in this fashion for a fixed number of rounds agreed in advance.

Our objective in this section is to write a program to play and score the game. We begin by introducing the types

data Move
= Paper | Rock | Scissors

type Round = (Move,Move)

To score a round we define

where

Each player in the game will be represented by a certain strategy. For instance, one simple strategy is, after the first round, always to produce what the opposing player showed in the previous round. This strategy will be called
copy
. Another strategy, which we will call
smart
, is to determine a move by analysing the number of times the opponent has produced each of the three possible objects, and calculating an appropriate response based on probabilities.

We will consider the details of particular strategies, and how they can be represented, in a moment. For now, suppose the type
Strategy
is given in some way. The function
rounds :: (Strategy,Strategy) -> [Round]

takes a pair of strategies and returns the infinite list of rounds that ensue when each player follows his or her assigned strategy. The function

match :: Int -> (Strategy,Strategy) -> (Int,Int)

match n = total . map score . take n . rounds

where total rs = (sum (map fst rs),sum (map snd rs))