• Observational Equavalence
• Logical Equivalence
  • Foundamental Theorm of Logical Relations
  • Closure under Converse Evalutaion
  • Relationship to Hereditary Termination

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$.

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

• For 2 closed programs of type $int$, $eequiv e’ iff exists k$ such that $emapsto^*k,e'mapsto^*k$.
  This is called Kleeve equivalence.
• For $e,e':tau,e=^{obs}_tau e' iff forall o:tauvdash P:int,P[e]equiv P[e']$,
  were $P$ is a program context, defined as an expression: $o:tauvdash P:int$, where
  $o$ can said as a “hole”, and $P[e]$ means $[e/o]P$. For example, in $2+(o+1)$, $o$ is type $int$;
  in $2+(o7+1)$, $o$ is type $intrightarrow 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: $esim_tau e'$ is consistent $iff esim_{int}e’$ implies $eequiv e'$.
In other words, it means it implies $equiv$ at $int$.

Congruence: if $esim_{tau_1} e'$, then $C[e]sim_{tau_2}C[e']$ for any
context, where context is $o:tau_1vdash C:tau_2$.

Coarsest: if $esim_tau e'$ by any consistent congruence, then $e=^{obs}_tau e'$

Proof:

• Consistent

We want to show $if e=^{obs}_{int}e',then eequiv e'$, which is obvious by the definition
of $=^{obs}$, just take $P$ to be $o$ itself. (identity)

• Congruence

We want to show $if e=^{obs}_{tau_1} e'then C[e]=^{obs}_{tau_2}C[e']$.
$e=^{obs}_{tau_1} e'$ means $forall P_{o:tau_1},P[e]equiv P[e']$.
$C[e]=^{obs}_{tau_2}C[e']$ means $forall P'_{o:tau_2},P'[C[e]]equiv P'[C[e']]$.
We take $P$ to be $P’[C/o]$, so $P[e]$ is just $P’[C[e]]$ (composition)

• Coarsest

By congruence, we have $P[e]sim P[e']$.

By consistency, we have $P[e]equiv P[e']$. 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:

$$e=^{obs}_tau e' iff e^{log}_tau e'$$

Logical Equivalence

It is equivalence defined by logical relations.

• $$e=^{log}_{int}e' iff eequiv e'$$
• $$e=^{log}_{tau_1rightarrow tau_2}e' iff forall e_1,e_1':tau_1, if e_1=^{log}_{tau_1}e_1',then ee_1=^{log}_{tau_2}e'e_1'$$

Thm:

$$e:tau implies e=^{obs}_{int}e$$

Proof $e=^{obs}_tau e' iff e^{log}_tau e'$:

From left to right should be easier because we are coming from $forall$ to $int$
and $tau_1rightarrow 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_1vdash C:tau_2,if e=^{log}_{tau_1}e',then C[e]=^{log}_{tau_2}C[e']$. We need a generalized version of $Thm(v3)$ from
here:

Foundamental Theorm of Logical Relations

$$If Gammavdash e:tau,and gamma=^{log}_Gammagamma', then hat{gamma}(e)=^{log}_tauhat{gamma'}(e)$$

Closure under Converse Evalutaion

Lemma:

$$If emapsto e_0,e_0=^{log}_tau e', then e=^{log}_tau e'$$

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 Termination

$$e=^{obs}_tau e iff HT_tau(e)$$