Added constraint as in issue-643
authorTom De Nies <tom.denies@ugent.be>
Thu, 28 Mar 2013 18:13:57 +0100
changeset 6010 784f5361aa03
parent 6009 7275c1c5e057
child 6012 0b2deecf9a53
Added constraint as in issue-643
dictionary/Overview.html
--- a/dictionary/Overview.html	Thu Mar 28 18:00:07 2013 +0100
+++ b/dictionary/Overview.html	Thu Mar 28 18:13:57 2013 +0100
@@ -836,7 +836,7 @@
 <li><span class='attribute' id="membership-d.key">key</span>: a key <span class="name">key_1</span> that is associated with the specified entity. <span class="name">key_1</span> is a <a href=" http://www.w3.org/TR/2013/PR-prov-dm-20130312/#term-value">value</a> ;</li>
 </ul>
 <p>Keys cannot be repeated in the same dictionary. However, a dictionary can contain the same entity more than once, as long as it is associated with different keys.</p>
-<p>Note that the <a href=" http://www.w3.org/TR/2013/PR-prov-dm-20130312/#term-membership">collection membership</a> relation, written <span class="name">prov:hadMember(c, e)</span>, can be used when <span class="name">c</span> has <span class="name">prov:type = 'prov:Collection'</span> or <span class="name">prov:type = 'prov:Dictionary'</span>. However, the <a href="#term-dictionary-membership">dictionary  membership</a>, written <span class="name">hadDictionaryMember(d, e, "k")</span>, can only be used when <span class="name">d</span> has <span class="name">prov:type = 'prov:Dictionary'</span>. </p>
+<p>Note that the <a href=" http://www.w3.org/TR/2013/PR-prov-dm-20130312/#term-membership">collection membership</a> relation, written <span class="name">hadMember(c, e)</span>, can be used when <span class="name">c</span> has <span class="name">prov:type = 'prov:Collection'</span> or <span class="name">prov:type = 'prov:Dictionary'</span>. However, the <a href="#term-dictionary-membership">dictionary  membership</a>, written <span class="name">hadDictionaryMember(d, e, "k")</span>, can only be used when <span class="name">d</span> has <span class="name">prov:type = 'prov:Dictionary'</span>. </p>
 	
 </div>
 
@@ -873,7 +873,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/2013/PR-prov-dm-20130312/#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 D2</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 D3</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>
@@ -882,7 +882,7 @@
 <p>
 An Insertion relation <span class="name">prov: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 and the specified key-entity-set are 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>
+Note that insertion and the specified key-entity-set are 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 D8</a>.</p>
 
 
 
@@ -950,7 +950,7 @@
 </div>
 
 <p>A Removal relation <span class="name">prov: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 and the specified key-set are 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>.
+  Note that removal and the specified key-set are 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 D8</a>.
 </p>
 
 <div class="anexample">
@@ -2644,12 +2644,20 @@
 	<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">prov:hadDictionaryMember(d, e1, k1)</span>
-   <span class='conditional'>THEN</span> <span class="name">prov:hadMember(d, e1)</span>
+   <span class='conditional'>THEN</span> <span class="name">hadMember(d, e1)</span>
+</p></div>
+
+<p id="cmembership-dmembership-inference_text"><a href=" http://www.w3.org/TR/2013/PR-prov-dm-20130312/#term-membership">Collection membership</a> for collections that are dictionaries implies <a href="#term-dictionary-membership">dictionary  membership</a>.</p>
+	 <div class='inference' id='cmembership-dmembership-inference'>
+	<span class='ruleTitle'><a class="internalDFN" href="#cmembership-dmembership-inference">Inference D2 (collection-membership-dictionary-membership)</a></span>
+<p>
+<span class="conditional">IF</span>  <span class="name">hadMember(d, e)</span> and <span class="name">'prov:Dictionary' &isin; typeOf(d)</span> <span class='conditional'>THEN</span> there exists a 
+key <span class="name">k</span> such that <span class="name">prov:hadDictionaryMember(d, e, k)</span>
 </p></div>
 
 	<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 D2 (key-single-entity)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#key-single-entity-inference">Inference D3 (key-single-entity)</a></span>
 <p>
 <span class="conditional">IF</span>  <span class="name">prov:hadDictionaryMember(d1, e1, k1)</span>
    and <span class="name">prov:hadDictionaryMember(d1, e2, k1)</span> 
@@ -2658,7 +2666,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 D3 (membership-insertion-membership)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#membership-insertion-membership-inference">Inference D4 (membership-insertion-membership)</a></span>
 <p>Here, KV1 is a set of key-entity pairs and K1 is the key-set of KV1.</p>
   <p>
 <span class="conditional">IF</span>  <span class="name">prov:hadDictionaryMember(d1, e, k)</span>
@@ -2676,7 +2684,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 D4 (insertion-membership)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#insertion-membership-inference">Inference D5 (insertion-membership)</a></span>
  <p>Here, KV1 is a set of key-entity pairs.</p>
   <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, KV1)</span> 
@@ -2695,14 +2703,14 @@
 
 <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 D5 (insertion-derivation)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#insertion-derivation-inference">Inference D6 (insertion-derivation)</a></span>
  <p>Here, KV1 is a set of key-entity pairs and K1 is a set of keys.</p>
  <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, KV1)</span> 
    <span class='conditional'>THEN</span> <span class="name">prov:wasDerivedFrom(d2, d1)</span>
 </p></div>
 	 <div class='inference' id='removal-derivation-inference'>
-	<span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference D6 (removal-derivation)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#removal-derivation-inference">Inference D7 (removal-derivation)</a></span>
 <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span> 
    <span class='conditional'>THEN</span> <span class="name">prov:wasDerivedFrom(d2, d1)</span>
@@ -2711,7 +2719,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 D7 (insertion-removal-membership)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#insertion-removal-membership-inference">Inference D8 (insertion-removal-membership)</a></span>
 <ol>
 	<li>
 	<span class="conditional">IF</span> <span class="name">prov:derivedByInsertionFrom(d2, d1, {("k1", e1)})</span> and 
@@ -2738,7 +2746,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 D8 (impossible-removal-membership)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-membership-constraint">Constraint D9 (impossible-removal-membership)</a></span>
 <p>
   <p>Here, <span class="name">K1</span> is a set of key-entity pairs.</p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span> and 
@@ -2748,7 +2756,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 D9 (impossible-removal-insertion)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-insertion-constraint">Constraint D10 (impossible-removal-insertion)</a></span>
   <p>Here, <span class="name">K1</span> is a set of keys and <span class="name">KV2</span> is a set of key-entity pairs.</p>
 <p>
 <span class="conditional">IF</span> <span class="name">prov:derivedByRemovalFrom(d2, d1, K1)</span> and 
@@ -2764,7 +2772,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 D11 (impossible-removal-removal)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#impossible-removal-removal-constraint">Constraint D12 (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">prov:derivedByRemovalFrom(d2, d1, K1)</span> and 
@@ -2785,7 +2793,7 @@
 <section id="dictionary-typing">
 		<h3>Typing</h3>
 	 <div class='constraint' id='typing'>
-	<span class='ruleTitle'><a class="internalDFN" href="#typing">Constraint D12 (typing)</a></span>
+	<span class='ruleTitle'><a class="internalDFN" href="#typing">Constraint D13 (typing)</a></span>
 		<ol>
 			<li>
 			<p>