modal stepping, determinism of stepping

[ivoysey]

this is silly on its face since with the red bracketed premises commented out the steps are intentionally not deterministic. this would mean changing the judgement form to have a flag about if you were in brackets mode or not and then showing that we really do have determinism for the (pretty standard) eager version.

[ivoysey]

i've changed the name of this issue to be a little bit less disingenuous and include something else we've talked about on and off. specifically, the current formulation of the rules does not include any of the red bracketed premises from the paper text and therefore allows whatever order of evaluation we want.

this is good enough for exposition because if any evaluation order has a property that we're interested in, then the specific one that happens to be strict eager left to right does as well. it may be worth parameterizing the stepping judgement by a flag bit that includes exactly those bracketed premises, though, so that we can also still prove things about the eager version of the system that are not true of any arbitrary version -- like this property of determinism of stepping.

[cyrus-]

If a stepping judgement is an input to a theorem than its fine to prove it for the version of the system without the bracketed premises, because that includes the eager interpretation.

But for theorems where the stepping judgement is an output, e.g. progress, you do technically need to prove it for the bracketed premises version separately because the bracketed premises rule out some possible proof paths.

[cyrus-]

We need to make at least one small change to have determinism in the +red brackets version: the ITApCast rule needs a premise that says \tau_1 -> \tau_2 != \tau_1' -> \tau_2', because otherwise we could either drop the identity cast first or do the cast expansion first.

We're not actually stating this property in the paper but it doesn't hurt anything. Should be a pretty easy mod to the proofs too. So I say we make the change?