From: Paulo J. M. <poc...@gm...> - 2009-06-17 14:23:00
|
On Wed, Jun 17, 2009 at 2:46 PM, Laurent Voisin<lau...@sy...> wrote: > Paulo, > > Le 17 juin 09 à 15:32, Paulo J. Matos a écrit : > >> On Wed, Jun 17, 2009 at 2:16 PM, Laurent >> Voisin<lau...@sy...> wrote: >>> >>> Hi, >>> >>> Le 17 juin 09 à 15:04, Paulo J. Matos a écrit : >>> >>>> In the wiki page: >>>> >>>> >>>> http://wiki.event-b.org/index.php/ASCII_Representations_of_the_Mathematical_Symbols_(Rodin_User_Manual) >>>> >>>> There is a reference in the bottom to: oftype >>>> It's the first time I hear about this character. What's its usage for >>>> in Event-B? >>> >>> it is used to specify a type for empty sets or bound identifiers. For >>> instance, if you type in a formula: >>> >>> ({} oftype POW(S)) >>> >> >> Isn't this inferred through type inference? > > Yes, most of the time, the type of an empty set can be inferred by type > inference, but not always. For instance, if you write the predicate > > {} = {} > > then the type of each empty set cannot be inferred, and this predicate will > be rejected by the static checker. Thanks to the "oftype" operator, you > write an equivalent predicate > > ({} : POW(S)) = {} > > which will type check and be accepted by the static checker. > Great, thanks! I didn't know this was possible. >>> it denotes the empty set of type POW(S). Similarly, you could type: >>> >>> !(a oftype INT). true >>> >> >> Would this be the same as: >> ! a . (a : INT => true) >> ? > > It would be equivalent (in a mathematical sense) but not identical. > Actually, the prover normalization would transform the latter in the > former. > That's great to know! Thanks for the explanations! Btw, what's the unicode character corresponding to the oftype operator? Doesn't seem to be neither in the mathematical language nor elsewhere. Thanks, Paulo Matos > Laurent. > >>> to write a typed universally quantified predicate. >>> >>> It is not expected that users need to use this operator when entering >>> models. However, when proving it can become very handy (e.g., for >>> instantianting a universal or existential quantifier). > > > -- Paulo Jorge Matos - pocmatos at gmail.com http://www.pmatos.net |