The main question is, how do we define two programs are equal, and how do we prove it.

So for setup we have type $int$, and $k$ which is a $int$, and $e_1+e_2$.

Observational EquavalencePermalink

We say that 2 programs are equal $iff$ you can’t tell them apart, which means:

• For 2 closed programs of type $int$, $e\equiv e^{\prime }iff\exists k$ such that $e{\mapsto }^{\ast }k,e^{\prime }{\mapsto }^{\ast }k$. This is called Kleeve equivalence.
• For $e,e^{\prime }:\tau ,e{=}_{\tau }^{obs}{e}^{\prime }iff\forall o:\tau ⊢P:int,P\left[e\right]\equiv P\left[e^{\prime }\right]$, were $P$ is a program context, defined as an expression: $o:\tau ⊢P:int$, where $o$ can said as a “hole”, and $P\left[e\right]$ means $\left[e/o\right]P$. For example, in $2+(o+1)$, $o$ is type $int$; in $2+(o7+1)$, $o$ is type $int\to int$. To rephrase the rule, it means that two programs are equal if we plug them in a larger program $P$, we get the same result. This is called observational equivalence.

Observational equivalence is characterized by a universal property:

• Observatinoal equivalence is the coarsest consistent congruence.

Consistent: $e{\sim }_{\tau }{e}^{\prime }$ is consistent $iffe{\sim }_{int}{e}^{\prime }$ implies $e\equiv e^{\prime }$. In other words, it means it implies $\equiv$ at $int$.

Congruence: if $e{\sim }_{{\tau }_1}{e}^{\prime }$, then $C\left[e\right]{\sim }_{{\tau }_2}C\left[e^{\prime }\right]$ for any context, where context is $o:{\tau }_1⊢C:{\tau }_2$.

Coarsest: if $e{\sim }_{\tau }{e}^{\prime }$ by any consistent congruence, then $e{=}_{\tau }^{obs}{e}^{\prime }$

Proof:

• Consistent

We want to show $ife{=}_{int}^{obs}{e}^{\prime },thene\equiv e^{\prime }$, which is obvious by the definition of ${=}^{obs}$, just take $P$ to be $o$ itself. (identity)

• Congruence

We want to show $ife{=}_{{\tau }_1}^{obs}{e}^{\prime }thenC\left[e\right]{=}_{{\tau }_2}^{obs}C\left[e^{\prime }\right]$. $e{=}_{{\tau }_1}^{obs}{e}^{\prime }$ means $\forall P_{o:{\tau }_1},P\left[e\right]\equiv P\left[e^{\prime }\right]$. $C\left[e\right]{=}_{{\tau }_2}^{obs}C\left[e^{\prime }\right]$ means $\forall P_{o:{\tau }_2}^{\prime },P^{\prime }\left[C\right[e\left]\right]\equiv P^{\prime }\left[C\right[e^{\prime }\left]\right]$. We take $P$ to be $P^{\prime }\left[C/o\right]$, so $P\left[e\right]$ is just $P^{\prime }\left[C\right[e\left]\right]$ (composition)

• Coarsest

By congruence, we have $P\left[e\right]\sim P\left[e^{\prime }\right]$.

By consistency, we have $P\left[e\right]\equiv P\left[e^{\prime }\right]$. So we are done.

So we proved the properties of observational equivalence, by how do we prove observational equivalence itself in the first place? Afterall, we need to show the rule holds for all contexts. The idea is to cutdown contexts that you need to consider using types. We need to introduce a new notion below ${=}^{log}$ to do that, so that we have a rule:

Logical EquivalencePermalink

It is equivalence defined by logical relations.

• $$e{=}_{int}^{log}{e}^{\prime }iffe\equiv e^{\prime }$$
• $$e{=}_{{\tau }_1\to {\tau }_2}^{log}{e}^{\prime }iff\forall e_1,e_1^{\prime }:{\tau }_1,if{e}_1{=}_{{\tau }_1}^{log}{e}_1^{\prime },thene{e}_1{=}_{{\tau }_2}^{log}{e}^{\prime }{e}_1^{\prime }$$

Thm:

Proof $e{=}_{\tau }^{obs}{e}^{\prime }iff{e}_{\tau }^{log}{e}^{\prime }$:

From left to right should be easier because we are coming from $\forall$ to $int$ and ${\tau }_1\to {\tau }_2$, so we are not gonna do it here.

From right to left:

Because observational equivalence is the coarsest consistent congruence, so we only need to show logical equivalence is a consistent congruence. Consistency comes for free, so we only need congruence.

We want to proof: $\forall o:{\tau }_1⊢C:{\tau }_2,ife{=}_{{\tau }_1}^{log}{e}^{\prime },thenC\left[e\right]{=}_{{\tau }_2}^{log}C\left[e^{\prime }\right]$. We need a generalized version of $Thm\left(v3\right)$ from here:

Foundamental Theorm of Logical RelationsPermalink

Closure under Converse EvalutaionPermalink

Lemma:

where $\mapsto$ is the transition in dynamics from here.

Then we can proof it by the above therom and lemma, we will just skip it here ;)

Relationship to Hereditary TerminationPermalink