collections axiomatization take 2
authorPaolo Missier <pmissier@acm.org>
Fri, 08 Jun 2012 20:14:53 +0100
changeset 3252 b71c7c028c56
parent 3251 44c3160e38d7
child 3253 ab95bc5bbd25
collections axiomatization take 2
model/working-copy/wd6-collections-constraints.html
--- a/model/working-copy/wd6-collections-constraints.html	Fri Jun 08 11:12:06 2012 -0400
+++ b/model/working-copy/wd6-collections-constraints.html	Fri Jun 08 20:14:53 2012 +0100
@@ -271,6 +271,50 @@
 -->
 
 
+
+<section id="dictionaries-and-contents-2">
+
+  
+<h4>Collections and Contents take 2</h4>
+
+The interpretation of Collection statements is defined by the following axioms. 
+
+Function Contents: C &rarr; &weierp;(E) maps a collection entity c &isin; C to a finite set {e1, &hellip; en} &sub; &weierp;(E) of entities, where C is the set of all Entities of type Collection, and E  is the set of all Entities.
+<ol>
+<li><span class="name">entity(c, [prov:type='prov:EmptyCollection'])</span> &rArr; Contents(c) = &empty;
+
+<li> <span class="name">derivedByInsertionFrom(c2, c1, E)</span>   &rArr; Contents(c) &sup; Contents(c1) &cup; E;
+
+<li> <span class="name">derivedByRemovalFrom(c2, c1, E)</span>    &rArr; Contents(c) &sup; Contents(c1) \ E;
+
+<li> <span class="name">memberOf(c, E)</span> &rArr; Contents(c) &sup; E
+
+<li> <span class="name">memberOf(c, E, true)</span> &rArr; Contents(c) = E
+  
+</ol>
+
+Note that a chain of insertions and removals that starts from statements of the form (1) or (2) leads to a precise characterisation of the contents of the resulting collection, for example:
+
+<span class="name">
+ entity(c, [prov:type='prov:EmptyCollection']),
+ derivedByInsertionFrom(c1, c, E1),
+ derivedByInsertionFrom(c2, c1, E2) 
+</span>
+        &rArr;   Contents(c2) = E1 &cup; E2
+
+<p/>Similarly: <p/>
+<span class="name">
+ entity(c, [prov:type='prov:Collection'])
+ memberOf(c, E, true)
+ derivedByInsertionFrom(c1, c, E1)
+ derivedByInsertionFrom(c2, c1, E2) 
+</span>
+        &rArr;   Contents(c2) = E &cup; E1 &cup; E2
+
+
+
+</section>
+
 <section id="dictionaries-and-contents">