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

• HackMD notes by Alexander Kurz