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

On Mon, Aug 6, 2012 at 4:47 PM, James Cheney <jcheney@inf.ed.ac.uk> wrote:
> 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.

I'm sorry, that reasoning is not good enough for me alone, as we don't
have "an entity statement" (yes, that old discussion again..) in DM,
simply "an entity":

> An entity ◊, written entity(id, [attr1=val1, ...]) in PROV-N, has:

wasStartedBy has:
> trigger: an optional identifier (e) for the entity triggering the activity;

Thus, if the trigger identifier is there, it's an entity.

Inference 8 says:

IF activity(a,t1,t2,_attrs) THEN there exist _id1, _e1, _id2, and _e2
such that wasStartedBy(_id1;a,_e1,_a1,t1,[]) and
wasEndedBy(_id2;a,_e2,_a2,t2,[]).

so _e1 exists, it even says so! And by what we see above it's an
entity, nothing else is allowed (unless we add the previously
discussed - for blank!).

Hence, at least in my mind, this implies:

entity(_e1)

and inference 7 triggers.


I see what you argue, because
http://dvcs.w3.org/hg/prov/raw-file/tip/model/releases/ED-prov-constraints-20120723/prov-constraints.html#type-constraints
does not specify the inference entity(e), just some typeOf(e)
relation, and there are no inference rules that imply an entity()
*statement*.

This implies that one way to avoid an entity to be  generated and
invalidated is simply to skip the entity() statements (and equivalent
skip activity to avoid wasStartedBy and wasEndedBy). I think I need to
read the whole specification again if this is the kind of
interpretation you really mean. This should then also be stated very
early on, as it is very unexpected to me.

It also means there could be implied activities without wasStartedBy
and wasEndedBy, and I am worried that those might then be using and
generating things in impossible orders, because the time constraints
rely on wasStartedBy/wasEndedBy/wasGeneratedBy/wasInvalidatedBy.



> 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.

Yes, but that would be the case for inference rule 7 and 8, because of
'there exists'.




-- 
Stian Soiland-Reyes, myGrid team
School of Computer Science
The University of Manchester

Received on Wednesday, 8 August 2012 09:11:34 UTC