Review Comment:
[editorial note: this review was converted from a pdf file; bold face text was emulated by _text_, sub- and superscript using the LaTeX notation; some formatting was lost in the conversion (e.g. \varphi vs \phi, {\cal K}) but were left as is for clarity; one item was described verbally using a LaTeX-like notation (arrow with text above it)]
1 General
The paper proposes an extension of Transaction Logic (TR), called External Transaction Logic (ETR), which incorporates external actions. The main difference with the actions used in TR is that the external actions cannot be rolled back if they fail. The main contributions are the extended semantics, which is not a trivial extension, and an extended proof theory that can handle external actions.
All in all, the paper definitely deserves to be published, but only after a major revision. The main problems in the current version is poor English, and the proofs in the appendixes are subpar to put it mildly. A big problem with the proofs is that sloppy and inadequate English, which is already felt as a major problem in the main part of the paper, gets in the way of understanding the proofs. I only got through 20% of the proofs and the last straw that caused me to stop reading was a reference to Lemma 19 in the proof of Lemma 8.
As far as English is concerned, the quality is very uneven, which leads me to think that the problem is sloppiness rather than the inadequate command of the language. The authors must spend time to fix innumerable issues in the English department. I marked only a small fraction of the lapses I found but even this amount is considerable. These include missing/incorrect articles, missing/wrong endings for the plural, tense, and the like. Lapses like “rollbacked” and “rollbacking” instead of “rolled back” and “rolling back,” “composed by” instead of “composed of,” missing propositions and, sometimes, entire phrases. In some other places all these are used correctly, so it is not the case that the authors don’t know the correct forms of these phrases.
There is also fair amount of words that are used completely out of place, like “enunciation of results,” “definition retrieves a path.”
The authors can find the specific places where these lapses occur via simple search, so, for the most part, I will not be pointing them out below.
2 Details
The following is a list of detailed comments in the order that corresponds to the flow of the text. The importance of these comments varies. The comments are identified either by a line number within the page/column or by a line number within a numbered example, lemma, and the like.
p.2,c.1,l.6: with _respect to_ the semantics
Ex1,l.1: As _an_ illustration
p.2,c.2,par2. The semantic of TR talks about _how_ ... To remind: this is just one of the uses of TR: [5,49] talk about reasoning about actions rather than the details of execution.
p.4,c.2,line above Sec 2 heading: “proofs of the anunciated results” −−> ... our results ...
Sec 2,par3,l.7: while φ ∧ ψ −−−> φ ∨ ψ
p.5,c.1,l.1: condidere_d_
l.4: denoted as −−> , called
+3 lines: under −−> in
Def 4: is a model of _a_ TR formula
p.7,c.2,ex8,l.12: consider −−> suppose
p.8,c.1,l.6: Thus, in a implementation −−> Thus, from the implementation ...
+3 lines: the umpteenth occurrence of the aforesaid nonexistent verb “rollback.”
+2 lines: alternative branching in a proof −−> ... branch from the proof theory perspective
+4 lines: double “is”
+4 lines: branching −−> branch.
p.8,c.1,l-8: use −−> used
Sec 3.1 minus 1 line: with _respect to_ ETR
Definition 8: Shouldn’t you say that ext(a,noop) cannot change the external state? Also, right after that definition, expand on the _ext_ primitive. Talk about the novelty of the semantics only after you explained the notation in Def 8.
Next paragraph: the stuff about the restrictions on the negation. This is not a proper way to define things. Here you are defining the syntax of your language and this important aspect cannot be crammed into one broken paragraph. The issue here is not that you are limiting negation to atoms, but that you are now limiting the syntax explicitly to statements of the form f oo ← bar1 ⊗ bar2 ⊗ .... This deserves a much more conspicuous place in that section.
Ex9, l.11: a treatment cannot be eligible – people can be: eligible −−> suitable.
p.9,c.2,l.22: delete “seen”
p.10, c.1,l-1: mapping from _pairs_ of external states _to_ formulas ...
c.2,l.3: execute _at_ state _identified by_ E_1 yielding the state _identified by_ E_2.
+4 lines: delete “at all”
c.2,bottom: Thus, we assume ... states. You already said this at the top of that column. I noticed a number of this kind of unhelpful repetitions.
p.11,c.1,l.11: how _it_ can be ...
Def9: he path notation is weird, is confusing, and is hard to parse in some contexts (e.g., when commas separate unrelated things). I strongly suggest to use something like S_1 \over{A_1}{−→} S_2 \over{A_2}{−→} ... \over{A_{k-1}}{−→} S_k. [editorial note: \over{A}{-->} denotes an arrow over which A is typeset]
+1 line: help the semantics _deal with_ recovery ...
+5 lines: allow −−> allows
+2 lines: advent −−> event
+3 lines: but now _they cater_ also _to_ the external oracle. Even better to say “but now they incorporate
the external oracle” or something like that.
Def 10: Is φ an atom? You said it is an arbitrary formula, but in items 2,3 in that definition you are writing (D_1, E), φ, (D_2, E), which has been defined only if φ is an oracle atom.
c.2, 1st par: Poor English here stands in the way of understanding. Just say that oracle atoms cannot occur in the rule heads and that this is not a limitation of the expressive power. Then give your explanation.
Def 11: Very badly written definition. On top of it, I don’t think you are actually using it.
par above Def 13: with...state −−> consisting of... state_s_
p.12,c.1,par 3: You already said this couple of times, but the third time isn’t a charm: English has deteriorated significantly compared to the previous two mentions of this trivial point. Delete the paragraph.
Ex 10: but where ... replaced −−> but now expressions like ... are replaced with external ...
c.2,par 3: In partial .... You already said this before.
c.2, l-11: so that _previously executed_ external actions can be ...
l-9: that either φ succeeds _classically_ (|=_c) _on_ path ...
p.13,c.1,l.6: obtained by −−> composed of
ll.11-12: double “with”
l.12: of −−> to
+2 lines: in case (no “the”). Same in the next line.
+4 lines: points −−> items. This occurs several times later in the same column
+1 line: _a_ “legitimate” _failure as one_ where ...
+2 lines: such −−> this
+2 lines: point −−> claim
+1 line: constrain_ed_
Next in Proposition 1 ... point: delete this part. Instead: “Claim 2 in the proposition states that ...”
a few lines below: “where a φ” – delete “a”. Same line: “executed, then” −−> executed, it is the case that ...
+2 lines: delete “the” in front of “partial”
+1 line: point −−> claim
Prop 1, claim 1: This claim seems very sloppy and even vacuous. First, how is “a” related to φ in that claim? Second, _failop_ seens to always satisfy this claim. Since you never related the “a” to φ, you have not really stated anything in this claim.
Def 15: give a clarifying example after the definition.
Definition 16. Previously you were using b1 ⊗ ... ⊗ b_k for compensation and now you are suddenly introducing new notation like A^{−1}? Choose one notation and stick with it.
General question about Defs 15-17. You never really said that compensation cannot fail, did you? It is a conjunction of oracle actions, but these actions might not stack together. What does such a failure mean to the theory? In practical terms?
p.14,c.1,l.8,9: the path as follows −−> the following path
c.1, l.-1: definition “retrieves” path. Definitions don’t “retrieve” anything. They “define” things. A dog may retrieve a ball, a query may retrieve data. But definitions don’t.
c.2, l.4: what −−> which
l.9 after Def 18: rollback for the initial state −−> roll back to the initial state
+1 line: branching −−> branch
c.2,l-2: formalize −−> state
p.15, par after Th2: Due to .... This is related to my previous comment about your restriction on negation. You should define the restriction properly. Maybe here so as to not split the description. In any case, this whole sentence “Due ...rule” is poorly written both mathematically and grammatically. Clearly, satisfying the rule bodies is not enough to satisfy rules, despite what this sentence says. You can drop this sentence without any harm.
c.1,l.-6: logical account _of execution of_ ETR
+1 line: inherite_d_
Th 3: paths π and π'. Give an inline example to show how one is obtained from the other. Will make the statement of the theorem much clearer.
p.16,c.1,par6: relate these rules to Fig 1, i.e., say that they correspond to rules 1-4. But don’t restate the meaning in English. At least, don’t restate the meaning in that kind of English.
Next par: contrarily. Not “contrarily” but “in addition.” Something like “Moreover, in addition to the TR proof rules, ETR includes a rule to deal ...”
+2 lines: handle −−> deal
+3 lines: “to rollback.” need to roll internal actions back, compensate the executed external actions,...
c.2, l.-3,4: “Contrarily ....” There is really no such a word. At best, it is a very clumsy word. Say this: “On the other hand, open world reasoning assumes that ...”
Fig 1: if all conditions hold −−> if all of the following conditions hold
The 4 items at the bottom of Fig 1: This is very terse and obscure. You need to explain this much better and _give an example_! I suggest not to use a figure here, but itemize the rules and provide an explanation immediately after each item.
p. 18, c.1, l.-16: of the following _form_
c.2, l.20: query q over _the KB_ K
c.2,l-4: as −−> a
p.19, Def 23. What does it mean “iff q ← ∃y conj(c, y)?” Such a rule is supposed to be true always. What you must have meant was K |= ∃y conj(c, y). Moreover, all that stuff about conjunctive queries on p.18 is not needed, including Eq (5). All you need are the statements like K |= ∃y conj(c, y) in your definitions and claims.
p.20, par 4, “To achieve...” Again, q drops in out of nowhere. As I said, you don’t need these q’s and the stuff about conjunctive queries on p.18.
General comment on Sec 4. I found this section not particularly useful or insightful. You give a bunch of obvious definitions and then don’t follow up on them to explain the consequences of using this or that oracle. So what if you gave some Holds-statements in Example 14 or in the event calculus part? What difference does it make if you use sitcalc or some other formalism? You have not shown anything interesting that illustrates how the choice of the oracle affects things. Without such considerations, the reader is left with the feeling that s/he was dragged through a series of tedious definitions without getting any reward. Same issue with Examples 15 and the DL oracle.
p.23,c.1,l-6: consider−−>considered
c.2,l-3: receives −−> uses
p.24,c.1, middle: “However, these solutions ...” What does “these” refer to?
c.2, middle: the discussion of TR-PAD, “oracles are abandoned” etc. TR-PAD is a strict extension of TR and oracles are not abandoned. Partially defined actions and oracle-defined actions live together happily. PADs are used for completely different purposes and your external actions are used for yet other purposes. So your comparison misses the point: you are comparing apples and oranges.
p. 28,c.1, l.11: .. splits ... −−> there is a split π_1 o π_2 = π ...
+4 lines: it exists −−−> there is
+7 lines: Then −−> Therefore,
+10lines: “is impossible” is missing before “for”
c.2, Lemma4, par 1, skeptical models. This whole explanation is inadequate. Explain in precise terms and symbolically whenever possible.
Lemma5: “both valid in TR and ETR.” Valid means true in all models. You want to say “that
is well-formed both in TR and CTR.” Now, when it comes to interpretations in the next sentence, “valid” makes no sense whatsoever. There (in the next line you want to say something like “such that M is also an interpretation for P in ETR.”
+6 lines: say −−> saying
+2 lines: with −−> to. Also: model_s_
+5 lines: “obtained from π' adding the” −−> obtained from π' _by_ adding _a_
same line: in connection with E_0 , what is this constant state? You are adding it where exactly? How?
+2 lines: “coincide with definitions”. Here you lost me completely. What does it mean?
+1 line: contain external _actions_ then ...
+1 line: this line (which is the last in the proof of L5), you are claiming that it follows from Th2, but this is not what Th2 says.
Same page, L6, last line of the proof: this is a non-sequitur. You are obviously relying on the fact that π = (S_0, S_1) ◦ π_2 , where π_1 = (S_0, S_1), but you neglected to mention this.
p.29, c.1,l.12: _a_ complete unfold_ing_ of formula
Lemma 7, last line before the proof: then −−> it is the case that. Otherwise you have too many “thens” and your text becomes unreadable. This problem occurs multiple times, so watch it.
Proof, base case, k = 1. What is k? Shouldn’t you state what the induction is based on?
Inductive case: Assume it is true: What is it that you are assuming to be true? You have not set up the inductive assumption properly and not even the base case. There are rules in formulating inductive proofs and you should follow them.
End of the 1st paragraph in the inductive case: This seems like an overkill. You have not stated it, but it seems you are assuming that each φ_1 is defined by an oracle, so π_2 must be the terminal 1-path of π.
p.29,c.2,l.14: “this case is only true” −−> then π must be a ...
+2 lines: missing _holds by assumption_, before “then”
+7 lines: then L_1 ∈ M ... −−> _it is the case that_ L_1 ∈ M ...
+9 lines: it exists −−> there is
Same line: L_i ⊗ L_{k+1} . Did you mean L_i ⊗ . . . ⊗ L_{k+1}?
+1 line: Then there −−> There
+2 lines: _I.H._ Spell out!!
+4 lines: it exists −−> there is
+2 lines: Lemma 19. Really? While proving Lemma 8 you are relying on Lemma 19? Who is going
to read this kind of proofs?
p.29,c.2,l-2: L_1 ⊗ L_k ⊗ L_{k+1}. Did you mean L_1 ⊗ . . . ⊗ L_k ⊗ L_{k+1} ?
last line: what is “a split for |=_c ”?
At this point, the accumulation of poorly constructed proofs, bad English, and sloppiness overwhelmed me to the extent that further reading became counter-productive. The burden is on the authors to revise the paper and make it readable.
|
