fixpoint operator for ULC with specific reduction property
Hello, I'm looking for a fixpoint operator Z for the untyped lambda calculus that has the property Z g --> g (Z g) for any g. The best-known fixpoint operator Y := \f. (\x. f (x x)) (\x. f (x x)) does not have this property, but only Y g --> T <-- g (Y g) for some T. Does anybody know such a Z I'm looking for? Greetings, ben ps. Please keep me in CC, since I'm not currently subscribed to the list.
ben wrote:
I'm looking for a fixpoint operator Z for the untyped lambda calculus that has the property
Z g --> g (Z g)
for any g.
The best-known fixpoint operator Y := \f. (\x. f (x x)) (\x. f (x x)) does not have this property, but only
Y g --> T <-- g (Y g)
for some T.
Does anybody know such a Z I'm looking for?
I think the Turing fixed point combinator does exactly that. It's defined as Theta = (λxf.f(xxf))(λxf.f(xxf)) Related: http://www.mail-archive.com/haskell-cafe@haskell.org/msg43467.html Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com
Heinrich Apfelmus wrote:
ben wrote:
I'm looking for a fixpoint operator Z for the untyped lambda calculus that has the property
Z g --> g (Z g)
for any g. [...]
I think the Turing fixed point combinator does exactly that. It's defined as
Theta = (λxf.f(xxf))(λxf.f(xxf)) [...]
Theta precisely meets my needs. Thanks a lot. ben
participants (2)
-
ben -
Heinrich Apfelmus