Make it practical: A generic linear-time algorithm for solving maximum-weightsum problems

In this paper we propose a new method for deriving a practical linear-time algorithm from the specification of a maximum-weightsum problem: From the e lements of a data structure x, find a subset which satisfies a certain prop erty p and whose weightsum is maximum. Previously proposed methods for auto matically generating linear-time algorithms are theoretically appealing, bu t the algorithms generated are hardly useful in practice due to a huge cons tant factor for space and time. The key points of our approach are to expre ss the property p by a recursive boolean function over the structure x rath er than a usual logical predicate and to apply program transformation techn iques to reduce the constant factor. We present an optimization theorem, gi ve a calculational strategy for applying the theorem, and demonstrate the e ffectiveness of our approach through several nontrivial examples which woul d be difficult to deal with when using the methods previously available.