×

A note on rewriting proofs and Fibonacci numbers. (English) Zbl 1133.05006

Artemov, Sergei N. (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2007, New York, NY, USA, June 4–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72732-3/pbk). Lecture Notes in Computer Science 4514, 284-292 (2007).
Summary: One basic activity in combinatorics is to establish combinatorial identities by so-called ‘bijective proofs,’ which amounts to constructing explicit bijections between two types of the combinatorial objects in question.
The aim of this paper is to show how techniques from the formal logic world can be applied directly to such problems studied completely independently in the world of combinatorics.
The basic idea is to characterize equinumerous partition ideals in terms of the minimal elements generating the order filters, the complements to the original ideals.
For the case where the minimal elements of each of these order filters are disjoint, we have developed a general automated method to remove the mystery of certain known results and establish new results in the theory of integer partitions: M. Kanovich [“Finding direct partition bijections by two-directional rewriting techniques”, Discrete Math. 285, No. 1–3, 151–166 (2004; Zbl 1044.05010 )], and M. Kanovich [“The two-way rewriting in action: Removing the mystery of Euler-Glaisher’s map”, Discrete Math. 307, No. 15, 1909–1935 (2007; Zbl 1124.05007)].
Here we address the case of filters having overlapping minimal elements. Essentially this is a case study related to the Fibonacci numeration system.
In addition to a ‘bijective proof’ for Zeckendorf’s theorem – that every positive integer is uniquely representable within the Fibonacci numeration system – we establish ‘bijective proofs’ for a new series of partition identities related to Fibonacci and Lucas numbers.
The main result is proved using the idea of filter supports, and rewriting systems on multisets having overlapping patterns.
The main technical step is a suitable construction of such a rewriting system and then a proof that this rewriting system and the system consisting of its reverse rewriting rules, both have the Church-Rosser property, with providing the bijections we are looking for.
For the entire collection see [Zbl 1121.03005].

MSC:

05A17 Combinatorial aspects of partitions of integers
05A20 Combinatorial inequalities
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI