hadMember updated and constraints added for PROV-DICTIONARY
authorTom De Nies <tom.denies@ugent.be>
Mon, 17 Dec 2012 11:56:57 +0100
changeset 5366 633adf09dc0f
parent 5364 7a06dfcb38ed
child 5367 996f0d82117e
hadMember updated and constraints added for PROV-DICTIONARY
dictionary/prov-dictionary.html
--- a/dictionary/prov-dictionary.html	Mon Dec 17 10:55:04 2012 +0000
+++ b/dictionary/prov-dictionary.html	Mon Dec 17 11:56:57 2012 +0100
@@ -825,45 +825,30 @@
 <p>The <strong>dictionary  membership</strong> has the same purpose as the <a href="#term-collection-membership">collection membership</a> relation, but it applies to entities having <span class="name">prov:type = 'prov:Dictionary'</span>. It allows stating the members of a Dictionary.</p>
 
 <div class="attributes" id="attributes-hadMember-d">
- A <dfn title="hadMember-d">membership</dfn> relation, written <span class="pnExpression">hadMember(id; c, {(key_1, e_1), ..., (key_n, e_n)}, cplt, attrs)</span>, has:
-<ul>
-<li><span class='attribute' id="membership-d.id">id</span>:  an OPTIONAL identifier identifying the relation;</li>
-<li><span class='attribute' id="membership-d.dictionary">dictionary</span>: an identifier (<span class="name">c</span>) for the dictionary whose members are asserted; </li>
-<li><span class='attribute' id="membership-d.key-entity-set">key-entity-set</span>: a set of key-entity pairs <span class="name">(key_1, e_1)</span>, ..., <span class="name">(key_n, e_n)</span> that are members of the dictionary;</li>
-<li><span class='attribute' id="membership-d.complete">complete</span>: an OPTIONAL boolean <a title="value">Value</a> (<span class="name">cplt</span>). It is interpreted as follows:
+ A <dfn title="hadMember-d">membership</dfn> relation, written <span class="pnExpression">hadMember(d, (key_1, e_1))</span>, has:
 <ul>
-<li>if it is present and set to true, then c is believed to include all and only the members specified in the key-entity-set;</li>
-<li>if it is present and set to false, then c is believed to include more members in addition to those specified in the key-entity-set;</li>
-<li>if it is not present, then c is believed to include all the members specified in the key-entity-set, and it MAY include more.</li>
-</ul>
-</li>
-<!-- if true, it indicates that no other member belongs to the dictionary;  if false, it indicates that other members belong to the dictionary; if unspecified, other members MAY belong to the dictionary; -->
-<li><span class='attribute' id="membership-d.attributes">attributes</span>: an OPTIONAL set (<span class="name">attrs</span>) of attribute-value pairs representing additional information about this relation.</li>
+<li><span class='attribute' id="membership-d.dictionary">dictionary</span>: an identifier (<span class="name">d</span>) for the dictionary whose members are asserted; </li>
+<li><span class='attribute' id="membership-d.key-entity-set">key-entity-pair</span>: a key-entity pair <span class="name">(key_1, e_1)</span> that is a member of the dictionary;</li>
 </ul>
 
 </div>
 
-<p id="complete-attribute-note-d">
-The attribute <a href="#membership-d.complete">complete</a> is interpreted as for  the general <a href="#term-collection">collection membership</a> relation. 
-</p>
 <div class="anexample">
 <pre class="codeexample">
-entity(d1, [prov:type='prov:Dictionary' ])    // d1 is a dictionary, with unknown content
-entity(d2, [prov:type='prov:Dictionary' ])    // d2 is a dictionary, with unknown content
+entity(d, [prov:type='prov:Dictionary' ])    // d1 is a dictionary, with unknown content
 
 entity(e1)
 entity(e2)
 
-hadMember(d1, {("k1", e1), ("k2", e2)} )  
-hadMember(d2, {("k1", e1), ("k2", e2)}, true)  
+hadMember(d, ("k1", e1))  
+hadMember(d, ("k2", e2))  
 
 </pre>
 From these descriptions, we conclude:
 <ul>
-<li> <span class="name">d1</span>  has  the following pairs as members: <span class="name">("k1", e1), ("k2", e2)</span>, and may contain others.</li>
-<li> <span class="name">d2</span>  exactly has  the following pairs as members: <span class="name">("k1", e1), ("k2", e2)</span>, and does not contain any other.</li>
+<li> <span class="name">d</span>  has  the following pairs as members: <span class="name">("k1", e1), ("k2", e2)</span>, and may contain others.</li>
 </ul>
-<p> Thus, the membership of <span class="name">d1</span> is only partially known.</p>
+<p> Thus, the membership of <span class="name">d</span> is only partially known, unless it was derived through insertions and removals from an empty dictionary (See <a href="#insertion-removal-membership-inference_text">Completeness constraints</a>).</p>
 </div>
 
 </section> <!-- end membership -->
@@ -1001,14 +986,9 @@
  <span class="nonterminal">membershipExpression</span>&nbsp;::=  
 <span class="name">hadMember</span> 
  <span class="name">(</span>
- <span class="optional"><span class="nonterminal">identifier</span>
- <span class="name">,</span></span>
-<span class="nonterminal">cIdentifier</span>
+<span class="nonterminal">dIdentifier</span>
  <span class="name">,</span>
-  <span class="name">{</span>
-  <span class="nonterminal">keyValuePairs</span>
-   <span class="name">}</span>
-<span class="nonterminal">optional-attribute-values</span>
+  <span class="nonterminal">keyValuePair</span>
   <span class="name">)</span>
   <br>
 </div>
@@ -1020,40 +1000,26 @@
 <tr><td><b>Dictionary Membership</b></td><td><b>Non-Terminal</b></td></tr>
 <tr><td style="border-width: 0px; "></td><td style="border-width: 0px; "></td></tr>
 
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.id"><span class='attribute' id="provn-membership-d.id">id</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-optionalIdentifier">optionalIdentifier</a></code></td></tr>
-
 <tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.dictionary"><span class='attribute' id="provn-membership-d.dictionary">dictionary</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-dIdentifier">dIdentifier</a></code></td></tr>
 
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.key-entity-set"><span class='attribute' id="provn-membership-d.key-entity-set">key-entity-set</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-keyEntitySet">keyEntitySet</a></code></td></tr>
-
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.complete"><span class='attribute' id="provn-membership-d.complete">complete</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-complete">complete</a></code></td></tr>
-
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.attributes"><span class='attribute' id="provn-membership-d.attributes">attributes</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-optionalAttributeValuePairs">optionalAttributeValuePairs</a></code></td></tr>
+<tr><td><a href="http://www.w3.org/TR/prov-dm/#membership-d.key-entity-set"><span class='attribute' id="provn-membership-d.key-entity-set">key-entity-set</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-keyEntitySet">keyEntityPair</a></code></td></tr>
+
 </table>
 </div>
 
 
 
 <div class="anexample">
-    <pre class="codeexample">
-   hadMember(c, e1)   // Collection membership
-   hadMember(mId, c, {("k4", v4), ("k5", v5)}, [])   // Dictionary membership
-  </pre>
-<p>  Here
-    <span class="name">mid</span> is the optional membership identifier,
-  <span class="name">c</span> is the  identifier for the collection whose membership is stated,
-  <span class="name"> {("k4", v4), ("k5", v5)}</span> is the set of key-value pairs that are members of 
-  <span class="name">c</span>,
-    and <span class="name">[]</span> is the optional (empty) set of attributes. </p>  
-The remaining examples show cases for Dictionaries, where some of the optionals are omitted. Key-entity sets are replaced with Entity sets for the corresponding  generic Collections examples.
-
+	<p>In this example, d is a dictionary known to have <span class="name">e0</span>, <span class="name">e1</span>, and <span class="name">e2</span> as members, and may have other members.</p>
 <pre class="codeexample">
-hadMember(c3, {("k4", v4), ("k5", v5)})
-hadMember(c3, {("k4", v4)})
-hadMember(c3, {("k4", v4)}, false)
-hadMember(c3, {("k4", v4)}, true)
-hadMember(c3, {("k4", v4), ("k5", v5)},[])  
-hadMember(c3, {("k4", v4), ("k5", v5)},true, [])  
+entity(e0)
+entity(e1)
+entity(e2)
+
+entity(d, [prov:type='prov:Dictionary'  ])      // d is a dictionary, with unknown content
+hadMember(d, ("k0", e0))
+hadMember(d, ("k1", e1))
+hadMember(d, ("k2", e2))
 </pre>
 </div>
 
@@ -1066,9 +1032,9 @@
  <span class="name">(</span>
  <span class="optional"><span class="nonterminal">identifier</span>
  <span class="name">,</span></span>
-<span class="nonterminal">cIdentifier</span>
+<span class="nonterminal">dIdentifier</span>
  <span class="name">,</span>
-<span class="nonterminal">cIdentifier</span>
+<span class="nonterminal">dIdentifier</span>
  <span class="name">,</span>
   <span class="name">{</span>
   <span class="nonterminal">keyValuePairs</span>
@@ -1086,9 +1052,9 @@
 
 <tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.id"><span class='attribute' id="provn-insertion.id">id</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-optionalIdentifier">optionalIdentifier</a></code></td></tr>
 
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.after"><span class='attribute' id="provn-insertion.after">after</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">cIdentifier</a></code></td></tr>
-
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.before"><span class='attribute' id="provn-insertion.before">before</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">cIdentifier</a></code></td></tr>
+<tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.after"><span class='attribute' id="provn-insertion.after">after</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">dIdentifier</a></code></td></tr>
+
+<tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.before"><span class='attribute' id="provn-insertion.before">before</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">dIdentifier</a></code></td></tr>
 
 
 <tr><td><a href="http://www.w3.org/TR/prov-dm/#insertion.key-entity-set"><span class='attribute' id="provn-insertion.key-entity-set">key-entity-set</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-keyEntitySet">keyEntitySet</a></code></td></tr>
@@ -1100,21 +1066,21 @@
 
 <div class="anexample">
     <pre class="codeexample">
- derivedByInsertionFrom(id; c1, c, {("k1", v1), ("k2", v2)}, [])  
+ derivedByInsertionFrom(id; d1, d, {("k1", e1), ("k2", e2)}, [])  
   </pre>
 <p>  Here
     <span class="name">id</span> is the optional insertion identifier,
-  <span class="name">c1</span> is the  identifier for the collection after the insertion,
-  <span class="name">c</span> is the  identifier for the collection before the insertion,
-  <span class="name"> {("k1", v1), ("k2", v2)}</span> is the set of key-value pairs that have been inserted in
-  <span class="name">c</span>,
+  <span class="name">d1</span> is the  identifier for the dictionary after the insertion,
+  <span class="name">d</span> is the  identifier for the dictionary before the insertion,
+  <span class="name"> {("k1", e1), ("k2", e2)}</span> is the set of key-entity pairs that have been inserted in
+  <span class="name">d</span>,
     and <span class="name">[]</span> is the optional (empty) set of attributes. </p>
 The remaining examples show cases where some of the optionals are omitted.
 
   <pre class="codeexample">
- derivedByInsertionFrom(c1, c, {("k1", v1), ("k2", v2)})  
- derivedByInsertionFrom(c1, c, {("k1", v1)})  
- derivedByInsertionFrom(c1, c, {("k1", v1), ("k2", v2)}, [])
+ derivedByInsertionFrom(d1, d, {("k1", e1), ("k2", e2)})  
+ derivedByInsertionFrom(d1, d, {("k1", e1)})  
+ derivedByInsertionFrom(d1, d, {("k1", e1), ("k2", e2)}, [])
 </pre>
 </div>
 
@@ -1128,9 +1094,9 @@
  <span class="name">(</span>
  <span class="optional"><span class="nonterminal">identifier</span>
  <span class="name">,</span></span>
-<span class="nonterminal">cIdentifier</span>
+<span class="nonterminal">dIdentifier</span>
  <span class="name">,</span>
-<span class="nonterminal">cIdentifier</span>
+<span class="nonterminal">dIdentifier</span>
  <span class="name">,</span>
   <span class="name">{</span>
   <span class="nonterminal">keySet</span>
@@ -1148,9 +1114,9 @@
 
 <tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.id"><span class='attribute' id="provn-removal.id">id</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-optionalIdentifier">optionalIdentifier</a></code></td></tr>
 
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.after"><span class='attribute' id="provn-removal.after">after</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">cIdentifier</a></code></td></tr>
-
-<tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.before"><span class='attribute' id="provn-removal.before">before</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">cIdentifier</a></code></td></tr>
+<tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.after"><span class='attribute' id="provn-removal.after">after</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">dIdentifier</a></code></td></tr>
+
+<tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.before"><span class='attribute' id="provn-removal.before">before</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-cIdentifier">dIdentifier</a></code></td></tr>
 
 
 <tr><td><a href="http://www.w3.org/TR/prov-dm/#removal.key-set"><span class='attribute' id="provn-removal.key-set">key-set</span></a></td><td><code class="content"><a class="grammarRef" href="#prod-keySet">keySet</a></code></td></tr>
@@ -1164,24 +1130,25 @@
 
 <div class="anexample">
     <pre class="codeexample">
- derivedByRemovalFrom(id; c3, c, {"k1", "k3"}, [])  
+ derivedByRemovalFrom(id; d3, d, {"k1", "k2"}, [])  
   </pre>
 <p>  Here
     <span class="name">id</span> is the optional removal identifier,
-  <span class="name">c1</span> is the  identifier for the collection after the removal,
-  <span class="name">c</span> is the  identifier for the collection before the removal,
-  <span class="name"> {("k1", v1), ("k2", v2)}</span> is the set of key-value pairs that have been removed from
-  <span class="name">c</span>,
+  <span class="name">d1</span> is the  identifier for the collection after the removal,
+  <span class="name">d</span> is the  identifier for the collection before the removal,
+  <span class="name"> {"k1", "k2"}</span> is the set of keys that have been removed from
+  <span class="name">d</span>,
     and <span class="name">[]</span> is the optional (empty) set of attributes. </p>
   The remaining examples show cases where some of the optionals are omitted.
 
   <pre class="codeexample">
-   derivedByRemovalFrom(c3, c1, {"k1", "k3"})               
-   derivedByRemovalFrom(c3, c1, {"k1"})               
-   derivedByRemovalFrom(c3, c1, {"k1", "k3"}, [])               
+   derivedByRemovalFrom(d2, d, {"k1", "k2"})               
+   derivedByRemovalFrom(d2, d, {"k1"})               
+   derivedByRemovalFrom(d2, d, {"k1", "k2"}, [])               
 </pre>
   </div>
 
+
 </section> <!-- removal -->
 
 </section>
@@ -2705,14 +2672,123 @@
 
 <section id="dictionary-xml-schema"> 
 <h2>XML Schema Dictionary</h2>
-
-TODO: PROV-XML Team?
+The XML serialization of Dictionary will follow once this document has passed a first round of internal review by the Working Group.
 </section>
 
 <section id="dictionary-constraints"> 
 <h2>Constraints Associated with Dictionary</h2>
-
-<a href="http://dvcs.w3.org/hg/prov/raw-file/default/dictionary/PROV-Dictionary_discussion.txt">Discussion on constraints for PROV-Dictionary</a>
+In this section, we specify some inferences and constraints associated with dictionaries. These inferences and constraints need to be applied to obtain valid provenance. 
+For more information on how to read this section, we refer to [[PROV-CONSTRAINTS]].
+<section id="dictionary-constraints-inferences">
+	<h3>Inferences</h3>
+	<p id="membership-membership-inference_text">Each key maps to a single entity.</p>
+	 <div class='inference' id='membership-membership-inference'>
+<p>
+<span class="conditional">IF</span>  <span class="name">hadMember(d1, ("k1",e1))</span>
+   and <span class="name">hadMember(d1, ("k1",e2))</span> 
+   <span class='conditional'>THEN</span> <span class="name">e1 = e2</span>
+</p></div>
+
+<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'>
+<p>
+<span class="conditional">IF</span>  <span class="name">hadMember(d1, ("k1",e1))</span>
+   and <span class="name">derivedByInsertionFrom(d2, d1, {("k2", _e2)})</span> and <span class="name">k1</span> &ne; <span class="name">k2</span>
+   <span class='conditional'>THEN</span> <span class="name">hadMember(d2, ("k1", e1))</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>
+	 <div class='inference' id='membership-update-membership-inference'>
+<p>
+<span class="conditional">IF</span>  <span class="name">hadMember(d1, ("k1", e1))</span>
+   and <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e2)})</span>
+   <span class='conditional'>THEN</span> <span class="name">hadMember(d2, ("k1", e2))</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>
+	 <div class='inference' id='insertion-membership-inference'>
+<p>
+<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {("k1", e1)})</span> 
+   <span class='conditional'>THEN</span> <span class="name">hadMember(d2, ("k1", e1))</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>
+	 <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">hadMember(d1, ("k1",_e1))</span>
+</p></div>
+
+<p id="insertion-derivation-inference_text">Insertion and removal are special cases of derivation.</p>
+	 <div class='inference' id='insertion-derivation-inference'>
+<p>
+<span class="conditional">IF</span> <span class="name">derivedByInsertionFrom(d2, d1, {_("k1", e1)})</span> 
+   <span class='conditional'>THEN</span> <span class="name">wasDerivedFrom(d2, d1)</span>
+</p></div>
+	 <div class='inference' id='removal-derivation-inference'>
+<p>
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {_"k1"})</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">hadMember(d1, ("k2",e2))</span> holds <span
+  class='conditional'>IF AND ONLY IF</span> <span class="name">hadMember(d3, ("k2",e2))</span>
+</p></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.
+  Here, completeness means that all key-entity pairs of the dictionary are known through a hadMember statement.
+	  </div>
+
+</section>
+	<!-- end inferences -->
+	
+<section id="dictionary-constraints-constraints">
+	<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'>
+<p>
+<span class="conditional">IF</span> <span class="name">derivedByRemovalFrom(d2, d1, {"k1"})</span> and 
+    <span class="name">hadMember(d2, {("k1",_e1)})</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'>
+<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
+	 class="conditional">INVALID</span>
+</p></div>
+<div class='constraint' id='impossible-insertion-insertion'>
+<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>
+</p></div>
+<div class='constraint' id='impossible-removal-removal'>
+<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>
+</p></div>
+
+<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">hadMember(d,("_k1", e1))</span> and 
+    <span class="name">'EmptyDictionary' &isin; typeOf(e1)</span><span class='conditional'>THEN</span> <span
+	 class="conditional">INVALID</span>
+</p></div>
+	
+</section> <!-- end constraints -->
+	
+	
 </section>