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.
- strong reduction took longer time even the size of the term is moderate.
- 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.
programming languages or other systems do not implement the strong reduction because it is inefficient (takes more time)?
programming languages or other systems don not implement the strong reduction because it is difficult to do?
which one is the reason, or something also?