Talk:Lambda calculus

Thanks for making this page. I don't understand this topic very well, and I'm wondering if someone could give some examples of l.c. expressions that are worked out step by step to a solution? Thanks a lot. Calamari 16:47, 3 Aug 2005 (GMT)

Sure, I'll just grab some examples from my Lambda Calculus pages. --Safalra 18:08, 3 Aug 2005 (GMT)

That's great. Thank you very much! Calamari 04:51, 4 Aug 2005 (GMT)

If, after looking at the various lambda calculus webpages, you want to get a more-thorough introduction, I think Introduction to Lambda Calculus (53 pages) by Barendregt & Barendsen is hard to beat. It's still available online in a few places (it used to be at citeseer, but no longer?). At the moment, one such place for the 2000 revision seems to be www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/geuvers.pdf --r.e.s. (Talk) 18:56, 4 Aug 2005 (GMT)

Printed! :D Calamari 16:22, 5 Aug 2005 (GMT)

Can't print it out but currently reading it on the screen. :) Cheers r.e.s.! --User:Keymaker

Fixed-point function

Just how does the fixed-point function let functions access themselves? --Ihope127 00:38, 17 Oct 2005 (GMT)

Call the fixed-point function Y. Then Yfx becomes f(Yf)x which becomes f(f(Yf))x. Here f can either throw away its first parameter, or use it to call itself on some value. Permit me to introduce some high-level syntax to make this easier to understand. Let f=lambda gn.(if n=1 then 1 else n*g(n-1)), then Yf is the factorial function. Consider Yf2. This becomes f(Yf)2 which becomes 2*(Yf)1, which becomes 2*f(Yf)1, which becomes 2*1, which becomes 2. I hope that's not too unclear. --Safalra 09:47, 17 Oct 2005 (GMT)

Now I get it. If you have a function ^tx.stuff, t can be used to mean "this function", if you first apply the fixed-point function to ^tx.stuff. So the "blackhole function" would be ^xy.x (i.e. K) with Y applied to it, so that you would have ^y.x where x is the blackhole function again. --Ihope127 18:26, 3 Nov 2005 (GMT)