Demand analysis with partial predicates

To alleviate the inefficiencies caused by the interaction of the logic and functional sides, integrated languages may take advantage of demand information, i.e. knowing in advance which computations are needed and, to which extent, in a particular context. This work studies demand analysis – which is closely related to backwards strictness analysis – in a semantic framework of partial predicates, which in turn are constructive realizations of ideals in a domain. This will allow us to give a concise, unified presentation of demand analysis, to relate it to other analyses based on abstract interpretation or strictness logics, some hints for the implementation, and, more important, to prove the soundness of our analysis based on demand equations. There are also some innovative results. One of them is that a set constraint-based analysis has been derived in a stepwise manner using ideas taken from the area of program transformation. The other one is the possibility of using program transformation itself to perform the analysis, specially in those domains of properties where algorithms based on constraint solving are too weak.

Local Computation of Simultaneous Fixed-Points

<!--DAIMI Standard Header Begin--> <p>We present a very simple, yet general algorithm for computing simultaneous, minimum fixed-points of monotonic functions, or turning the newpoint slightly, an algorithm for computing minimum solutions to a system of monotonic equations. The algorithm is local (demand-driven, lazy, ... ), i.e. it will try to determine the value of a single component in the simultaneous fixed-point by investigating only certain necessary parts of the description of the monotonic function, or in terms of the equational presentation, it will determine the value of a single variable by investigating only a part of the equational system.</p><p>In the worst-case this involves inspecting the complete system, and the algorithm will be a logarithmic factor worse than a global algorithm (computing the values of all variables simultaneously). But despite its simplicity the local algorithm has some advantages which promise much better performance on typical cases. The algorithm should be seen as a schema that for any particular application needs to be refined to achieve better efficiency, but the general mechanism remains the same. As such it seems to achieve performance comparable to, and for some examples improving upon, carefully designed <em>ad hoc</em> algorithms, still maintaining the benefits of being local.</p><p>We illustrate this point by tailoring the general algorithm to concrete examples in such (apparently) diverse areas as type inference, model checking, and strictness analysis. Especially in connection with the last example, strictness analysis, and more generally abstract interpretation, it is illustrated how the local algorithm provides a very minimal approach when determining the fixed-points, reminiscent of, but improving upon, what is known as Pending Analysis. In the case of model checking a specialised version of the algorithm has already improved on earlier known local algorithms.</p>