Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMSRevised


Ignore:
Timestamp:
Jan 1, 2007 10:01:33 PM (9 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}}}