Conversation

Behold the power of the Ultimate Decision Procedure for substitution lemmas #Autosubst (ps.uni-saarland.de/autosubst/)! And it's just a dozen rewrite rules! Yes, the syntax is a bit scary. Proving these lemmas by hand is just more so!

Beta-reduction and substitution commute, with the help of Autosubst. Stated with either alphabetic or symbolic operators (syntax blizzard mode, I admit).

read image description

ALT

The convergent rewriting system of the σ -calculus

read image description

ALT

Brendan Zabarauskas

@brendanzab

Aug 21, 2018

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

Brendan Zabarauskas

@brendanzab

Aug 21, 2018

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

Paolo G. Giarrusso

@Blaisorblade

Aug 21, 2018

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

Brendan Zabarauskas

@brendanzab

Replying to

@Blaisorblade

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

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

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

Paolo G. Giarrusso

@Blaisorblade

Aug 21, 2018

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.

Show replies