Frontend generated semantics to implement the `SUBSTITION` module

[gtrepta]

Here's a rough specification of how a frontend pass in the compiler pipeline would implement variable binding semantics for the SUBSTITUTION module without using any hooked sorts or function symbols.

First, the user would import the SUBSTITUTION module.

Then, the user defines a symbol with the binder attribute:

  syntax S1 ::= binder( KVar, S2 ) [binder]

• It must have exactly 2 nonterminals
• The first nonterminal must be KVar, which is imported from SUBSTITUTION

If the user hasn't declared KVar as a subsort of S2, then the compiler will create that declaration so variables can appear in productions of sort S2.

Syntax/Rule generation

Given the above binder production, the compiler will generate the following productions/rules:

The free variable set

A function to obtain the set of free variables for any production of sort S2 get produced.

  syntax Set ::= freeVars(S2) [function]
  rule freeVars(V:KVar) => SetItem(V)
  // rules for every production of sort P
  rule freeVars(symbol(X0,...,Xn):S2) => {freeVars(X) for X:S2 in X0,...,Xn}

If the binder production itself is of sort S2, then it has a special case:

  rule freeVars(binder(V, X)) => freeVars(X) -Set SetItem(V)

The fresh variable generation

Given a set of free variables, produce a fresh variable that doesn't collide with any of the free variables

  syntax KVar ::= freshVar(KVar, Int, Set) [function]
  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi

(KVar is going to be a subsort of Id, so we use Id manipulation functions to create the fresh variables)

The substitution function

Substitute the occurrence of a variable in a production of sort S2 with a production also of sort S2

  syntax S2 ::= S2 "[" S2 "/" KVar "]" [function]

  rule X [_ / _] => X [owise]
  rule X:KVar [ V / X ] => V

  // rules for all other productions of sort P
  rule symbol(X0,...,Xn):S2 [V / X] => symbol([Y [V / X] if Y:S2 else Y for Y in X0,...Xn])

If the binder production itself is of sort S2, then it has a special case for substitution semantics:

  rule binder(X,E) [_ / X] => binder(X,E)
  rule binder(X,E) [V / Y] => binder(X,E[V / Y]) requires X =/=K Y andBool notBool X in freeVars(E)
  rule binder(X,E) [V / Y] => #let Z = freshVar(X, 0, freeVars(E) freeVars(V)) #in binder(Z,E[Z/X][V/Y])
    requires X =/=K Y andBool X in freeVars(E)

These transformations should be an adequate replacement of the hooked symbols in the SUBSTITUTION module. There's possibly an improvement to be made by making some slightly different rules depending on whether kompilation is being done on a concrete or symbolic backend (ie. on a symbolic backend, fresh variable generation can be freshVar(_,_,S) => ?X:KVar ensures notBool ?X in S)

[dwightguth]

Note that right now binders can have more than two non terminals as long as the first is KVar and the last is the bound term. I think we should preserve this behavior if we can because I believe some parts of the pl tutorial use this ability to implement let X = Y in Z

[gtrepta]

Noted. It shouldn't be any more difficult to implement.

[Baltoli]

It shouldn't be any more difficult to implement

Yep, I guess you just want to relax the restriction to exactly one non-terminal of sort KVar, and to treat binder a bit like strict is treated currently. If I were to write:

binder(KVar, Sa, Sb, Sc) [binder]

then the substitution logic should apply over the three non-KVar arguments. We could also say:

binder(KVar, Sa, Sb, Sc) [binder(2, 3)]

to skip the Sc argument when substituting. It should be an error to specify binder(1) here.

Given a set of free variables, produce a fresh variable that doesn't collide with any of the free variables

The implementation here can just be written by hand into the SUBSTITUTION module, right? It doesn't need to be generated for the specific sorts in question.

[Baltoli]

This looks good though @gtrepta; nice work!

[Scott-Guest]

LGTM, and I agree with @Baltoli's suggestions.

If the user hasn't declared KVar as a subsort of S2, then the compiler will create that declaration so variables can appear in productions of sort S2.

I'd personally prefer if this gets reported as an error instead of automatically declaring the subsorting - it feels unintuitive to change the user's types behind their back.

[gtrepta]

@Scott-Guest good suggestion, I'll make it an error.

@Baltoli I believe to preserve the semantics, the substitution should only apply over the last non-KVar nonterminal. Adding the optional parameter sounds like a good idea, though!

[Baltoli]

Putting this in the backlog until we need to revisit it on a review of the PL tutorial and any associated teaching activities.