strong reduction of $\lambda$-terms, useful?

Question

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?

Answer 1

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.