Peter G. Harrison, R. Lyndon While
We apply algebraic transformation techniques to synthesise Horner's rule for polynomial evaluation. Horner's rule is then transformed into a pipeline by the application of further axioms. The syntheses demonstrate the power of the algebraic style, in which inductive proof is replaced by constructive unfolding and folding of standard higher-order functions defined on lists.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.