From: Matthias Schmalz <Matthias.S<chmalz@in...>  20111208 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 welldefined >> or also over illdefined 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 > welldefined (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 illdefined. 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/illdefined iff B is >> true/false/illdefined, respectively. This emphasizes that the left and >> righthand 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/illdefined" 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 illdefined case is > ruledout by the WDcondition. 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 righthand side are actually not interchangeable. For, >> if S is the empty set and T illdefined, then the lhs is illdefined 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 welldefined? Or am I > too naive here? You are right (and not too naive). If you assume that S and T are welldefined, 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 EventB 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 EventB'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 welldefinedness 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 EventB 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 welldefined values or over arbitrary values. In my thesis, I need two kinds of variables: welldefined 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 