[Haskell-beginners] Re: howto reason infinite lists

[Heinrich Apfelmus]

prad wrote:
> i'm trying to figure out how to think out the circular definition for
> an infinite list and would appreciate suggestions.
> 
> consider
> ones = 1 : ones
> this essentially says 1 : (1 : (1 : (1 : ones))) with ones being given
> by the original def.
> 
> however, i had trouble with this one
> fib = 1 : 1 : [ a+b | (a,b) <- zip fib (tail fib) ]

The Haskell wikibook has some material on this:

   http://en.wikibooks.org/wiki/Haskell/Denotational_semantics


Basically, the key question is: "What is a recursive definition, 
anyway?". The answer to that is that any recursively defined value is 
obtained from a sequence of approximations. We start with the worst 
approximation called ⊥ ("bottom") which basically means "it's undefined, 
we don't know what it is".

   fib_0 = ⊥

To get a better approximation, we apply the definition of  fib  to that.

   fib_1 = 1 : 1 : [ a+b | (a,b) <- zip fib_0 (tail fib_0) ]
         = 1 : 1 : [ a+b | (a,b) <- zip ⊥ (tail ⊥) ]
         = 1 : 1 : [ a+b | (a,b) <- zip ⊥ ⊥ ]
         = 1 : 1 : [ a+b | (a,b) <- ⊥ ]
         = 1 : 1 : ⊥

To get an even better approximation, we once again apply the equation 
for  fib  to this approximation:

   fib_2 = 1 : 1 : [ a+b | (a,b) <- zip fib_1 (tail fib_1) ]
         = 1 : 1 : [ a+b | (a,b) <- zip (1:1:⊥) (tail (1:1:⊥)) ]
         = 1 : 1 : [ a+b | (a,b) <- zip (1:1:⊥) (1:⊥) ]
         = 1 : 1 : [ a+b | (a,b) <- (1,1):⊥ ]
         = 1 : 1 : 2 : ⊥

and so on and so on. The limit of these approximations

   fib_0 = ⊥
   fib_1 = 1 : 1 : ⊥
   fib_2 = 1 : 1 : 2 : ⊥
   fib_3 = 1 : 1 : 2 : 3 : ⊥
   ...

is the infinite list

   fib = 1 : 1 : 2 : 3 : 5 : ...


This is the thinking that you have described, with a minor, but crucial 
change. Namely, it's not clear that your list elements  a,b,c,d,  etc. 
exist a priori, i.e. that the list is already created in this form. For 
instance, it wouldn't be right to say that the example

   foo = 1 : 1 : loop
       where loop = loop

can be written as

   foo = [1,1,a,b,c, ..]

because the recursion simply won't progress past

   foo = 1 : 1 : ⊥

The formulation with ⊥ can handle such cases. In other words, your 
thinking is right but somewhat restricted to a few particular examples 
while the method using ⊥ as shown here will *always* apply.

The key message to take away is that you also need some way (⊥) to 
express recursive definitions that might loop forever.


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com