§ full abstraction in semantics (TODO)
- Observational equivalence: same results when run,
- 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 For example, I thought that the problem will
or and PCF
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
g diverge on all inputs).
- SEP reference
§ Relationship between full abstraction and adequacy
- Adequacy: iff . This says that the denotation agress on observations.
- See that this is silent on divergence .
§ Theorem relating full abstraction and adequacy
- Suppose that . When is the converse true? ( ?)
- It is true iff we have that iff .
§ Full abstraction between languages
- say two languages have a translation and have the same observables .
- Then the translation is fully abstract iff
- See that cannot be more expressive than if there is a full abstract translation from into .