Bottom-up rewriting with smart constructors, hereditary substitution & normalization by evaluation: julesjacobs.com/notes/smartcon
Conversation
Is your definition of NbE a bit more narrow than mine? I use a closure-converted form, for example, with De Bruijn levels in neutral values. I've also seen strings used in place of levels in other implementations of NbE.
3
2
“Closure-converted NbE” is definitely a thing (used by e.g. Abel) and the term seems to generates vigorous* reactions in people** who are only used to “normal” NbE.
*almost wrote “violent”
**including me a while ago
1
2
What is “normal” NbE? Are you saying people felt weoird about the term “Closure-converted NbE”, or the people using “Closure-converted NbE” calling what they are doing “NbE”? More just curious to know the history that I am stumbling into!
My memory betrays me, but I thought that jonmsterling.com/pdfs/modal-mlt avoided saying whether *defunctionalized* NbE is NbE (they don't say closure-converted). The distinction might be original in that paper.
It looks like a reviewer might have objected, but I'm not sure.
1