![]() 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. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |