cps & contification

[Stephen Weeks]

Matthew, I finally sat down and carefully read your analysis.  Here's a summary
of your previous emails, as I understand them.

  Label = Func U Jump
  RCont = Label U {bot}
  REnv = Label -> RCont
  
  For every l in Label, there is a partial order <=l on RCont defined by
  	for all l' in Label, bot <=l l' 
  	for all l' in Label, if l <> l', then l' <=l l
  Under <=l, RCont is a flat lattice (with the obvious join).
  
  There is a partial order, <=, on REnv, defined by
  	G <= G' iff for all l in label, G(l) <=l G'(l)
  Under <= and pointwise join, REnv is a lattice.
  
  Program analysis:
  Anal[<fun fi (<xij>*) = ei>*] = fix (fn Gamma => V_i R[ei] Gamma'(fi))
   where Gamma' = Gamma V {ft |--> ft}
     and ft is the main function
  (fixed point necessary because top level CPS functions are mutually recursive)
  (initializing ft to "return to ft" marks the main function and ensures
  that bot really corresponds to no calls)
  
  Dec analysis:
  R[let fun k <xi>* = e in e']p = R[e]p' V Gamma
   where Gamma = R[e']p and p' = Gamma(k)
  R[let val x = s in e']p = R[e']p
  
  Transfer analysis:
  R[f (<xi>*)]p = {f |--> p}
  R[k (f (<xi>*))]p = {k |--> p} V {f |--> k}
  R[k (<xi>*)]p = {k -> p}
  R[<xi>*]p = {}
  R[case x of <Ci => ki>]p = V_i {ki |--> p}
  
  The notation <exp(i)>* indicates a list of expressions, indexed by i.
  The notation V_i indicates the join over all i.
  
  If Gamma = Anal[program]  and Gamma(l) = r  and  r <> l, r <> bot,
   then the function with label l has exactly one continuation 
   and is contifiable.
  Further, if Gamma(l) = bot, then the function with label l is never called.
  

Here's what I don't understand.  It seems to me that the function you're
attempting to take a fixed-point of is not monotone.  Lets call that function F.
	F = fn Gamma => V_i R[ei] Gamma'(fi)
Consider the following program.
	fun h () = ... K (i ()) ... L (f ()) ... 
	fun f () = g ()
	fun g () = 13
	fun i () = f ()
Define four elements (G0, G1, G2, G3) of REnv by the following table
		f	g	h	i
		---	---	---	---
	G0 	Bot	Bot	Bot	Bot
	G1 	L	Bot	h	K
	G2	f	L	h	K
	G3	f	f	h	K
Notice that
	F (G0) = G1
	F (G1) = G2
	F (G2) = G3
Notice also that
	G0 <= G1 and G1 <= G2 
But that G2 is not <= G3 because L is not <=g f.

That is, G1 <= G2 but F(G1) is not <= F(G2).

That is, F is not monotone.

The essential problem is that there are different orders on different components 
of REnv but that the tail call rule propagates from one component to another.
Hence, moving up in one component causes movement "sideways" in another.

So, I don't understand what the definition of your analysis is and what
fixed-point it is computing.  I glanced at your code, and noticed that there is
more than what I would usually expect in a least-fixed-point implementation.  I
would usually expect only a "lessThan" list and a value ref that is increasing
monotonically.  I see there is a lot more going on in your code, in particular a
moreThan list and repeated computations ("redo").

I am not saying I think the analysis is wrong at all.  I am just saying I don't
yet understand it.  I could probably get an operational understanding from
reading the code carefully and then reconstruct a more POPLesque description,
but I am hoping you can provide the latter.