Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMS

Dec 19, 2006 11:38:32 PM (9 years ago)



  • TypeFunctionsSynTC/PlanMS

    v1 v1  
     4Ax    axioms
     5C     locals
     6W     wanted
     8The task:
     10Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible).
     12For this purpose we normalize C and W, written (C | W) -->* (C' | W'),
     13by performing the following steps
     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)
     19We can verify that W follows from C wrt Ax if
     20all constraints in W' are either True, or are syntactically
     21present in C'.
     23Normalization 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
     26generates equations which are already present in C').
     28The individual normalization steps are:
     29(I'll skip the rigid/wobbly issue)
     301) Axiom step (affects C and W)
     32We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W'
     34We exhaustively apply rewritings implied by Ax on terms
     35in C and W and obtain C' and W' (no surprise here).
     36We also apply the common rules such as
     38 [t]=[s] --> t=s etc
     402) Local step (affects only C)
     42We build the closure of all locals:  (C | W) --> (C' | W)
     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
     47  a) if s'[s] =t' in C
     49     then C cup W --> C cup {s'[t]=t'} cup W
     51  b) if t'=s'[s] in C
     53     then C cup W --> C cup {t'=s'[t]} cup W
     55  c) if s'=t'[t] in C
     57     then C cup W --> C cup {s'=t'[s]} cup W
     59  d) if t'[t]=s' in C
     61     then C cup W --> C-{t'=s'} cup {t'[t]=s'} cup W
     64We write t[s] to denote the occurrence of a term s in
     65a term t.
     67Point 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.
     723) Wanted step (affects only W)
     74We rewrite W wrt C:  (C | W) --> (C' | W)
     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,
     79I wrote "Let s=t in W ..." but of course we reduce W wrt C)
     81    a') if s'[s] =t' in W
     83     then C cup W --> C cup W-{s'=t'} cup {s'[t]=t'}
     84                            ^^^^^^^^^^^^^^^^^^^^^^^^
     85                  we replace s'=t' by s'[t]=t'
     87Point to note:
     89We actually rewrite s'[s]=t' in W to s'[t]=t'.
     90The other cases b'), c') and d') are similar to the
     91above cases b), c) and d).
     93The above algorithm is inspired by the typefunction vs chr
     96How to build evidence during the application of
     97axiom, local and wanted steps is obvious
     98(but please yell if there's something I've overlooked).
     103Example 1:
     105forall a. S [a] = [S a]  -- axiom, Ax
     107T Int = Int         (2)  -- locals, C
     108T [Int] = S [Int]   (3)
     109T Int = S Int       (4)
     112T [Int] = [Int]          -- wanted, W
     115We'll only show the reduction of W.
     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
     130The above normalization steps can be mapped directly to CHR solving
     131steps. Application of axioms correspond to CHR rule applications.
     132Application of local assumptions correspond to FD rule applications.
     135Example 2:
     137no axioms
     139Bool = G Int      (1)   -- locals, C
     140F (G Int) = Int   (2)
     142F Bool = Int            -- wanted, W
     144In this example, we actually need to build the closure of C
     145to verify W.
     147We find that
     149     Bool = G Int   
     150     F (G Int) = Int
     152-->* Bool = G Int   
     153     F (G Int) = Int
     154     F Bool = Int
     156Thus, we can immediately verify W
     161At this point you may wonder what about termination?
     162For example, in case of the local assumptions
     164T Int = Int     (1)
     165T Int = S Int   (2)
     167we 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'
     169means that we apply the axiom and local steps until the set C' remains
     170stable. The claim is that the size of C' is bound. This must be the
     171case because the local steps correspond almost directly to FD rule
     172applications. For example, the above local assumptions
     173are represented as the following CHR constraints
     175T Int Int,
     176T Int b, S Int b
     178Application of the FD rule yields
     180b=Int, T Int Int,
     181T Int b, S Int b
     183<--> equivalent to
     185b=Int, T Int Int, S Int Int
     187the above can be interpreted as
     189T Int= Int
     190T Int = S Int
     191S Int = Int
     193The point here is that although the number of local steps may be
     194infinite, we'll eventually reach a stable constraint store.
     195As said above, each local step corresponds almost directly to a FD
     196rule application step.
     197Guess it may be more appropriate to say that the above method is
     198specificed declaratively rather than algorithmic.
     199(more on how to avoid infinite application of local steps below).
     201Actually, there's another termination issue.
     202Recall the earlier example
     205   S [[Int]] = [T Int]
     206   S [[Int]] = T Int
     208   -->
     210   T Int = [T Int]
     211   S [[Int]] = [T Int]
     212   S [[Int]] = T Int
     214It seems we have introduced a non-terminating local rewrite relation
     215T Int = [T Int]. As observed earlier, such "non-terminating"
     216relations correspond to inconsistent CHR stores.
     217I'm sure the condition that rewrite relations must be "decreasing"
     218is sufficient to guarantee termination, not sure whether it's also
     219necessary. The brute force method would be to translate
     220C cup W into its CHR form and check the CHR store for consistency.
     224Let's consider again the example
     226T Int = Int     (1)
     227T Int = S Int   (2)
     229As observed above, normalization yields the fixpoint
     231T Int = Int
     232T Int = S Int
     233S Int = Int
     235but a naive algorithm may keep applying (2) on (1), thus
     236adding in the already present equation S Int = Int.
     238Is there a smart method to avoid infinite local steps?
     239(thus we don't need to check whether we've reached a fixpoint,
     240this may be costly).
     241We may get some insight from the CHR derivation. Eg
     243T Int = Int     (1)
     244T Int = S Int   (2)
     246is represented as the CHR constraint store
     248T Int Int,
     249T Int b, S Int b
     251Application of the FD rule yields
     253b=Int, T Int Int,
     254T Int b, S Int b
     256<--> equivalent to
     258b=Int, T Int Int, S Int Int
     260In terms of the type function notation, we can thus argue that
     262T Int = Int     (1)
     263T Int = S Int   (2)
     265is normalized to
     267T Int = Int
     268S Int = Int
     270There's no termination issue anymore. Of course, the details have yet
     271to be worked out.