Hacker News Reader

Comment by maest | Hacker News Reader

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.

View on HN

In 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.)

You 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.

Reply on news.ycombinator.com