3 ms·
He (Morris, actually) defines observational equivalence as: e1 == e2 iff for all contexts C, C[e1] halts iff C[e2] halts. Which is a great tr
by maest 6y ago
He (Morris, actually) defines observational equivalence as:
e1 == e2 iff
for all contexts C,
C[e1] halts iff C[e2] halts.
Which is a great trick to avoid having to compare contexts. Around 29:00 they discuss how to show 5 != 6.
One question I have is: what if your language doesn't allow for ways to halt? For example, a language where you have no loops. That definition would imply everything equals everything, since all contexts eventually halt.
- marvy 6y agoYou can tweak the definition to take advantage of whatever your language DOES allow. He alludes to this during the Q&A at the end. For instance: two expression are equal if (and only if), for all possible contexts C, you have C[e1] and C[e2] send the same bytes to standard output.
- fanf2 6y agoIn most of the talk he’s using Ω to mean the program doesn’t halt, i.e. does not produce an answer. He also mentions when explaining Ω that it is often used as a stand-in for a run-time error. An uncaught exception can do the same job, for example. (The reason for this that if you are describing the semantics of a language using a collection of reduction rules, and evaluation gets to a point where no reduction rule applies, then the program gets “stuck”. You would normally implement this as a runtime error but semantically it has the same effect as an infinite loop.)