Timeline for Alternatives to Normalization by Evaluation
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 26, 2021 at 15:28 | answer | added | cody | timeline score: 1 | |
| May 17, 2021 at 9:00 | comment | added | Andrej Bauer | You should be careful with terminology here because it is not universally agreed upon. Some people call "evaluation" what you're describing, but others equation evaluation and normalization. | |
| May 17, 2021 at 7:32 | comment | added | Siddharth Bhat |
I too would like to know alternatives to nbe other than heriditary substitution. The difference between NBE and evaluation is that evaluation, for example, does not reduce "inside" a lambda term. Given the term t = (λ x ((λ y y) x)), evaluation will get stuck, since there is no outer redex. NBE will evaluate the inner redex of (λ y y) x) to the normal form x. This normalizes the term t into t -> (λ x x). Intuitively, NBE extends the evaluation rules of lambda calculus to work "inside stuck terms" as well.
|
|
| May 17, 2021 at 7:07 | review | First posts | |||
| May 17, 2021 at 8:34 | |||||
| May 17, 2021 at 7:01 | history | asked | nbe | CC BY-SA 4.0 |