Certification Problem
Input (COPS 152)
We consider the TRS containing the following rules:
|
+(x,0) |
→ |
x |
(1) |
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
|
+(x,p(y)) |
→ |
p(+(x,y)) |
(3) |
|
+(0,y) |
→ |
y |
(4) |
|
+(s(x),y) |
→ |
s(+(x,y)) |
(5) |
|
+(p(x),y) |
→ |
p(+(x,y)) |
(6) |
|
s(p(x)) |
→ |
x |
(7) |
|
p(s(x)) |
→ |
x |
(8) |
|
-(0) |
→ |
0 |
(9) |
|
-(s(x)) |
→ |
p(-(x)) |
(10) |
|
-(p(x)) |
→ |
s(-(x)) |
(11) |
|
+(+(x,y),z) |
→ |
+(x,+(y,z)) |
(12) |
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(13) |
|
-(+(x,y)) |
→ |
+(-(x),-(y)) |
(14) |
The underlying signature is as follows:
{+/2, 0/0, s/1, p/1, -/1}Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by csi @ CoCo 2020)
1 Redundant Rules Transformation
To prove that the TRS is (non-)confluent, we show (non-)confluence of the following
modified system:
|
+(x,0) |
→ |
x |
(1) |
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
|
+(x,p(y)) |
→ |
p(+(x,y)) |
(3) |
|
+(0,y) |
→ |
y |
(4) |
|
+(s(x),y) |
→ |
s(+(x,y)) |
(5) |
|
+(p(x),y) |
→ |
p(+(x,y)) |
(6) |
|
s(p(x)) |
→ |
x |
(7) |
|
p(s(x)) |
→ |
x |
(8) |
|
-(0) |
→ |
0 |
(9) |
|
-(s(x)) |
→ |
p(-(x)) |
(10) |
|
-(p(x)) |
→ |
s(-(x)) |
(11) |
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(13) |
|
-(+(x,y)) |
→ |
+(-(x),-(y)) |
(14) |
All redundant rules that were added or removed can be
simulated in 4 steps
.
1.1 Locally confluent and terminating
Confluence is proven by showing local confluence and termination.
1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [-(x1)] |
= |
2 · x1 + 0 |
| [p(x1)] |
= |
1 · x1 + 2 |
| [s(x1)] |
= |
1 · x1 + 1 |
| [+(x1, x2)] |
= |
1 · x1 + 1 · x2 + 1 |
| [0] |
= |
0 |
all of the following rules can be deleted.
|
+(x,0) |
→ |
x |
(1) |
|
+(0,y) |
→ |
y |
(4) |
|
s(p(x)) |
→ |
x |
(7) |
|
p(s(x)) |
→ |
x |
(8) |
|
-(p(x)) |
→ |
s(-(x)) |
(11) |
|
-(+(x,y)) |
→ |
+(-(x),-(y)) |
(14) |
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [-(x1)] |
= |
1 · x1 + 0 |
| [p(x1)] |
= |
1 · x1 + 1 |
| [s(x1)] |
= |
1 · x1 + 1 |
| [+(x1, x2)] |
= |
1 · x1 + 2 · x2 + 0 |
| [0] |
= |
0 |
all of the following rules can be deleted.
|
+(x,s(y)) |
→ |
s(+(x,y)) |
(2) |
|
+(x,p(y)) |
→ |
p(+(x,y)) |
(3) |
1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [-(x1)] |
= |
1 · x1 + 0 |
| [p(x1)] |
= |
1 · x1 + 4 |
| [s(x1)] |
= |
1 · x1 + 4 |
| [+(x1, x2)] |
= |
1 · x1 + 2 · x2 + 1 |
| [0] |
= |
0 |
all of the following rules can be deleted.
|
+(x,+(y,z)) |
→ |
+(+(x,y),z) |
(13) |
1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [-(x1)] |
= |
2 · x1 + 0 |
| [p(x1)] |
= |
1 · x1 + 0 |
| [s(x1)] |
= |
1 · x1 + 0 |
| [+(x1, x2)] |
= |
4 · x1 + 1 · x2 + 0 |
| [0] |
= |
2 |
all of the following rules can be deleted.
1.1.1.1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [-(x1)] |
= |
4 · x1 + 0 |
| [p(x1)] |
= |
1 · x1 + 1 |
| [s(x1)] |
= |
1 · x1 + 1 |
| [+(x1, x2)] |
= |
4 · x1 + 1 · x2 + 0 |
all of the following rules can be deleted.
|
+(s(x),y) |
→ |
s(+(x,y)) |
(5) |
|
+(p(x),y) |
→ |
p(+(x,y)) |
(6) |
|
-(s(x)) |
→ |
p(-(x)) |
(10) |
1.1.1.1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.1.2 Local Confluence Proof
All critical pairs are joinable which can be seen by computing normal forms of all critical pairs.