axiomatisaion of dictionaries
authorLuc Moreau <l.moreau@ecs.soton.ac.uk>
Thu, 07 Jun 2012 11:09:50 +0100
changeset 3211 d14a65873d8d
parent 3210 571628474716
child 3212 65e37b32ad81
axiomatisaion of dictionaries
model/prov-constraints.html
--- a/model/prov-constraints.html	Thu Jun 07 10:58:38 2012 +0100
+++ b/model/prov-constraints.html	Thu Jun 07 11:09:50 2012 +0100
@@ -1883,32 +1883,32 @@
 
 </section> <!-- constraints -->
 
-<section id="collection-constraints">
-<h2>Collection Constraints</h2>
+<section id="dictionary-constraints">
+<h2>Dictionary Constraints</h2>
 <div class="note">
-  Work on collections and on these constraints is deferred until after
+  Work on dictionaries and on these constraints is deferred until after
   the next working draft, so this section may not be stable.
   </div>
 
 <hr>
   
-<p id='membership-as-insertion_text'>Membership is a convenience notation, since it can be expressed in terms of an insertion into some collection. The membership definition is formalized by <a class="rule-ref" href="#membership-as-insertion"><span/></a>.</p>
+<p id='membership-as-insertion_text'>Membership is a convenience notation, since it can be expressed in terms of an insertion into some  dictionary. The membership definition is formalized by <a class="rule-ref" href="#membership-as-insertion"><span/></a>.</p>
 
 <div class='definition' id='membership-as-insertion'>
 <p>
- <span class="name">memberOf(c, {(k1, v1), ...})</span> holds
-<span class='conditional'>IF AND ONLY IF</span> there exists a collection <span class="name">c0</span>, such that
-<span class="name">derivedByInsertionFrom(c, c0, {(k1, v1), ...})</span>.</p>
+ <span class="name">memberOf(d, {(k1, v1), ...})</span> holds
+<span class='conditional'>IF AND ONLY IF</span> there exists a dictionary <span class="name">d0</span>, such that
+<span class="name">derivedByInsertionFrom(d, d0, {(k1, v1), ...})</span>.</p>
 </div>
 
 <p>
 
 <hr>
 
-<p id='collection-unique-derivation_text'>A collection may be obtained by insertion or removal, or said to satisfy the membership relation.
-To provide an interpretation of collections, PROV-DM 
- restricts one collection to be involved in a single derivation by insertion or removal, or to one membership relation.
-PROV-DM does not provide an interpretation for statements that consist of two (or more) insertion, removal, membership relations that result in the same collection.</p>
+<p id='dictionary-unique-derivation_text'>A dictionary may be obtained by insertion or removal, or said to satisfy the membership relation.
+To provide an interpretation of dictionaries, PROV-DM 
+ restricts one dictionary to be involved in a single derivation by insertion or removal, or to one membership relation.
+PROV-DM does not provide an interpretation for statements that consist of two (or more) insertion, removal, membership relations that result in the same dictionary.</p>
 
 
 
@@ -1916,36 +1916,36 @@
 
 
 <div class='note'> The following constraint is unclear.</div>
-<div class='constraint' id='collection-unique-derivation'>
-<p>A collection MUST NOT be derived through multiple insertions, removal,
+<div class='constraint' id='dictionary-unique-derivation'>
+<p>A dictionary MUST NOT be derived through multiple insertions, removal,
   or membership relations. </p>
 </div>
 
 <div class="anexample">
-Consider the following statements about three collections.
+Consider the following statements about three dictionaries.
   <pre class="codeexample">
-entity(c1, [prov:type='prov:Dictionary'])
-entity(c2, [prov:type='prov:Dictionary'])
-entity(c3, [prov:type='prov:Dictionary'])
-
-
-derivedByInsertionFrom(c3, c1, {("k1", e1), ("k2", e2)})
-derivedByInsertionFrom(c3, c2, {("k3", e3)})
+entity(d1, [prov:type='prov:Dictionary'])
+entity(d2, [prov:type='prov:Dictionary'])
+entity(d3, [prov:type='prov:Dictionary'])
+
+
+derivedByInsertionFrom(d3, d1, {("k1", e1), ("k2", e2)})
+derivedByInsertionFrom(d3, d2, {("k3", e3)})
 </pre>
-<p>There is no interpretation for such statements since <span class="name">c3</span> is derived multiple times by insertion.</p>
+<p>There is no interpretation for such statements since <span class="name">d3</span> is derived multiple times by insertion.</p>
 </div>
 
 
 <div class="anexample">
-<p>As a particular case, collection <span class="name">c</span> is derived multiple times from the same <span class="name">c1</span>. </p>
+<p>As a particular case, dictionary <span class="name">d</span> is derived multiple times from the same <span class="name">d1</span>. </p>
 <pre class="codeexample">
-derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2)})
-derivedByInsertionFrom(id2, c, c1, {("k3", e3), ("k4", e4)})
+derivedByInsertionFrom(id1, d, d1, {("k1", e1), ("k2", e2)})
+derivedByInsertionFrom(id2, d, d1, {("k3", e3), ("k4", e4)})
 </pre>
 <p>The interpretation of such statements is also unspecified. </p>
 <p>To describe the insertion of the 4 key-entity pairs, one would instead write:</p>
 <pre class="codeexample">
-derivedByInsertionFrom(id1, c, c1, {("k1", e1), ("k2", e2), ("k3", e3), ("k4", e4)})
+derivedByInsertionFrom(id1, d, d1, {("k1", e1), ("k2", e2), ("k3", e3), ("k4", e4)})
 </pre>  
 </div>
 
@@ -1953,43 +1953,43 @@
 <div class="anexample">
 <p>The following statements</p>
 <pre class="codeexample">
-derivedByInsertionFrom(c, c1, {("k1", e1)})
-derivedByRemovalFrom(c, c2, {"k2"})
+derivedByInsertionFrom(d, d1, {("k1", e1)})
+derivedByRemovalFrom(d, d2, {"k2"})
 </pre>
 have no interpretation.
 Nor have the following:
 <pre class="codeexample">
-derivedByInsertionFrom(c, c1, {("k1", e1)})
-memberOf(c, {"k2",e2})
+derivedByInsertionFrom(d, d1, {("k1", e1)})
+memberOf(d, {"k2",e2})
 </pre>
 </div>
 
 
 
-<section id="collection-branching">
-<h4>Collection branching</h4>
-
-It is allowed to have multiple derivations from a single root collection, as long as the resulting entities are distinct, as shown in the following example.
+<section id="dictionary-branching">
+<h4>Dictionary branching</h4>
+
+It is allowed to have multiple derivations from a single root dictionary, as long as the resulting entities are distinct, as shown in the following example.
 
 <div class="anexample">
 <pre class="codeexample">
-entity(c0, [prov:type='prov:EmptyDictionary'])    // c0 is an empty collection
-entity(c1, [prov:type='prov:Dictionary'])
-entity(c2, [prov:type='prov:Dictionary'])
-entity(c3, [prov:type='prov:Dictionary'])
+entity(d0, [prov:type='prov:EmptyDictionary'])    // d0 is an empty dictionary
+entity(d1, [prov:type='prov:Dictionary'])
+entity(d2, [prov:type='prov:Dictionary'])
+entity(d3, [prov:type='prov:Dictionary'])
 entity(e1)
 entity(e2)
 entity(e3)
 
-derivedByInsertionFrom(c1, c0, {("k1", e1)})      
-derivedByInsertionFrom(c2, c0, {("k2", e2)})       
-derivedByInsertionFrom(c3, c1, {("k3", e3)})       
+derivedByInsertionFrom(d1, d0, {("k1", e1)})      
+derivedByInsertionFrom(d2, d0, {("k2", e2)})       
+derivedByInsertionFrom(d3, d1, {("k3", e3)})       
 </pre>
 From this set of statements, we conclude:
 <pre class="codeexample">
-  c1 = { ("k1", e1) }
-  c2 = { ("k2", e2) }
-  c3 = { ("k1", e1), ("k3", e3)}
+  d1 = { ("k1", e1) }
+  d2 = { ("k2", e2) }
+  d3 = { ("k1", e1), ("k3", e3)}
 </pre>
 </div>
 
@@ -1997,38 +1997,38 @@
 
   
 
-<section id="collections-and-derivation">
+<section id="dictionaries-and-derivation">
 
   
-<h4>Collections and Weaker Derivation Relation</h4>
-
-<p>The state of a collection is only known to the extent that a chain
-of derivations starting from an empty collection can be found. Since a
-set of statements regarding a collection's evolution may be
+<h4>Dictionaries and Weaker Derivation Relation</h4>
+
+<p>The state of a dictionary is only known to the extent that a chain
+of derivations starting from an empty dictionary can be found. Since a
+set of statements regarding a dictionary's evolution may be
 incomplete, so is the reconstructed state obtained by querying those
-statements. In general, all statements reflect partial knowledge regarding a sequence of data transformation events. In the particular case of collection evolution, in which some of the state changes may have been missed, the more generic derivation relation should be used to signal that some updates may have occurred, which cannot be expressed as insertions or removals. The following  example illustrates this.</p>
+statements. In general, all statements reflect partial knowledge regarding a sequence of data transformation events. In the particular case of dictionary evolution, in which some of the state changes may have been missed, the more generic derivation relation should be used to signal that some updates may have occurred, which cannot be expressed as insertions or removals. The following  example illustrates this.</p>
 
 
  
  <div class="anexample">
-In the example, the state of <span class="name">c2</span> is only partially known because the collection is constructed from partially known other collections.
+In the example, the state of <span class="name">d2</span> is only partially known because the dictionary is constructed from partially known other dictionaries.
  <pre class="codeexample">
-entity(c0, [prov:type='prov:EmptyDictionary'])    // c0 is an empty dictionary
-entity(c1, [prov:type='prov:Dictionary'])    
-entity(c2, [prov:type='prov:Dictionary'])    
-entity(c3, [prov:type='prov:Dictionary'])    
+entity(d0, [prov:type='prov:EmptyDictionary'])    // d0 is an empty dictionary
+entity(d1, [prov:type='prov:Dictionary'])    
+entity(d2, [prov:type='prov:Dictionary'])    
+entity(d3, [prov:type='prov:Dictionary'])    
 entity(e1)
 entity(e2)
 
-derivedByInsertionFrom(c1, c0, {("k1", e1)})       
-wasDerivedFrom(c2, c1)                       
-derivedByInsertionFrom(c3, c2, {("k2", e2)})       
+derivedByInsertionFrom(d1, d0, {("k1", e1)})       
+wasDerivedFrom(d2, d1)                       
+derivedByInsertionFrom(d3, d2, {("k2", e2)})       
  </pre>
 From this set of statements, we conclude:
 <ul>
-<li>    <span class="name">c1 = { ("k1", e1) }</span>
-<li>    <span class="name">c2</span> is somehow derived from <span class="name">c1</span>, but the precise sequence of updates is unknown
-<li>    <span class="name">c3</span>  includes  <span class="name">("k2", e2)</span> but the earlier "gap" leaves uncertainty regarding  <span class="name">("k1", e1)</span>  (it may have been removed) or any other pair that may have been added as part of the derivation activities.
+<li>    <span class="name">d1 = { ("k1", e1) }</span>
+<li>    <span class="name">d2</span> is somehow derived from <span class="name">d1</span>, but the precise sequence of updates is unknown
+<li>    <span class="name">d3</span>  includes  <span class="name">("k2", e2)</span> but the earlier "gap" leaves uncertainty regarding  <span class="name">("k1", e1)</span>  (it may have been removed) or any other pair that may have been added as part of the derivation activities.
 </ul>
  </div>
 
@@ -2041,10 +2041,10 @@
   </div>
   
 
-<section id="collections-and-contents">
+<section id="dictionaries-and-contents">
 
   
-<h4>Collections and Contents</h4>
+<h4>Dictionaries and Contents</h4>
 
 <p>We model the contents of a dictionary  with a function contents that has the following signature
  Dictionary x Value -> Entity U {&#8869,?}.</p>
@@ -2166,7 +2166,7 @@
 </section>
 
  
-</section> <!-- collection-constraints -->
+</section> <!-- dictionary-constraints -->
 
 <section id="account-constraints">
 <h2>Account Constraints</h2>