[Haskell-beginners] Re: howto reason infinite lists
Heinrich Apfelmus
apfelmus at quantentunnel.de
Wed Jun 23 07:02:38 EDT 2010
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
More information about the Beginners
mailing list