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 elements of a data structure x, find a subset which satisfies a certain property p and whose weightsum is maximum. Previously proposed methods for automatically generating linear-time algorithms are theoretically appealing, but the algorithms generated are hardly useful in practice due to a huge constant factor for space and time. The key points of our approach are to express the property p by a recursive boolean function over the structure x rather than a usual logical predicate and to apply program transformation techniques to reduce the constant factor. We present an optimization theorem, give a calculational strategy for applying the theorem, and demonstrate the effectiveness of our approach through several nontrivial examples which would be difficult to deal with when using the methods previously available.
|出版ステータス||Published - 2000 12 1|
|イベント||5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00) - Montreal, Que, Can|
継続期間: 2000 9 18 → 2000 9 21
|Other||5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00)|
|City||Montreal, Que, Can|
|Period||00/9/18 → 00/9/21|
ASJC Scopus subject areas