[Haskell-cafe] Infinite lists and lambda calculus

[Lennart Augustsson]

Greg Woodhouse wrote:
> Perhaps the issue is that the manipulations below are purely syntactic,
But all the computation rules of the lambda calculus are "syntactic"
in that sense.  When you can prove things by symbol pushing it's
the easiest way.

But as Paul Hudak mentioned, there definitions that are equal, but
you need something stronger to prove it, like fix point induction.

> and though they work, it is not at all clear how to make contact with
> other notions of computability. Perhaps it is that
> 
> Y = (\f. (\x. f (x x)) (\x. f (x x))) 
> 
> is a perfect sensible definition, it's still just a recipe for a
> computation. Maybe I'm thinking too hard, but it reminds me of the mu
> operator. Primiive recursive functions are nice and constructive, but
> minimization is basically a "search", there's no guarantee it will
> work. If I write
> 
> g(x) = mu x (f(x) - x)
> 
> then I've basically said "look at every x and stop when you find a
> fixed point". Likewise, given a candidate for f, it's easy to verify
> that Y f = f (Y f), as you've shown, but can the f be found without
> some kind of "search"?
There is no search with this defintion (as you can see), it's very
constructive.

It computes the fix point which you can also define as
                  oo
	fix f = lub f^i(_|_)
                 i=0
where f^i is f iterated i times.  Is that a definition
of fixpoint that makes you happier?

> Since there are recursive functions that aren't
> primitive recursive, the answer has to be "no".
Where did primitive recursion come from?  Y is used
to express general recursion.

> 
> Finally, you've exhibited a sequence of fixed points, and in this case
> it's intuitively clear how these correspond to something we might call
> an infinite list. But is there an interpetration that makes this
> precise? The notation
> 
> ones = cons 1 ones
> ones = cons 1 (cons 1 ones)
> ...

The list ones is the least upper bound in the domain of lazy (integer)
lists of the following chain
_|_, cons 1 _|_, cons 1 (cons 1 _|_), ...

How much domain theory have you studied?  Maybe that's where you can
find the connection you're missing?

	-- Lennart