Non-deterministic behavior when running on grandpa.raz about rusty-razor HOT 1 CLOSED

Investigation:

• Razor (sometimes) constructs models (for grandpa) when sequents are not instantiated in a deterministic order (the reason why Razor didn't behave deterministically as we discussed). However, when the sequents are instantiated deterministically, Razor doesn't terminate (on grandpa).

• Razor constructs models (for grandpa) when the sequent selection strategy is not "fair". Surprisingly, when the strategy is unfair, Razor constructs models successfully.

Another contributing factor

Razor's strategy for choosing the next sequent to instantiate is determined by a "Selector".
In a chase step, if a sequent can be triggered with multiple variable assignments, the sequent gets triggered by the first assignment only (and not all possible assignments). Triggering the sequent with other assignments gets postponed to future chase steps, when the selector selects the same sequent again. For example, given the following theory and a selector that interleaves between the two sequents:

P(x) -> Q(x)
Q(x) -> R(x)

the model below will be expanded in the following order:

P(0), P(1)
---------------------
P(0), P(1), Q(0)
---------------------
P(0), P(1), Q(0), R(0)
---------------------
P(0), P(1), Q(0), R(0), Q(1)
---------------------
P(0), P(1), Q(0), R(0), Q(1), R(1)

and not by the following:

P(0), P(1)
---------------------
P(0), P(1), Q(0)
---------------------
P(0), P(1), Q(0), Q(1)
---------------------
P(0), P(1), Q(0), Q(1), R(0)
---------------------
P(0), P(1), Q(0), Q(1), R(0), R(1)
---------------------

So what is going on?

The next theory is a minimal example to explain Razor's execution on grandpa ('a and 'b are constants):

(A) P(f('a))
(B) P('b)
(C) P(x) -> x = 'a
(D) P(y) -> P(f(y))

Given an unfair selector, where the selector always picks the first applicable sequent from the top (and triggers it only for one assignment), a run of Razor looks like below:

Sequent: A
Model:
'a -> 0, f('a) -> 1
P(1)
---------------------
Sequent: B
Model:
'a -> 0, f('a) -> 1, 'b -> 2
P(1), P(2)
---------------------
Sequent: C
Model:
'a -> 0, f('a) -> 0, 'b -> 2
P(0), P(2)
---------------------
Sequent: C
Model:
'a -> 0, f('a) -> 0, 'b -> 0
P(0)

In contrast, a fair selector, which continues with the next sequent after triggering a sequent (for only one assignment), results in a non-terminating run of Razor:

(repeating the theory here)

(A) P(f('a))
(B) P('b)
(C) P(x) -> x = 'a
(D) P(y) -> P(f(y))

The run:

Sequent: A
Model:
'a -> 0, f('a) -> 1
P(1)
---------------------
Sequent: B
Model:
'a -> 0, f('a) -> 1, 'b -> 2
P(1), P(2)
---------------------
Sequent: C
Model:
'a -> 0, f('a) -> 0, 'b -> 2
P(0), P(2)
---------------------
Sequent: D
Model:
'a -> 0, f('a) -> 0, 'b -> 2, f(2) -> 3
P(0), P(2), P(3)
---------------------
Sequent: C
Model:
'a -> 0, f('a) -> 0, 'b -> 0, f(2) -> 3
P(0), P(0), P(3)
---------------------
Sequent: D
Model:
'a -> 0, f('a) -> 0, 'b -> 0, f(2) -> 3, f(3) -> 4
P(0), P(0), P(3), P(4)
---------------------
.
.
.

Notice that, choosing assignments deterministically, e.g., instantiating (C) with x -> 2 before x -> 3 and x -> 3 before x -> 4 is another contributing factor to the non-terminating run.

Is there any theoretical significance?

I really don't know the answer. My intuitive response is: no, because there is a homomorphism from the infinite model to the initial model and any other model of the theory. However, this makes me appreciate the importance of the strategy by which sequents get selected. It's not surprising that a fair selector is leading to the homomorphically minimal model. But what is interesting is that the first selector is fair for this particular theory (since (C) doesn't extend the domain of the model), and it eventually gives a chance to (D). However, the example shows that just the order of selecting sequents (even by a fair selector) can drastically influence the output of the chase algorithm, especially from a user's perspective.

Potential resolutions:

• Make Razor run deterministically: when evaluating a sequent assign variables to model elements deterministically.
• Introduce a user option for selector type
• When model-finding is bounded, try other selectors when a model cannot be found.
• Explore other algorithms for selecting sequents: (1) that doesn't visit the sequents in the same order in every iteration (2) try all possible assignments when triggering a sequent

from rusty-razor.