4 ms·

That's not immediately clear at all! A β-reduction is basically the same as a function call, we know how to implement those, and they take constant time. Your

That's not immediately clear at all! A β-reduction is basically the same as a function call, we know how to implement those, and they take constant time. Your example could be directly interpreted as a program in e.g. Lisp or ML, and there the function call is definitely not implemented by stepping through the entire program symbol by symbol. I think the issue in the stackoverflow post above is that the lambda calculus is nondeterministic, so if you try to define the cost as the smallest number of β-reductions to reduce a term to a value, then you're in trouble because it's in general very hard to figure out what the optimal way of reducing a program would be. But that also shows that it's a completely unrealistic model. Surely what we should do is pick an evaluation order, e.g. call-by-value, and then count the number of reductions there. This corresponds to what actually happens when you run your program on a real computer. In fact, CBV evaluation is really well-behaved, and you can given an extremely intuitive cost semantics to such a lambda calculus: see section 7.4 in [1], and also see [2] to show that this semantics is sound in the sense that you can compile it down to an abstract machine respecting the cost. (Incidentally, this is something that Bob Harper has been talking about for a long time, see e.g. his blog post [3] for some polemics.) If anything, I think what this argument shows is that Turing machines are bad for complexity-theoretic purposes. We do not want to "analyze our algorithms in terms of atomic operations that can be implemented in O(1) on a Turing machine", we want to count atomic operations that can be executed in O(1) time on the actual computers we run stuff on. So Turing machines are ok if you just want to distinguish polynomial from non-polynomial time, but for finer-grained distinctions you need a more accurate model, like a RAM, or... like the lambda calculus! [1] https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf [2] http://www.cs.cmu.edu/~blelloch/papers/BG95.pdf http://www.cs.cmu.edu/~blelloch/papers/BG95.pdf [3] https://existentialtype.wordpress.com/2011/03/16/languages-and-machines/ https://existentialtype.wordpress.com/2011/03/16/languages-a...

olooney 7y ago
Consider the following lambda calculus expression: ((λ x . ((x x) (x x))) (λ x . ((x x) (x x)))) Under β-reduction, this blows up: doubling with every reduction, never repeating itself, growing infinitely long. Let's name this expression "BlowsUp". Recall that the Church encoding for "false" is "(λ x . (λ y . y))". Recall that this acts like an "if/else" statement, taking two arguments and always returning the second, discarding the first. Then its clear that this expression: ((false BlowsUp) (λ y . y)) or more explicitly, (((λ x . (λ y . y)) ((λ x . ((x x) (x x))) (λ x . ((x x) (x x)))) ) (λ y . y)) should evaluate to "(λ y . y)", the identity function. However, under a call-by-value evaluation strategy, which is eager, the value BlowsUp will need to be evaluated first. Only a lazy evaluation strategy will which first the "false" expression (thereby discarding the part of the program containing BlowsUp entirely, without evaluating it) will succeed. This is an extraordinarily important case, because recursive functions are typically written with two branches: a base case that terminates, and a recursive case that goes on for ever. For example, consider everyone's favorite recursive function, factorial: def factorial(n): if n <= 1: return 1 else: return n * factorial(n-1) Translated into the lambda calculus via the Y combinator, this (and pretty much every other non-trivial recursive function) will exhibit the same property of the above, and will never terminate if evaluated under a strictly eager, call-by-value strategy. Therefore, specifying the call-by-value evaluation strategy is not useful for the purposes of evaluating non-trivial algorithms, which almost always involve recursion. (In the lambda calculus even unbounded iteration must be implemented via recursion so this excludes basically all algorithms of interest to complexity theorists.) Note that languages which use call-by-value for function calls usually have a separate, built-in construct for if/else or && (short-circuiting boolean AND) which allows the programmer to decide when they want to use the "lazy" strategy; the lambda calculus unfortunately is too elegant to admit of such a pragmatic distinction. :) There is of course a so-called "normal" evaluation strategy for lambda calculus (which is guaranteed to work) but it is basically "call-by-name" (to contrast it with the call-by-value nomenclature) and it has the problems I describe above and is hard to analyze. https://sookocheff.com/post/fp/evaluating-lambda-expressions/ https://sookocheff.com/post/fp/evaluating-lambda-expressions...
- vilhelm_s 7y ago
  It's true that some constructions that work under normal/CBN order will go into an infinite loop under CBV order, but this is easy to work around, typically you just need to add an extra lambda to prevent it from evaluating too eagerly. For example, instead of translating if b then e1 else e2 as b e1 e2 you can translate it to (b (λx. e1) (λx. e2)) tt where tt is any value (it doesn't matter what). Similarly, you can make a CBV-version of the Y combinator by eta-expanding some subexpressions to prevent it from evaluating it too eagerly [0]. The exact details of the encoding don't matter too much, because when you actually write programs you want to use some syntactic sugar like "if then else" or "let rec", so you just care that it can be translated into lambda calculus in some way which preserves the operational semantics. [0] https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_fixed_point_combinator https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_...

olooney 7y ago

Consider the following lambda calculus expression: ((λ x . ((x x) (x x))) (λ x . ((x x) (x x)))) Under β-reduction, this blows up: doubling with every reduction, never repeating itself, growing infinitely long. Let's name this expression "BlowsUp". Recall that the Church encoding for "false" is "(λ x . (λ y . y))". Recall that this acts like an "if/else" statement, taking two arguments and always returning the second, discarding the first. Then its clear that this expression: ((false BlowsUp) (λ y . y)) or more explicitly, (((λ x . (λ y . y)) ((λ x . ((x x) (x x))) (λ x . ((x x) (x x)))) ) (λ y . y)) should evaluate to "(λ y . y)", the identity function. However, under a call-by-value evaluation strategy, which is eager, the value BlowsUp will need to be evaluated first. Only a lazy evaluation strategy will which first the "false" expression (thereby discarding the part of the program containing BlowsUp entirely, without evaluating it) will succeed. This is an extraordinarily important case, because recursive functions are typically written with two branches: a base case that terminates, and a recursive case that goes on for ever. For example, consider everyone's favorite recursive function, factorial: def factorial(n): if n <= 1: return 1 else: return n * factorial(n-1) Translated into the lambda calculus via the Y combinator, this (and pretty much every other non-trivial recursive function) will exhibit the same property of the above, and will never terminate if evaluated under a strictly eager, call-by-value strategy. Therefore, specifying the call-by-value evaluation strategy is not useful for the purposes of evaluating non-trivial algorithms, which almost always involve recursion. (In the lambda calculus even unbounded iteration must be implemented via recursion so this excludes basically all algorithms of interest to complexity theorists.) Note that languages which use call-by-value for function calls usually have a separate, built-in construct for if/else or && (short-circuiting boolean AND) which allows the programmer to decide when they want to use the "lazy" strategy; the lambda calculus unfortunately is too elegant to admit of such a pragmatic distinction. :) There is of course a so-called "normal" evaluation strategy for lambda calculus (which is guaranteed to work) but it is basically "call-by-name" (to contrast it with the call-by-value nomenclature) and it has the problems I describe above and is hard to analyze. https://sookocheff.com/post/fp/evaluating-lambda-expressions/ https://sookocheff.com/post/fp/evaluating-lambda-expressions...

vilhelm_s 7y ago
It's true that some constructions that work under normal/CBN order will go into an infinite loop under CBV order, but this is easy to work around, typically you just need to add an extra lambda to prevent it from evaluating too eagerly. For example, instead of translating if b then e1 else e2 as b e1 e2 you can translate it to (b (λx. e1) (λx. e2)) tt where tt is any value (it doesn't matter what). Similarly, you can make a CBV-version of the Y combinator by eta-expanding some subexpressions to prevent it from evaluating it too eagerly [0]. The exact details of the encoding don't matter too much, because when you actually write programs you want to use some syntactic sugar like "if then else" or "let rec", so you just care that it can be translated into lambda calculus in some way which preserves the operational semantics. [0] https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_fixed_point_combinator https://en.wikipedia.org/wiki/Fixed-point_combinator#Strict_...