|
|
```wiki
|
|
|
A rough set of examples (using the refined 'chr-based' algorithm)
|
|
|
|
|
|
|
|
|
Assuming a normal form of equations, it is sufficient to apply
|
|
|
the following 'FD'-rule step.
|
|
|
|
|
|
e1: F t1 = t2
|
|
|
|
|
|
e2: F t1 = t3
|
|
|
|
|
|
==>
|
|
|
|
|
|
e1: F t1 = t2
|
|
|
e2: F t1 = t3
|
|
|
e3: t2 = t3
|
|
|
|
|
|
where e3 = (sym e1) trans e2
|
|
|
|
|
|
|
|
|
Here are some examples:
|
|
|
|
|
|
EXAMPLE 1
|
|
|
|
|
|
Assume (given)
|
|
|
|
|
|
g : forall a. S [a] = [S a] -- axiom
|
|
|
|
|
|
d1 : T Int = Int -- local equations
|
|
|
d2 : T [Int] = S [Int]
|
|
|
d3 : T Int = S Int
|
|
|
|
|
|
|
|
|
wanted
|
|
|
|
|
|
? : T [Int] = [Int]
|
|
|
|
|
|
|
|
|
Step 1: Normalize (local and wanted) equations
|
|
|
(also applies to axioms but we skip this step here)
|
|
|
|
|
|
g : forall a. S [a] = [S a] (0)
|
|
|
|
|
|
|
|
|
g1 : T Int = Int (1)
|
|
|
g2 : T [Int] = a (2)
|
|
|
g3 : S [Int] = a (3)
|
|
|
g4 : T Int = b (4)
|
|
|
g5 : S Int = b (5)
|
|
|
|
|
|
|
|
|
? : T [Int] = [Int] (6)
|
|
|
|
|
|
Reduction steps:
|
|
|
|
|
|
|
|
|
2+6 => ?' : a = [Int]
|
|
|
|
|
|
? = g2 trans ?'
|
|
|
|
|
|
03 from 0+3 =>
|
|
|
g03 : a = [S Int]
|
|
|
g03 = (sym g3) trans (g Int)
|
|
|
|
|
|
503 from 5+03 =>
|
|
|
g503 : a = [b]
|
|
|
g503 = g03 trans ([] g5)
|
|
|
|
|
|
14 from 1+4 =>
|
|
|
g14 : b = Int
|
|
|
g14 = (sym g4) trans g1
|
|
|
|
|
|
Apply 14 on 503 =>
|
|
|
g' : a = [Int]
|
|
|
g' = g503 trans ([] g14)
|
|
|
|
|
|
We found a match for the (reduced) wanted constraint.
|
|
|
|
|
|
? = g2 trans ?'
|
|
|
= g2 trans (g503 trans ([] g14))
|
|
|
= g2 trans ((g03 trans ([] g5)) trans ([] g14))
|
|
|
= g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14))
|
|
|
|
|
|
How to map back to the original (given) local equations?
|
|
|
|
|
|
|
|
|
The same calculation using the original (given) local equations.
|
|
|
|
|
|
g : forall a. S [a] = [S a] (0) -- axiom
|
|
|
|
|
|
d1 : T Int = Int (1) -- local equations
|
|
|
d2 : T [Int] = S [Int] (2)
|
|
|
d3 : T Int = S Int (3)
|
|
|
|
|
|
wanted:
|
|
|
d4 : T [Int] = [Int] (4)
|
|
|
|
|
|
Reduction steps:
|
|
|
|
|
|
24: 2+4 =>
|
|
|
d24 : S [Int] = [Int]
|
|
|
d4 = d2 trans d24 -- wanted, we're interested how to construct d4!
|
|
|
|
|
|
024: 0+24 =>
|
|
|
d024 : [S Int] = [Int]
|
|
|
d24 = (sym (g Int)) trans d024
|
|
|
|
|
|
deompose =>
|
|
|
d024' : S Int = Int
|
|
|
d024 = [] d024'
|
|
|
|
|
|
13 : 1+3 =>
|
|
|
d13 : S Int = Int
|
|
|
d13 = (sym d3) trans d1
|
|
|
|
|
|
|
|
|
We found a match for the (reduced) wanted constraint.
|
|
|
|
|
|
d024' = d13
|
|
|
= (sym d3) trans d1
|
|
|
|
|
|
Thus,
|
|
|
|
|
|
d4 = d2 trans d24
|
|
|
= d2 trans ((sym (g Int)) trans d024)
|
|
|
= d2 trans ((sym (g Int)) trans ([] d024'))
|
|
|
= d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1)))
|
|
|
|
|
|
|
|
|
Compare the normalized result
|
|
|
|
|
|
g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14))
|
|
|
|
|
|
against the 'unnormalized' result
|
|
|
|
|
|
d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1)))
|
|
|
|
|
|
|
|
|
EXAMPLE 2
|
|
|
|
|
|
no axioms involved
|
|
|
|
|
|
given:
|
|
|
d1 : G Int = Bool
|
|
|
d2 : F (G Int) = Int
|
|
|
|
|
|
wanted:
|
|
|
|
|
|
d : F Bool = Int
|
|
|
|
|
|
clearly d = (sym (F d1)) trans d2
|
|
|
|
|
|
|
|
|
The normalized case:
|
|
|
|
|
|
g1 : G Int = Bool (1)
|
|
|
g2 : G Int = a (2)
|
|
|
g3 : F a = Int (3)
|
|
|
|
|
|
Reductions:
|
|
|
|
|
|
12 from 1 + 2 =>
|
|
|
g12 : a = Bool
|
|
|
g12 = (sym g2) trans g1
|
|
|
|
|
|
apply 12 on g3:
|
|
|
|
|
|
g3' : F Bool = Int
|
|
|
g3' = (sym (F g12)) trans g3
|
|
|
|
|
|
Match found, we find
|
|
|
|
|
|
d = (sym (F g12)) trans g3
|
|
|
= (sym (F ((sym g2) trans g1))) trans g3
|
|
|
|
|
|
compare with
|
|
|
|
|
|
(sym (F d1)) trans d2
|
|
|
``` |
|
|
\ No newline at end of file |