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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
