[Haskell-cafe] Formalizing lazy lists?
gregory.woodhouse at sbcglobal.net
Fri Nov 18 19:14:54 EST 2005
--- Lennart Augustsson <lennart at augustsson.net> 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 <gregory.woodhouse at sbcglobal.net>
"Interaction is the mind-body problem of computing."
More information about the Haskell-Cafe