From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3JE9Lqk020583 for ; Thu, 19 Apr 2012 16:09:21 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEDAC8bkE9KN1ZKnGdsb2JhbABDhWWrfwEBAQEBCAsJHSeCCQEBBAEjVgULCxoCGA4CAj0KEAYbiAIFBAenQ5MtgS+NdjVjBJcBhE+NQw X-IronPort-AV: E=Sophos;i="4.75,446,1330902000"; d="scan'208";a="154744449" Received: from mail6.webfaction.com (HELO smtp.webfaction.com) ([74.55.86.74]) by mail1-smtp-roc.national.inria.fr with ESMTP; 19 Apr 2012 16:09:15 +0200 Received: from heyho.local (53-232.197-178.cust.bluewin.ch [178.197.232.53]) by smtp.webfaction.com (Postfix) with ESMTP id AEE1D20C65F0; Thu, 19 Apr 2012 09:09:13 -0500 (CDT) Date: Thu, 19 Apr 2012 16:09:06 +0200 From: =?utf-8?Q?Daniel_B=C3=BCnzli?= To: Satoshi Ogasawara Cc: caml-list@inria.fr Message-ID: <2B7FE930300F440ABE0F439A3418222C@erratique.ch> In-Reply-To: <4F900CCD.5050102@itpl.co.jp> References: <4F8D9D0E.1040007@itpl.co.jp> <4F8E1FF4.5070702@itpl.co.jp> <4F8EA91C.3060001@itpl.co.jp> <2B372C89CE4F408688B67B090FA5105C@erratique.ch> <4F8EFC34.7080906@itpl.co.jp> <4F8FD3EB.5050307@itpl.co.jp> <4F900CCD.5050102@itpl.co.jp> X-Mailer: sparrow 1.5 (build 1043.1) MIME-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Disposition: inline Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q3JE9Lqk020583 Subject: Re: [Caml-list] [ANN] PEC ver. 1.1 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