Journal of Functional Programming

Functional pearls

FUNCTIONAL PEARL Derivation of a logarithmic time carry lookahead addition circuit

a1 Computing Science Department, University of Glasgow, Glasgow G12 8QQ, UK (email: [email protected])
a2 Department of Computer Science, Chemnitz University of Technology, 09107 Chemnitz, Germany (email: [email protected])

Article author query
o'donnell jt   [Google Scholar] 
runger g   [Google Scholar] 


Using Haskell as a digital circuit description language, we transform a ripple carry adder that requires $O(n)$ time to add two $n$-bit words into a parallel carry lookahead adder that requires $O(\log n)$ time. The ripple carry adder uses a scan function to calculate carry bits, but this scan cannot be parallelized directly since it is applied to a non-associative function. Several techniques are applied in order to introduce parallelism, including partial evaluation and symbolic function representation. The derivation given here constitutes a semi-formal correctness proof, and it also brings out explicitly each of the ideas underlying the algorithm.