Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMSRevised

Jan 1, 2007 10:01:33 PM (9 years ago)



  • TypeFunctionsSynTC/PlanMSRevised

    v1 v1  
     4=== Problem with Plan MS: Termination is still an issue === 
     8F and G are type function constructors. Consider the local assumptions 
     10F (G Int) = Int    -- (1)  
     11G Int = F (G Int)  -- (2) 
     13Applying (2) on (1) yields 
     15    F (G Int) = Int 
     16--> F (F (G Int)) = Int 
     17--> F (F (F (G Int))) = Int 
     18--> ... 
     21Plan MC rejects (2), cause the type equation is non-decreasing. 
     22Here we are after a more liberal type checking method. 
     24=== Plan MS revised overview === 
     26Plan MS only works if we "normalize" terms. Effectively, we represent 
     27terms via CHR constraints, "term reductions" are then performed via 
     28CHR solving steps. 
     30The big picture: 
     32Step 1 (normal form step): 
     34(a) We transform local and wanted type equations to CHR constraints.     
     35(b) We transform type instances to CHR simplification rules. 
     37Step 2 (solving step): 
     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. 
     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. 
     52=== CHR vs Term reductions === 
     54How to phrase term reduction steps in terms of CHR solving steps. 
     55The main task is to put terms into normal from. 
     57==== Normal form ===== 
     59Terms are formed as follows 
     61t ::= a        -- variable 
     62   |  F        -- type function constructor 
     63   |  T        -- ordinary type constructor 
     64   |  t t      -- type application 
     66Type equations are formed as follows 
     68Eq ::= t = t 
     69    |  Eq /\ Eq 
     72Type equations can easily be put into the following normal form 
     74n ::= a 
     75   |  T 
     76   |  n n 
     78C ::= a = n 
     79   |  F n = n 
     80   | C /\ C 
     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. 
     90The normal form of 
     92F (G Int) = Int      
     93G Int = F (G Int)   
     95from above is 
     97F a = Int 
     98G Int = a 
     99G Int = b 
     100F b = c 
     101G Int = c 
     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. 
     109NOTE: We consider a, b, c as wobbly type variables. 
     112Similarly, we build the normal form of type instances. 
     113For example, the normal form of 
     115forall a. F [a] = [F a] 
     119forall a. exists b. F [a] = b /\ b=[F a] 
     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. 
     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 
     136==== Mapping CHR derivations to term derivations and vice versa ==== 
     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. 
     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).  
     150The CHR solving steps in detail: 
     152FD solving step: 
     154Let C \equiv C' /\ F n1 = n2 /\ F n1 = n3. 
     156Then, C --> C' /\ F n1 = n2 /\ n2 = n3 
     158In the above, we still use the (normal form) term representation. 
     159In the CHR constraint notation, the FD solving step is written 
     161       C' /\ F n1 n2 /\ F n1 n3 
     162-->    C  /\ F n1 n2 /\ n2 = n3 
     164The point is that the "actual" type equations only contain 
     165normal form types. 
     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). 
     173t1=t1' /\ .... /\ tk=tk' --> t1''=t1''' /\ ... /\ tl''=tl''' 
     175this is now a term reduction step  
     176(using the type equation rules of the FC system) 
     179Type instance step: 
     181Let C \equiv C' /\ F n1 = n2 
     183and forall a. F n3 = n4 /\ C in TT_n such that 
     184phi(n3) = n1 for some substitution phi where dom(phi)=a. 
     186Then, C --> C' /\ phi(n4) = n2 /\ phi(C). 
     188As before, we also give the derivation in CHR constraint notation. 
     189     C' /\  F n1 n2 
     190-->  C' /\  phi(n4) = n2 /\ phi(C) 
     192This solving step can be mapped back to a term reduction step 
     193(a type instance application step). 
     196Equivalence step: 
     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). 
     203=== Plan MS revised details === 
     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. 
     209We check that W follows from C wrt TT as follows. 
     211We rewrite (C | W) to (C' | W') by performing the following steps. 
     213Reduce C step: 
     214Apply FD and CHR simp steps on C, ie C -->* C', we obtain 
     216      (C | W) --> (C' | W) 
     218Reduce W type instance step 
     219Apply CHR simp steps on W, ie W -->* W', we obtai 
     222      (C | W) --> (C | W') 
     224NOTE: we could also apply FD steps on W, no harm. 
     226Reduce W wrt C step: 
     228If C \equiv C' /\ F n1 = n2      and W \equiv F n1 = n3 /\ W' 
     231      (C | W) --> (C | W' /\ n2 = n3) 
     234We exhaustively apply the above steps (if TT is terminating the steps 
     235are terminating). That is, 
     237(C | W) -->* (C' | W') 
     239then check if W' is a subset of C'. If yes, W follows from C wrt TT. 
     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). 
     249==== A note on efficiency ==== 
     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.     
     264==== A note on evidence construction ==== 
     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) 
     270e : F (G Int) = Int 
     272In the normal form representation, the above is represented as 
     274    e1 : F a = Int 
     275    e2 : G Int = a 
     277for some evidence e1 and e2. What's the connection between e and e1,e2? 
     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. 
     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 
     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.