From: Alex Kozlenkov <alex.kozlenkov@betfair.com>

Date: Wed, 3 Sep 2008 14:43:27 +0100

Message-ID: <E39E50172D7A6546BCE3E981C985C98731E0E2EB@UKMAIL.sportex.com>

To: <public-rif-wg@w3.org>

Date: Wed, 3 Sep 2008 14:43:27 +0100

Message-ID: <E39E50172D7A6546BCE3E981C985C98731E0E2EB@UKMAIL.sportex.com>

To: <public-rif-wg@w3.org>

I've been focusing for awhile on our involvement in Complex Event Processing related activities so reading the August set of RIF documents now. First of all, congratulations to Christian and co. for their courage to boldly go ahead and propose an operational semantics in PRD. I remember a long time ago, a few people were shouted at for even daring to think it was OK. In fact, the specification that has emerged so far is quite compatible with Process Algebraic approaches that are in turn closely related to functional programming and Category theory. In particular, the notion of a "configuration" is quite alike a "term" in process algebras. The LTS described together with actions then forms a category of terms as objects and actions as arrows. The behaviour can then be described as a mapping f:T->BT where T is a term and B is a behavioural functor capturing all the target terms reachable from T. This definition is slightly superior to using an LTS since the transition relation in the latter is completely symmetrical and hence the intuition that behaviour is represented by outgoing transitions (but not incoming ones) is not captured. Extending the functor equivalence, for each configuration, there exists a unique "final" coalgebra that corresponds to sets of "runs" Action* (finite due to the existence of the terminal configurations). That set of runs uniquely describes a configuration (state, term) in terms of its all possible subsequent action histories. Also, a notion of simulation and bisimulation in linear or branching time could be discussed for such systems. Finally, deductive systems being equivalent to categories with terms as objects and arrows as proofs, we actually can see a good synergy of the BLD and PRD semantics. I could not immediately see the restriction that given a pair (cs,a), the target configuration ct will be unique (as this is not part of an LTS definition). A non-uniqueness would imply that the transition is non-deterministic (unless there is provision for selecting the specific target configuration). It is interesting that actions selected from a set L of labels could be generalised to actions other than assert and retract, for example, message passing, which brings us closer to process algebras. It is also interesting to note that there in fact exists an equivalence class of configurations that will behave in exactly the same way given the same set of rules RL. This minimality or possible factorisation is not discussed in the PRD document. The same minimality argument applies to each individual transition as a question may be asked, what minimal subset of the configuration exhibits the same behaviour. Cheers, Alex Kozlenkov ________________________________________________________________________ In order to protect our email recipients, Betfair Group use SkyScan from MessageLabs to scan all Incoming and Outgoing mail for viruses. ________________________________________________________________________Received on Wednesday, 3 September 2008 13:43:39 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:47:52 UTC
*