RG interprets typing contexts as substitutions. Substitutions should not only be values, since a Let nonstrict bs t can bind non-strict values.
Strictness context
Whether a substitution contains a value or term depends on the strictness of the binder, which is static information. Therefore, RG should not only be an interpretation of the typing context $\Gamma$, but also a strictness context $S$.
Closed values/terms
Our substitutions are always closed, this is an invariant from our big-step semantics, and it is witnessed in RG by the typing derivation that has to hold in RV, which requires empty contexts. There is a helper function RG_env_closed, which
subst [(y, x), (x, 5)] (let x = 3 in x + y) = (let x = 3 in x + x)
In our dynamic semantics, this would never happen, as evaluating the x = 5 binding would directly substitute in the rest of the expression. Resulting in let ~y = 5 + 1 in ....
I don't know if this is causing any problems in the fundamental property proof or LetNonRec DSP proof.
Other
We also need to change pure_open (in DeadCode/DSP/Lemmas), which should allow for substitutions containing terms (not values).
jaccokrijnen
commented
11 months ago
RGinterprets typing contexts as substitutions. Substitutions should not only be values, since aLet nonstrict bs tcan bind non-strict values.Strictness context
Whether a substitution contains a value or term depends on the strictness of the binder, which is static information. Therefore,
RGshould not only be an interpretation of the typing context $\Gamma$, but also a strictness context $S$.Closed values/terms
Our substitutions are always closed, this is an invariant from our big-step semantics, and it is witnessed in RG by the typing derivation that has to hold in
RV, which requires empty contexts. There is a helper functionRG_env_closed, whichIn our dynamic semantics, this would never happen, as evaluating the
x = 5binding would directly substitute in the rest of the expression. Resulting inlet ~y = 5 + 1 in ....I don't know if this is causing any problems in the fundamental property proof or LetNonRec DSP proof.
Other
We also need to change
pure_open(in DeadCode/DSP/Lemmas), which should allow for substitutions containing terms (not values).This will break quite some proofs.