As we know many programming languages and systems don't implement the strong reduction of $\lambda$-terms, instead they do weak reduction (no reduction under abstraction).

I recently experimented several tests on $\lambda$-terms. I applied strong reduction and call by value reduction on them.

  1. strong reduction took longer time even the size of the term is moderate.
  2. call by value reduction is very fast.

I believe if we ignore inefficiency, strong reduction is more useful than weak one. These are what I felt from my experiments. That makes me think about some questions. here I would like to share them with you.

  1. programming languages or other systems do not implement the strong reduction because it is inefficient (takes more time)?

  2. programming languages or other systems don not implement the strong reduction because it is difficult to do?

  3. which one is the reason, or something also?

  • 1
    $\begingroup$ I think this was purely commercial decision at some time in the past to improve performance. With purely functional languages it really true that to have a copy of object/value with large dependency graph would take more time rather that pass a reference etc. Hope next link would help: mitpress.mit.edu/sicp/full-text/book/book-Z-H-20.html $\endgroup$ – PavelOliynyk Nov 24 '16 at 11:59
  • $\begingroup$ I'm confused why you're contrasting strong reduction and call-by-value: they're very different things, and the "opposite" of call-by-value is not strong reduction. $\endgroup$ – cody Dec 8 '17 at 20:02

There are several possible answers to your question:

1) Strong reduction is not implemented because it is not that useful: why take the trouble to reduce a term with un-instantiated variables when you'll have to go back in later to do the reduction when the variables get values anyway? And if the variables never get instantiated, then you've wasted your time entirely! More generally, it's easier to compute with concrete values than symbolic ones.

2) Strong reduction is implemented, because it is useful. It's just that this is usually done at compile time: inlining and constant propagation is just that, a way to do strong reduction.

  • $\begingroup$ It would be great if you recommend some books related to your second reason. I am curious about these implementations. $\endgroup$ – alim Dec 11 '17 at 5:44
  • 1
    $\begingroup$ @alim Any decent book on compilation should address these issues, my personal pick would be Appel's Modern Compiler Implementation in ML $\endgroup$ – cody Dec 12 '17 at 19:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.