Conversation

In my implementation of normalisation by evaluation, I have two partial functions: f₁ : Env × Term → Value f₂ : Level × Value → Term What should I call them? I'd love to know why, if possible!

reflect, reify
20%
eval, readback
17.1%
eval, quote
62.9%
other (please write)
0%

35 votesFinal results

Kristopher Micinski

@krismicinski

Aug 31, 2021

sorry for being naive here, but what is level here? how is f1 not just interpretation as a (say) C,E (control, environment) machine? I guess the idea is these are mutually recursive, but not sure what level is here.

Brendan Zabarauskas

@brendanzab

Replying to

@krismicinski

No worries! Sorry for being unclear. It is the de Bruijn level of the environment. I'm using de Bruijn indices in my terms and levels in my values. The level of the environment lets you convert the levels in the values back to indices using `envLevel - varLevel + 1`

5:29 AM · Aug 31, 2021Twitter Web App

Replying to

and

There is a description of this in 3.1 of Andreas Abel's thesis: cse.chalmers.se/~abela/habil.p - but I probably need to re-read it again. At the moment the level of my understanding is ‘do this magic trick to avoid expensive, error-prone shifting or maintenance of substitutions’.