--- a/model/prov-constraints.html Mon Nov 19 16:41:14 2012 +0000
+++ b/model/prov-constraints.html Mon Nov 19 16:43:27 2012 +0000
@@ -498,7 +498,7 @@
Provenance is a record that describes the people, institutions, entities, and activities involved in producing, influencing, or delivering a piece of data or a thing.
This document complements
the PROV-DM specification [[PROV-DM]] that defines a data model for
- provenance on the Web. This document defines how to precisely validate provenance documents. </p>
+ provenance on the Web. This document defines a form of validation for provenance. </p>
@@ -589,7 +589,8 @@
Applications producing provenance SHOULD ensure that it is
<a>valid</a>, and similarly applications consuming provenance MAY reject provenance that is not <a>valid</a>. Applications
which are determining whether PROV instances or documents convey the same
-information SHOULD check equivalence as specified here, and SHOULD
+information SHOULD check equivalence as specified here. As a
+guideline, applications should
treat equivalent instances or documents in the same way. This is a
guideline only, because meaning of "in the same way" is
application-specific. For example, applications that manipulate the syntax of
@@ -1839,8 +1840,101 @@
</section>
+ <section id="concepts">
+ <h2>Basic concepts</h2>
+
+ <p>This section specifies the key concepts of terms, statements, instances, substitution,
+ satisfaction, and unification, which have already been discussed in
+ <a href="#rationale">Section 2</a>.
+ </p>
+
+ <p> A <dfn id="term">PROV term</dfn> is a constant identifier
+ <span class="math">c</span>, a placeholder <span
+ class="name">-</span>, a literal value,
+ or an existential variable <span class="math">x</span>. An
+ arbitrary PROV term is written <span class="math">t</span>.</p>
+
+ <p> A <dfn id="statement">PROV statement</dfn> is an expression of
+ the form <span class="math">p(t<sub>1</sub>,...,t<sub>n</sub>)</span> or <span class="math">p(id;t<sub>1</sub>,...,t<sub>n</sub>)</span> where
+ <span class="math">id,t<sub>1</sub>,...,t<sub>n</sub></span> are
+ PROV <a>term</a>s and <span class="math">p</span> is one of the
+ basic PROV relations. An arbitrary PROV statement is written <span class="math">P</span>.</p>
+
+<p> A <dfn id="instance">PROV instance</dfn> is a set of PROV
+ statements. Two instances are considered to be the same if they
+ contain the same statements, without regard to order or repetition.
+ An arbitrary PROV instance is written <span class="math">I</span>.
+</p>
+
+ <p>A <dfn id="substitution">substitution</dfn> <span
+ class="math">S</span> is a mapping <span class="math">
+ [x<sub>1</sub>=t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span> associating existential variables
+ with terms. A substitution is <em>applied</em> to a term, statement
+ or instance by replacing all occurrences of each of the variables
+ <span class="math">x<sub>i</sub></span> with the corresponding <span class="math">t<sub>i</sub></span>. Specifically, if <span class="math">S =
+ [x<sub>1</sub>=t<sub>1</sub>,...,x<sub>n</sub>=t<sub>n</sub>]</span>
+ then the application of <span class="math">S</span> to a term, statement or instance, written <span class="math">S(t)</span>, <span class="math">S(P)</span> and
+ <span class="math">S(I)</span> respectively, is defined as follows:</p>
+<ul><li><span class="math">S(c) = c</span> if <span class="math">c</span> is a constant identifie.r</li>
+<li><span class="math">S(x<sub>i</sub>) = t<sub>i</sub></span> if <span class="math">x<sub>i</sub></span> is one of the variables bound to a
+ term <span class="math">t<sub>i</sub></span> in <span class="math">S</span>.</li>
+<li><span class="math">S(x) = x</span> if <span class="math">x</span> is a variable not bound in <span class="math">S</span>.</li>
+<li><span class="math">S(p(t<sub>1</sub>,...,t<sub>n</sub>) = p(S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
+<li><span class="math">S(p(id;t<sub>1</sub>,...,t<sub>n</sub>) = p(S(id);S(t<sub>1</sub>),...,S(t<sub>n</sub>))</span>.</li>
+<li><span class="math">S(I) = { S(P) | P ∈ I } </span> if <span class="math">I</span> is an instance.</li>
+</ul>
+
+ <p>Suppose <span class="math">P</span> is a statement and <span class="math">I</span> is an
+ instance and <span class="math">S</span> a substitution. We say that <span class="math">P</span> is
+ <dfn>satisfied</dfn> in <span class="math">I</span> by <span
+ class="math">S</span> if <span class="math">S(P) ∈ I</span>. Likewise,
+ we say that a set of statements <span class="math">{P<sub>1</sub>,...,P<sub>n</sub>}</span> is satisfied in
+ <span class="math">I</span> if each <span
+ class="math">P<sub>i</sub></span> is satisfied in <span
+ class="math">I</span> by <span class="math">S</span>. Finally, we
+ say that a set of statements is <dfn>satisfiable</dfn>
+ in <span class="math">I</span> if there is soms substitution <span class="math">S</span> that satisfies the
+ statements in <span class="math">I</span>.
+</p>
-
+ <p> <dfn>Unification</dfn> is an operation that can be applied
+ to a pair of terms.
+ The result of unification is either a <dfn>unifier</dfn>, that is,name a substitution <span class="math">S</span> such that <span class="math">S(t)
+ = S(t')</span>, or failure, indicating
+ that there is no <a>unifier</a>. Unification of pairs of terms is defined as follows.</p>
+
+ <ul>
+ <li> If <span class="math">t</span> and <span
+ class="math">t'</span> are constant identifiers or literal values
+ (including the placeholder <span class="name">-</span>), then
+ there are two cases. If <span class="math">t = t'</span> then their <a>unifier</a> is the
+ empty substitution, otherwise unification
+fails. </li>
+ <li> If <span class="math">x</span> is an existential variable
+ and
+ <span class="math">t'</span> is any term (identifier, constant,
+ placeholder <span class="name">-</span>, or
+ existential variable), then their
+ <a>unifier</a> is
+ <span class="math">[x=t']</span>. In the special case where
+ <span class="math">t'=x</span>, the <a>unifier</a> is the empty substitution.</li>
+ <li> If <span class="math">t</span> is any term (identifier, constant,
+ placeholder <span class="name">-</span>, or
+ existential variable) and
+ <span class="math">x'</span> is an existential variable, then their
+ <a>unifier</a> is the same as the <a>unifier</a> of <span class="math">x</span>
+ and <span class="math">t</span>.</li>
+ </ul>
+
+
+
+<div class="remark">Unification is analogous to unification in
+ logic programming and theorem proving, restricted to flat terms with
+constants and variables but no function symbols. No occurs check is needed because there are no
+ function symbols.</div>
+
+
+</section>
<section id="inferences">
<h2>Definitions and Inferences</h2>
<p>
@@ -1902,7 +1996,7 @@
<span class="name">hyp<sub>1</sub></span>... <span class="name">hyp<sub>k</sub></span>
can be found in the instance, then we check whether the conclusion
<span class="name">concl<sub>1</sub></span> ... <span
- class="name">concl<sub>n</sub></span> is satisfied for some values
+ class="name">concl<sub>n</sub></span> is <a>satisfied</a> for some values
of existential variables. If so, application of the inference has
no effect on the instance. If not, then a copy the
conclusion should be added to the instance, after
@@ -2939,42 +3033,6 @@
class="name">a</span>) is <span
class="name">activity(a,2011-11-16T16:00:00,2011-11-16T18:00:00,[a=1,b=2])</span>. </p>
- <p> <dfn>Unification</dfn> is an operation that can be applied
- to a pair of terms.
- The result of unification is either a <dfn>unifier</dfn>, that is,
- a substitution <span class="math">S</span> such that <span class="math">S(t)
- = S(t')</span>, or failure, indicating
- that there is no <a>unifier</a>. Unification of pairs of terms is defined as follows.</p>
-
- <ul>
- <li> If <span class="name">t</span> and <span
- class="name">t'</span> are constant identifiers or values
- (including the placeholder <span class="name">-</span>), then
- there are two cases. If <span class="name">t = t'</span> then their <a>unifier</a> is the
- empty substitution, otherwise unification
-fails. </li>
- <li> If <span class="name">x</span> is an existential variable
- and
- <span class="name">t'</span> is any term (identifier, constant,
- placeholder <span class="name">-</span>, or
- existential variable), then their
- <a>unifier</a> is
- <span class="name">[x=t']</span>. In the special case where
- <span class="name">t'=x</span>, the <a>unifier</a> is the empty substitution.</li>
- <li> If <span class="name">t</span> is any term (identifier, constant,
- placeholder <span class="name">-</span>, or
- existential variable) and
- <span class="name">x'</span> is an existential variable, then their
- <a>unifier</a> is the same as the <a>unifier</a> of <span class="name">x</span>
- and <span class="name">t</span>.</li>
- </ul>
-
-
-
-<div class="remark">Unification is analogous to unification in
- logic programming and theorem proving, restricted to flat terms with
-constants and variables but no function symbols. No occurs check is needed because there are no
- function symbols.</div>
<p>
A typical uniqueness constraint is as follows:
@@ -4943,7 +5001,9 @@
<li>Dropped RDF as a normative reference.</li>
<li>Made PROV-DM and PROV-N into normative references.</li>
<li>Added "document" and "endDocument" to sec. 6.2.</li>
+ <li>Added sentence of explanation of purpose to beginning.</li>
<li>Moved "mention" to a separate note. </li>
+
</ul>
</section>