Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMSRevised

Jan 1, 2007 10:01:33 PM (11 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.