Program equivalence for Core.Main

[lukaszcz]

Defines step-indexed approximation and equivalence relations, sound for contextual approximation and equivalence, respectively. The steps count the nesting of executed function/constructor applications and recursion (letrec) unfoldings.

Work in progress. The current definitions are not yet correct, but I've worked out a plan to proceed with basic definitions and high-level proofs checked on paper.

Background

First of all, with functions as values represented syntactically (by a closure: expression + environment), the desired equivalence relation on values cannot simply compare them for exact equality. We would like two closures (function values) to be equivalent when they behave in the same way for all admissible arguments, not only when their concrete representations are literally equal.

A correct way to define program equivalence is by contextual equivalence. A context is an expression with exactly one hole. By $C[e]$ we denote the expression obtained by substituting the hole in the context $C$ with the expression $e$. An expression $e_1$ contextually approximates an expression $e_2$, denoted $e_1 \lesssim^c e_2$, if for every context $C$ and environment $E$ such that $E \vdash C[e_1] \downarrow$ (i.e. $C[e_1]$ evaluates to a value in environment $E$), we have $E \vdash C[e_2] \downarrow$. Intuitively, $e_1 \lesssim^c e_2$ means that $e_1$ may always be replaced by $e_2$ preserving the evaluation result (program meaning). Two expressions $e_1, e_2$ are contextually equivalent if $e_1 \lesssim^c e_2$ and $e_2 \lesssim^c e_1$.

Contextual equivalence essentially states that the programs (expressions) cannot be distinguished by any other program (context). This is the desired notion of program equivalence, but it is hard to work with because the definition requires reasoning about arbitrary contexts.

To prove equivalence of concrete expressions, we would like to have a more "structural" version of program equivalence, defined along the following lines. An expression $e_1$ is an approximation of $e_2$, denoted $e_1 \lesssim e_2$, if for every environment $E$ and value $v_1$ such that $E \vdash e_1 \mapsto v_1$ (i.e. $e_1$ evaluates to $v_1$ in environment $E$), there exists a value $v_2$ such that $E \vdash e_2 \mapsto v_2$ and $v_1 \lesssim_v v_2$ (value approximation). A value $v_1$ approximates value $v_2$, denoted $v_1 \lesssim_v v_2$, if:

• $v_1 = v_2$ and $v_1, v_2$ are atomic constants (integers, etc.), or
• $v_1 = c a_1 \ldots a_n$, $v_2 = c b_1 \ldots b_n$ (constructor applications with the same constructor $c$), and $a_i \lesssim_v b_i$ for $i = 1,\ldots,n$, or
• $v_1 = [E_1]\lambda x e_1$, $v_2 = [E_2]\lambda x e_2$ (closures: environment + lambda-expression) and: for all values $a_1,a_2,r_1$ such that $a_1 \lesssim_v a_2$ and $E_1[x := a_1] \vdash e_1 \mapsto r_1$, there exists $r_2$ such that $E_2[x := a_2] \vdash e_2 \mapsto r_2$ and $r_1 \lesssim_v r_2$.

With such a definition, proving program equivalence for concrete expressions is more manageable.

However, the "definition" as stated above is not well-founded: $\lesssim_v$ occurs negatively in $a_1 \lesssim_v a_2$. We cannot replace $a_1 \lesssim_v a_2$ by $a_1 = a_2$, because then we would not be able to prove that our approximation implies contextual approximation. A solution is to index $\lesssim_v$ by an appropriately defined number of execution steps: $v_1 \lesssim_v^k v_2$ means that $v_1$ approximates $v_2$ in no more than $k$ program execution steps. We ensure the step index $k$ decreases when referring to $\lesssim_v^k$ recursively in its definition.

The general technique of step-indexing is well-established [1, 2], but it needs to be adapted to the particular case of JuvixCore and its evaluation semantics. This adaptation is not straightforward.

Checklist

• Make recursion explicit in expressions by adding letrec. Replace global identifiers with letrec.
• Define step-indexed version of the big-step operational evaluation relation.
• Define step-indexed program approximation relation, similar to [1], [2]. Step-indexed equivalence is approximation both ways.
• Prove anti-monotonicity of approximation w.r.t. the indices.
• Prove that step-indexed approximation is preserved by step-indexed evaluation, with appropriate indices. Needs anti-monotonicity.
• Prove reflexivity of step-indexed approximation. Needs preservation under step-indexed evaluation.
• Prove transitivity of step-indexed approximation. Needs reflexivity.
• Prove that the closure condition without indices is equivalent to the indexed closure condition, i.e., to the premise of the step-indexed approximation rule for the closure case. Needs reflexivity, transitivity and preservation under step-indexed evaluation.
• Prove that step-indexed approximation is preserved by evaluation (non-indexed version).
• Define contextual approximation and equivalence.
• Prove soundness: step-indexed approximation implies contextual approximation. Needs preservation of step-indexed approximation under evaluation.

References

• [1] Amal Ahmed, Step-indexed syntactic logical relations for recursive and quantified types
• [2] Andrew Appel, David McAllester, An indexed model of recursive types for foundational proof-carrying code