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 q3JD2D7l018041 for ; Thu, 19 Apr 2012 15:02:13 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AksFAAMMkE/Y5v4vmGdsb2JhbABDgxyCSZgckCqDFiIBAQEBAQgJDRsnggkBAQUjDwEFQAEQCxgCAgUWCwICCQMCAQIBRQYNAQcBAYgKAac3ky6BL412gRgEiFqNFYV0jT0 X-IronPort-AV: E=Sophos;i="4.75,446,1330902000"; d="scan'208";a="154731790" Received: from amout07.alpha-mail.net ([216.230.254.47]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 19 Apr 2012 15:02:07 +0200 Received: from webarc04.alpha-mail.jp (webarc04 [216.230.254.84]) by amout07.alpha-mail.net with ESMTP id q3JD22wQ000441; Thu, 19 Apr 2012 22:02:02 +0900 X-Virus-Scanned: amavisd-new at Alpha-Mail Out Received: from ltsub02.alpha-mail.net (ltsub02 [216.230.254.30]) by webarc04.alpha-mail.jp (Postfix) with ESMTP id DA8111C080CB; Thu, 19 Apr 2012 22:01:54 +0900 (JST) Received: from [192.168.0.110] (196.62.205.61.west.global.crust-r.net [61.205.62.196]) by ltsub02.alpha-mail.net (Alpha-mail) with ESMTP id 5645F746004C; Thu, 19 Apr 2012 22:02:01 +0900 (JST) Message-ID: <4F900CCD.5050102@itpl.co.jp> Date: Thu, 19 Apr 2012 22:02:05 +0900 From: Satoshi Ogasawara User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120327 Thunderbird/11.0.1 MIME-Version: 1.0 To: =?UTF-8?B?RGFuaWVsIELDvG56bGk=?= CC: caml-list@inria.fr 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> In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] [ANN] PEC ver. 1.1 Thank you for helping me understand with your explanation. 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]. 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. (2012/04/19 19:31), Daniel Bünzli wrote: > Right. But you still have to maintain some kind of mapping between the primitive event and the leaves they may influence to know which ones to update when the corresponding primitive event occurs. Do you store that in the primitive event itself or do you use a global data structure ? Primitive events has list of leaves. Best Regards, Ogasawara