Return to Answer

Our proof proceeds by structural induction on a.
For the base case let a be Zero. plus Zero Zero = match Zero with |Zero -> Zero | Succ(c) -> let r = plus c b in Succ(r) so we know plus Zero Zero = Zero. Let a be a nat. Assume the inductive hypothesis that plus a Zero = a. We now show that plus (Succ(a)) Zero = Succ(a) this is obvious since plus (Succ(a)) Zero = match a with |Zero -> Zero | Succ(a) -> let r = plus a Zero in Succ(r) = let r = a in Succ(r) = Succ(a) Thus, by induction plus a Zero = a for all a in nat

data Stream a = Stream a (Stream a) --"data" not "newtype"

and this is a perfectly valid definition. Whats more, we can perform co-recursion on this co-data. Actually, it is possible for a function to be both co-recursive and recursive. While recursion was defined by the function having a domain consisting of data, co-recursion just means it has a co-domain (also called the range) that is co-data. Primitive recursion meant always "calling oneself" on smaller data until reaching some smallest data. Primitive co-recursion always "calls itself" on data greater than or equal to what you had before.

fibs = 0:1:zipWith (+) fibs (tail fibs)
fib' n = fibs !! n --the !! is haskell syntax for index at

an interesting example of induction/coinduction is proving that these two definitions compute the same thing. This is left as an exercise for the reader.

Our proof proceeds by structural induction on a.

1. For the base case let a be Zero. plus Zero Zero = match Zero with | Zero -> Zero | Succ(c) -> (let r = plus c b in Succ(r)) = Zero so we know plus Zero Zero = Zero.
2. Let a be a nat. Assume the inductive hypothesis that plus a Zero = a. We now show that plus (Succ(a)) Zero = Succ(a). This is obvious since plus (Succ(a)) Zero = match (Succ(a)) with | Zero -> Zero | Succ(c) -> (let r = plus c Zero in Succ(r)) = (let r = plus a Zero in Succ(r)) = (let r = a in Succ(r)) = Succ(a)
3. Thus, by induction plus a Zero = a for all a in nat

data Stream a = SCons a (Stream a) --"data" not "newtype"

and this is a perfectly valid definition. Whats more, we can perform co-recursion on this co-data. Actually, it is possible for a function to be both co-recursive and recursive.

While recursion was defined by the function having a domain consisting of data, co-recursion just means it has a co-domain (also called the range) that is co-data.

Primitive recursion meant always "calling oneself" on smaller data until reaching some smallest data. Primitive co-recursion always "calls itself" on data greater than or equal to what you had before.

fibs = 0:1:zipWith (+) fibs (tail fibs)
fib' n = fibs !! n --the !! is haskell syntax for "at index"

an interesting example of induction/coinduction is proving that these two definitions, fib and fib', compute the same thing. This is left as an exercise for the reader.

One thing to not about this definition is that the number

Or, perhaps more usefully for a computer scientist:

One thing to note about this definition is that a number

Or, perhaps more useful for a computer scientist:

Let a be a set. The set "Stream of a" is defined as the largest set such that given x such that x is in stream of a, x consists of the ordered pair (head,tail) such that head is in a, and tail is in Stream of a

Let a be a set. The set "Stream of a" is defined as the largest set such that for each x in the stream of a, x consists of the ordered pair (head,tail) such that head is in a and tail is in Stream of a