Certification Problem
Input (COPS 94)
We consider the TRS containing the following rules:
|
F(D(x),y) |
→ |
F(D(x),G(G(y))) |
(1) |
|
F(x,E(y)) |
→ |
F(G(x),E(y)) |
(2) |
|
G(x) |
→ |
x |
(3) |
|
H(I(x)) |
→ |
K(J(x)) |
(4) |
|
J(x) |
→ |
K(J(x)) |
(5) |
|
I(x) |
→ |
I(J(x)) |
(6) |
|
J(x) |
→ |
J(K(J(x))) |
(7) |
|
S(x,T(x)) |
→ |
T(x) |
(8) |
The underlying signature is as follows:
{F/2, D/1, G/1, E/1, H/1, I/1, K/1, J/1, S/2, T/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2023)
1 Persistent Decomposition (Many-Sorted)
Confluence
is proven, because
the maximal
systems
induced by the sorts in the following many-sorted sort attachment
are
confluent.
| F |
: |
4 ⨯ 4 → 0 |
| D |
: |
6 → 4 |
| G |
: |
4 → 4 |
| E |
: |
5 → 4 |
| H |
: |
3 → 3 |
| I |
: |
3 → 3 |
| K |
: |
3 → 3 |
| J |
: |
3 → 3 |
| S |
: |
2 ⨯ 1 → 1 |
| T |
: |
2 → 1 |
The subsystems are(1.1)
|
F(D(x),y) |
→ |
F(D(x),G(G(y))) |
(1) |
|
F(x,E(y)) |
→ |
F(G(x),E(y)) |
(2) |
|
G(x) |
→ |
x |
(3) |
(1.2)
(1.3)
|
H(I(x)) |
→ |
K(J(x)) |
(4) |
|
J(x) |
→ |
K(J(x)) |
(5) |
|
I(x) |
→ |
I(J(x)) |
(6) |
|
J(x) |
→ |
J(K(J(x))) |
(7) |
1.1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
All redundant rules that were added or removed can be
simulated in 4 steps
.
1.1.1 Critical Pair Closing System
Confluence is proven using the following terminating critical-pair-closing-system R:
There are no rules.
1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
All redundant rules that were added or removed can be
simulated in 2 steps
.
1.2.1 Locally confluent and terminating
Confluence is proven by showing local confluence and termination.
1.2.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [T(x1)] |
= |
4 · x1 + 1 |
| [S(x1, x2)] |
= |
1 · x1 + 1 · x2 + 3 |
all of the following rules can be deleted.
1.2.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2.1.2 Local Confluence Proof
All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.
1.3 Decreasing Diagrams
1.3.2 Rule Labeling
Confluence is proven, because all critical peaks can be joined decreasingly
using the following rule labeling function (rules that are not shown have label 0).
The critical pairs can be joined as follows. Here,
↔ is always chosen as an appropriate rewrite relation which
is automatically inferred by the certifier.
-
The critical peak s = K(J(x))←→ε J(K(J(x))) = t can be joined as follows.
s
↔ K(J(K(J(x)))) ↔
t
-
The critical peak s = H(I(J(x)))←→ε K(J(x)) = t can be joined as follows.
s
↔ K(J(J(x))) ↔ K(J(K(J(x)))) ↔
t
-
The critical peak s = H(I(J(x)))←→ε K(J(x)) = t can be joined as follows.
s
↔ H(I(K(J(x)))) ↔ K(J(K(J(x)))) ↔
t
-
The critical peak s = J(K(J(x)))←→ε K(J(x)) = t can be joined as follows.
s
↔ K(J(K(J(x)))) ↔
t
/>