Deriving the Fast Fourier Algorithm by Calculation

This paper reports an explanation of an intricate algorithm in the terms of a potentially mechanisable rigorous-development method. It uses notations and techniques of Sheeran 1] and Bird and Meertens 2, 3]. We have claimed that these techniques are applicable to digital signal processing circuits, and have previously applied them to regular array circuits 4, 5, 6]. This paper shows that they can deal with an apparently very di erent and more complex algorithm: the fast Fourier transform. Similar papers to this one 7, 8, 9] perform most of the same calculations, but experiment with di erent ways of expressing the algorithms and their development. Twenty- ve years ago Cooley and Tukey rediscovered an optimising technique usually attributed to Gauss, who used it in hand calculation. They applied the technique to the discrete Fourier transform, reducing an apparently O(n2) problem to the almost instantly ubiquitous O(nlogn) `fast Fourier transform' 10]. The fast Fourier transform is...

• Type: Conference
• Year: 1989
• Where: FP
• Authors: Geraint Jones
• Keywords: Di Erent Transform, Discrete Fourier Transform, Fast Fourier Transform, Formal Methods, FP 1989