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 Equavalence

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’\ iff\ \exists k$ such that . This is called**Kleeve equivalence**. - For ,
were $P$ is a program context, defined as an expression: , 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 $int\rightarrow 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*: is *consistent* $iff\ e\sim_{int}e’$ implies .
In other words, it means it implies $\equiv$ at $int$.

*Congruence*: if , then for any
context, where context is .

*Coarsest*: if by any consistent congruence, then

Proof:

- Consistent

We want to show , which is obvious by the definition
of $=^{obs}$, just take $P$ to be $o$ itself. (**identity**)

- Congruence

We want to show .
means .
means .
We take $P$ to be $P’[C/o]$, so $P[e]$ is just $P’[C[e]]$ (**composition**)

- Coarsest

By *congruence*, we have .

By *consistency*, we have . 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
to do that, so that we have a rule:

# Logical Equivalence

It is equivalence defined by *logical relations*.

Thm:

Proof :

From left to right should be easier because we are coming from $\forall$ to $int$ and $\tau_1\rightarrow \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: . We need a generalized version of $Thm(v3)$ from here:

## Foundamental Theorm of Logical Relations

## Closure under Converse Evalutaion

Lemma:

where is the transition in dynamics from here.

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