{{{ ALGORITHM Ax axioms C locals W wanted The task: Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible). For this purpose we normalize C and W, written (C | W) -->* (C' | W'), by performing the following steps - axiom step, apply axioms on C and W - local step, build the closure of C - wanted step, reduce W wrt C (in the axiom step we reduce W wrt Ax) We can verify that W follows from C wrt Ax if all constraints in W' are either True, or are syntactically present in C'. Normalization terminates if - we have exhaustively applied the axiom and wanted steps and - the set C' of locals remains stable (ie any local step generates equations which are already present in C'). The individual normalization steps are: (I'll skip the rigid/wobbly issue) 1) Axiom step (affects C and W) We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W' We exhaustively apply rewritings implied by Ax on terms in C and W and obtain C' and W' (no surprise here). We also apply the common rules such as [t]=[s] --> t=s etc 2) Local step (affects only C) We build the closure of all locals: (C | W) --> (C' | W) Let s=t or t=s in C such that s \equiv S s1 ... sn where S is a type function and si are terms a) if s'[s] =t' in C then C cup W --> C cup {s'[t]=t'} cup W b) if t'=s'[s] in C then C cup W --> C cup {t'=s'[t]} cup W c) if s'=t'[t] in C then C cup W --> C cup {s'=t'[s]} cup W d) if t'[t]=s' in C then C cup W --> C-{t'=s'} cup {t'[t]=s'} cup W We write t[s] to denote the occurrence of a term s in a term t. Point to note: We don't care about the orientation of locals. The "order issue" is solved by simpling computing the fixpont (ie closure of C). Steps a)-d) effectively build the closure of all local assumptions. 3) Wanted step (affects only W) We rewrite W wrt C: (C | W) --> (C' | W) Let s=t in C such that s \equiv S s1 ... sn where S is a type function and si are terms (NOTE: there was a typo in my earlier email, I wrote "Let s=t in W ..." but of course we reduce W wrt C) a') if s'[s] =t' in W then C cup W --> C cup W-{s'=t'} cup {s'[t]=t'} ^^^^^^^^^^^^^^^^^^^^^^^^ we replace s'=t' by s'[t]=t' Point to note: We actually rewrite s'[s]=t' in W to s'[t]=t'. The other cases b'), c') and d') are similar to the above cases b), c) and d). The above algorithm is inspired by the typefunction vs chr correspondence. How to build evidence during the application of axiom, local and wanted steps is obvious (but please yell if there's something I've overlooked). EXAMPLES Example 1: forall a. S [a] = [S a] -- axiom, Ax T Int = Int (2) -- locals, C T [Int] = S [Int] (3) T Int = S Int (4) T [Int] = [Int] -- wanted, W We'll only show the reduction of W. T [Int] = [Int] --> apply (3) from left to right S [Int] = [Int] --> apply axiom [S Int] = [Int] --> "decompose" S Int = Int --> apply (4) from right to left T Int = Int --> apply (2) from left to right Int = Int --> True The above normalization steps can be mapped directly to CHR solving steps. Application of axioms correspond to CHR rule applications. Application of local assumptions correspond to FD rule applications. Example 2: no axioms Bool = G Int (1) -- locals, C F (G Int) = Int (2) F Bool = Int -- wanted, W In this example, we actually need to build the closure of C to verify W. We find that Bool = G Int F (G Int) = Int -->* Bool = G Int F (G Int) = Int F Bool = Int Thus, we can immediately verify W TERMINATION OF NORMALIZATION At this point you may wonder what about termination? For example, in case of the local assumptions T Int = Int (1) T Int = S Int (2) we may repetively apply (2) on (1) and thus we keep adding in "copies" of S Int = Int. Notice that normalization of C to the form C' means that we apply the axiom and local steps until the set C' remains stable. The claim is that the size of C' is bound. This must be the case because the local steps correspond almost directly to FD rule applications. For example, the above local assumptions are represented as the following CHR constraints T Int Int, T Int b, S Int b Application of the FD rule yields b=Int, T Int Int, T Int b, S Int b <--> equivalent to b=Int, T Int Int, S Int Int the above can be interpreted as T Int= Int T Int = S Int S Int = Int The point here is that although the number of local steps may be infinite, we'll eventually reach a stable constraint store. As said above, each local step corresponds almost directly to a FD rule application step. Guess it may be more appropriate to say that the above method is specificed declaratively rather than algorithmic. (more on how to avoid infinite application of local steps below). Actually, there's another termination issue. Recall the earlier example S [[Int]] = [T Int] S [[Int]] = T Int --> T Int = [T Int] S [[Int]] = [T Int] S [[Int]] = T Int It seems we have introduced a non-terminating local rewrite relation T Int = [T Int]. As observed earlier, such "non-terminating" relations correspond to inconsistent CHR stores. I'm sure the condition that rewrite relations must be "decreasing" is sufficient to guarantee termination, not sure whether it's also necessary. The brute force method would be to translate C cup W into its CHR form and check the CHR store for consistency. AVOIDING INFINITE LOCAL STEPS/SMARTER LOCAL STEPS Let's consider again the example T Int = Int (1) T Int = S Int (2) As observed above, normalization yields the fixpoint T Int = Int T Int = S Int S Int = Int but a naive algorithm may keep applying (2) on (1), thus adding in the already present equation S Int = Int. Is there a smart method to avoid infinite local steps? (thus we don't need to check whether we've reached a fixpoint, this may be costly). We may get some insight from the CHR derivation. Eg T Int = Int (1) T Int = S Int (2) is represented as the CHR constraint store T Int Int, T Int b, S Int b Application of the FD rule yields b=Int, T Int Int, T Int b, S Int b <--> equivalent to b=Int, T Int Int, S Int Int In terms of the type function notation, we can thus argue that T Int = Int (1) T Int = S Int (2) is normalized to T Int = Int S Int = Int There's no termination issue anymore. Of course, the details have yet to be worked out. }}}