![]() ![]() (in particular the “001-infinitary” one), where $y \rightarrow_\beta^\infty \lambda f.fff\ldots$, see for instance the original paper, the survey in Barendregt and Manzonetto's Satellite, or some recent presentations here or there. This can be turned into a “real” common reduct in an infinitary λ-calculus ![]() Recall the head-internal decomposition of β-reduction: a reduction $M \rightarrow_(\theta) = \lambda f.fff\ldots$ I’ll also go through some exercises in my upcoming post.The result, left as an exercise by Barendregt (Exercise 6.8.9), is proved by Klop in a 2007 paper (Proposition 1.2). If you want to know more terminology and formal illustrations, this medium article and the lambda calculus wikipedia page may be a good start. So, we have Y g = g (Y g)! Just like rec!Ĭool right? By now you have grasped the concepts of the Y combinator. = g (g ((λx.g (x x)) (λx.g (x x)))) (infinite replacements can be made)įrom lines 2 and 3 above, we can see that Y g = (λx.g (x x)) (λx.g (x x)) = g ((λx.g (x x)) (λx.g (x x))) = (λx.g (x x)) (λx.g (x x)) (replace f with input g) x ( U U x)) g, so after the second you have g(UUg) g ( U U g) as required, but you havent substituted the second x x correctly, leaving both it and the g g that the function is applied to, giving you g(UUx)g g ( U U. Let’s verify that it behaves like rec by giving it an input g: Y g = λf.(λx.f (x x)) (λx.f (x x)) g (replace Y with its definition) After the first reduction, you (should) have (x. Like loop, we can encode rec in lambda calculus too! But we call rec ‘Y’ in lambda calculus this time, because this encoding is the famous Y-combinator that lets you have recursion in any languages: Y = λf.(λx.f (x x))(λx.f (x x)) The general recursion function can easily become any recursive function because f can be whatever you like! The Y-combinator = f (f (f (.)).) (infinite replacements can be made) = f (f (rec f)) (replace rec f with f (rec f)) In mathematics, it looks like this: rec f = f (rec f) A general recursion function (named rec) takes itself as the input. Self-application takes us to general recursion. (λx.x x) is applied to an input like itself! General Recursion We got this property from the self-application of the function (λx.x x). You can see that encoding loop as above gives us a function that behaves like loop. = (λx.x x)(λx.x x) (infinite replacements can be made) In loop, one applies the function (λx.x x) to the input (λx.x x): (λx.x x)(λx.x x) = (λx.x x)(λx.x x) (replace each x with the input) Recall that in lambda calculus, what we do with two items side by side is to apply the first item as a function to the second item as an input. When you evaluate loop, you go to loop‘s definition, which is loop! We can encode a function that behaves like loop in lambda calculus: loop = (λx.x x)(λx.x x) The function loop does only one thing: calling itself. In this video, Professor Hutton shows us the simplest recursion he can think of: If you haven’t read my last post already, please do so! It’d be easier for you to follow this post, especially if you don’t know any lambda calculus. This enables you to do recursion in any languages! In this post I further proves the point by encoding recursion in it. In the last post I talked about how powerful lambda calculus is. ![]()
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |