Conversation

Oooh, will have to try it out! This looks like one of the nice metatheory lib thingos I've seen for Coq! Also seems like there's a Lean port in the works! ps.uni-saarland.de/~mameche/bache

Any idea why a pure debruijn approach was used, as opposed to something like locally nameless? (Just curious)

Paolo G. Giarrusso

@Blaisorblade

They don’t quite say, but I’m not sure LN is warranted at this point (other than complexity with multi-sorted syntaxes). I also don’t kmow if sigma-calculus still works for LN (you need to adapt it, but is the result a confluent, terminating and complete rewrite system?)

12:53 PM · Aug 21, 2018Twitter Web Client

Yeah, just curious mainly because I'm using it in my Moniker library: github.com/brendanzab/mon (it's based on Unbound). One of my current annoyances is that it seems like it is getting in the way of me moving toward a visitor-based approach in Pikelet: github.com/pikelet-lang/p

Replying to

and

By 'sigma-calculus' do you mean the specific explicit substitution calculus that they are using in austosubst? Kind of curious if explicit substitutions could get me out of my visitor woes... by allowing me to delay applying the substitutions as I traverse... 🤔

Replying to

That’s the name they use. But I’m not familiar with all the variants of sigma-calculus; if you add beta-reduction, some variants lose strong normalization, and I’ve never browsed the relevant literature as it’s not gentle. ps.uni-saarland.de/Publications/d has pointers.