W3C home > Mailing lists > Public > public-rif-wg@w3.org > September 2008

RE: Congratulations on Christian's and co. courage

From: Alex Kozlenkov <alex.kozlenkov@betfair.com>
Date: Wed, 3 Sep 2008 14:49:33 +0100
Message-ID: <E39E50172D7A6546BCE3E981C985C98731E0E312@UKMAIL.sportex.com>
To: <public-rif-wg@w3.org>

Minor correction: deductive systems deal with formulas (not terms) as
objects and arrows as proofs.

-----Original Message-----
From: public-rif-wg-request@w3.org [mailto:public-rif-wg-request@w3.org]
On Behalf Of Alex Kozlenkov
Sent: 03 September 2008 14:43
To: public-rif-wg@w3.org
Subject: PRD: Congratulations on Christian's and co. courage


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.

________________________________________________________________________


________________________________________________________________________
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:49:42 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Tuesday, 2 June 2009 18:33:54 GMT