Re: PROV-ISSUE-465 (avoid-infinite-inferences): Avoid infinite loops in inferences [prov-dm-constraints]

This is not true, and the solution proposed isn't necessary (nor would it be sufficient to restore termination, if termination were a problem).

We had a long internal discussion before releasing the review draft about how to avoid this.  My preference would be to get rid of inferences 7 and 8.  Instead, we agreed to weaken the type inferences so that they don't infer new entity() or activity() facts.

This suffices because inference 7 and 8 only allow inferring start/end for entity/activity that are declared using entity() and activity().  There are no rules that allow inferring new entity() or activity() facts (well, there is one, but it can only be applied due to specialization, and we don't infer specializations from entity or wasGeneratedBy etc. facts).

It's true that you can keep applying any existential rule forever as its hypotheses stay true forever, but this is not a problem since we only apply such a rule (generating a new existential variable) if the RHS is not already satisfiable.  If it were a problem, it would be a problem for all of our (existential) inferences.

I propose that we add clearer explanation (with an example) showing why the infinite inference sequence in the example isn't possible with the existing system.  The specific characteristics of the design that prevent this should also be advertised earlier.

--James

On Aug 6, 2012, at 4:24 PM, Provenance Working Group Issue Tracker wrote:

> PROV-ISSUE-465 (avoid-infinite-inferences): Avoid infinite loops in inferences [prov-dm-constraints]
> 
> http://www.w3.org/2011/prov/track/issues/465
> 
> Raised by: Stian Soiland-Reyes
> On product: prov-dm-constraints
> 
> 
> Following the inferences literally causes infinite loops, chaining back to the generation of the universe, and the generation of the trigger of the generation of the universe activity, etc.
> 
> I believe a note to avoid further inferences on statements with purely existential variables would be sufficient. 
> 
> 
>> From Stian's review of PROV-Constraint
> http://lists.w3.org/Archives/Public/public-prov-wg/2012Aug/0021.html
> 
> 
> 
> Combining inference 7 and 8 means inference rules loops forever,
> creating triggers and activities, giving a chicken-and-egg problem
> going back to the beginning of the universe, and beyond.
> 
> I only find a way out of this if an activity (phys:evolutionOfUniverse
> ?) creates its own trigger, which I am glad to see is allowed as
> Constraint 39 luckily does not use "strictly precedes".
> 
> 
> Here's a whiteboard drawing I made (this freaked out the office..)
> when trying to figure out which loops can be formed from the
> inferences (I've crossed out the 'dead ends', an arrow shows 'THEN'
> links between statements and/or variables of statements):
> 
>  http://www.w3.org/2011/prov/wiki/File:PROV-Constraint-inference-loops.jpg
> 
> 
> I think this is problematic, at least, the document should say
> something like "Care should be taken when implementing inference rules
> 7 and 8 in combination, as by recursively following  inference rules
> for statements with only existential variables an endless loop would
> be formed."  (In SPARQL this could for instance be by using FILTER
> (!isBlank(?c)) although you would need to exclude bnodes from the
> original graph)
> 
> As far as I can tell from my lovely picture, stopping inference at
> purely existential variables should be enough, as these inferences
> would quickly not pass on potential 'real' variables.
> 
> 
> 
> 
>> 6. Normalization, Validity, and Equivalence
>> Because of the potential interaction among inferences, definitions and constraints, the above algorithm is recursive. Nevertheless, all of our constraints fall into a class of tuple-generating dependencies and equality-generating dependencies that satisfy a termination condition called weak acyclicity that has been studied in the context of relational databases [DBCONSTRAINTS].
> 
> I find I need to add a condition to not follow inferences on purely
> existential variables to avoid a recursive loop. So I would add that
> to point 4.
> 
> 
> 
> 
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Received on Monday, 6 August 2012 15:47:41 UTC