7 October 2004A Syntactic Commutativity Format for SOS
I recently had a look at the paper A Syntactic Commutativity Format for SOS (Computer Science Report CSR-04-25, Department of Mathematics and Computer Science, Eindhoven University of Technology, 2004) written by Mohammad Reza Mousavi, Michel A. Reniers and Jan Friso Groote.
I already mentioned some of the work on SOS by these authors in one of my previous postings. I am happy to say that, at least to my mind, these authors have demonstrated yet again in this paper the results that can be achieved by asking simple and natural questions. Indeed, this one-theorem paper addresses a very natural question in the meta-theory of SOS that, surprisingly, had not been asked before in the literature---at the least to the best of my knowledge. The question is whether there is a reasonably general syntactic format of SOS rules that guarantees that certain language operators are commutative in all arguments. The rule format proposed by the authors is a pleasing variation on the well known tyft format due to Groote and Vaandrager, with an unexpected twist that adds to the generality of the proposal. (I was surprised to see that premises of a commutative mirror rule could be mapped to conclusions of the rule it mirrors.)
The proof of the main result is a variation on that of the classic congruence proof for the tyft/tyxt format by Groote and Vaandrager, and is well presented.
Overall, this is a good paper that addresses and solves a natural and interesting problem. I recommend it to anybody interested in the theory of SOS.
Congratulations to the authors for asking a good question, and answering it professionally and efficiently. I wish that I could take a leaf out of their book.
Last modified: Thursday, 07-Oct-2004 09:58:00 CEST.