Implementation Notes for the Termination-Guaranteeing Binding-Time Analysis

This note describes some of the implementation aspects of the termination analysis for partial evaluation described by Glenstrup and Jones (2003). 1 Algorithm overview Figure 1 gives an overview of the modules that constitute the termination analysis for partial evaluation. Note that the call graph is only needed for efficiency. When bounded anchoring has determined a set of specialisation points, the standard BTA and bounded anchoring must be reiterated because a static function call may have become dynamic due to the specialisation point. Thus more variables may need to be reclassified from static to dynamic, which in turn may invalidate anchors and cause bounded anchoring to make more variables dynamic. 2 Algorithm modules In the following sections we will briefly describe all the modules of the algorithm except the standard BTA which can be found in the literature (Jones et al., 1993; Christensen et al., 2000; Thiemann, 1997, 1999; Henglein, 1991). 2.1 Call graph generator This module generates a graph with p’s functions as nodes and an edge f − → g whenever the body of f contains a function call to g. Using an algorithm for grouping graph nodes into strongly connected components (SCCs) and sorting the resulting SCC DAG topologically (Cormen et al., 1990), it should be possible to implement SCC generation and sorting in time O ( f + s) where f is the number of functions and s the number of call sites in p. 2.2 Decreasing size approximation generator E ↓ The decreasing expression size approximation operator E ↓ is shown in Figure 2. The first argument, to E ↓ e is a fixpoint φ computed by applying a fixpoint operator fix to a function F such that F φ = φ. In general a fixpoint operator can be implemented by fix F = fix ′ F ⊥φ fix ′ F φ = if φ = F φ then φ else fix ′ F (F φ) where ⊥φ is the bottom element of the domain of F. The problem is how to compute the expression φ = F φ because both sides of the equation are functions