Formalizing lazy lists?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Formalizing lazy lists?

Gregory Woodhouse
Maybe this is old hat, but the question about detecting loops in data
structures got me thinking about this. I know you can encode the cons
operator (and ordinary lists) in pure lambda calculus, but how could
you possibly represent something like [0, 1..]? One thought that
occurss to me is to treat it ass a kind of direct limit, but of course,
the essence of a structure like this is that the ith entry is
computable in a natural way, and it seems that an algebraic limit
couldn't really capture this intuition unless we were to introduce some
sort of higher order structure (which may be what we want, anyway).


===
Gregory Woodhouse  <[hidden email]>


"Interaction is the mind-body problem of computing."

--Philip Wadler











_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Lennart Augustsson
What do you mean by represent?
It's easy enough to write down the lambda term that is the
encoding of [0..].

        -- Lennart


Greg Woodhouse wrote:

> Maybe this is old hat, but the question about detecting loops in data
> structures got me thinking about this. I know you can encode the cons
> operator (and ordinary lists) in pure lambda calculus, but how could
> you possibly represent something like [0, 1..]? One thought that
> occurss to me is to treat it ass a kind of direct limit, but of course,
> the essence of a structure like this is that the ith entry is
> computable in a natural way, and it seems that an algebraic limit
> couldn't really capture this intuition unless we were to introduce some
> sort of higher order structure (which may be what we want, anyway).
>
>
> ===
> Gregory Woodhouse  <[hidden email]>
>
>
> "Interaction is the mind-body problem of computing."
>
> --Philip Wadler
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Gregory Woodhouse


--- Lennart Augustsson <[hidden email]> wrote:

> What do you mean by represent?
> It's easy enough to write down the lambda term that is the
> encoding of [0..].
>
> -- Lennart
>

You mean like \x -> x ? If I apply it to the Church numeral i, I get i
in return.  But that hardly seems satisifying because infinite lists
seem to be a wholly different type of object.


===
Gregory Woodhouse  <[hidden email]>


"Interaction is the mind-body problem of computing."

--Philip Wadler











_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Lennart Augustsson
How about:

nil = \ n c . n
cons x xs = \ n c . c x xs

zero = \ z s . z
suc n = \ z s . s n

listFromZero = Y ( \ from n . cons n (from (suc n))) zero

(Untested, so I might have some mistake.)

        -- Lennart

Greg Woodhouse wrote:

>
> --- Lennart Augustsson <[hidden email]> wrote:
>
>
>>What do you mean by represent?
>>It's easy enough to write down the lambda term that is the
>>encoding of [0..].
>>
>> -- Lennart
>>
>
>
> You mean like \x -> x ? If I apply it to the Church numeral i, I get i
> in return.  But that hardly seems satisifying because infinite lists
> seem to be a wholly different type of object.
>
>
> ===
> Gregory Woodhouse  <[hidden email]>
>
>
> "Interaction is the mind-body problem of computing."
>
> --Philip Wadler
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Gregory Woodhouse


--- Lennart Augustsson <[hidden email]> wrote:

> How about:
>
> nil = \ n c . n
> cons x xs = \ n c . c x xs
>
> zero = \ z s . z
> suc n = \ z s . s n
>
> listFromZero = Y ( \ from n . cons n (from (suc n))) zero
>
> (Untested, so I might have some mistake.)
>
> -- Lennart
>

Okay, I see what you mean here. What I was thinking is that repeatedly
unfolding Y give us kind of an algorithm to extract initial segments of
the list (like "from"), but there's something disquieting about all of
this. Maybe it's just my lack of familiarity with lambda calculus, but
I think one thing I got used to as a student was the idea that if I
started peeling back layers from an abstract defintion or theorem, I'd
end up with something that looked familiar. Now, to me a list
comprehension is something like an iterative recipe. Maybe [0, 1, ..]
is something "primitive" that can only really be understood
recursively, and then a comprehension like

[ x*x | x <- [0, 1..] ]

is something easily built from that (or itself defined as a fixed
point), but it would be nice to see the iterative recipe somehow "fall
out" of the more formal definition in terms of Y.


===
Gregory Woodhouse  <[hidden email]>


"Interaction is the mind-body problem of computing."

--Philip Wadler











_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Lennart Augustsson
Greg Woodhouse wrote:

>
> --- Lennart Augustsson <[hidden email]> wrote:
>
>
>>How about:
>>
>>nil = \ n c . n
>>cons x xs = \ n c . c x xs
>>
>>zero = \ z s . z
>>suc n = \ z s . s n
>>
>>listFromZero = Y ( \ from n . cons n (from (suc n))) zero
>>
>>(Untested, so I might have some mistake.)
>>
>> -- Lennart
>>
>
>
> Okay, I see what you mean here. What I was thinking is that repeatedly
> unfolding Y give us kind of an algorithm to extract initial segments of
> the list (like "from"), but there's something disquieting about all of
> this.

Unfolding Y is indeed part of the algorithm to generate the list.
The lambda calculus is "just" another programming language, so
why does this disturb you?


  Maybe it's just my lack of familiarity with lambda calculus, but

> I think one thing I got used to as a student was the idea that if I
> started peeling back layers from an abstract defintion or theorem, I'd
> end up with something that looked familiar. Now, to me a list
> comprehension is something like an iterative recipe. Maybe [0, 1, ..]
> is something "primitive" that can only really be understood
> recursively, and then a comprehension like
>
> [ x*x | x <- [0, 1..] ]
>
> is something easily built from that (or itself defined as a fixed
> point), but it would be nice to see the iterative recipe somehow "fall
> out" of the more formal definition in terms of Y.

List comprehensions are just a different way of writing concats
and maps, both of which have recursive definitions.

What is an "iterative recipe"?

        -- Lennart
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Gregory Woodhouse


--- Lennart Augustsson <[hidden email]> wrote:

>
> Unfolding Y is indeed part of the algorithm to generate the list.
> The lambda calculus is "just" another programming language, so
> why does this disturb you?
>

Well...think about this way. The function

f i = [1, 1 ..]!!i

is just a constant function expressed in a complicated way. Can I
algoritmically determine that f is a constant function? For any
particular value of i, the calculations you give demonstrate that f i =
1. It's a little less obvious that f really is constant. Yes, I know
this can be proved by induction, but verifying a proof is not the same
as discovering the theorem in the first place.

I suppose the big picture is whether I can embed the theory of finite
lists in the theory of infinite lists, preferably in such a way that
the isomorphism of the theory "finite lists" with the embedded
subtheory is immediately obvious.


===
Gregory Woodhouse  <[hidden email]>


"Interaction is the mind-body problem of computing."

--Philip Wadler











_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Formalizing lazy lists?

Lennart Augustsson
Greg Woodhouse wrote:
> Well...think about this way. The function
>
> f i = [1, 1 ..]!!i
>
> is just a constant function expressed in a complicated way. Can I
> algoritmically determine that f is a constant function?

In general, no.  Even in this case I'm pretty sure you'll need induction
somewhere.


> I suppose the big picture is whether I can embed the theory of finite
> lists in the theory of infinite lists, preferably in such a way that
> the isomorphism of the theory "finite lists" with the embedded
> subtheory is immediately obvious.

I don't think you'll find such an embedding that is "satisfying", i.e.,
that gives you much insight.  Reasoning about total functions on
finite lists can be done with sets (and set theory), reasoning about
partial functions and/or lazy lists needs domains.
An example
        reverse . reverse = id
is true for all finite lists, but not true for any infinite lists
(nor any partial lists).
(What remains true for all lists is that
        reverse . reverse <= id
where <= is the usual domain ordering.)

        -- Lennart
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe