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?

  • $\begingroup$ Probably useful to think function composition, where things happen right-to-left. $\endgroup$ – D. Ben Knoble Jan 21 at 23:19
  • $\begingroup$ But this is exactly not function composition. Category theory texts emphasize the difference between (f;g) and (g o f) $\endgroup$ – Gergely Jan 22 at 14:12
  • $\begingroup$ 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. $\endgroup$ – D. Ben Knoble Jan 22 at 15:35
  • $\begingroup$ 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) $\endgroup$ – Gergely Jan 23 at 9:52
  • $\begingroup$ interesting. I learned something, thanks! $\endgroup$ – D. Ben Knoble Jan 23 at 13:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.