Master Thesis Defense: Peter Urbak - A Formal Study of Moessner's Sieve
Info about event
Time
Location
Turing-230
Organizer
Title:
A Formal Study of Moessner's Sieve
Abstract:
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).