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... 🤔
Conversation
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.
1
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.
1
1
Hence me just porting Unbound which was confusing in itself (hopefully I managed to simplify and clarify some things in the process).
1
And this is all *with* skipping the proofs and stuff because I haven't really got to grips with all that stuff yet.
1
1
I was pretty thankful for Charguéraud's "The Locally Nameless Representation", which was a great help early on: chargueraud.org/research/2009/
1
1
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).
1
1
Heh, yeah I do actually forget it’s actually kind of a tutorial for LN as well. I was just using it as a tute for learning the technique itself!
1
One of the cool things it also covers is pattern matching. Alas I didn’t find any examples of implementing pattern matching with autosubst... 🤔
1
Never gotten to that part, but pattern matching seems just another set of binders, no? Oh, not sure how to annotate that for autosubst tho...
2
Replying to
Yeah, you have another index to describe where you are in the pattern: scm.gforge.inria.fr/anonscm/gitweb