I dunno any other name for it. It’s what I use in rust-nbe-for-mltt and I think it’s used in mini-tt. You use indices in the terms and levels in the values. Avoids you having to do all the shifting you’d need to do with pure indices.
Conversation
perso.ens-lyon.fr/pierre.lescann / semanticscholar.org/paper/Explicit
looks like co-debruijn as for as I know ?
1
1
Ooh that might be it. I’d need to investigate more deeply. Thanks!
2
I find the levels vs indices or syntax vs domain vs terms to be kinda fuzzy descriptively
1
syntax vs domain comes up a bit in NbE
1
Syntax is the thing you are evaluating from - the 'terms', domain are what you evaluate to - the 'values'. I think. But it's still kinda confusing why they ended up being called that.
1
I know the concepts. I just think it’s terrible jargon that fails to communicate unless everyone first syncs up on nbe.
1
1
Agreed. I'm definitely interested in figuring out something better, even just for NbE. Let me know if you have any ideas!
1
I'm trying to figure out a better way to organise my modules in my core crate: github.com/brendanzab/rus
1
atm core (the syntax) is inside the syntax module. and domain is in the syntax module too (kind of at odds with nbe). Not sure what to call these modules and where to put them.
1
At least I'm pretty happy with the names I've used for the variants in my core syntax and elsewhere: github.com/brendanzab/rus
I've found 'level' to be annoying, because it really feels like it should be called an 'index'. Because you're indexing from the start of the environment.
1
ok, so phrased differently: you’re using codebruijn aka “debruijn levels” aka distance from the top for static semantics, and debruijn indices / aka stack offset for dynamic semantics?
2
1
Show replies
Replying to
Apparently you use "literal" for sum or inductive types? I've always thought of that word as meaning "introduction form".
1
Oh, I don’t have inductive types yet. Maybe ‘builtin’ might be better?
1
Show replies