--- a/dictionary/prov-dictionary.html Wed Jan 23 13:05:17 2013 -0700
+++ b/dictionary/prov-dictionary.html Thu Jan 24 12:07:47 2013 +0100
@@ -485,6 +485,7 @@
+
.remark {
padding: 1em;
margin: 1em 0em 0em;
@@ -805,7 +806,7 @@
<ul>
<li> <span class="name">prov:Dictionary</span> is a subtype of <span class="name">prov:Collection</span>. It denotes an entity of type dictionary, i.e. an entity that can participate in relations amongst dictionaries;</li>
- <li><span class="name">prov:EmptyDictionary</span> is a subtype of <span class="name">prov:EmptyCollection</span>. It denotes an empty dictionary.</li>
+ <li><span class="name">prov:EmptyDictionary</span> is a subtype of both <span class="name">prov:EmptyCollection</span> and <span class="name">prov:Dictionary</span>. It denotes an empty dictionary.</li>
</ul>
@@ -1162,7 +1163,7 @@
<section id="dictionary-ontological-definition">
<h2>Ontological Definition of Dictionary</h2>
-<p>In this section, the ontological definition of <code>prov:Dictionary</code> is given, in order to extend [[PROV-O]] with dictionaries.</p>
+<p>In this section, the ontological definition of <code>prov:Dictionary</code> is given, in order to extend [[PROV-O]] with dictionaries. For more information on the terminology, syntax and conventions used in this section, we refer to [[PROV-O]]</p>
<p> A <code><a class="qname"
href='#Dictionary'>prov:Dictionary</a></code> is a <code
class="repeated">prov:Entity</code> that acts as a container to some members,
@@ -2667,14 +2668,16 @@
<section id="dictionary-constraints-inferences">
<h3>Inferences</h3>
<p id="dmembership-cmembership-inference_text"><a href="#term-dictionary-membership">Dictionary membership</a> implies <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/#term-membership">collection membership</a>.</p>
- <div class='inference' id='membership-membership-inference'>
+ <div class='inference' id='dmembership-cmembership-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#dmembership-cmembership-inference">Inference 1 (dictionary-membership-collection-membership)</a></span>
<p>
<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d, e1, "k1")</span>
<span class='conditional'>THEN</span> <span class="name">hadMember(d, e1)</span>
</p></div>
<p id="membership-membership-inference_text">Each key maps to a single entity.</p>
- <div class='inference' id='membership-membership-inference'>
+ <div class='inference' id='key-single-entity-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#key-single-entity-inference">Inference 2 (key-single-entity)</a></span>
<p>
<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d1, e1, "k1")</span>
and <span class="name">hadDictionaryMember(d1, e2, "k1")</span>
@@ -2683,57 +2686,72 @@
<p id="membership-insertion-membership-inference_text">If a dictionary was derived from another dictionary by an insertion, then the former holds all key-entity pairs of the latter, except those updated by the insertion.</p>
<div class='inference' id='membership-insertion-membership-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#membership-insertion-membership-inference">Inference 3 (membership-insertion-membership)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d1, e1, "k1")</span>
- and <span class="name">derivedByInsertionFrom(d2, d1, {("k2", _e2)})</span> and <span class="name">k1</span> ≠ <span class="name">k2</span>
- <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d2, e1, "k1")</span>
+<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d1, e, "k")</span>
+ and <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1),...,("kn", en)})</span> and <span class="name">k</span> ∉ <span class="name">{k1,...,kn}</span>
+ <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d2, e, "k")</span>
</p></div>
-<p id="membership-update-membership-inference_text">Insertion provides an "update semantics" for the keys that are already present in a dictionary. A new pair replaces an existing pair with the same key in the new dictionary. </p>
+<!--REMOVED CONSTRAINT <p id="membership-update-membership-inference_text">Insertion provides an "update semantics" for the keys that are already present in a dictionary. A new pair replaces an existing pair with the same key in the new dictionary. </p>
<div class='inference' id='membership-update-membership-inference'>
<p>
<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d1, e1, "k1")</span>
and <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e2)})</span>
<span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d2, e2, "k1"))</span>
</p></div>
-
-<p id="insertion-membership-inference_text">A dictionary that was derived by an insertion of key-entity pairs, holds all these specified key-entity pairs.</p>
+/REMOVED CONSTRAINT-->
+
+<p id="insertion-membership-inference_text">A dictionary that was derived by an insertion of key-entity pairs, holds all these specified key-entity pairs. This inference also means that Insertion provides an "update semantics" for the keys that are already present in a dictionary.</p>
<div class='inference' id='insertion-membership-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-membership-inference">Inference 4 (insertion-membership)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1)})</span>
- <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d2, e1, "k1")</span>
+<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1),...,("kn",en)})</span>
+ <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d2, ei, "ki") for each i ∈ [1..n]</span>
</p></div>
-<p id="removal-membership-inference_text">Only keys that actually mapped to an entity in a dictionary can be removed from it.</p>
+<!--REMOVED CONSTRAINT <p id="removal-membership-inference_text">Only keys that actually mapped to an entity in a dictionary can be removed from it.</p>
<div class='inference' id='removal-membership-inference'>
<p>
<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1"})</span>
<span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d1, e1, "k1")</span>
</p></div>
<div class="remark"><b>Note from the editors:</b> this constraint seems too restrictive for some implementations, and the editors would like to remove it, unless there is strong consensus to keep it. Removal of this constraint would also allow for duplicate dictionaries to be derived by "removal" of a non-existing key.</div>
+/REMOVED CONSTRAINT-->
<p id="insertion-derivation-inference_text">Insertion and removal are special cases of derivation.</p>
<div class='inference' id='insertion-derivation-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-derivation-inference">Inference 5 (insertion-derivation)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {_("k1", e1)})</span>
+<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1),...,("kn",en)})</span>
<span class='conditional'>THEN</span> <span class="name">wasDerivedFrom(d2, d1)</span>
</p></div>
<div class='inference' id='removal-derivation-inference'>
+ <span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference 6 (removal-derivation)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {_"k1"})</span>
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1",...,"kn"})</span>
<span class='conditional'>THEN</span> <span class="name">wasDerivedFrom(d2, d1)</span>
</p></div>
<p id="insertion-removal-membership-inference_text">Insertions and removals do not introduce any new key-entity pairs, other than those specified.</p>
<div class='inference' id='insertion-removal-membership-inference'>
-<p>
-<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", _e1)})</span> and <span class="name">derivedByRemovalFrom(d3, d2, {"k1"})</span>
- <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d1, e2, "k2")</span> holds <span
- class='conditional'>IF AND ONLY IF</span> <span class="name">hadDictionaryMember(d3, e2, "k2")</span>
-</p></div>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-removal-membership-inference">Inference 7 (insertion-removal-membership)</a></span>
+<ol>
+ <li>
+ <span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", _e1)})</span> and
+ <span class="name">derivedByRemovalFrom(d3, d2, {"k1"})</span> and <span class="name">hadDictionaryMember(d1, e2, "k2")</span> and
+ <span class="name">k1 ≠ k2</span> <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d3, e2, "k2")</span>
+ </li>
+ <li>
+ <span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", _e1)})</span> and
+ <span class="name">derivedByRemovalFrom(d3, d2, {"k1"})</span> and <span class="name">hadDictionaryMember(d3, e2, "k2")</span> and
+ <span class="name">k1 ≠ k2</span> <span class='conditional'>THEN</span> <span class="name">hadDictionaryMember(d1, e2, "k2")</span>
+ </li>
+</ol>
+</div>
<div class="remark">
- Note that this inference, together with the constraints that specify that a dictionary cannot be derived by multiple insertions or removals, and that an EmptyDictionary does not contain any key-entity pairs, guarantees <b>completeness</b> of a dictionary, if it can be traced back to an EmptyDictionary through insertions and removals.
+ Note that this inference, together with constraints <a class="internalDFN" href="#impossible-removal-insertion-constraint">9</a>, <a class="internalDFN" href="#impossible-insertion-insertion-constraint">10</a> and <a class="internalDFN" href="#impossible-removal-removal-constraint">11</a>, and the fact that an EmptyDictionary does not contain any key-entity pairs, guarantees <b>completeness</b> of a dictionary, if it can be traced back to an EmptyDictionary through insertions and removals.
Here, completeness means that all key-entity pairs of the dictionary are known through a hadDictionaryMember statement.
</div>
@@ -2744,46 +2762,53 @@
<h3>Constraints</h3>
<p id="impossible-removal-membership_text">A dictionary that was derived by removal from another dictionary, cannot contain the key-entity pairs that were removed from the latter.</p>
- <div class='constraint' id='impossible-removal-membership'>
+ <div class='constraint' id='impossible-removal-membership-constraint'>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-membership-constraint">Constraint 8 (impossible-removal-membership)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1"})</span> and
- <span class="name">hadDictionaryMember(d2, e1, "k1")</span><span class='conditional'>THEN</span> <span
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1",...,"kn"})</span> and
+ <span class="name">hadDictionaryMember(d2, e, "ki")</span> and <span class="name">i ∈ [1..n]</span> <span class='conditional'>THEN</span> <span
class="conditional">INVALID</span>
</p></div>
<p id="impossible-removal-insertion_text">A dictionary must not be derived through multiple insertion or removal relations.</p>
- <div class='constraint' id='impossible-removal-insertion'>
+ <div class='constraint' id='impossible-removal-insertion-constraint'>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-insertion-constraint">Constraint 9 (impossible-removal-insertion)</a></span>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {_"k1"})</span> and
- <span class="name">derivedByInsertionFrom(d2, d1, {_("k2", e2)})</span><span class='conditional'>THEN</span> <span
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1",...,"kn"})</span> and
+ <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1),...,("km",em)})</span><span class='conditional'>THEN</span> <span
class="conditional">INVALID</span>
</p></div>
-<div class='constraint' id='impossible-insertion-insertion'>
+<div class='constraint' id='impossible-insertion-insertion-constraint'>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-insertion-insertion-constraint">Constraint 10 (impossible-insertion-insertion)</a></span>
+<p>Here, <span class="name">KV1</span> and <span class="name">KV2</span> are sets of key-entity pairs.</o>
<p>
-<span class="conditional">IF</span> <span class="name">IF derivedByInsertionFrom(d2, d1, {_("k1", e1)})</span> and
- <span class="name">derivedByInsertionFrom(d2, d1, {_("k2", e2)})</span><span class='conditional'>THEN</span> <span
- class="conditional">INVALID</span>
+<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, KV1)</span> and
+ <span class="name">derivedByInsertionFrom(d2, d1, KV2)</span><span class='conditional'>THEN</span> <span
+ class="name">KV1 = KV2</span>
</p></div>
-<div class='constraint' id='impossible-removal-removal'>
+<div class='constraint' id='impossible-removal-removal-constraint'>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-removal-constraint">Constraint 11 (impossible-removal-removal)</a></span>
+<p>Here, <span class="name">K1</span> and <span class="name">K2</span> are sets of keys.</p>
<p>
-<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {_"k1"})</span> and
- <span class="name">derivedByRemovalFrom(d2, d1, {_"k2"})</span><span class='conditional'>THEN</span> <span
- class="conditional">INVALID</span>
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, K1)</span> and
+ <span class="name">derivedByRemovalFrom(d2, d1, K2)</span><span class='conditional'>THEN</span> <span
+ class="name">K1 = K2</span>
</p></div>
-<p id="impossible-removal-insertion_text">An empty dictionary cannot hold any key-entity pairs.</p>
+<!--REMOVED CONSTRAINT <p id="impossible-removal-insertion_text">An empty dictionary cannot hold any key-entity pairs.</p>
<div class='constraint' id='impossible-removal-insertion'>
<p>
<span class="conditional">IF</span> <span class="name">hadDictionaryMember(d, e1, "k1")</span> and
<span class="name">'prov:EmptyDictionary' ∈ typeOf(d)</span><span class='conditional'>THEN</span> <span
class="conditional">INVALID</span>
-</p></div>
+</p></div> /REMOVED CONSTRAINT-->
</section> <!-- end constraints -->
<section id="dictionary-typing">
<h3>Typing</h3>
<div class='constraint' id='typing'>
+ <span class='ruleTitle'><a class="internalDFN" href="#typing">Constraint 12 (typing)</a></span>
<ol>
<li>
<p>