Changes between Initial Version and Version 1 of TypeFunctionsSynTC/PlanMSRevised

Show
Ignore:
Timestamp:
01/01/07 14:01:33 (6 years ago)
Comment:

--

Unmodified
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}}}