Conversation

Normalisation, how to do it fast for the untyped lambda-calculus by means of evaluation, and why we care (together with some of the required type theory/PLT background): first of a series, hopefully. Feel free to yell at me in replies about mistakes etc! colimit.net/posts/normalis

David Thrane Christiansen

@d_christiansen

Feb 3, 2020

You've got a "TODO how?" in there :-)

swann

@evertedsphere

Feb 3, 2020

I think I'll leave that in until I understand that part to my satisfaction haha

David Thrane Christiansen

@d_christiansen

Feb 3, 2020

Here's my take: with de Bruijn indices, variables need to be incremented when you put them under a new binder. They refer to binding sites relative to their occurrence. Levels refer to them absolutely and thus don't need incrementing under a new binder.

Replying to

and

My (probably bad) understanding is that the nifty thing about indices is that you can avoid having to rename things. The nifty thing about levels is that you can move around terms without having to shift indices. Combining them together with NbE gets you the best of both somehow?

9:11 PM · Feb 3, 2020Twitter Web App

David Thrane Christiansen

Replying to

and

Indices are nicer for writing evaluators (they basically say how far up the stack to look for the value). The way I see it, levels are nice for free variables, and indices for bound variables. Boundness vs freeness depends on your perspective :-)

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

The thing that kind of makes me unhappy about the approach is the fact that you have to copy around the entire environment all the time, regardless of if any of it is used. Seems a tad wasteful, but I dunno.

Show replies