| 1 | {{{ |
| 2 | ALGORITHM |
| 3 | |
| 4 | Ax axioms |
| 5 | C locals |
| 6 | W wanted |
| 7 | |
| 8 | The task: |
| 9 | |
| 10 | Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible). |
| 11 | |
| 12 | For this purpose we normalize C and W, written (C | W) -->* (C' | W'), |
| 13 | by performing the following steps |
| 14 | |
| 15 | - axiom step, apply axioms on C and W |
| 16 | - local step, build the closure of C |
| 17 | - wanted step, reduce W wrt C (in the axiom step we reduce W wrt Ax) |
| 18 | |
| 19 | We can verify that W follows from C wrt Ax if |
| 20 | all constraints in W' are either True, or are syntactically |
| 21 | present in C'. |
| 22 | |
| 23 | Normalization terminates if |
| 24 | - we have exhaustively applied the axiom and wanted steps and |
| 25 | - the set C' of locals remains stable (ie any local step |
| 26 | generates equations which are already present in C'). |
| 27 | |
| 28 | The individual normalization steps are: |
| 29 | (I'll skip the rigid/wobbly issue) |
| 30 | 1) Axiom step (affects C and W) |
| 31 | |
| 32 | We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W' |
| 33 | |
| 34 | We exhaustively apply rewritings implied by Ax on terms |
| 35 | in C and W and obtain C' and W' (no surprise here). |
| 36 | We also apply the common rules such as |
| 37 | |
| 38 | [t]=[s] --> t=s etc |
| 39 | |
| 40 | 2) Local step (affects only C) |
| 41 | |
| 42 | We build the closure of all locals: (C | W) --> (C' | W) |
| 43 | |
| 44 | Let s=t or t=s in C such that s \equiv S s1 ... sn where |
| 45 | S is a type function and si are terms |
| 46 | |
| 47 | a) if s'[s] =t' in C |
| 48 | |
| 49 | then C cup W --> C cup {s'[t]=t'} cup W |
| 50 | |
| 51 | b) if t'=s'[s] in C |
| 52 | |
| 53 | then C cup W --> C cup {t'=s'[t]} cup W |
| 54 | |
| 55 | c) if s'=t'[t] in C |
| 56 | |
| 57 | then C cup W --> C cup {s'=t'[s]} cup W |
| 58 | |
| 59 | d) if t'[t]=s' in C |
| 60 | |
| 61 | then C cup W --> C-{t'=s'} cup {t'[t]=s'} cup W |
| 62 | |
| 63 | |
| 64 | We write t[s] to denote the occurrence of a term s in |
| 65 | a term t. |
| 66 | |
| 67 | Point to note: |
| 68 | We don't care about the orientation of locals. |
| 69 | The "order issue" is solved by simpling computing the fixpont (ie closure of C). |
| 70 | Steps a)-d) effectively build the closure of all local assumptions. |
| 71 | |
| 72 | 3) Wanted step (affects only W) |
| 73 | |
| 74 | We rewrite W wrt C: (C | W) --> (C' | W) |
| 75 | |
| 76 | Let s=t in C such that s \equiv S s1 ... sn where |
| 77 | S is a type function and si are terms |
| 78 | (NOTE: there was a typo in my earlier email, |
| 79 | I wrote "Let s=t in W ..." but of course we reduce W wrt C) |
| 80 | |
| 81 | a') if s'[s] =t' in W |
| 82 | |
| 83 | then C cup W --> C cup W-{s'=t'} cup {s'[t]=t'} |
| 84 | ^^^^^^^^^^^^^^^^^^^^^^^^ |
| 85 | we replace s'=t' by s'[t]=t' |
| 86 | |
| 87 | Point to note: |
| 88 | |
| 89 | We actually rewrite s'[s]=t' in W to s'[t]=t'. |
| 90 | The other cases b'), c') and d') are similar to the |
| 91 | above cases b), c) and d). |
| 92 | |
| 93 | The above algorithm is inspired by the typefunction vs chr |
| 94 | correspondence. |
| 95 | |
| 96 | How to build evidence during the application of |
| 97 | axiom, local and wanted steps is obvious |
| 98 | (but please yell if there's something I've overlooked). |
| 99 | |
| 100 | |
| 101 | EXAMPLES |
| 102 | |
| 103 | Example 1: |
| 104 | |
| 105 | forall a. S [a] = [S a] -- axiom, Ax |
| 106 | |
| 107 | T Int = Int (2) -- locals, C |
| 108 | T [Int] = S [Int] (3) |
| 109 | T Int = S Int (4) |
| 110 | |
| 111 | |
| 112 | T [Int] = [Int] -- wanted, W |
| 113 | |
| 114 | |
| 115 | We'll only show the reduction of W. |
| 116 | |
| 117 | T [Int] = [Int] |
| 118 | --> apply (3) from left to right |
| 119 | S [Int] = [Int] |
| 120 | --> apply axiom |
| 121 | [S Int] = [Int] |
| 122 | --> "decompose" |
| 123 | S Int = Int |
| 124 | --> apply (4) from right to left |
| 125 | T Int = Int |
| 126 | --> apply (2) from left to right |
| 127 | Int = Int |
| 128 | --> True |
| 129 | |
| 130 | The above normalization steps can be mapped directly to CHR solving |
| 131 | steps. Application of axioms correspond to CHR rule applications. |
| 132 | Application of local assumptions correspond to FD rule applications. |
| 133 | |
| 134 | |
| 135 | Example 2: |
| 136 | |
| 137 | no axioms |
| 138 | |
| 139 | Bool = G Int (1) -- locals, C |
| 140 | F (G Int) = Int (2) |
| 141 | |
| 142 | F Bool = Int -- wanted, W |
| 143 | |
| 144 | In this example, we actually need to build the closure of C |
| 145 | to verify W. |
| 146 | |
| 147 | We find that |
| 148 | |
| 149 | Bool = G Int |
| 150 | F (G Int) = Int |
| 151 | |
| 152 | -->* Bool = G Int |
| 153 | F (G Int) = Int |
| 154 | F Bool = Int |
| 155 | |
| 156 | Thus, we can immediately verify W |
| 157 | |
| 158 | |
| 159 | TERMINATION OF NORMALIZATION |
| 160 | |
| 161 | At this point you may wonder what about termination? |
| 162 | For example, in case of the local assumptions |
| 163 | |
| 164 | T Int = Int (1) |
| 165 | T Int = S Int (2) |
| 166 | |
| 167 | we may repetively apply (2) on (1) and thus we keep adding in |
| 168 | "copies" of S Int = Int. Notice that normalization of C to the form C' |
| 169 | means that we apply the axiom and local steps until the set C' remains |
| 170 | stable. The claim is that the size of C' is bound. This must be the |
| 171 | case because the local steps correspond almost directly to FD rule |
| 172 | applications. For example, the above local assumptions |
| 173 | are represented as the following CHR constraints |
| 174 | |
| 175 | T Int Int, |
| 176 | T Int b, S Int b |
| 177 | |
| 178 | Application of the FD rule yields |
| 179 | |
| 180 | b=Int, T Int Int, |
| 181 | T Int b, S Int b |
| 182 | |
| 183 | <--> equivalent to |
| 184 | |
| 185 | b=Int, T Int Int, S Int Int |
| 186 | |
| 187 | the above can be interpreted as |
| 188 | |
| 189 | T Int= Int |
| 190 | T Int = S Int |
| 191 | S Int = Int |
| 192 | |
| 193 | The point here is that although the number of local steps may be |
| 194 | infinite, we'll eventually reach a stable constraint store. |
| 195 | As said above, each local step corresponds almost directly to a FD |
| 196 | rule application step. |
| 197 | Guess it may be more appropriate to say that the above method is |
| 198 | specificed declaratively rather than algorithmic. |
| 199 | (more on how to avoid infinite application of local steps below). |
| 200 | |
| 201 | Actually, there's another termination issue. |
| 202 | Recall the earlier example |
| 203 | |
| 204 | |
| 205 | S [[Int]] = [T Int] |
| 206 | S [[Int]] = T Int |
| 207 | |
| 208 | --> |
| 209 | |
| 210 | T Int = [T Int] |
| 211 | S [[Int]] = [T Int] |
| 212 | S [[Int]] = T Int |
| 213 | |
| 214 | It seems we have introduced a non-terminating local rewrite relation |
| 215 | T Int = [T Int]. As observed earlier, such "non-terminating" |
| 216 | relations correspond to inconsistent CHR stores. |
| 217 | I'm sure the condition that rewrite relations must be "decreasing" |
| 218 | is sufficient to guarantee termination, not sure whether it's also |
| 219 | necessary. The brute force method would be to translate |
| 220 | C cup W into its CHR form and check the CHR store for consistency. |
| 221 | |
| 222 | AVOIDING INFINITE LOCAL STEPS/SMARTER LOCAL STEPS |
| 223 | |
| 224 | Let's consider again the example |
| 225 | |
| 226 | T Int = Int (1) |
| 227 | T Int = S Int (2) |
| 228 | |
| 229 | As observed above, normalization yields the fixpoint |
| 230 | |
| 231 | T Int = Int |
| 232 | T Int = S Int |
| 233 | S Int = Int |
| 234 | |
| 235 | but a naive algorithm may keep applying (2) on (1), thus |
| 236 | adding in the already present equation S Int = Int. |
| 237 | |
| 238 | Is there a smart method to avoid infinite local steps? |
| 239 | (thus we don't need to check whether we've reached a fixpoint, |
| 240 | this may be costly). |
| 241 | We may get some insight from the CHR derivation. Eg |
| 242 | |
| 243 | T Int = Int (1) |
| 244 | T Int = S Int (2) |
| 245 | |
| 246 | is represented as the CHR constraint store |
| 247 | |
| 248 | T Int Int, |
| 249 | T Int b, S Int b |
| 250 | |
| 251 | Application of the FD rule yields |
| 252 | |
| 253 | b=Int, T Int Int, |
| 254 | T Int b, S Int b |
| 255 | |
| 256 | <--> equivalent to |
| 257 | |
| 258 | b=Int, T Int Int, S Int Int |
| 259 | |
| 260 | In terms of the type function notation, we can thus argue that |
| 261 | |
| 262 | T Int = Int (1) |
| 263 | T Int = S Int (2) |
| 264 | |
| 265 | is normalized to |
| 266 | |
| 267 | T Int = Int |
| 268 | S Int = Int |
| 269 | |
| 270 | There's no termination issue anymore. Of course, the details have yet |
| 271 | to be worked out. |
| 272 | }}} |