![]() The internals of many functional programming languages such as Haskell, are heavily based on lambda calculus It embodies some of the most important concepts of functional programmingįor example, pure functions, unary functions, currying. There are a few reasons to learn lambda calculus, the main ones I can think of are: If after reading this you are interested in learning more about functional programming in JavaScript, I recommend this Udemy course (affiliate link):įunctional Programming For Beginners With JavaScript Why should I learn lambda calculus? In this article I want to look at what lambda calculus is, why you might want to learn about it, and explain the key concepts and the terminology of lambda calculus using both lambda syntax and ‘equivalent’ JavaScript code snippets. One of the main areas of study that is often cited as significant for functional programmers is lambda calculus. Simply typed lambda calculus is confluent as well, and so in that context we can say β-reduction always terminates in a unique expression (again up to α-conversion).I have recently become very interested in functional programming - using pure functional languages such as Haskell, as well as functional programming in JavaScript. This implies that if β-reduction does terminate, then it terminates in a unique expression (up to α-conversion, i.e. That is, if an expression P can be transformed by β-reduction two different ways into expressions M and N, then there is an expression T such that both M and N can be reduced to T. ConfluenceĪlthough β-reduction is not normalizing for untyped lambda calculus, the Church-Rosser theorem says it is confluent. To summarize, β-reduction is not normalizing, not even weakly, in the context of untyped lambda calculus, but it is strongly normalizing in the context of simply typed lambda calculus. You can prove that not only does this rule out specific examples like those above, it rules out all possible examples that would prevent β-reduction from terminating. This is because x takes something of type A, not something of type function from A to B. If x is a function that takes an argument of type A and returns an argument of type B then you can’t apply x to itself. This additional structure prevents examples such as those above that fail to normalize. In simply typed lambda calculus, we assign types to every variable, and functions have to take the right type of argument. Beta reduction is neither strongly nor weakly normalizing in the context of (untyped) lambda calculus. It’s weakly normalizing if there’s at least some sequence of applying the rules that terminates. A rewrite system is strongly normalizing if applying the rules in any order eventually terminates. The technical term for what we’ve seen is that β-reduction is not normalizing. ![]() Beta “reduction” doesn’t reduce the expression at all but makes it bigger. ![]() Applying β-reduction the first time gives (λ x. Beta reduction gets stuck in an infinite loop. But when we do that, we get the original expression (λ x. Beta reduction says to replace each of the red xs with the expression in blue. Au contraire!Ĭonsider the expression (λ x. You might reasonably expect that if you apply β-reduction enough times you eventually get an expression you can’t reduce any further. ![]() When you do apply β-reduction several times, does the process always stop? And if you apply β-reduction to parts of an expression in a different order, can you get different results? Failure to normalize In a more complicated expression, you might be able to apply β-reduction several times. Then β-reduction rewrites this expression as y + 2. x + 2) y, which means apply to y the function that takes its argument and adds 2. We will first show that β-reduction holds some surprises, then explain how these surprises go away when you add typing. If you have a function described by what it does to x and apply it to an argument t, you rewrite the xs as ts. The formal definition of β-reduction is more complicated than this in order to account for free versus bound variables, but this informal description is sufficient for this blog post. Beta reduction is essentially function application. ![]()
0 Comments
Leave a Reply. |