A Formal Study of Moessner's Sieve

In this dissertation, we present a new characterization of Moessner's sieve that brings a range of new results with it. As such, we present a dual to Moessner's sieve that generates a sequence of so-called Moessner triangles, instead of a traditional sequence of successive powers, where each triangle is generated column by column, instead of row by row. Furthermore, we present a new characteristic function of Moessner's sieve that calculates the entries of the Moessner triangles generated by Moessner's sieve, without having to calculate the prefix of the sequence.
We prove Moessner's theorem adapted to our new dual sieve, called Moessner's idealized theorem, where we generalize the initial configuration from a sequence of natural numbers to a seed tuple containing just one non-zero entry. We discover a new property of Moessner's sieve that connects Moessner triangles of different rank, thus acting as a dual to the existing relation between Moessner triangles of different index, thereby suggesting the presence of a 2-dimensional grid of triangles, rather than the traditional 1-dimensional sequence of values.
We adapt Long's theorem to the dual sieve and obtain a simplified initial configuration of Long's theorem, consisting of a seed tuple of two non-zero entries. We conjecture a new generalization of Long's theorem that has a seed tuple of arbitrary entries for its initial configuration and connects Moessner's sieve with polynomial evaluation. Lastly, we approach the connection between Moessner's sieve and polynomial evaluation from an alternative perspective and prove an equivalence relation between the triangle creation procedures of Moessner's sieve and the repeated application of Horner's method for polynomial division.
All results presented in this dissertation have been formalized in the Coq proof assistant and proved using a minimal subset of the constructs and tactics available in the Coq language. As such, we demonstrate the potential of proof assistants to inspire new results while lowering the gap between programs (in computer science) and proofs (in mathematics).

Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant

reference manual–version 7.2. Technical Report 255, INRIA, Paris, 2002. (Cited on pages 11 and 16.)

Yves Bertot. Filters on CoInductive Streams, an Application to Eratosthenes’ Sieve. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, volume 3461 of Lecture Notes in Computer Science, pages 102–115. Springer, Heidelberg, 2005. (Cited on page 11.)

Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq’Art: the Calculus of Inductive Constructions. Springer, Heidelberg, 2004. (Cited on pages 11 and 16.)

Mark Bickford, Dexter Kozen, and Alexandra Silva. Formalizing Moessner’s theorem in Nuprl. http://www.nuprl.org/documents/Moessner/, August 2011. (Cited on page 10.)

Mark Bickford, Dexter Kozen, and Alexandra Silva. Formalizing Moessner’s Theorem and Generalizations in Nuprl. In Ralph Matthes and Aleksy Schubert, editors, Types 2013 Post-proceedings, pages 1–7. Leibniz International Proceedings in Informatics, 2013. (Cited on page 10.)

Florian Cajori. Horner’s method of approximation anticipated by Ruffini. Bulletin of the American Mathematical Society, 17(8):409–414, November 1911. (Cited on pages 9 and 127.)

Christian Clausen, Olivier Danvy, and Moe Masuko. A characterization of Moessner’s sieve. Theoretical Computer Science, 2014. DOI: 10.1016/j.tcs.2014.03.012. (Cited on pages 11, 13, 45, 69, and 164.)

Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and computation, 76(2):95–120, 1988. (Cited on page 16.)

Haskell Brooks Curry, Robert Feys, William Craig, J Roger Hindley, and Jonathan P Seldin. Combinatory logic, volume 2. North-Holland Amsterdam, 1972. (Cited on page 16.)

Peter Fox. Cambridge University Library: the great collections. Cambridge University Press, 1998. (Cited on page 52.)

George Gonthier. Formal proof – the four-color theorem. Notices of the AMS, 55(11):1382–1393, December 2008. (Cited on page 16.)

Ronald L. Graham, Donald E. Knuth, and Oren Patashnik. Concrete Mathematics. Addison-Wesley Publishing Company, 1989. (Cited on page 10.)

Tian-Xiao He and Peter J.-S. Shiue. A Note on Horner’s Method. Journal of Concrete and Applicable Mathematics, 10(1):53, January 2012. (Cited on pages 127 and 148.)

Ralf Hinze. Concrete Stream Calculus: An extended study. Journal of Functional Programming, 20(5-6):463–535, 2010. (Cited on pages 12, 46, and 68.)

Ralf Hinze. Scans and Convolutions - A Calculational Proof of Moessner’s Theorem. In Sven-Bodo Scholz and Olaf Chitil, editors, Implementation and Application of Functional Languages, 20th International Workshop, IFL 2008, number 5836 in Lecture Notes in Computer Science, pages 1–24. Springer, Hatfield, UK, September 2011. (Cited on pages 12 and 59.)

William G. Horner. A new method of solving numerical equations of all orders, by continuous approximation. Philosophical Transactions of the Royal Society of London, 109:308–335, 1819. (Cited on pages 9, 127, and 129.)

Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The Power of Parameterization in Coinductive Proof. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 193–206. ACM, 2013. (Cited on page 19.)

Dexter Kozen and Alexandra Silva. On Moessner’s Theorem. Technical report, Computing and Information Science, Cornell University, June 2011. (Cited on page 10.)

Robert Krebbers, Louis Parlant, and Alexandra Silva. Moessner’s Theorem: an exercise in coinductive reasoning in Coq, 2013. (Cited on pages 11 and 13.)

Christoph Kreitz. The Nuprl Proof Development System, Version 5: Reference Manual and User’s Guide. Department of Computer Science, Cornell University, 2002. (Cited on page 10.)

Xavier Leroy. The CompCert C Verified Compiler, 2012. (Cited on page 16.)

Calvin T. Long. On the Moessner Theorem on Integral Powers. The American Mathematical Monthly, 73(8):846–851, 1966. (Cited on pages 7, 12, 13, 40, 46, 59, 68, and 114.)

Calvin T. Long. Mathematical Excitement - The Most Effective Motivation. The Mathematics Teacher, 75(5):413–415, 1982. (Cited on pages 9 and 13.)

Calvin T. Long. Strike it out: Add it up. The Mathematical Gazette, 66(438):273–277, 1982. (Cited on page 8.)

Calvin T. Long. A Note on Moessner’s Process. The Fibonacci Quarterly, 24(4):349–356, November 1986. (Cited on page 8.)

Alexander Markowich Ostrowski. On Two Problems in Abstract Algebra Connected with Horner’s Rule. In Studies in Mathematics and Mechanics presented to Richard von Mises, pages 40–48, New York, 1954. (Cited on pages 128 and 129.)

Alfred Moessner. Eine Bemerkung über die Potenzen der natürlichen Zahlen. Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 29(3):9, March 1951. (Cited on pages 1, 6, and 164.)

Milad Niqui and Jan J.M.M. Rutten. Sampling, Splitting and Merging in Coinductive Stream Calculus. In Mathematics of Program Construction, pages 310–330. Springer, 2010. (Cited on page 10.)

Milad Niqui and Jan J.M.M. Rutten. A proof of Moessner’s theorem by coinduction. Higher-Order and Symbolic Computation, 24(3):191–206, 2011. (Cited on pages 11, 12, and 13.)

Milad Niqui and Jan J.M.M. Rutten. An exercise in coinduction: Moessner’s theorem. Technical Report 1103, CWI Amsterdam, 2011. (Cited on pages 11 and 12.)

Milad Niqui and Jan J.M.M. Rutten. Stream processing coalgebraically. Science of Computer Programming, 78(11):2192–2215, 2013. (Cited on page 10.)

Ivan Paasche. Ein neuer Beweis der Moessnerschen Satzes. Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 30(1):1–5, Feburary 1952. (Cited on page 7.)

Alex Pathan and Tony Collyer. The wonder of Horner’s method. The Mathematical Gazette, 87(509):230 242, July 2003. (Cited on pages 127, 137, and 148.)

Oskar Perron. Beweis des Moessnerschen Satzes. Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematischnaturwissenschaftliche Klasse, 29(4):31–34, May 1951. (Cited on page 7.)

Karel A. Post. Moessnerian theorems. How to prove them by simple graph theoretical inspection. Elemente der Mathematik, (2):46–51, 1990. (Cited on page 10.)

Charles L. Rino. A Mathematical Tour of Babbage Difference Engine No. 2. http://chuckrino.com/wordpress/wp-content/uploads/2011/05/BabbageDE2NotesVER1.pdf, November 2011. (Cited on page 148.)

Jan J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. (Cited on page 10.)

Jan J.M.M. Rutten. A coinductive calculus of streams. Mathematical Structures in Computer Science, 15(1):93–147, 2005. (Cited on pages 10 and 28.)

Jan J.M.M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs. Theoretical Computer Science, 343(3):443–481, 2005. (Cited on page 12.)

Hans Salié. Bemerkung zu einem Satz von A. Moessner. Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften, Mathematisch-naturwissenschaftliche Klasse, 30(2):7–11, Februray 1952. (Cited on page 7.)

Saed Samadi, M. Omair Ahmad, and M. N. S. Swamy. Multiplier-Free Structures for Exact Generation of Natural Powers of Integers. In International Symposium on Circuits and Systems (ISCAS 2005), pages 1146–1149, Kobe, Japan, May 2005. IEEE. (Cited on page 10.)

John G. Slater. Strike it out - some exercises. The Mathematical Gazette, 67(442):288–290, 1983. (Cited on page 8.)

The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. (Cited on page 16.)

Jan van Yzeren. A Note on an Additive Property of Natural Numbers. The American Mathematical Monthly, 66(1):53–54, January 1959. (Cited on pages 9, 13, and 140.)

Victor Ya Pan. Methods of computing values of polynomails. Russian Mathematical Surveys, 21(1):105, 1966. (Cited on pages 128 and 129.)