/ 19
Table of contents

Document in text mode:

Pumping, With or Without Choice?Aquinas Hobor1 2, Elaine Li1, and Frank Stephan2 31 Yale-NUS [email protected] School of Computing, National University of Singapore{hobor, fstephan}@comp.nus.edu.sg3 Department of Mathematics, National University of SingaporeAbstract. We present the first machine-checked formalization of Jaffeand Ehrenfeucht, Parikh and Rozenberg’s (EPR) pumping lemmas in theCoq proof assistant. We formulate regularity in terms of finite derivatives,and prove that both Jaffe’s pumping property and EPR’s block pumpingproperty precisely characterize regularity. We illuminate EPR’s classicalproof that the block cancellation property implies regularity, and discoverthat—as best we can tell—their proof relies on the Axiom of Choice. Weprovide a new proof which eliminates the use of Choice. We explicitlyconstruct a function which computes block cancelable languages fromwell-formed short languages.Keywords: Pumping lemmas · Axiom of Choice · Coq1 OverviewPum...