Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMS


Ignore:
Timestamp:
Dec 19, 2006 11:38:32 PM (7 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/PlanMS

    v1 v1  
     1{{{ 
     2ALGORITHM 
     3 
     4Ax    axioms 
     5C     locals 
     6W     wanted 
     7 
     8The task: 
     9 
     10Verify that W follows from C wrt Ax (at least 'reduce' W as much as possible). 
     11 
     12For this purpose we normalize C and W, written (C | W) -->* (C' | W'), 
     13by 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 
     19We can verify that W follows from C wrt Ax if 
     20all constraints in W' are either True, or are syntactically 
     21present in C'. 
     22 
     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'). 
     27 
     28The individual normalization steps are: 
     29(I'll skip the rigid/wobbly issue) 
     301) Axiom step (affects C and W) 
     31 
     32We rewrite C and W wrt the axioms: C cup W -->Ax C' cup W' 
     33 
     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 
     37 
     38 [t]=[s] --> t=s etc 
     39 
     402) Local step (affects only C) 
     41 
     42We 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 
     64We write t[s] to denote the occurrence of a term s in 
     65a term t. 
     66 
     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. 
     71 
     723) Wanted step (affects only W) 
     73 
     74We 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, 
     79I 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     
     87Point to note: 
     88 
     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). 
     92 
     93The above algorithm is inspired by the typefunction vs chr 
     94correspondence. 
     95 
     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). 
     99 
     100 
     101EXAMPLES 
     102 
     103Example 1: 
     104 
     105forall a. S [a] = [S a]  -- axiom, Ax 
     106 
     107T Int = Int         (2)  -- locals, C 
     108T [Int] = S [Int]   (3) 
     109T Int = S Int       (4) 
     110 
     111 
     112T [Int] = [Int]          -- wanted, W 
     113 
     114 
     115We'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 
     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. 
     133 
     134 
     135Example 2: 
     136 
     137no axioms 
     138 
     139Bool = G Int      (1)   -- locals, C 
     140F (G Int) = Int   (2) 
     141 
     142F Bool = Int            -- wanted, W 
     143 
     144In this example, we actually need to build the closure of C 
     145to verify W. 
     146 
     147We 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 
     156Thus, we can immediately verify W 
     157 
     158 
     159TERMINATION OF NORMALIZATION 
     160 
     161At this point you may wonder what about termination? 
     162For example, in case of the local assumptions 
     163 
     164T Int = Int     (1) 
     165T Int = S Int   (2) 
     166 
     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 
     174 
     175T Int Int, 
     176T Int b, S Int b 
     177 
     178Application of the FD rule yields 
     179 
     180b=Int, T Int Int, 
     181T Int b, S Int b 
     182 
     183<--> equivalent to 
     184 
     185b=Int, T Int Int, S Int Int 
     186 
     187the above can be interpreted as 
     188 
     189T Int= Int 
     190T Int = S Int 
     191S Int = Int 
     192 
     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). 
     200 
     201Actually, there's another termination issue. 
     202Recall 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 
     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. 
     221 
     222AVOIDING INFINITE LOCAL STEPS/SMARTER LOCAL STEPS 
     223 
     224Let's consider again the example 
     225 
     226T Int = Int     (1) 
     227T Int = S Int   (2) 
     228 
     229As observed above, normalization yields the fixpoint 
     230 
     231T Int = Int 
     232T Int = S Int 
     233S Int = Int 
     234 
     235but a naive algorithm may keep applying (2) on (1), thus 
     236adding in the already present equation S Int = Int. 
     237 
     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 
     242 
     243T Int = Int     (1) 
     244T Int = S Int   (2) 
     245 
     246is represented as the CHR constraint store 
     247 
     248T Int Int, 
     249T Int b, S Int b 
     250 
     251Application of the FD rule yields 
     252 
     253b=Int, T Int Int, 
     254T Int b, S Int b 
     255 
     256<--> equivalent to 
     257 
     258b=Int, T Int Int, S Int Int 
     259 
     260In terms of the type function notation, we can thus argue that 
     261 
     262T Int = Int     (1) 
     263T Int = S Int   (2) 
     264 
     265is normalized to 
     266 
     267T Int = Int 
     268S Int = Int 
     269 
     270There's no termination issue anymore. Of course, the details have yet 
     271to be worked out. 
     272}}}