Formalizing the translation method in Agda

Abstract

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.

Ef P og Q eru mengi af fléttufræðilegum hlutum, þá gefur þýðingaraðferðin, sem sett var fram af Wood og Zeilberger (2009), umbreytingu á algebrulegri sönnun á jöfnunni |P| = |Q| í gagntæka vörpun á milli P og Q. Við gefum formlega útfærslu á þýðingaraðferðinni í forritunarmálinu Agda. Í samanburði við útfærsluna sem var áður gefin af Wood og Zeilberger, þá eru gagntæku varpanirnar sem eru framleiddar af okkar útfærslu formlega staðfestar, sem gerir okkar útfærslu stöðugri. Við nýtum okkur einnig að Agda getur veitt aðstoð við að útbúa sannanir, og gerum við notendum útfærslu okkar kleift að nota þá aðstöðu sem Agda veitir til þess. Sér í lagi er oft einfalt að undirbúa gamlar algebrulegar sannanir til notkunnar í útfærslu okkar.Við sönnum að segðirnar sem eru notaðar í útfærslunni okkar mynda víxlinn hálfbaug. Með þetta í huga útfærum við svokallaðan leysara fyrir hálfbauga, sem gerir notendum kleift að framkvæma þýðingaraðferðina sjálfvirkt á ákveðnar jöfnur. Við sýnum líka hvernig svokölluð afturköllunarferli, sem sett voru fram af Feldman og Propp (1995), geta verið nýtt til að gefa frádrætti, deilingu, og k-tu rótum þýðingu í þýðingaraðferðinni, og útfærum við afturköllunarferlið sem samsvarar frádrætti. Að lokum gefum við heimspekilega umfjöllun um hvernig þýðingaraðferðin virkar, og notum það til að telja fjölda "náttúrulegra" gagntækra varpana fyrir jöfnu sem var skoðuð af Wood og Zeilberger.