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?)

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

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... 🤔

Paolo G. Giarrusso

@Blaisorblade

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.

Yeah, I found delving into all the variants of naming and substitution and autobinding and explicit substitutions and scope graphs and director strings and indices and levels and.... arrrgh.... super overwhelming.

Hence me just porting Unbound which was confusing in itself (hopefully I managed to simplify and clarify some things in the process).

1:09 PM · Aug 21, 2018Twitter Web Client

And this is all *with* skipping the proofs and stuff because I haven't really got to grips with all that stuff yet.

Replying to

and

I was pretty thankful for Charguéraud's "The Locally Nameless Representation", which was a great help early on: chargueraud.org/research/2009/

Replying to

Yep, it's a very good tutorial, one of the best thing going for LN (I was also happy they have an actual proof scripts since they omit some proof details — such as generalizing the statement to make the induction go through).