Re: [Caml-list] [ANN] PEC ver. 1.1

["Daniel Bünzli" <daniel.buenzli@erratique.ch>]

Le jeudi, 19 avril 2012 à 15:02, Satoshi Ogasawara a écrit :
> Your event semantics has two invariant.
>  
> 1. for all e, t : occurrence of [e] at time [t] is one or zero.
> 2. if primitive [e] is occurred in time [t], update cycle runs in time [t].


Yes. You can read about the denotational semantics of React here:

http://erratique.ch/software/react/doc/React#sem

Besides all the combinators of React have a complete description of their denotational semantics. Note that in general for users of FRP I think it really doesn't help to think about update cycles, it seems to bring in more confusion. Users should care and think in terms of the semantics of events and signals. Update cycles are an implementation detail and should be understood only by programmers who need to interface the FRP system to a problem domain.  

> Do you have any experience to proof a theorem against event combination term
> by using above axiom and event combinators semantics? I'm interested in this
> kind of reasoning.


In this post I use the semantics and equational reasoning to understand why something doesn't happen.  

https://sympa-roc.inria.fr/wws/arc/caml-list/2009-12/msg00054.html

(you may have to read the whole thread to fully understand the example).  

> It's correct. But the performance can be optimized in future I think.
>  
> When subscribing a event, we can collect and store information about tree structure.
> Present implementation discards these information.




I didn't think hard about this but I suspect you'll hit problems with dynamic changes to the dependency graph (e.g. switching). And besides one should be careful not to make the creation of signals and events too expensive. I'm doubtful but I'm interested in hearing if you get any results in that direction.
  
Best,

Daniel