Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMS


Ignore:
Timestamp:
Dec 19, 2006 11:38:32 PM (9 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}}}