## § full abstraction in semantics (TODO)

- Observational equivalence: same results when run, $\sim_O$
- Denotational equivalence: same denotation.
- Full abstraction: the two equivalences coincide: observationally equivalent iff denotationally equivalent.
- I thought full abstraction meant that everything in the denotational side has a program that realises it!

#### § Parallel `or`

and PCF

For example, I thought that the problem will `por`

in PCF was that it wasnt't possible to implement in the language.
- However, this is totally wrong.
- The reason
`por`

is a problem is that one can write a *real programs * in PCF of type `(bool -> bool -> bool) -> num`

, call these `f, g`

, such that `[[f]](por) != [[g]](por)`

, even though both of these have the same operational semantics! (both `f`

, `g`

diverge on all inputs). - SEP reference

#### § Relationship between full abstraction and adequacy

- Adequacy: $O(e) = v$ iff $[[e]] = [[v]]$. This says that the denotation agress on observations.
- See that this is silent on
*divergence *.

#### § Theorem relating full abstraction and adequacy

- Suppose that $O(e) = v \implies [[e]] = [[v]]$. When is the converse true? ( $[[e]] = [[v]] \implies O(e) = v$?)
- It is true iff we have that $e =_M e'$ iff $e =_O e'$.

#### § Full abstraction between languages

- say two languages $L, M$ have a translation $f: L \to M$ and have the same observables $O$.
- Then the translation $f$ is fully abstract iff $l \sim_O l' \iff f(l) \sim_O f(l')$
- See that $L$ cannot be more expressive than $M$ if there is a full abstract translation from $L$ into $M$.