§ full abstraction in semantics

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

• HackMD notes by Alexander Kurz