Dead code correctness: how to prove strictly bound variables will always be a value

[jaccokrijnen]

Consider:

let x = 1 + 1 in
let y = x in
x + x

Here it is safe to remove binding y, since y is not used, and its RHS x can not diverge/error out (it is 'pure'). We have a syntactic relation is_pure : list (string * binder_info) -> Term -> Prop that captures this. The first parameter carries info about if a variable was bound strict or non-strict.

is_pure should somehow imply that given $\Gamma \vdash t : \tau$, any substitution $\gamma$ for $\Gamma$ only has values for variables that are bound strictly. $\Gamma$ doesn't have this information though. Should we add it to the typing relation?

Or should we keep another environments that relates to $\Gamma$ by having the variable names, but with strictness information. How do we actually prove though that a strict binding site means that the substitution will only contain a (non-error) value?

We really want to separate the syntactic notion is_pure env t (which is an approximation) from the more general semantic notion: $\gamma(t) \Downarrow_k v \wedge \neg \text{error}(v) $.

• Call a term $t$ pure iff it is closed and $\exists k\ v . t \Downarrow_k v \wedge \neg \text{error}(v) $.
• Call a substitution $\gamma$ a pure substitution iff $\forall x\ t. (x, t) \in \gamma \Rightarrow \text{pure}(t)$

[jaccokrijnen]

For now we could probably change RG to require ~(is_error v) and ~(is_error v'), then RG Γ γ γ' -> pure_substitution Γ γ.

This would change when we add semantics for non-strict bindings, because RG should capture terms too. We will change $\Gamma$ from type list (string * Ty) to list (string * Strictness * Ty).

We then need a proof in dead-code correctness that Γ can be shrinked to Γ', i.e. Γ' ⊆ Γ, such that Γ' only has strictly bound vars, and therefore all γ for Γ' are pure substitutions. The right place to add this is in RG/Helpers.v