
From:  Paul F. Dietz 
Subject:  [Gcldevel] Re: Looking for a good type propagation algorithm 
Date:  Sat, 17 Sep 2005 20:21:12 0500 
Useragent:  Mozilla/5.0 (X11; U; Linux i686; enUS; rv:1.7.11) Gecko/20050729 
Camm Maguire wrote:
Greetings! As many may know, GCL autodeclares constant let bindings, and this allows for many optimizations to proceed. We could also autodeclare bindings which are changed, but changed to a subtype of the original type, let alone autodeclaring loop counters afterchecking loop bounds, etc.The problem is that I cannot think of a decent algorithm which is not exponential in the let form nesting. I.e., start by setting the variable types to the type of the initializing form in the outermost let, then using these settings, do likewise for all sublets, until one hits the setq, at which point one can determine whether the setq preserves the type. Otherwise, mark the type as t (could alternatively iterate with `(or ,type ,setqtype)), and then process the outer let for real. The outermost let is processed twice, the next innermost four times, etc. Anyone know of a better algorithm? I was thinking about just one pass, and building up a network of linked typesetter functions as you go, but this appears too ambitious at present.
You might be thinking of something like Abstract Interpretation. In this technique, the values that some program constract may have are approximated by some element of a lattice of finite height. When a variable can have more than one possible value, the lattice element is the join (least upper bound) of the lattice elements for those values. If there are n such values (corresponding to the variables and forms of the program, say), you get a set of equations of the form v_i = \/ f_{i,j}(v_1,...,v_n) where f_{i,j} is a function on the lattice values that is continuous in the lattice (that is, moving one of its arguments up in the lattice causes the value of the function to either remain the same or also move up.) The fixpoint of this system of equations can be found in O(n height(L)) function evaluations, where height(L) is the height of the lattice, by the obvious algorithm of starting variables with bottom values and propagating changes around the graph. In our case, the lattice would be some approximation of Lisp's type system, since lisps full type system is not finitely high (and even limited integer subrange types would lead to exponentially high lattices.) Paul
[Prev in Thread]  Current Thread  [Next in Thread] 