wrong termination claim

[abau]

matchbox claims that ~/Downloads/tpdb-8.0/TRS/Strategy_removed_mixed_05/toyama.xml is terminating, but it isn't. CeTa says:

termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the split processor
 1.1.1: error when applying the semlab processor on the DP problem
  pairs:

  f#(0, 1, x1) -> f#(x1, x1, x1)
  rules:

  g(x1, x2) -> x1
  g(x1, x2) -> x2
  f(0, 1, x1) -> f(x1, x1, x1)

  (minimal)
  problem during labeling:
  labeled rule g[[0, 0]](x1, x2) -> x1 missing

[jwaldmann]

Yes. I will fix this. The reason is that matchbox computes g(*,*)->* as not usable, but then compatibility with C_E needs to be added. This is explained in Section 5 of http://colo6-c703.uibk.ac.at/ttt/rta04.pdf

[rene-thiemann]

It will not be possible to just apply the usable rules processor separately (unless one can switch to innermost). Even if one would add C_E, then in general minimality cannot be ensured, so further applications of usable rules would be prohibited. Therefore, one has to find a model for ALL rules, but only has to orient the usable rules within the reduction pair processor.

If one wants to only provide a model for the usable rules, then one should have a look at "predictive labeling": there not all rules have to be a model, but it requires the quasi-model setting and again, the quasi-model condition also has to be ensured for C_E. However, CeTA does not support predictive labeling.

[jwaldmann]

without semantic labelling - should be fixed by commit 0e3f5290aeb50aede4480d5290ec910ff3daed80

with semantic labelling - still broken. recent commit 610498509eae31218f8e21cdb235cf3054f90bb4 results in P is not empty in the following DP-problem (see https://github.com/jwaldmann/co4/blob/usable-rules/JFP_Ex31.cpf.2) This is a regression?

[jwaldmann]

In the example CPF, it is obvious that again the unlabeling proof is wrong, it fails to mention the two non-deleted rules

top(mark(x1)) -> top(proper(x1))
top(ok(x1))   -> top(active(x1))

which then remain as strict rules in the relative DP problem where P_is_empty is applied.

[jwaldmann]

I added the plain ASCII version of the proof: https://github.com/jwaldmann/co4/blob/usable-rules/JFP_Ex31.plain.2 Note that semantic labelling should remove one pair of the two pairs in the first SCC.

[rene-thiemann]

Exactly, it should remove one pair, but none of the rules. And since the unlab-Processor requires the remaining pairs and rules, in this example it has to provide the one remaining pairs and all rules. The modified CPF where one inserts the two mentioned rules in the unlab-Proc is certified!

See new proof is at https://github.com/apunktbau/co4/blob/master/cpfs/JFP_Ex31.cpf.3

[jwaldmann]

I need to understand what our source code does. I notice that after removing one pair, (the labelled versions of) the missing rules are unusable:

...
usable f^[1, 0, 1] (ok^[1] (x1), ok^[0] (x2), ok^[1] (x3)) -> ok^[1] (f^[1, 0, 1] (x1, x2, x3))
usable f^[1, 1, 0] (ok^[1] (x1), ok^[1] (x2), ok^[0] (x3)) -> ok^[0] (f^[1, 1, 0] (x1, x2, x3))
usable f^[1, 1, 1] (ok^[1] (x1), ok^[1] (x2), ok^[1] (x3)) -> ok^[0] (f^[1, 1, 1] (x1, x2, x3))
unusable top^[0] (mark^[0] (x1)) -> top^[0] (proper^[0] (x1))
unusable top^[0] (mark^[0] (x1)) -> top^[0] (proper^[0] (x1))
unusable top^[0] (mark^[0] (x1)) -> top^[0] (proper^[0] (x1))
unusable top^[0] (mark^[0] (x1)) -> top^[0] (proper^[0] (x1))
unusable top^[1] (mark^[1] (x1)) -> top^[1] (proper^[1] (x1))
unusable top^[1] (mark^[1] (x1)) -> top^[1] (proper^[1] (x1))
unusable top^[1] (mark^[1] (x1)) -> top^[1] (proper^[1] (x1))
unusable top^[1] (mark^[1] (x1)) -> top^[1] (proper^[1] (x1))
unusable top^[0] (ok^[0] (x1)) -> top^[0] (active^[0] (x1))
unusable top^[0] (ok^[0] (x1)) -> top^[0] (active^[0] (x1))
unusable top^[0] (ok^[0] (x1)) -> top^[0] (active^[0] (x1))
unusable top^[0] (ok^[0] (x1)) -> top^[0] (active^[0] (x1))
...

but still it is not allowed to remove them (to the unlab proc).

Note that the continuation of the proof search (with matrix interpretation) really does get to see all rules: https://github.com/jwaldmann/co4/blob/usable-rules/JFP_Ex31.plain.2#L101

so it must be some error in some output routine.

[abau]

but none of the rules

I dumped only useable rules in the unlabel-proof.

Should be fixed by https://github.com/apunktbau/co4/commit/9bd0c626c565d41f9095ae8735b1d4e99e51ad47

[jwaldmann]

OK, I confirm that your fix works for JFP_Ex31 . Very good!