Different kinds of assumptions

[John Tang Boyland]

Currently in SASyLF, the form of contexts is

 Gamma ::= only-terminals | Gamma one-variable-and-other-normal-nonterminals
                          | Gamma another-variable-and-other-normal-nonterminals

Then one has to define an "assumption" rule for each variable case for Gamma in a judgment. Then in LF, we treat judgments using contexts with variables as being functions with two curried parameters: the variable type and the judgment.

Sometimes one wants to have just a variable and no judgment to make substitution easier (of course one can, and I have done so, in cut-elimination, define a judgment that is always true, but this is dead-weight and confuses the SASyLF read).

Sometimes one wants to have just a judgment and no fresh variable, again cut-elimination is an example where I had to add a spurious variable.

[John Tang Boyland]

So it would be nice to define different kinds of contexts:

    Gamma one-variable-and-no-nonterminals

this would have no judgment associated with it. Not having a judgment would mean it would be impossible to refer to it in any judgment. Maybe this is not a good idea.

Another possibility would be

    Gamma no-variables

This would require a judgment, but wouldn't have a variable.

In both cases, by substitution would work differently: we would use the syntax in the first case and the judgment in the second case. We could permit a three argument version of substitution for the normal case, and deprecate the old two argument version while continuing to accept it.

How would we know something is a context without having variables? We would see the "assumes Gamma" declaration. If there were no such judgments and no variables then nothing needs to be a context anyway.

[John Tang Boyland]

An easy way forward is to not complain about the lack of an assumption rule for a variable case with no non-terminals except the recursive Gamma case. Then if someone wants an assumption judgment, they can give it, and if someone doesn't they don't give it.