--- a/dictionary/prov-dictionary.html Tue Jan 29 15:07:22 2013 +0100
+++ b/dictionary/prov-dictionary.html Tue Jan 29 15:15:59 2013 +0100
@@ -827,7 +827,7 @@
<span class="glossary-ref" data-ref="glossary-dictionary-membership"></span>
<p>Similar to the <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/#term-membership">collection membership</a> relation, the <strong>dictionary membership</strong> allows stating the members of a Dictionary. However, it provides additional structure.
- Note that <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>, but not vice versa. This implication is formalized in <a href="#dmembership-cmembership-inference">Inference 1</a>.
+ Note that <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>, but not vice versa. This implication is formalized in <a href="#dmembership-cmembership-inference">Inference D1</a>.
</p>
<div class="attributes" id="attributes-hadMember-d">
@@ -875,7 +875,7 @@
<li><span class='attribute' id="insertion.after">after</span>: an identifier (<span class="name">d2</span>) for the dictionary <em>after</em> insertion; </li>
<li><span class='attribute' id="insertion.before">before</span>: an identifier (<span class="name">d1</span>) for the dictionary <em>before</em> insertion;</li>
<li><span class='attribute' id="insertion.key-entity-set">key-entity-set</span>: all inserted key-entity pairs <span class="name">(key_1, e_1)</span>, ..., <span class="name">(key_n, e_n)</span>. Here, each <span class="name">key_i</span> is a <a href="http://www.w3.org/TR/2012/CR-prov-dm-20121211/#term-value">value</a>, and <span class="name">e_i</span> is an identifier for the entity that has been inserted with the key;
- each <span class="name">key_i</span> is expected to be unique for the key-entity-set, as formalized in <a href="#key-single-entity-inference">Inference 2</a>;
+ each <span class="name">key_i</span> is expected to be unique for the key-entity-set, as formalized in <a href="#key-single-entity-inference">Inference D2</a>;
</li>
<li><span class='attribute' id="insertion.attributes">attributes</span>: an OPTIONAL set (<span class="name">attrs</span>) of attribute-value pairs representing additional information about this relation.</li>
</ul>
@@ -884,7 +884,7 @@
<p>
An Insertion relation <span class="name">derivedByInsertionFrom(id; d2, d1, {(key_1, e_1), ..., (key_n, e_n)})</span> states that <span class="name">d2</span> is the dictionary
following the insertion of pairs <span class="name">(key_1, e_1)</span>, ..., <span class="name">(key_n, e_n)</span> into dictionary <span class="name">d1</span>.
-Note that insertion is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary after an insertion. This is formalized in <a href="#insertion-removal-membership-inference">Inference 7</a>.</p>
+Note that insertion is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary after an insertion. This is formalized in <a href="#insertion-removal-membership-inference">Inference D7</a>.</p>
@@ -952,7 +952,7 @@
</div>
<p>A Removal relation <span class="name">derivedByRemovalFrom(id; d2,d1, {key_1, ..., key_n})</span> states that <span class="name">d2</span> is the dictionary following the removal of the set of pairs corresponding to keys <span class="name">key_1...key_n</span> from <span class="name">d1</span>. If a key that is not present in the dictionary is removed, the dictionary remains unchanged.
- Note that removal is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary after a removal. This is formalized in <a href="#insertion-removal-membership-inference">Inference 7</a>.
+ Note that removal is considered to be complete. This means that we assume that no unknown keys were inserted in or removed from a dictionary after a removal. This is formalized in <a href="#insertion-removal-membership-inference">Inference D7</a>.
</p>
<div class="anexample">
@@ -1310,7 +1310,7 @@
the keys <code>"k1"</code> and <code>"k2"</code> from the dictionary
<code>:d2</code>. Thus, <code>:d3</code> does not contain the
members <code>("k1", :e1)</code> and <code>("k2",
- :e2(</code> from <code>:d2</code>.
+ :e2)</code> from <code>:d2</code>.
</p>
<div about="#narrative-example-dictionaries-3" typeof="prov:Entity" class="exampleOuter" xmlns:prov="http://www.w3.org/ns/prov#">
@@ -2689,7 +2689,7 @@
<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='dmembership-cmembership-inference'>
- <span class='ruleTitle'><a class="internalDFN" href="#dmembership-cmembership-inference">Inference 1 (dictionary-membership-collection-membership)</a></span>
+ <span class='ruleTitle'><a class="internalDFN" href="#dmembership-cmembership-inference">Inference D1 (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>
@@ -2697,7 +2697,7 @@
<p id="membership-membership-inference_text">Each key maps to a single entity.</p>
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#key-single-entity-inference">Inference D2 (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>
@@ -2706,7 +2706,7 @@
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#membership-insertion-membership-inference">Inference D3 (membership-insertion-membership)</a></span>
<p>
<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>
@@ -2723,7 +2723,7 @@
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-membership-inference">Inference D4 (insertion-membership)</a></span>
<p>
<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>
@@ -2741,13 +2741,13 @@
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-derivation-inference">Inference D5 (insertion-derivation)</a></span>
<p>
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference D6 (removal-derivation)</a></span>
<p>
<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>
@@ -2756,7 +2756,7 @@
<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'>
- <span class='ruleTitle'><a class="internalDFN" href="#insertion-removal-membership-inference">Inference 7 (insertion-removal-membership)</a></span>
+ <span class='ruleTitle'><a class="internalDFN" href="#insertion-removal-membership-inference">Inference D7 (insertion-removal-membership)</a></span>
<ol>
<li>
<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", _e1)})</span> and
@@ -2771,7 +2771,7 @@
</ol>
</div>
<div class="remark">
- 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.
+ Note that this inference, together with constraints <a class="internalDFN" href="#impossible-removal-insertion-constraint">D9</a>, <a class="internalDFN" href="#impossible-insertion-insertion-constraint">D10</a> and <a class="internalDFN" href="#impossible-removal-removal-constraint">D11</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>
@@ -2783,7 +2783,7 @@
<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-constraint'>
- <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-membership-constraint">Constraint 8 (impossible-removal-membership)</a></span>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-membership-constraint">Constraint D8 (impossible-removal-membership)</a></span>
<p>
<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
@@ -2792,7 +2792,7 @@
<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-constraint'>
- <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-insertion-constraint">Constraint 9 (impossible-removal-insertion)</a></span>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-insertion-constraint">Constraint D9 (impossible-removal-insertion)</a></span>
<p>Here, <span class="name">KV1</span> and <span class="name">KV2</span> are sets of key-entity pairs.</p>
<p>
<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, KV1)</span> and
@@ -2800,7 +2800,7 @@
class="conditional">INVALID</span>
</p></div>
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-insertion-insertion-constraint">Constraint D10 (impossible-insertion-insertion)</a></span>
<p>Here, <span class="name">KV1</span> and <span class="name">KV2</span> are sets of key-entity pairs.</p>
<p>
<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, KV1)</span> and
@@ -2808,7 +2808,7 @@
class="name">KV1 = KV2</span>
</p></div>
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-removal-constraint">Constraint D11 (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
@@ -2829,7 +2829,7 @@
<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>
+ <span class='ruleTitle'><a class="internalDFN" href="#typing">Constraint D12 (typing)</a></span>
<ol>
<li>
<p>
@@ -2854,14 +2854,17 @@
</p>
</li>
<li>
+
+ <p>Here, KV is a set of key-entity pairs</p>
<p>
- <span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1)})</span> <span class='conditional'>THEN</span>
+ <span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, KV)</span> <span class='conditional'>THEN</span>
<span class="name">'prov:Dictionary' ∈ typeOf(d1)</span> and <span class="name">'prov:Dictionary' ∈ typeOf(d2)</span> and <span class="name">'prov:Collection' ∈ typeOf(d1)</span> and <span class="name">'entity' ∈ typeOf(d1)</span> and <span class="name">'prov:Collection' ∈ typeOf(d2)</span> and <span class="name">'entity' ∈ typeOf(d2)</span> and <span class="name">'entity' ∈ typeOf(e1)</span>
</p>
</li>
<li>
+ <p>Here, K is a set of keys</p>
<p>
- <span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1"})</span> <span class='conditional'>THEN</span>
+ <span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, K)</span> <span class='conditional'>THEN</span>
<span class="name">'prov:Dictionary' ∈ typeOf(d1)</span> and <span class="name">'prov:Dictionary' ∈ typeOf(d2)</span> and <span class="name">'prov:Collection' ∈ typeOf(d1)</span> and <span class="name">'entity' ∈ typeOf(d1)</span> and <span class="name">'prov:Collection' ∈ typeOf(d2)</span> and <span class="name">'entity' ∈ typeOf(d2)</span>
</p>
</li>