Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMSRevised


Ignore:
Timestamp:
Jan 1, 2007 10:01:33 PM (8 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/PlanMSRevised

    v1 v1  
     1{{{ 
     2 
     3 
     4=== Problem with Plan MS: Termination is still an issue === 
     5 
     6Example: 
     7 
     8F and G are type function constructors. Consider the local assumptions 
     9 
     10F (G Int) = Int    -- (1)  
     11G Int = F (G Int)  -- (2) 
     12 
     13Applying (2) on (1) yields 
     14 
     15    F (G Int) = Int 
     16--> F (F (G Int)) = Int 
     17--> F (F (F (G Int))) = Int 
     18--> ... 
     19 
     20NOTE: 
     21Plan MC rejects (2), cause the type equation is non-decreasing. 
     22Here we are after a more liberal type checking method. 
     23 
     24=== Plan MS revised overview === 
     25 
     26Plan MS only works if we "normalize" terms. Effectively, we represent 
     27terms via CHR constraints, "term reductions" are then performed via 
     28CHR solving steps. 
     29 
     30The big picture: 
     31 
     32Step 1 (normal form step): 
     33 
     34(a) We transform local and wanted type equations to CHR constraints.     
     35(b) We transform type instances to CHR simplification rules. 
     36 
     37Step 2 (solving step): 
     38 
     39To derive wanted from local type equations wrt type instances, 
     40we perform CHR solving steps. These CHR solving steps can be mapped 
     41to "term reduction" steps. 
     42 
     43 
     44The advantage of this method is that we can deal with 
     45"non-terminating" local type equations (see above) and 
     46"non-confluent" local type equations, e.g. 
     47S Int = Int /\ S Int = F Int, and we don't need to orient 
     48type equations. 
     49Of course, we need to impose the usual conditions on 
     50type instances, ie termination and confluence. 
     51 
     52=== CHR vs Term reductions === 
     53 
     54How to phrase term reduction steps in terms of CHR solving steps. 
     55The main task is to put terms into normal from. 
     56 
     57==== Normal form ===== 
     58 
     59Terms are formed as follows 
     60 
     61t ::= a        -- variable 
     62   |  F        -- type function constructor 
     63   |  T        -- ordinary type constructor 
     64   |  t t      -- type application 
     65 
     66Type equations are formed as follows 
     67 
     68Eq ::= t = t 
     69    |  Eq /\ Eq 
     70 
     71 
     72Type equations can easily be put into the following normal form 
     73 
     74n ::= a 
     75   |  T 
     76   |  n n 
     77 
     78C ::= a = n 
     79   |  F n = n 
     80   | C /\ C 
     81 
     82 
     83a set of type equations in normal form C, consists of equations of 
     84the form a = n or F n = n where the normal form type n does not refer  
     85to type function constructors. 
     86 
     87 
     88Example: 
     89 
     90The normal form of 
     91 
     92F (G Int) = Int      
     93G Int = F (G Int)   
     94 
     95from above is 
     96 
     97F a = Int 
     98G Int = a 
     99G Int = b 
     100F b = c 
     101G Int = c 
     102 
     103The first two equations are derived from F (G Int) = Int. That is, we  
     104replace G Int by a where a is a fresh wobbly variable. 
     105The last three equations result from replacing G Int on the rhs of 
     106G Int = F (G Int) by b which leads to G Int = F b, then we replace 
     107F b by c and we are done. 
     108 
     109NOTE: We consider a, b, c as wobbly type variables. 
     110 
     111 
     112Similarly, we build the normal form of type instances. 
     113For example, the normal form of 
     114 
     115forall a. F [a] = [F a] 
     116 
     117is 
     118 
     119forall a. exists b. F [a] = b /\ b=[F a] 
     120 
     121 
     122NOTE: 
     123 
     124We must build the normal form of type instances. Otherwise, application of 
     125type instances may break the normal form property. Eg. consider 
     126application of forall a. F [a] = [F a] 
     127on F [Int] = b /\ S Int = b. 
     128 
     129It should be clear that a normal form equation such as F a = Int, 
     130can be viewed as the CHR constraint F a Int, and 
     131forall a. exists b. F [a] = [b] /\ b=F a as 
     132the CHR simplification  
     133rule F [a] [b] <==> F a b 
     134 
     135 
     136==== Mapping CHR derivations to term derivations and vice versa ==== 
     137 
     138 
     139Let t1=t1' /\ .... /\ tk=tk' be a set of type equations and 
     140C its normal form. Let TT be a set of type instances and 
     141TT_n its normal form. 
     142 
     143We build a canonical form of t1=t1' /\ .... /\ tk=tk' 
     144by solving C wrt rules TT_n plus the standard FD rule, ie 
     145C -->* C'. This CHR derivation can be mapped to a term derivation 
     146t1=t1' /\ .... /\ tk=tk' -->* t1''=t1''' /\ ... /\ tl''=tl''' 
     147(ie a sequence of rule applications using the FC type equation rules).  
     148 
     149 
     150The CHR solving steps in detail: 
     151 
     152FD solving step: 
     153 
     154Let C \equiv C' /\ F n1 = n2 /\ F n1 = n3. 
     155 
     156Then, C --> C' /\ F n1 = n2 /\ n2 = n3 
     157 
     158In the above, we still use the (normal form) term representation. 
     159In the CHR constraint notation, the FD solving step is written 
     160 
     161       C' /\ F n1 n2 /\ F n1 n3 
     162-->    C  /\ F n1 n2 /\ n2 = n3 
     163 
     164The point is that the "actual" type equations only contain 
     165normal form types. 
     166 
     167This solving step can be mapped back to a term reduction step. 
     168Let t1''=t1''' /\ ... /\ tl''=tl''' be the term representation 
     169of C' /\ F n1 = n2 /\ n2 = n3 (ie we remove the wobbly variables 
     170we've introduced earlier in the normal form step). 
     171Then, 
     172 
     173t1=t1' /\ .... /\ tk=tk' --> t1''=t1''' /\ ... /\ tl''=tl''' 
     174 
     175this is now a term reduction step  
     176(using the type equation rules of the FC system) 
     177 
     178 
     179Type instance step: 
     180 
     181Let C \equiv C' /\ F n1 = n2 
     182 
     183and forall a. F n3 = n4 /\ C in TT_n such that 
     184phi(n3) = n1 for some substitution phi where dom(phi)=a. 
     185 
     186Then, C --> C' /\ phi(n4) = n2 /\ phi(C). 
     187 
     188As before, we also give the derivation in CHR constraint notation. 
     189     C' /\  F n1 n2 
     190-->  C' /\  phi(n4) = n2 /\ phi(C) 
     191 
     192This solving step can be mapped back to a term reduction step 
     193(a type instance application step). 
     194 
     195 
     196Equivalence step: 
     197 
     198The FD and type instance step introduce equations among normal form types. 
     199We build the mgu of these normal form equations (for this step it's 
     200helpful to use the CHR constraint notation). 
     201 
     202 
     203=== Plan MS revised details === 
     204 
     205Let TT be a set of type instances, 
     206C and W a set of constraints already in normal form where 
     207C are the local equations and W are the wanted equations. 
     208 
     209We check that W follows from C wrt TT as follows. 
     210 
     211We rewrite (C | W) to (C' | W') by performing the following steps. 
     212 
     213Reduce C step: 
     214Apply FD and CHR simp steps on C, ie C -->* C', we obtain 
     215 
     216      (C | W) --> (C' | W) 
     217 
     218Reduce W type instance step 
     219Apply CHR simp steps on W, ie W -->* W', we obtai 
     220 
     221 
     222      (C | W) --> (C | W') 
     223 
     224NOTE: we could also apply FD steps on W, no harm. 
     225 
     226Reduce W wrt C step: 
     227 
     228If C \equiv C' /\ F n1 = n2      and W \equiv F n1 = n3 /\ W' 
     229then 
     230 
     231      (C | W) --> (C | W' /\ n2 = n3) 
     232 
     233 
     234We exhaustively apply the above steps (if TT is terminating the steps 
     235are terminating). That is, 
     236 
     237(C | W) -->* (C' | W') 
     238 
     239then check if W' is a subset of C'. If yes, W follows from C wrt TT. 
     240 
     241NOTE: 
     242 
     243In the reduce W wrt C step, adding n2 = n3 to C as well is wrong. 
     244We could also first reduce C -->* C', then 
     245C' /\ W -->* C'' and check that C'' and C' are equivalent (by exploiting 
     246the fact that C implies W iff C <-> C /\ W). 
     247 
     248 
     249==== A note on efficiency ==== 
     250 
     251The normal from representation has the advantage that searching for 
     252"matchings" becomes "easier". Eg in case of the (earlier) plan MS and plan MC, 
     253given the local assumption S s1 ... sn = t we traverse/search all 
     254terms to find matching partners S s1 ... sn which then will be replaced by t. 
     255Consider the local G Int = Int and the term [Tree [G Int]] where we first 
     256traverse two list nodes and a tree node before we find the matching partner. 
     257In the normal from representation, we use a "flat" representation, all potential 
     258matchings must be at the "outer" level. We could even use hashing. That is, 
     259the local F a = Int is assigned the hash index F, so is the wanted 
     260constraint F a = Int (trivial example). When applying locals/type functions 
     261we'll only need to consider the entries with hash index F.     
     262 
     263 
     264==== A note on evidence construction ==== 
     265 
     266We yet need to formalize the exact details how to map CHR evidence back 
     267to term evidence. In fact, there's an issue. 
     268Consider the type equation (with evidence) 
     269 
     270e : F (G Int) = Int 
     271 
     272In the normal form representation, the above is represented as 
     273 
     274    e1 : F a = Int 
     275    e2 : G Int = a 
     276 
     277for some evidence e1 and e2. What's the connection between e and e1,e2? 
     278 
     279In case  e : F (G Int) = Int is wanted, the method outlined above 
     280will attempt to find evidence for e1 and e2. Given e1 and e2 we can then 
     281build evidence e. 
     282 
     283In case e : F (G Int) = Int is local (ie given), the normal form construction 
     284seems to be the wrong way around. Indeed, from e we can't necessarily build e1 and e2. 
     285Well, the method outlined here simply assumes that   
     286       e1 : F a = Int, e2 : G Int = a  
     287is the internal representation for 
     288       e : F (G Int) = Int 
     289 
     290NOTE: 
     291 
     292The user can of course use the more "compact" term representation of local assumptions, 
     293but internally we'll need to keep local assumptions in normal form. 
     294 
     295 
     296}}}