I like to think that I am not a procrastinator by nature and I try (but often fail) to apply Littlewood's zero-infinity law in my work, but am I the only one who feels that the number of things to do keeps increasing while the available time to carry them out decreases very fast?
end rant
One of the many things that I have been struggling to get done on time in this hectic early 2009 was a report on the first year for one of my ongoing grants. This reminded me of two papers I recently co-authored that I had meant to mention on this blog. Both papers offer a modest contribution to the meta-theory of Structural Operational Semantics.
Structural Operational Semantics (SOS) was introduced by Gordon Plotkin as a logical and structural approach to defining operational semantics for programming and specification languages. The logical structure of SOS specifications supports a variety of reasoning principles that can be used to prove properties of programs whose semantics is given using SOS. Moreover, SOS language specifications can be used for rapid prototyping of language designs and to provide experimental implementations of computer languages. Thanks to its intuitive appeal and flexibility, SOS has become the de facto standard for defining operational semantics, and a wealth of programming and executable specification languages have been given formal semantics using it.
The meta-theory of SOS provides powerful tools for proving semantic properties for programming and specification languages without investing too much time on the actual proofs; it offers syntactic templates for SOS rules, called rule formats, which guarantee semantic properties once the SOS rules conform to the templates (see, e.g., the papers in this bibliography maintained by MohammadReza Mousavi). In some sense, this is akin to an axiomatic development of the theory of operational semantics. One devises some rule patterns (the aforementioned rule formats) that "axiomatize" sufficient syntactic conditions guaranteeing that all programs in a language afford some desirable semantic property.
There are various rule formats in the literature for many different semantic properties, ranging from basic properties such as commutativity and associativity of operators, and congruence of behavioral equivalences to more technical and involved ones such as non-interference and (semi-)stochasticity.
The most recent paper I wanted to mention here is entitled Rule Formats for Determinism and Idempotency and is coauthored with Arnar Birgisson, Anna Ingolfsdottir, MohammadReza Mousavi and Michel Reniers. (An extended abstract of this work will appear in the Proceedings of Third FSEN: IPM International Conference on Fundamentals of Software Engineering (FSEN09), Iran, April 15-17 2009. Lecture Notes in Computer Science, Springer-Verlag, 2009.) In that paper, we propose rule formats for two properties, namely, determinism and idempotency of binary operators. In hindsight, it is quite surprising that no rule format guaranteeing determism had been proposed before. After all, determinism is a natural and important semantic property, which holds for sub-languages of many process calculi and programming languages, and is also a crucial property for many formalisms for the description of timed systems---where time transitions are required to be deterministic, because the passage of time should not resolve any choice.
Idempotency is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. Idempotency of a binary operator f is concisely expressed by the following algebraic equation.
f (x, x) = x
Determinism and idempotency may seem unrelated at first sight. However, it
turns out that, in order to obtain a rule format for idempotency that is sufficiently general to cover the special cases we wanted to cover, we need
to have the determinism of certain transition relations in place. Therefore, having a syntactic condition for determinism, apart from its intrinsic value, results in a powerful, yet purely syntactic framework for idempotency.
The second paper, On the Expressibility of Priority (Information Processing Letter 109(1):83-85, 2008), is joint work with Anna Ingolfsdottir. It is more modest in scope and offers results confirming that the priority operator of Baeten, Bergstra and Klop cannot be expressed using positive rule formats for operational semantics. Although expected, this inexpressibility result does not seem to have appeared before in the literature.
Overall, I really enjoyed working on those two papers. Thanks to my coauthors (old and new) for having given me the opportunity to work with them on these projects.
No comments:
Post a Comment