: Bjarki Ágúst Guðmundsson (MSc thesis)
If P and Q are sets of combinatorial objects, the translation method, introduced by Wood and Zeilberger (2009), allows one to turn an algebraic proof of the identity |P| = |Q| into a bijection between P and Q. We give a formalized implementation of the translation method in the programming language Agda. In contrast to the implementation previously given by Wood and Zeilberger, the bijections produced by our implementation are formally verified, making our implementation more robust. We also take advantage of the fact that Agda is a proof assistant, allowing users of our implementation to use the existing facilities provided by Agda for developing proofs. In particular, converting an existing algebraic proof for use in our implementation is often straightforward.
We prove that the expressions used in our implementation form a commutative semiring. Based on this we implement a semiring solver, allowing one to apply the translation method automatically to certain identities. We also show how cancellation procedures, introduced by Feldman and Propp (1995), can be used to give meaning to subtraction, division and k-th roots in the translation method, and we implement the cancellation procedure that represents subtraction. Finally we give a philosophical discussion about the inner workings of the translation method, and use that to count the number of “natural” bijections for an identity considered by Wood and Zeilberger.
See source code at GitHub.
Defended at Reykjavík University, Iceland, June 2017 by Bjarki Ágúst Guðmundsson (PDF)