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

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.

Received on Monday, 6 August 2012 15:24:33 UTC