[Haskell-cafe] Functional progr., infinity, and the Universe
Paul Hudak
paul.hudak at yale.edu
Thu Jun 22 22:30:19 EDT 2006
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
More information about the Haskell-Cafe
mailing list