Difference between revisions of "Errata First Edition"
(→1)) |
(→Proposed Erratum 16) |
||
Line 400: | Line 400: | ||
==== Erratum 16.3 ==== | ==== Erratum 16.3 ==== | ||
+ | |||
+ | Jesse Weaver noticed that, while the above modifications corrected previously raised issues, it did not guaranty symmetry and transitivity of equality, see [http://lists.w3.org/Archives/Public/public-rif-comments/2012Sep/0000.html here] (neither reflexivity, by the way). | ||
+ | |||
+ | PROPOSED: Adding the following constraints to the definition of state of the fact base, [[PRD#Condition_satisfaction|section 2.2.2]]: | ||
+ | * for every pair of constants ''c<sub>1</sub>'' and ''c<sub>2</sub>'', if ''c<sub>1</sub> = c<sub>2</sub>'' ∈ ''Φ'', then ''c<sub>2</sub> = c<sub>1</sub>'' ∈ ''Φ''; | ||
+ | * for every triple of constants ''c<sub>1</sub>'', ''c<sub>2</sub>'' and ''c<sub>3</sub>'', if ''c<sub>1</sub> = c<sub>2</sub>'' ∈ ''Φ'' and ''c<sub>2</sub> = c<sub>3</sub>'' ∈ ''Φ'', then ''c<sub>1</sub> = c<sub>3</sub>'' ∈ ''Φ'';" | ||
+ | |||
+ | and add the following condition in the definition of matching substitution in [[PRD#Matching_substitution|section 2.2.1]], under "''ψ'' is an equality formula, <tt>t<sub>1</sub> = t<sub>2</sub></tt> and either...": | ||
+ | ** or the ground terms ''σ(t<sub>1</sub>)'' and ''σ(t<sub>2</sub>)'' are the same ground term; | ||
+ | |||
+ | ==== Erratum 16.4 ==== | ||
While correcting erratum 16.1 and 16.2, I (csma) realized that, as they were defined, matching substitutions did not handle list equality. | While correcting erratum 16.1 and 16.2, I (csma) realized that, as they were defined, matching substitutions did not handle list equality. | ||
Line 414: | Line 425: | ||
*** or the ground terms ''σ(t<sub>1</sub>)'' and ''σ(t<sub>2</sub>)'' are constants in symbol spaces that are data types and they have the same value; | *** or the ground terms ''σ(t<sub>1</sub>)'' and ''σ(t<sub>2</sub>)'' are constants in symbol spaces that are data types and they have the same value; | ||
* ... | * ... | ||
+ | |||
+ | ==== Erratum 16.5 ==== | ||
+ | |||
+ | Jesse Weaver noticed that erratum 16.4 introduced the counter-intuitive possibility to equate a constant in a data type and a list, e.g. to a fact base may validly contain fact "3=List()" (see [http://lists.w3.org/Archives/Public/public-rif-comments/2012Sep/0000.html here]) | ||
+ | |||
+ | PROPOSED: add the following constraint in the definition of state of the fact base, [[PRD#Condition_satisfaction|section 2.2.2]]: | ||
+ | * for every equality formula ''c<sub>1</sub> = c<sub>2</sub>'' ∈ ''Φ'', either c<sub>1</sub> is not a constant in a symbol space that is a data type, of c<sub>2</sub> is not a list term;. | ||
=== Proposed Erratum 17 === | === Proposed Erratum 17 === |
Revision as of 16:39, 14 November 2012
Please report any suspected errors to public-rif-comments@w3.org (public archive). Confirmed errors will be documented on this page.
Contents
- 1 Proposed Erratum 1
- 2 Proposed Erratum 2
- 3 Proposed Erratum 3
- 4 Proposed Erratum 4
- 5 Proposed Erratum 5
- 6 Proposed Erratum 6
- 7 Proposed Erratum 7
- 8 Proposed Errata for RIF-PRD
- 8.1 Proposed Erratum 8
- 8.2 Proposed Erratum 9
- 8.3 Proposed Erratum 10
- 8.4 Proposed Erratum 11
- 8.5 Proposed Erratum 12
- 8.6 Proposed Erratum 13
- 8.7 Proposed Erratum 14
- 8.8 Proposed Erratum 15
- 8.9 Proposed Erratum 16
- 8.10 Proposed Erratum 17
- 8.11 Proposed Erratum 18
- 8.12 Proposed Erratum 19
- 8.13 Typos, simplifications, clarifications
- 9 Proposed Erratum 20
- 10 Proposed Erratum 21
- 11 Proposed Errata for RIF-FLD
- 12 Proposed Errata in DTB
- 13 Proposed Errata in OWL2/RL
- 14 More To Investigate
Proposed Erratum 1
Typos in BLD#Semantic_Structures (reported here)
- In item: I(o[a_{1}->v_{1} ... a_{k}->v_{k}]) = I_{frame}(I(o))({<I(a_{1}),I(v_{1})>, ..., <I(a_{n}),I(v_{n})>})
Thus, for instance, [a->b a->b] and o[a->b] always have the same truth value.
should read
Thus, for instance, o[a->b a->b] and o[a->b] always have the same truth value.
- Last sentence before The effect of datatypes
This implies that the equalities like t(a->1 b->2 c->3) = t(c->3 a->2 b->2) are tautologies in RIF-BLD.
should read
This implies that the equalities like t(a->1 b->2 c->3) = t(c->3 a->1 b->2) are tautologies in RIF-BLD.
Corrected
Proposed Erratum 2
XML serialization of rdf:PlainLitteral (reported here and here). See WG reply (here)
- PROPOSE to make it explicit (in DTB) that the xml:lang attribute must be used with value equal langTag for rdf:PlainLitteral constant where the langTag is not empty and that the content of a Const element with type="&rdf;PlainLitteral" is either the data value if the xml:lang attribute is not present, or the first element in the data value pair if the xml:lang attribute is present.
Proposed Erratum 3
Empty args tag must be omitted in RIF/XML (reported here)
- As discussed here and [1] here, and as published to the dev community here
- Requires corrections in BLD (as proposed by Harold here) and in FLD
Added 10 July 2012 by csma:
We have the same pb with the items role sub-element in List. PRD says explicitely that an empty list has an empty items sub-element (section 8.3.1.3), but the XML schema says that the empty items sub-element must be omitted. BLD and FLD may have the same pb (I am not comfortable enough with the notation in the XML mapping to be sure :-).
PROPOSED: correct:
- section 8.3.1.3 in PRD corrected (see here)
- the empty args XML mapping in BLD.
Corrected: http://www.w3.org/2005/rules/wiki/index.php?title=BLD&diff=14569&oldid=14564
- the empty args XML mapping in FLD.
Corrected: http://www.w3.org/2005/rules/wiki/index.php?title=FLD&diff=14572&oldid=14451
Proposed Erratum 4
Possible typo in all RIF documents (reported here)
- At the end of first paragraph in XML Schema Datatypes Dependency
required as otherwise specified
should read?
required unless otherwise specified
PROPOSED: remove the XML Schema Datatypes Dependency section in all documents.
Proposed Erratum 5
No action: it looks like that one had been corrected before REC already...
XML Schema VS presentation syntax mismatch (reported here and here)
- BLD and PRD presentation syntaxes say
Import ::= IRIMETA? 'Import' '(' LOCATOR PROFILE? ')' LOCATOR ::= ANGLEBRACKIRI PROFILE ::= ANGLEBRACKIRI
whereas the XML Schemata say
<xs:element name="Import"> <xs:complexType> <xs:sequence> <xs:group ref="IRIMETA" minOccurs="0" maxOccurs="1"/> <xs:element ref="location"/> <xs:element ref="profile" minOccurs="0" maxOccurs="1"/> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="location" type="xs:anyURI"/> <xs:element name="profile" type="xs:anyURI"/>
- In BLD, the mapping of the rule language must be corrected as well
- PS: there is a note in section 2.3 in BLD that says:
Note that although Base, Prefix, and Import all use symbols of the form <iri> to indicate the connection of these symbols to IRIs, these symbols are not rif:iri constants, as semantically they are interpreted in a way that is quite different from constants.
So, it would be a clarification rather than an erratum properly said.
Proposed Erratum 6
PRD and BLD disagree on use of xml:base (see also the last item in this comment)
- PRD says (section 8.2)
Relative IRIs are allowed in RIF-PRD XML syntax, anywhere IRIs are allowed, including constant types, symbol spaces, location, and profile. The attribute xml:base [XML-Base] is used to make them absolute.
while BLD says (section 2.3)
Like the Base directive, the Prefix directives define shorthands to allow more concise representation of constants that come from the symbol space rif:iri (we will call such constants rif:iri constants).
and (section 4.2)
A Base directive in the presentation syntax becomes an xml:base attribute [XML-Base] in the XML Document tag. The base IRI specified as the value of that attribute applies to content of the RIF/XML element that deals with rif:iri constants, namely to relative-IRI content of the <Const type="&rif;iri"> element.
- DTB is not specific on this, and says only (section 2.2.3)
Relative IRIs in RIF documents are resolved with respect to the base IRI.
- Based on the discussion and resolution taken during the 2 Feb 2010 telecon, the intent seemed to be as specified in PRD:
RESOLVED: We clarify that relative IRIs are allowed in RIF syntaxes (anywhere IRIs are allowed, including Const rif:iri, symbol spaces, location, and profile), and that xml:base is used in making them absolute; the absolute form is seen and used internally, so that's the lexical space.
- So does WG reply to comments say.
Corrected: http://www.w3.org/2005/rules/wiki/index.php?title=BLD&diff=14564&oldid=14558
Proposed Erratum 7
Remove editor's note in Core section 6.2 (reported here)
Corrected+: http://www.w3.org/2005/rules/wiki/index.php?title=Core&diff=14456&oldid=13188
Proposed Errata for RIF-PRD
Proposed Erratum 8
Handling of frame atomic formulas in RIF-PRD (reported here, item #1)
According to Definition of Matching Substitution (sect. 2.2.1) the empty substitution does not match the ground formula s[p1->v1] to { s[p1->v1 p2->v2] } since s[p1->v1] does not belong to { s[p1->v1 p2->v2] }. Is this the intended behaviour? A related problem is when the action is retract( s[p1->v1] ) applied to state { s[p1->v1 p2->v2] }. The result according to the specification is apparently { s[p1->v1 p2->v2] }. Is this the intended behaviour? In summary, is { s[p1->v1 ... pn -> vn] } equivalent to { s[p1->v1], ..., s[pn->vn]} or not?
This not the intended behaviour: { s[p1->v1 ... pn -> vn] } is intended to behave exactly like { s[p1->v1], ..., s[pn->vn]}.
PROPOSED (corrected see here):
- to modify the definition of matching substitution, in section 2.2.1, to read
Definition (Matching substitution). Let ψ be a RIF-PRD condition formula; let σ be a ground substitution such that Var(ψ) ⊆ Dom(σ); and let Φ be a set of ground RIF-PRD atomic formulas.
We say that the ground substitution σ matches ψ to Φ if and only if one of the following is true:
- ψ is an atomic formula and either
- σ(ψ) ∈ Φ, or
- ψ is a frame with multiple slots, o[s_{1}->v_{1}...s_{n}->v_{n}], n > 1, and there is one i, 1≤i≤n, such that σ matches the conjunction And(o[s_{i}->v_{i}] o[s_{1}->v_{1}...s_{i-1}->v_{i-1} s_{i+1}->v_{i+1}...s_{n}->v_{n}] to Φ; or
- ...
- to modify the definition of atomic action in section 3.1.1 to read
Definition (Atomic action). ...
- Assert simple fact: If φ is ... a single slot frame ...
- Retract simple fact: If φ is ... a single slot frame ...
- ...
- to modify the definition of compound action in section 3.1.1 to read
Definition (Compound action). A compound action is a construct that can be replaced equivalently by a pre-defined, and fixed, sequence of atomic actions. In RIF-PRD, a compound action can have three different forms, defined as follows:
- Assert compound fact: If φ is a frame with multiple slots: φ = o[s_{1}->v_{1}...s_{n}->v_{n}], n > 1; then Assert(φ) is a compound action, defined by the sequence Assert(o[s_{1}->v_{1}]) ... Assert(o[s_{n}->v_{n}]). φ is called the target of the action.
- Retract compound fact: If φ is a frame with multiple slots: φ = o[s_{1}->v_{1}...s_{n}->v_{n}], n > 1; then Retract(φ) is a compound action, defined by the sequence Retract(o[s_{1}->v_{1}]) ... Retract(o[s_{n}->v_{n}]). φ is called the target of the action.
- Modify fact: if φ is a frame in the RIF-PRD condition language: φ = o[s_{1}->v_{1}...s_{n}->v_{n}], n > 0; then Modify(φ) is a compound action, defined by the sequence: Retract(o s_{1}) ... Retract(o s_{n}), followed by Assert(φ). φ is called the target of the action. ☐
- to modify the definition of state of the fact base, section 2.2.2, to restrict Φ to contain only single-slot frames
- and to add a note in the definition of frame, section 2.1.2, to say that frames with multiple slots are a shortcut for, and semantically equivalent to conjunctions of single slot frames with the same object.
Proposed Erratum 9
Definition of rule variables in RIF-PRD (section 4.2.3) (reported here, item #2)
The concept of rule variable is never formally defined (the notion of rule variable appears afterwards in Section 7.3 and 8.5.1.3 Forall). My interpretation is the following: for unconditional action blocks, rule variables are empty (i.e. free variables). - for conditional action blocks, rule variables are the free variables. - for rules with variable declarations, the rule variables are the universally quantified variables.
Is this correct? Wouldn't it make more sense to equate rule variables to free variables in all cases? In this way, universally quantified variables would be ignored for comparing instances of two rules, while free variables would be used for that purpose in all cases. This behaviour is probably more coherent and easier to explain to users.
The term "rule variables" is used to denote the variables that are universally quantified in a rule, to differentiate them from the variables that are existentially quantified in rule conditions, and from the action variables.
Equivalently, the rule variables are the free variables in the conditional action block in a rule after steps 2 and 3 of Core-ification.
Proposed modification (corrected see here): Add the following sentence, after the definition of well-formed group, in section 4.1.4:
"The variables that are universally quantified in a rule are sometimes called rule variables in the remainder of this document, to distinguish them from the action variables and from the existentially quantified variables. The function CVar, that maps a rule to the set of its rule variables is defined as follows:
- if r is a conditional or unconditional action block, CVar(r) = ∅
- if r is a rule with variable declaration, Forall ?v_{1}...?v_{n} (r'), CVar(r) = CVar(r') ∪ {?v_{1}...?v_{n}}.
Proposed Erratum 10
Handling of variable name clashes in Core-ification of RIF-PRD rules (reported here, last paragraph in item #2)
A related problem occurs in Section 7.3, where in case 2 of the algorithm clashes of names among rule variables are not taken care.
Name clashes are not taken care of in the RIF-PRD spec, indeed: the assumption was that the variables would be renamed to avoid them, I assume.
Proposed modification: In step 2 of the Core-ification algorithm, section 7.3, change the sentence
"If the rule inside a rule with variable delcaration, r1, is also a rule with variable declaration, r2, all the rule variable delarations and all the patterns that occur in r1 (and not in r2) should be added to the rule variable declarations and the patterns that occur in r2, and, after the transform, r1 should be replaced by r2, in the rule set"
for (taking the opportunity to correct the typos as well)
"If the rule inside a rule with variable declaration, r1, is also a rule with variable declaration, r2, all the rule variable declarations and all the patterns that occur in r1 should be added to the rule variable declarations and the patterns that occur in r2, and, after the transform, r1 should be replaced by r2, in the rule set. If the names of some variables declared in r1 are the same as the names of some variables declared in r2, the former names must be changed prior to the transform."
Corrected (see here)
Proposed Erratum 11
Errors in the PS in the example 9.1 and issues wrt the PS EBNF (reported here)
The proposed corrections are valid (checked 10 July 2012). Here is a shorter valid version:
Document( Prefix( ex1 <http://example.com/2009/prd2> ) (* ex1:CheckoutRuleset *) Group ( (* ex1:GoldRule *) Group ( Forall ?customer such that And(?customer # ex1:Customer ?customer[ex1:status -> "Silver"]) (Forall ?shoppingCart such that ?customer[ex1:shoppingCart -> ?shoppingCart] (If Exists ?value (And(?shoppingCart[ex1:value -> ?value] External(pred:numeric-greater-than-or-equal(?value 2000)))) Then Do(Modify(?customer[ex1:status -> "Gold"]))))) (* ex1:DiscountRule *) Group ( Forall ?customer such that ?customer # ex1:Customer (If Or( ?customer[ex1:status -> "Silver"] ?customer[ex1:status -> "Gold"]) Then Do ((?s ?customer[ex1:shoppingCart -> ?s]) (?v ?s[ex1:value -> ?v]) Modify(?s [ex1:value -> External(func:numeric-multiply (?v 0.95))])))) (* ex1:NewCustomerAndWidgetRule *) Group ( Forall ?customer such that And(?customer # ex1:Customer ?customer[ex1:status -> "New"] ) (If Exists ?shoppingCart ?item (And(?customer[ex1:shoppingCart -> ?shoppingCart] ?shoppingCart[ex1:containsItem -> ?item] ?item # ex1:Widget ) ) Then Do( (?s ?customer[ex1:shoppingCart -> ?s]) (?val ?s[ex1:value -> ?val]) Retract(?customer ex1:voucher) Modify(?s[ex1:value -> External(func:numeric-multiply(?val 0.90))])))) (* ex1:UnknownStatusRule *) Group ( Forall ?customer such that ?customer # ex1:Customer (If Not(Exists ?status (And(?customer[ex1:status -> ?status] External(pred:list-contains(List("New" "Bronze" "Silver" "Gold") ?status)) ))) Then Do( Execute(act:print(External(func:concat("New customer: " ?customer)))) Assert(?customer[ex1:status -> "New"])))) ) )
Corrected (see here)
Proposed Erratum 12
Error in comment in XML Schema for PRD (reported here)
In a comment of RIF PRD XML Schema <xs:group name="RULE"> <!-- RULE ::= (IRIMETA? 'Forall' Var+ '(' CLAUSE ')') | CLAUSE --> should be <xs:group name="RULE"> <!-- RULE ::= (IRIMETA? 'Forall' Var+ (' such that ' FORMULA+)? '(' RULE ')') | CLAUSE -->
Proposed modification: correct the typo.
Corrected (see here)
Proposed Erratum 13
Unbindable action variable in RIF-PRD (reported here)
The RIF-PRD spec does not say what happens with a rule instance where the rule contains an action variable binding (?v ?o[?p->?v]) and there is no substitution for ?v that matches ?o[?p->?v] to the state of facts for the rule instance substitution of ?o and ?p.
PROPOSED (see also discussion here): Add a clarification, after the definition of action instance, in section 4.2.3, to the effect that RIF-PRD does not specify a semantics for that case, because the specification of the context where an otherwise valid RIF-PRD rule is validly applicable is out os the scope of RIF-PRD.
Corrected (see here): Added the following paragraph after the definiiton of action instance in section 4.2.3:
Notice that RIF-PRD does not specify semantics for the case where there is no matching substitution for the binding frame formula o[s->vi] in an action variable declaration (vi o[s->vi]). Indeed, although the rule might be valid from an interchange viewpoint, applying it in a context where object o has no value for attribute s is applying it outside the domain where it is meaningful, and the specification of the context where an otherwise valid RIF-PRD rule is validly applicable is out of the scope of RIF-PRD.
Proposed Erratum 14
Errors in the semantics of Assert and Retract (reported here)
Erratum 14.1
The semantics of the Assert atomic action is described as follows at: Rule 1 says that *all the condition formulas that were satisfied before an assertion will be satisfied after*, and that, in addition, the condition formulas that are satisfied by the asserted ground formula will be satisfied after the assertion. No other condition formula will be satisfied after the execution of the action. where, Rule 1 is formally defined as: α is Assert(φ), where φ is a ground atomic formula, and *w' = w ∪ {φ}*; But an assertion could change the satisfaction of negation formula, right? ie. a negation formula may be satisfied in w but not in w'. (A similar argument follows for Rule 2)
PROPOSED (see also reply here): Modify the text explaining the effect of rule 1 and rule 2 to read:
Corrected (see here)
Rule 1 says that all the atomic condition formulas that were satisfied ..., and that, in addition the atomic condition formula that are satisfied ... No other atomic condition formula will be satisfied after the execution of the action.
Rule 2 says that all the atomic condition formulas that were satisfied ... No other atomic condition formula will be satisfied after the execution of the action.
Erratum 14.2
Furthermore, the formal definition doesn't mention conditional formula while the description (referred above) does. Is something missing there?
PROPOSED (see also here): modify the definition of the RIF-PRD transition relation, in section 3.2 to read:
Corrected (see here)
Definition (RIF-PRD transition relation). The semantics of RIF-PRD atomic actions is specified by the transition relation →_{RIF-PRD} ⊆ W × L × W. (w, α, w') ∈ →_{RIF-PRD} if and only if w ∈ W, w' ∈ W, α is a ground atomic action, and one of the following is true, where Φ is a set of ground atomic formulas that represents w and Φ' is a set of ground atomic formulas that represent w' :
- α is Assert(φ), where φ is a ground atomic formula, and Φ' = Φ ∪ {φ};
- α is Retract(φ), where φ is a ground atomic formula, and Φ' = Φ \ {φ};
- α is Retract(o s), where o and s are constants, and Φ' = (Φ \ {o[s->v] | for all the values of v});
- α is Retract(o), where o is a constant, and Φ' = Φ \ {o[s->v] | for all the values of terms s and v} - {o#c | for all the values of term c};
- α is Execute(φ), where φ is a ground atomic builtin action, and Φ' = Φ. ☐
Proposed Erratum 15
In PRD, a matching substitution for an equality formula is defined wrt the value of ground terms (section 2.2.1). But the value of ground terms is not defined precisely, except for constants in a data types (reported here).
Corrected: see Erratum 16.2, infra.
Proposed Erratum 16
Possibly inconsistent matching substitutions for equality formulas due to incomplete definition in PRD (reported by Jesse Weaver in a private email).
Erratum 16.1
RIF-PRD says (section 2.2.1):
Because RIF-PRD covers only externally defined interpreted functions, a ground functional term can always be replaced by its value. As a consequence, a ground substitution can always be restricted, without loss of generality, to assign only constants to the variable in its domain. In the remainder of this document, it will always be assumed that a ground substitution assigns only constants to the variables in its domain.
But a ground list can be assigned to a variable as well! The purpose of the above sentence is, really, to say that ground external terms can always be replaced by the (non-external) ground term to which they evaluate, and that it will be assumed in the remainder of the document that ground formulas never contain external ground terms (that is, that external ground terms are always replaced by their evaluation in ground formulas). As a consequence, a variable is never assigned an external ground term.
PROPOSED: to replace above paragraph with the following:
Corrected (see here)
Because RIF-PRD covers only externally defined interpreted functions, a ground positional term can always be replaced by the (non-positional) ground term to which it evaluates. As a consequence, a ground RIF-PRD formula can always be restricted, without loss of generality, to contain no positional term; that is, to be such that any ground positional terms have been replaced with the non-positional ground terms to which they evaluate. In the remainder of this document, it will always be assumed that a ground condition formula never contains any positional term. As a consequence, a ground substitution never assigns a ground positional term to the variables in its domain.
Erratum 16.2
a set of facts \Phi representing a state of the fact base may include ground, equality, atomic formulas. In that case, the definition of matching substitution implies: \sigma matches t1=t2 to \Phi iff \sigma(t1) and \sigma(t2) "have the same value" ***OR*** \sigma(t1=t2) \in \Phi. So as things are currently defined, it seems there are two ways to match t1=t2 to \Phi. One is for the two sides to be mapped to the same value, and the other is to match a fact.
Correct. The problem is that the current definition of a state of the fact base (section 2.2.2) allows the two ways to match an equality to disagree (e.g. if the state of the fact base contains the atomic equality "1^^xs:integer=2^^xs:integer").
PROPOSED: change the definition of state of the fact base, section 2.2.2, to read:
Corrected (see here)
Definition (State of the fact base). A state of the fact base, w_{Φ}, is associated to every set of ground atomic formulas, Φ, that contains no frame with multiple slots and that satisfies all the following conditions:
- for every equality formula t_{1}=t_{2} in Φ, if t_{1} and t_{2} are, both, constants in symbol spaces that are data types, then they have the same value;
- for all triple of constants c_{1}, c_{2}, c_{3}...
And clarify the definition of matching substitution in section 2.2.1 to read:
Corrected (see here)
...
- ψ is an atomic formula and either
- σ(ψ) ∈ Φ, or
- ...
- ψ is an equality formula, t_{1} = t_{2}, and the ground terms σ(t_{1}) and σ(t_{2}) are constants in symbol spaces that are data types and they have the same value;
- ...
Erratum 16.3
Jesse Weaver noticed that, while the above modifications corrected previously raised issues, it did not guaranty symmetry and transitivity of equality, see here (neither reflexivity, by the way).
PROPOSED: Adding the following constraints to the definition of state of the fact base, section 2.2.2:
- for every pair of constants c_{1} and c_{2}, if c_{1} = c_{2} ∈ Φ, then c_{2} = c_{1} ∈ Φ;
- for every triple of constants c_{1}, c_{2} and c_{3}, if c_{1} = c_{2} ∈ Φ and c_{2} = c_{3} ∈ Φ, then c_{1} = c_{3} ∈ Φ;"
and add the following condition in the definition of matching substitution in section 2.2.1, under "ψ is an equality formula, t_{1} = t_{2} and either...":
- or the ground terms σ(t_{1}) and σ(t_{2}) are the same ground term;
Erratum 16.4
While correcting erratum 16.1 and 16.2, I (csma) realized that, as they were defined, matching substitutions did not handle list equality.
PROPOSED: Modify the definition of matching substitution in section 2.2.1 to read:
corrected (here)
- ψ is an atomic formula and either
- σ(ψ) ∈ Φ, or
- ...
- ψ is an equality formula, t_{1} = t_{2}, and either
- the ground terms σ(t_{1}) and σ(t_{2}) are list terms with the same length n≥0 and, for all i, 0≤i≤n-1, such that l_{1i} and l_{2i} are the ground terms of rank i in σ(t_{1}) and σ(t_{2}), respectively, either l_{1i} and l_{2i} are both constants in symbol spaces that are data types and they have the same value, or l_{1i} = l_{2i} ∈ Φ,
- or the ground terms σ(t_{1}) and σ(t_{2}) are constants in symbol spaces that are data types and they have the same value;
- ...
Erratum 16.5
Jesse Weaver noticed that erratum 16.4 introduced the counter-intuitive possibility to equate a constant in a data type and a list, e.g. to a fact base may validly contain fact "3=List()" (see here)
PROPOSED: add the following constraint in the definition of state of the fact base, section 2.2.2:
- for every equality formula c_{1} = c_{2} ∈ Φ, either c_{1} is not a constant in a symbol space that is a data type, of c_{2} is not a list term;.
Proposed Erratum 17
Propagation of membership through class hierarchy when asserting class membership (reported by Jesse Weaver, see reply here).
Consider a set of facts \Phi = {c_2##c_1} which represents a state of a fact base. Consider the following rule: Do( (?y New()]) Assert(?y#c_2) ) ) By definition of RIF-PRD transition relation (section 3.2), assuming that the new frame object is identified as _new, the next state of the fact base is represented by \Phi* = \Phi \cup {_new#c_2}, which is \Phi* = { _new#c_2, c_2##c_1 } . However, since _new#c_2 \in \Phi and c_2##c_1 \in \Phi and _new#c_1 \notin \Phi, then by definition of state of the fact base (section 2.2.2), \Phi* cannot represent a state of the fact base.
PROPOSED: move the constraint that all members of a subclass must also be members of all the super classes from the definition of a state of the fact base to the definition of a matching substitution, that is
Corrected (see here)
- remove from the definition of state of the fact base the condition that for all triple of constants c_{1}, c_{2}, c_{3}, if c_{1}#c_{2} ∈ Φ and c_{2}##c_{3} ∈ Φ, then c_{1}#c_{3} ∈ Φ
- modify the definition of matching substitution (section 2.2.1) to say
...
- ψ is an atomic formula and either
- σ(ψ) ∈ Φ, or
- ψ is a membership formula o # c, and there is a ground term c' such that σ matches the conjunction And(o#c' c'##c) to Φ, or
- ...
Proposed Erratum 18
Action variable binding to a (ground) list (report by Jesse Weaver, see here, last comment).
the definition of action instance requires that d be a constant, which seems overly restrictive. What if a[p->List()] \in \Phi, which is allowed by definition of frame atomic formula (section 2.1.2) and definition of term (section 2.1.1).)
PROPOSED: change the second bullet in the definition of action instance (section 4.2.3) to read:
Corrected (see here)
- if vi is assigned the value of a frame's slot by the action variable declaration: (vi o[s->vi]), then σ(vi) is a ground term such that the substitution σ matches the frame formula o[s->vi] to w.
Proposed Erratum 19
In PRD, section 8.6.1 seems to restrict the use of the RIF/XML element Import to importing RDF or OWL, and to exclude the import of RIF PRD documents, as described in section 5.
PROPOSED: Modify the first sentence in section 8.6.1 to read:
Corrected (see here)
The Import directive is used to serialize the reference to an RDF graph, an OWL ontology or another RIF document to be combined with a RIF document. The Import directive is inherited from [RIF-Core]. The abstract syntax and semantics of RDF graph and OWL ontology imports are specified in [RIF-RDF-OWL].
Typos, simplifications, clarifications
- Various typos corrected (see here)
- Remove the confusing and unnecessary condition that "there is at least one term, v, such that o[s->v] is a well-formed frame atomic formula", in the definition of a well-formed Retract with two arguments (see correction here)
Proposed Erratum 20
In SWC, section 9 Appendix: Embeddings it is stated that "Simple, RDF, and RDFS entailment for RIF-RDF combinations are embedded in RIF Core", therefore the above restriction holds. This seems to be contradictory to "Forall ?x ?y (?x # ?y :- ?x[rdf:type -> ?y])" in SWC section 9.1.3 Embedding simple entailment (reported here).
PROPOSED (Dave Reynolds): Change the second paragraph of section 9 from:
Simple, RDF, and RDFS entailment for RIF-RDF combinations are embedded in RIF Core. RIF-OWL 2 RL combinations require reasoning with equality, and thus could not be embedded in RIF Core; they are embedded in RIF BLD.
to
Simple, RDF, RDFS and OWL 2 RL entailment for RIF-RDF combinations are embedded in RIF BLD. Note that Simple, RDF and RDFS entailments are superficially embeddable within RIF Core. However, condition 7 of the semantics of RIF-RDF combinations cannot be axiomatized in RIF Core due to restrictions on the use isa (#) in rule heads. OWL 2 RL is not embeddable in RIF Core due the the need for equality reasoning.
Corrected (see here)
Proposed Erratum 21
- In RIF-BLD: Definitions in Section Interpretation of Documents have been rewritten and significantly simplified.
- In SectionThe Semantics of RIF-BLD as a Specialization of RIF-FLD, a paragraph added about specialization from RIF-FLD semantic multi-structures.
corrected
Proposed Errata for RIF-FLD
- Added anti-monotonicity requirement for ~ in Definition (set of truth values).
- Changed Definition (truth valuation of document formulas) to define truth valuation of not only document formulas but other formulas as well.
- Acknowledgements added.
- The old notion of semantic multi-structures has been changed to fix the problems with the semantics of document formulas found in Recommendation of June 22 2010. These problems were pointed out in [DAA]. As a result, sections Interpretation of Documents and Logical Entailment have largely been rewritten.
Corrected: http://www.w3.org/2005/rules/wiki/index.php?title=FLD&diff=14451&oldid=14355
Proposed Errata in DTB
(Proposed by Axel, who commented: "Summarizing, I do understand that only 1)+5) are mandatory changes, whereas the changes 2)- 4) are not necessarily mandatory, but would make the RIF-DTB spec cleaner.")
Any remaining issues would in my opinion depend on whether the Xpath working group sees any effects on [XPath-Functions], since we don't have any other direct dependencies on [XML Schema Datatypes], but only indirectly by reuse of definitions from [XPath-Functions].
1. http://www.w3.org/TR/rif-dtb/
1)
Firstly, a couple of references need to be fixed to the latest specs.
[XML Schema Datatypes] --> http://www.w3.org/TR/xmlschema11-2/ (now points to the CR from 30 April 2009)
Done: changed the template (see here)
Further, [XDM] + [XPath] [XPath-Functions]
all point to the first edition recs and should probably be updated to the Dec 2010 Second Edition versions.
2)
In fact, it seems that the reference to [XDM] could be removed, since we only needed it because the two subtypes of duration we are referring to didn't appear in the earlier version of [XML Schema Datatypes].
As far as I know, the main question was whether the latest changes in [XML Schema Datatypes] do affect us, as shown in http://www.w3.org/2001/sw/CG/docs/XSD1.1-diffs.html,
as the other docs only had minor updates, I assume.
3) Section 2.2.1 Symbol Spaces
The lexical spaces of the above symbol spaces are defined in the document [XML Schema Datatypes].
.xs:dayTimeDuration (http://www.w3.org/2001/XMLSchema#dayTimeDuration), short name: dayTimeDuration .xs:yearMonthDuration (http://www.w3.org/2001/XMLSchema#yearMonthDuration), short name: yearMonthDuration
These two symbol spaces represent two subtypes of the XML Schema datatype xs:duration. The lexical spaces of the above symbol spaces are defined in the document [XDM].
Although this is not wrong, the lexical spaces for these two datatypes are now defined in the last iteration of [XML Schema Datatypes], so this *could* be changed to simply
.xs:dayTimeDuration (http://www.w3.org/2001/XMLSchema#dayTimeDuration), short name: dayTimeDuration .xs:yearMonthDuration (http://www.w3.org/2001/XMLSchema#yearMonthDuration), short name: yearMonthDuration
The lexical spaces of the above symbol spaces are defined in the document [XML Schema Datatypes].
Done (see here)
4) Section 2.3
Similarly, the following could be changed/simplified, if we refer to the leatest [XML Schema Datatypes] version:
Their value spaces and the lexical-to-value-space mappings are defined as follows:
.For the XML Schema datatypes of RIF, namely all RIF datatypes within the xs: namespace, except xs:dayTimeDuration and xs:yearMonthDuration, the value spaces and the lexical-to-value-space mappings are defined in the XML Schema specification [XML Schema Datatypes]. .The value spaces and the lexical-to-value-space mappings for the datatypes xs:dayTimeDuration and xs:yearMonthDuration are defined in the XQuery 1.0 and XPath 2.0 Data Model [XDM].
to
Their value spaces and the lexical-to-value-space mappings are defined as follows:
.For the XML Schema datatypes of RIF, namely all RIF datatypes within the xs: namespace, the value spaces and the lexical-to-value-space mappings are defined in the XML Schema specification [XML Schema Datatypes].
Done (see here)
5) Section 2.3.1 XML Schema Datatypes
Although - again - it is not wrong, this section could be removed, I suppose.
Done (see here)
Proposed Errata in OWL2/RL
Fixed typos and syntactic errors in the Template Rules algorithm of appendix 8 identified by Henrick Marx, reported (here and here). Rules affected: prp-adp, cax-adc, prp-spo2, prp-key, scm-int, cls-maxqc2, eq-diff2 and eq-diff3.
More To Investigate
- http://lists.w3.org/Archives/Public/public-rif-comments/2010Aug/0000.html (Not an error: Fitting's paper [1] is listed in the informative references but never cited in the spec => no erratum?
- http://lists.w3.org/Archives/Public/public-rif-comments/2011Mar/0001.html (Not an error: request for explanation => no erratum? Or should the spec be clarified?)