Efficient Leftmost Unfolding with Ancestor Stacks

Abstract. The most successful unfolding rules used nowadays in partial evaluation of logic programs are based on well founded orders (wfo) or well quasi orders (wqo) applied over (covering) ancestors, i.e., a subsequence of the atoms selected during a derivation. The use of ancestor (sub)sequences improves the specialization power of unfolding while still guaranteeing termination and also reduces the number of atoms for which the wfo or wqo has to be checked. Unfortunately, maintaining the structure of the ancestor relation introduces a high operational cost during unfolding. In an attempt to facilitate the uptake of partial evaluation techniques, we herein present a very efficient unfolding based on the notion of covering ancestors which can be used in combination with any wfo or wqo as long as leftmost unfolding is performed, i.e., the leftmost atom of the goal is always selected for further unfolding. Our implementation technique is able to handle large unfolding trees more efficiently than existing state-ofthe-art partial evaluation systems. We believe that our approach makes well-known orderings, like homeomorphic embedding, more practically applicable.