Certification Problem
Input (COPS 292)
The rewrite relation of the following conditional TRS is considered.
|
le(0,s(x)) |
→ |
true |
|
le(x,0) |
→ |
false |
|
le(s(x),s(y)) |
→ |
le(x,y) |
|
min(cons(x,nil)) |
→ |
x |
|
min(cons(x,l)) |
→ |
x |
| le(x,min(l)) ≈ true
|
|
min(cons(x,l)) |
→ |
min(l) |
| le(x,min(l)) ≈ false
|
|
min(cons(x,l)) |
→ |
min(l) |
| min(l) ≈ x
|
Property / Task
Prove or disprove confluence.Answer / Result
Yes.Proof (by ConCon @ CoCo 2020)
1 Quasi-reductive SDTRS where all CCPs are joinable
The given strongly deterministic oriented 3-CTRS is quasi-reductive and all CCPs are joinable.
1.1 Quasi-Reductive CTRS
The given CTRS is quasi-reductive
1.1.1 Unraveling
To prove that the CTRS is quasi-reductive, we show termination of the following
unraveled system.
| For |
le(0,s(x))true we get |
| For |
min(cons(x,l))min(l)le(x,min(l))false we get |
| For |
le(s(x),s(y))le(x,y) we get |
| For |
le(x,0)false we get |
| For |
min(cons(x,l))min(l)min(l)x we get |
| For |
min(cons(x,l))xle(x,min(l))true we get |
| For |
min(cons(x,nil))x we get |
1.1.1.1 Rule Removal
Using the
linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1
over the naturals
| [cons(x1, x2)] |
= |
· x1 + · x2 +
|
| [U2(x1, x2, x3)] |
= |
· x1 + · x2 + · x3 +
|
| [s(x1)] |
= |
· x1 +
|
| [true] |
= |
|
| [min(x1)] |
= |
· x1 +
|
| [0] |
= |
|
| [false] |
= |
|
| [nil] |
= |
|
| [U1(x1, x2, x3)] |
= |
· x1 + · x2 + · x3 +
|
| [le(x1, x2)] |
= |
· x1 + · x2 +
|
all of the following rules can be deleted.
|
le(0,s(x)) |
→ |
true |
(1) |
|
min(cons(x,l)) |
→ |
U1(le(x,min(l)),x,l) |
(2) |
|
le(s(x),s(y)) |
→ |
le(x,y) |
(4) |
|
le(x,0) |
→ |
false |
(5) |
|
min(cons(x,l)) |
→ |
U2(min(l),x,l) |
(6) |
|
min(cons(x,l)) |
→ |
U1(le(x,min(l)),x,l) |
(2) |
|
min(cons(x,nil)) |
→ |
x |
(9) |
1.1.1.1.1 Rule Removal
Using the
Knuth Bendix order with w0 = 1 and the following precedence and weight functions
| prec(U2) |
= |
1 |
|
weight(U2) |
= |
4 |
|
|
|
| prec(false) |
= |
0 |
|
weight(false) |
= |
2 |
|
|
|
| prec(U1) |
= |
1 |
|
weight(U1) |
= |
3 |
|
|
|
| prec(min) |
= |
0 |
|
weight(min) |
= |
6 |
|
|
|
| prec(true) |
= |
0 |
|
weight(true) |
= |
2 |
|
|
|
all of the following rules can be deleted.
|
U1(false,x,l) |
→ |
min(l) |
(3) |
|
U2(x,x,l) |
→ |
min(l) |
(7) |
|
U1(true,x,l) |
→ |
x |
(8) |
1.1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.
1.2 All CCPs are joinable
A CCP is joinable if it is context-joinable, infeasible, or unfeasible.
-
The
1st
CCP
min(x')
=
min(x') | le(y',min(x'))falsemin(x')y'
is context-joinable.
-
The
2nd
CCP
min(nil)
=
x' | min(nil)x'
is context-joinable.
-
The
3rd
CCP
x'
=
min(nil) | min(nil)x'
is context-joinable.
-
The
4th
CCP
y'
=
min(x') | le(y',min(x'))truemin(x')y'
is context-joinable.
-
The
5th
CCP
x'
=
x' | le(x',min(nil))true
is context-joinable.
-
The
6th
CCP
x'
=
x' | le(x',min(nil))true
is context-joinable.
-
The
7th
CCP
min(x')
=
y' | min(x')y'le(y',min(x'))true
is context-joinable.
-
The
8th
CCP
min(x')
=
min(x') | min(x')y'le(y',min(x'))false
is context-joinable.
-
The
9th
CCP contains
the condition le(x',min(nil)) ≈ false
1.2.1 Infeasible Equation
The equation
is infeasible.
1.2.1.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.2.1.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
-
The
10th
CCP contains
the condition le(x',min(nil)) ≈ false
1.2.2 Infeasible Equation
The equation
is infeasible.
1.2.2.1 Non-reachability
We show non-reachability w.r.t. the underlying TRS.
1.2.2.1.1 Non-reachability by TCAP
Non-reachability is shown by the TCAP approximation.
-
The
11th
CCP stemming from the overlap of rules
and
with mgu
{z/y', y/x'}
is unfeasible.
-
The
12th
CCP stemming from the overlap of rules
and
with mgu
{z/y', y/x'}
is unfeasible.