No subject

	   Zero < Succ undefined				-- Note: same as Zero < Succ _|_

	=3D True						-- by the 2nd equation defining order

And Succ (Succ _|_ ) is an element of Nat:

	   Succ Zero < Succ (Succ undefined)		-- Note: same as Zero < Succ (Succ _=
|_ )

	=3D Zero < Succ undefined				-- by the 4th equation defining order

	=3D True						-- by the 2nd equation defining order

And Succ (Succ (Succ _|_ ) is an element of Nat, and so forth.

So the list of elements in Nat expands:

..., Succ (Succ (Succ _|_ )),  Succ (Succ _|_ ),  Succ _|_, _|_,  Zero,  Su=
cc Zero,  Succ (Succ Zero),  Succ (Succ (Succ Zero)), ...

One can interpret the extra values in the following way:=20

_|_ corresponds to the natural number about which there is absolutely no in=
formation

Succ _|_ to the natural number about which the only information is that it =
is greater than Zero

Succ (Succ _|_ ) to the natural number about which the only information is =
that it is greater than Succ Zero

And so on

There is one further value of Nat, namely the "infinite" number:

	Succ (Succ (Succ (Succ ...)))

It can be defined by this function:

	infinity :: Nat
	infinity =3D Succ infinity

It is different from all the other Nat values because it is the only number=
 for which Succ m < infinity for all finite numbers m:=20

	Zero < infinity
	=3D True

	Succ Zero < infinity
	=3D True

	Succ (Succ Zero) < infinity
	=3D True

Thus, the values of Nat can be divided into three classes:

-  The finite values, Zero,  Succ Zero,  Succ (Succ Zero), and so on.
-  The partial values, _|_,  Succ _|_,  Succ (Succ _|_ ), and so on.
-  The infinite value.

Important: the values of *every* recursive data type can be divided into th=
ree classes:

-  The finite values of the data type.
-  The partial values, _|_, and so on.
-  The infinite values.

Although the infinite Nat value is not of much use, the same is not true of=
 the infinite values of other data types.

Recap: We have discussed two aspects of the holy trinity of functional prog=
ramming: recursive data types and recursively defined functions over those =
data types. The third aspect is induction, which is discussed now.

Induction allows us to reason about the properties of recursively defined f=
unctions over a recursive data type.=20

In the case of Nat the principle of induction can be stated as follows: in =
order to show that some property P(n) holds for each finite number n of Nat=
, it is sufficient to treat two cases:

	Case (Zero). Show that P(Zero) holds.

	Case (Succ n). Show that if P(n) holds, then P(Succ n) also holds.

As an example, let us prove this property (the identity for addition):

	Zero + n =3D n

Before proving this, recall that + is defined by these two equations:

	m + Zero =3D m
	m + Succ n =3D Succ(m + n)

Proof: The proof is by induction on n.=20

Case (Zero). Substitute Zero for n in the equation Zero + n =3D n. So we ha=
ve to show that Zero + Zero =3D Zero, which is immediate from the first equ=
ation defining +.

Case (Succ n). Assume P(n) holds; that is, assume Zero + n =3D n holds. Thi=
s equation is referred to as the induction hypothesis. We have to show that=
 P(Succ n) holds; that is, show that Zero + Succ n =3D Succ n holds. We do =
so by simplifying the left-hand expression:

	   Zero + Succ n

	=3D Succ (Zero + n) 			-- by the 2nd equation defining +

	=3D Succ (n) 				-- by the induction hypothesis

We have proven the two cases and so we have proven that Zero + n =3D n hold=
s for all finite numbers of Nat.

Full Induction. To prove that a property P holds not only for finite member=
s of Nat, but also for every partial (undefined) number, then we have to pr=
ove three things:

	Case ( _|_ ). Show that P( _|_ ) holds.

	Case (Zero). Show that P(Zero) holds.

	Case (Succ n). Show that if P(n) holds, then P(Succ n) holds also.

To just prove that a property P holds for every partial (undefined) number,=
 then we omit the second case.

To illustrate proving a property that holds for every partial number (not f=
or the finite numbers), let us prove the rather counterintuitive result tha=
t m + n =3D n for all numbers m and all partial numbers n.

For easy reference, we repeat the definition of +

	m + Zero =3D m
	m + Succ n =3D Succ(m + n)

Proof: The proof is by partial number induction on n.

Case ( _|_ ). Substitute _|_ for n in the equation m + n =3D n. So we have =
to show that m + _|_ =3D _|_, which is true since _|_ does not match either=
 of the patterns in the definition of +.

Case (Succ n). We assume P(n) holds; that is, assume m + n =3D n holds. Thi=
s equation is the induction hypothesis. We have to show that P(Succ n) hold=
s; that is, show that m + Succ n =3D Succ n holds. For the left-hand side w=
e reason

	   m + Succ n

	=3D Succ(m + n)				-- by the second equation for +

	=3D Succ(n)				-- by the induction hypothesis

Since the right-hand side is also Succ n, we are done.

The omitted case (m + Zero =3D Zero) is false, which is why the property do=
es not hold for finite numbers.

As an added bonus, having proved that an equation holds for all partial (un=
defined) numbers, we can assert that it holds for the infinite number too; =
that is, P(infinity) holds. Thus, we can now assert that m + infinity =3D i=
nfinity for all numbers m.