Dead code specification using uniqueness and well-scoped

[jaccokrijnen]

TODO

• [ ] Rewrite Let case with simple induction over both lists.
• [ ] Figure out how this spec seemingly solved the complexity with letrec compared to the other style of specification (there we would have to carry around the whole list of bindings to determine whether the bound var does not occur free in the post-term)
• [ ] Include strictness map
• [ ] Include datatype case where only type is used, but not constructors

Former problem: how to prove this implies $x \notin FV(\texttt{let bs' in t'})$

note: this is solved, see first comment I don't see a simple way of proving that $x \notin FV(\texttt{let bs' in t'})$, given $unique(\texttt{let bs' in t'})$ and $wellscoped(\texttt{let bs' in t'})$.

One way would be by considering the "context" (i.e. one-hole context of the term). The reasoning would go something like this:

• Suppose $x \in FV(...)$, where $x$ is a variable bound in an eliminated let
• Then there must be a binder in the context C' (of the post-term)
• Then there must be the same binder in the context C (of the pre-term)
• Then by uniqueness there is a contradiction in the pre-term, since it is bound twice.

[jaccokrijnen]

Suppose $t \triangleright t'$ and

• on the pre-term: $\Gamma \vdash t$ (well-scoped) and $\Gamma \vdash \text{Unique}(t)$
• on the post-term: $\Gamma' \vdash t'$

The following invariant holds throughout the translation relation:

• $\Gamma' \subseteq \Gamma$

Lemma

• $\Gamma \vdash \text{Unique}(t) \to \text{Disjoint}(\Gamma, BoundVars(t))$

Case Remove-Let: $\texttt{let } x = t_x \texttt{ in } t \triangleright t' $. Proof that $x \notin t'$. In

1. Suppose $x \in FV(t')$, then $x \in \Gamma'$, by well-scopedness
2. By invariant: $x \in \Gamma$
3. But $x$ is also bound in the pre-term: $\texttt{let } x = t_x \texttt{ in } t$. Contradiction by Lemma with uniqueness assumption.

[jaccokrijnen]

Improving the accuracy of the purity approximation

The plutus compiler implementation has a more precise approximation of pure terms: it uses the "strictness map" (maintained in a MonadState DepState m, where type DepState = Map Unique Strictness, see Dependencies.hs).

The translation relation spec

We should therefore include more static information in the elim relation: a strictness map $S$ that maintains strictness for each binder. The elim translation relation will have the form

S \vdash t \triangleright t'

In the semantic preservation proof we will have to consider only substitutions that respect the strictness map, i.e. for a terms $\Gamma \otimes S \vdash t : \tau$, we define logical approximation as:

\Gamma \otimes S \vDash t \leq t' : \tau ~ := ~ \forall (\gamma, \gamma') \in [\Gamma \oplus S]. RC(\gamma(t), \gamma(t'))

Modularity

We could instead extend the relation in a more abstract way: instead of the strictness map, we only have a function or predicate that decides if a Term is pure. This function can change (just like the strictness map) as we descend down the ASTs.

For the current implementation, it would be sufficient to supply the is_pure predicate, which is context-independent as it doesn't consider the strictness of variables. Ideally, we would abstract this predicate out of elim. Adding a parameter of Term -> Prop would not suffice, since it needs to be able to consider the context. StrictnessMap -> Term -> Prop would suffice, but not be very abstract: now elim still needs to maintain a strictnessmap and pass it to the predicate.

If instead we would describe the translation relation with induction on the pre-term in a modular way, like attribute grammars, we could define an attribute to compute the strictness map $inh{\text{Strictness}}$, an attribute to describe a decidable purity approximation $inh{\text{pure}}$, which has a dependency on $inh{\text{Strictness}}$ . Then elim can be described as an attribute with dependency on $inh{\text{pure}}$.

Attributes in the traditional sense are functions (mapping inherited parent attributes and synthesized child attributes to synthesized attributes and inherited child attribtues). I think that in this case, we need to consider predicates/relations (or perhaps partial functions) instead. For example, elim will only need to relate a pre-term Apply s t with a post-term of the form Apply s' t'. A rule for the case Apply should therefore be a predicate instead of a function.

[jaccokrijnen]

Q: elim is type-changing, why does our limited definition of $\leq$ suffice for proving semantics preservation?

The dead-code relation is slightly type-changing: the environments of the post-term may contain fewer variables. While investigating the inliner pass, I needed to constrain substitutions to be consistent with let bindings I needed a more general definition of $\leq$.

In dead-code, logical approximation requires that $\Gamma \vdash t : \tau$ and $\Gamma \vdash t' : \tau$. Even though $t'$ may be typable with smaller $\Gamma'$.

A: It is not a problem here, since typings can be weakened: if $\Gamma' \vdash t' : \tau$ and $\Gamma' \subseteq \Gamma$, then also $\Gamma \vdash t' : \tau$.

This highlights again the need for maintaining the invariant $\Gamma' \subseteq \Gamma$ in the induction proof (i.e. it is an inherited attribute).