search

salmans / Razor

5 stars 0 forks source link

Recursive provenance construction with functions #48

Open salmans opened 9 years ago

salmans commented 9 years ago

On the model generated for the following theory exists x . P(x); P(x) => exists y . Q(f(y));

when I ask for name* e^1, Razor doesn't display origin of e^0

thedotmatrix commented 9 years ago

@salmans The skolem term returned by the Element Provenance for e^1 is just exists3(). I was expecting something like exists3(e^1) back. It didn't recurse to e^1 because the skolem term was a constant.

salmans commented 9 years ago

Ah, that's interesting. This is one of the side effects of the last changes to the Chase: since x in the body doesn't appear in the head, it is considered to be existentially quantified. That's the reason it doesn't show up in the provenance of y. Let's just keep the issue open until we figure out the right way of dealing with situations like this. Just as a naive idea, we may have to change origin* to display origins of the the elements appearing (only) in the body of sequents as well. Do you agree that in the previous example we should show also display the origin of e^0?

thedotmatrix commented 9 years ago

I think we should allow the display of e^0. However, when we discussed this in person, it raised an interesting point...

There seems to be two types of thinking about origins.

  1. origins are merely the skolem information; since e^0 is not bound to the existence of e^1 (it only occurs in the body), then it should not be included in the origin* output.
  2. a user may have the notion that anything true in the body helped originate the existence of e^1. Even though e^0 could have be any element true for that relation, it is the one that is reported via provenance. In that way, a user may want to follow the existence of even these "free elements" in the body.

For now, since I already made the changes, I will push it to include e^0, and any "free elements" in the origin* printout. But, discussing this distinction, what we think is correct / should be allowed, and remaining consistent is important.

@dandougherty do you have any opinions on this?