Much ado about two (pearl): a pearl on parallel prefix computation

ABSTRACT

This pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0-1 is not quite enough here. The perfect hammer for the nails we are going to drive in is relational parametricity.

REFERENCES

• 1: G. E. Blelloch. Prefix sums and their applications. In J. H. Reif, editor, Synthesis of Parallel Algorithms, pages 35--60. Morgan Kaufmann, 1993.
• 2: S. Böhme. Free theorems for sublanguages of Haskell. Master's thesis, Technische Universität Dresden, 2007a.
• 3: S. Böhme. Much ado about two. Formal proof development. In G. Klein, T. Nipkow, and L. Paulson, editors, The Archive of Formal Proofs. http://afp.sf.net/entries/MuchAdoAboutTwo.shtml, 2007b.
• 4: A. Bove and T. Coquand. Formalising bitonic sort in type theory. In Types for Proofs and Programs, TYPES 2004, Revised Selected Papers, volume 3839 of LNCS, pages 82--97. Springer-Verlag, 2006.
• 5: R. P. Brent , H. T. Kung, The chip complexity of binary arithmetic, Proceedings of the twelfth annual ACM symposium on Theory of computing, p.190-200, April 28-30, 1980, Los Angeles, California, United States [doi>10.1145/800141.804666]
• 6: Nils Anders Danielsson , John Hughes , Patrik Jansson , Jeremy Gibbons, Fast and loose reasoning is morally correct, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.206-217, January 11-13, 2006, Charleston, South Carolina, USA
• 7: N. A. Day, J. Launchbury, and J. Lewis. Logical abstractions in Haskell. In Haskell Workshop, Proceedings. Technical Report UU--CS--1999--28, Utrecht University, 1999.
• 8: P. Dybjer, Q. Haiyan, and M. Takeyama. Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology, 46(15):1011--1025, 2004.
• 9: Jeremy Gibbons , Graham Hutton, Proof Methods for Corecursive Programs, Fundamenta Informaticae, v.66 n.4, p.353-366, December 2005
• 10: R. Hinze. An algebra of scans. In Mathematics of Program Construction, Proceedings, volume 3125 of LNCS, pages 186--210. Springer--Verlag, 2004.
• 11: Patricia Johann , Janis Voigtländer, Free theorems in the presence of seq, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.99-110, January 14-16, 2004, Venice, Italy
• 12: Simon Knowles, A Family of Adders, Proceedings of the 15th IEEE Symposium on Computer Arithmetic, p.277, June 11-13, 2001
• 13: Donald E. Knuth, The art of computer programming, volume 3: (2nd ed.) sorting and searching, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1998
• 14: Richard E. Ladner , Michael J. Fischer, Parallel Prefix Computation, Journal of the ACM (JACM), v.27 n.4, p.831-838, Oct. 1980 [doi>10.1145/322217.322232]
• 15: Yen-Chun Lin , Jun-Wei Hsiao, A new approach to constructing optimal parallel prefix circuits with small depth, Journal of Parallel and Distributed Computing, v.64 n.1, p.97-107, January 2004 [doi>10.1016/j.jpdc.2003.09.004]
• 16: T. Lynch and E. Swartzlander. The redundant cell adder. In Computer Arithmetic, Proceedings, pages 165--170. IEEE Press, 1991.
• 17: T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer-Verlag, 2002.
• 18: S. L. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003.
• 19: J. C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing, Proceedings, pages 513--523. Elsevier Science Publishers B. V., 1983.
• 20: M. Sheeran. Finding regularity: Describing and analysing circuits that are not quite regular. In Correct Hardware Design and Verification Methods, Proceedings, volume 2860 of LNCS, pages 4--18. Springer-Verlag, 2003.
• 21: M. Sheeran. Hardware design and functional programming: a perfect match. Journal of Universal Computer Science, 11(7):1135--1158, 2005.
• 22: M. Sheeran. Searching for prefix networks to fit in a context using a lazy functional programming language. Talk at Hardware Design and Functional Languages, 2007.
• 23: J. Sklansky. Conditional-sum addition logic. IRE Transactions on Electronic Computers, EC-9(6):226--231, 1960.
• 24: H. S. Stone and P. M. Kogge. A parallel algorithm for the efficient solution of a general class of recurrence equations. IEEE Transactions on Computers, 22(8):786--793, 1973.
• 25: Philip Wadler, Theorems for free!, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.347-359, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99404]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Algorithms, Languages, Verification

Keywords:
0-1-principle, free theorems, parallel prefix computation, relational parametricity