[Haskell-cafe] Functional progr., infinity, and the Universe

[Paul Hudak]

Actually Brian's intuition is right on target.  One way to define an 
infinite list is as the limit of an infinite chain of partial lists 
(which, in domain theory, is essentially how all elements are defined). 
  A chain is a sequence a1 <= a2 <= ... <= an, where <= is the domain 
ordering.  A partial list is any list ending in _|_ (i.e. bottom).

So, for example, the infinite list of ones can be defined as the limit 
of the following chain:
_|_
<= 1 : _|_
<= 1 : 1 : _|_
<= 1 : 1 : 1 : _|_
...
To verify that this is a chain, remember that (:) is right associative, 
and _|_ <= x for all x.

Or, another way to look at this, is that the infinite list is the LUB 
(least upper bound) of the infinite set of all of these partial (but 
finite) lists.  That explanation corresponds most closely with Brian's 
intuition.

If anyone thinks that this explanation is baroque, I should also point 
out that in a pragmatic sense this idea forms the basis for doing 
inductive proofs on programs generating infinite lists (as described in 
my book, as well as in many other sources).

   -Paul


jerzy.karczmarczuk at info.unicaen.fr wrote:
> Brian Hulley wrote:
> 
>> Couldn't an infinite list just be regarded as the maximum element of 
>> the (infinite) set of all finite lists?
> 
> Brian, I will say something you might find acrimonious and impolite, but
> it is serious, you might find this in some philosophical works.
> If you are right, then YOU JUST PROVED THE EXISTENCE OF GOD.
> =========================================
> More seriously...
> Perhaps you (and possibly Piotr Kalinowski) would look up some materials
> on intuitionism in mathematics, on the constructive theory of sets, etc.
> 
> Jerzy Karczmarczuk