## rodin-b-sharp-handbook

 Re: [Rodin-handbook] Rodin-b-sharp-handbook Digest, Vol 7, Issue 1 From: Matthias Schmalz - 2011-12-08 13:34:35 Hi Daniel, > Hello Matthias, > > On 28.11.2011 14:12, Matthias Schmalz wrote: >> Hi Michael, >> >> Here is some feedback on the Rodin handbook. >> >> 1) Actually I have already used the email feedback feature. I asked for >> a confirmation that my feedback has been received, but I never got a >> confirmation. Apparently, there is a problem with the email feedback. > we have received several feedback messages from you. The feedback is > collected in a spreadsheet first and not all messages are attended to > yet. I'm sorry if you might had the impression that we do not read the > feedback. Thanks for explaining. Apparently, the problem was on my side. > First, thank you for your feedback. This is exactly the kind of feedback > I hoped for because I'm a little bit unsure regarding some topics of the > reference section. I still have some questions about what you said about > section 3: > >> 2) Proving / Provers: [...] >> 3) On Mathematical Notation / Sets: >> >> I have some feedback on how you introduce the various operators. >> I focus on the example of subset (\subseteq), but it applies to other >> definitions as well. Here is the "definition": >> >> S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T >> >> There is some room for interpretation what this actually means; here is >> what I understood: >> - It is not entirely clear whether S and T range over only well-defined >> or also over ill-defined values. I assume the latter. For, otherwise the >> statement L(S \box T) \triangleq L(S) \land L(T) would be pointless. > > My intention was this: Under the assumption that the predicate is > well-defined (as defined by the statement > "L(S \ T)<: L(S)& L(T)"), "S<: T" is logically equivalent to "!e. > e:S => e:T". > I think in this context "L(S<:T) == L(S)& L(T)" is not pointless, > because it just defines under which conditions the equivalence holds. My question is whether S and T may be ill-defined. Is this the case? Also, your intention is not obvious from what you have written. Maybe you should write "L(A) => (A \triangleq B)" instead of "A \triangleq B" >> - Then it is not entirely clear what the \triangleq means. A logic of >> partial functions has many notions of equality. I assume that A >> \triangleq B means that A is true/false/ill-defined iff B is >> true/false/ill-defined, respectively. This emphasizes that the left- and >> right-hand side of a definition are interchangeable. > I agree with you here. There is currently no definition of the operator > in the handbook yet. My understanding is that A \triangleeq B means A is > true/false iff B is true/false. There is a syntactical difference between mine and your definition of \triangleeq. ("true/false/ill-defined" vs. "true/false") On a closer look, they have the same semantics. I take that as a confirmation for my definition. > As said above, the ill-defined case is > ruled-out by the WD-condition. See above. >> With this in mind, I spotted some problems: >> >> - Did you introduce "\in"? I could not find it. I admit, it is not >> possible to define "\in". But maybe you should say at some point what >> you take as granted and what you define on your own. That prevents >> readers from searching for definitions that do not exist. > Yes, \in is defined in 3.3.2. Somewhat arbitrary, maybe it fits better > into the sets section. Okay. I have overlooked it. >> - The left- and right-hand side are actually not interchangeable. For, >> if S is the empty set and T ill-defined, then the lhs is ill-defined and >> the rhs is true. >> One may go one step further: the two equalities >> S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T >> and >> L(S \box T) \triangleq L(S) \land L(T) >> imply >> L(\forall e\qdot e \in S \limp e \in T) \triangleq L(S) \land L(T), >> which is certainly not the case. > But is this still the case if we assume S and T as well-defined? Or am I > too naive here? You are right (and not too naive). If you assume that S and T are well-defined, the problem with L(\forall e\qdot e \in S \limp e \in T) \triangleq L(S) \land L(T) disappears (both sides are true). >> - Actually you have two kinds of variables and two kinds of equalities >> in the handbook. This makes it difficult to infer what is actually >> meant. I would make the difference between the two kinds of variables >> syntactically visible, and explain the semantical difference between the >> two kinds of variables/equalities up front. > With two kinds of variables you mean > a) a variable as a placeholder for an arbitrary expression and > b) an Event-B identifier? Yes. > I'm not sure what you do mean by the second equality? Do you mean > statements like: "S \/ T = { x | x:S or x:T }"? > In that case, does that really leads to any confusion? The two equalities are "=" and "\triangleq". I see two sources of confusion: - It is not explained what "\triangleq" means. - In some definitions, \triangleq is used; in others, it is "=". >> I believe that almost every reader of the handbook has already seen the >> subset relation and will find the equation >> S \subseteq T \triangleq \forall e\qdot e \in S \limp e \in T >> rather obvious. So he will not learn anything from reading this >> definition. Instead of emphasizing what the reader already knows, the >> handbook should point out how Event-B's operators deviate from the >> reader's intuition. > I do not agree fully here. For most (if not all) it is obvious. But > where do we draw the line? Using prose everywhere just to avoid a formal > notion would make the reference much more clumsy to read. First off, I do not suggest to kick out the definition of \subseteq or to avoid formal notation altogether. Currently, it is rather clear that \subseteq is somehow the subset relation. The details on well-definedness are currently rather implicit, and on a closer look also contradictory. >> 4) Some miscellaneous comments: >> >> In Section 3.3 you refer to the Z reference manual. There was never an >> agreement how partial functions are handled in Z. I would therefore not >> try to understand Event-B from the Z reference manual. > I agree. But the note is a reference for handbook writers as an example > for a handbook for a mathematical notion, not for Z's foundations. The > note will be removed before the final release. Good. The overall problem remains: - You have to clarify whether your variables range over well-defined values or over arbitrary values. In my thesis, I need two kinds of variables: well-defined variables x, y, z, and operator variables $x,$y, $z that range over arbitrary values. - You have to clarify the definition of "\triangleq". Under the current definition "$A <: $B \triangleq ! x. x :$A => x : $B" is invalid. I see two ways out: -- Use ordinary variables, i.e., "A <: B \triangleq ! x. x : A => x : B" -- Use \sqsubseteq instead of \triangleq, where "$P \sqsubseteq $Q" iff "L($P) => ($P \triangleq$Q)". The definition is then: "$A <:$B \sqsubseteq !x. x : $A => x :$B" Good luck, Matthias