Denotational semantics of command sequencing

Moved from cstheory.stackexchange upon request

Winskel, in his book The formal semantics of programming languages, on page 58, writes:

C[c0;c1] = C[c1] o C[c0] a composition of relations, the definition of which explains the order-reversal in c0 and c1

For me C[c0] is the relation of pairs (s,s') where starting from state s executing the command c0 we arrive at state c1

and C[c1] is of pairs (s',s'') so their composition would be {(s,s'') | exists s' so (s,s') in C[c0] and (s',s'') in C[c1]}.

So it would be C[c0] o C[c1], just the opposite as in the book.

Is my thought wrong? Why?

• Probably useful to think function composition, where things happen right-to-left. – D. Ben Knoble Jan 21 '20 at 23:19
• But this is exactly not function composition. Category theory texts emphasize the difference between (f;g) and (g o f) – Gergely Jan 22 '20 at 14:12
• I'm certainly not an expert in category theory, but is there that large of a difference between composition of relations and composition of functions? (That is, isn't the set of functions a subset of the set of relations?). Just suggesting an intuition. – D. Ben Knoble Jan 22 '20 at 15:35
• Computer scientists tend to use the (f;g) notation to emphasize that f is applied first. Sorry for my wording, this is also function composition but not in the order of (g o f) – Gergely Jan 23 '20 at 9:52
• interesting. I learned something, thanks! – D. Ben Knoble Jan 23 '20 at 13:16