Pumping, with or Without Choice | SpringerLink
Skip to main content
Springer Nature Link
Log in

Pumping, with or Without Choice

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11893))

Included in the following conference series:

  • 591 Accesses

Abstract

We present the first machine-checked formalization of Jaffe and Ehrenfeucht, Parikh and Rozenberg’s (EPR) pumping lemmas in the Coq proof assistant. We formulate regularity in terms of finite derivatives, and prove that both Jaffe’s pumping property and EPR’s block pumping property precisely characterize regularity. We illuminate EPR’s classical proof that the block cancellation property implies regularity, and discover that—as best we can tell—their proof relies on the Axiom of Choice. We provide a new proof which eliminates the use of Choice. We explicitly construct a function which computes block cancelable languages from well-formed short languages.

Aquinas Hobor is supported in part by Yale-NUS College grant R-607-265-322-121. Elaine Li is supported in part by Runtime Verification, Inc. Frank Stephan is supported in part by MOE AcRF Tier 2 grant MOE2016-T2-1-019/R146-000-234-112. Authors are ordered alphabetically.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In our Coq development, we define block_cancellable_matching_with as the two-sided cancellation property, i.e. both L and L’s complement satisfy it, while block_cancellable_with refers to the one-sided cancellation (pumping) property. The same applies for the block pumping property.

  2. 2.

    We postpone discussion of why this condition works until Sect. 5.3.

References

  1. Almeida, J.C.B., Moreira, N., Perira, D., de Sousa, S.M.: Partial derivative automata formalized in Coq. In: The 15th International Conference on Implementation and Application of Automata, pp. 10:59–10:68 (2010)

    Chapter  Google Scholar 

  2. Banach, S., Tarski, A.: Sur la décomposition de ensebles de points en parties respectivement congruentes. Fundam. Math. 6, 244–277 (1924)

    Article  Google Scholar 

  3. Berardi, S., Bezem, M., Coquand, T.: On the computational content of the axiom of choice. J. Symbolic Logic 63(2), 600–622 (1998)

    Article  MathSciNet  Google Scholar 

  4. Chak, C.H., Freivalds, R., Stephan, F., Yik, H.T.W.: On block pumpable languages. Theore. Comput. Sci. (2016)

    Google Scholar 

  5. Chomsky, N.: On certain formal properties of grammars. Inf. Control 2(2), 137–167 (1959)

    Article  MathSciNet  Google Scholar 

  6. Chomsky, N., Schützenberger, M.P.: The algebraic theory of context free languages. Comput. Program. Formal Lang. (1963)

    Google Scholar 

  7. The Coq Development Team. The Coq Proof Assistant Reference Manual – Version8.10.0 (2019). http://coq.inria.fr

  8. Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988)

    Article  MathSciNet  Google Scholar 

  9. Coquand, T., Siles, V.: A decision procedure for regular expression equivalence in type theory. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 119–134. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25379-9_11

    Chapter  Google Scholar 

  10. Constable, R., Jackson, P.B., Naumov, P., Uribe, J.: Constructively formalizing automata theory. In: Proof, Language and Interaction (1998)

    Google Scholar 

  11. Diaconescu, R.: Axiom of choice and complementation. Proc. Am. Math. Soc. 51, 176–178 (1975)

    Article  MathSciNet  Google Scholar 

  12. Doczkal, C., Kaiser, J.-O., Smolka, G.: A constructive theory of regular languages in Coq. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 82–97. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03545-1_6

    Chapter  Google Scholar 

  13. Doczkal, C., Smolka, G.: Regular language representations in the constructive type theory of coq. J. Autom. Reasoning (2018)

    Google Scholar 

  14. Ehrenfeucht, A., Parikh, R., Rozenberg, G.: Pumping lemmas for regular sets. SIAM J. Comput. 10, 536–541 (1981)

    Article  MathSciNet  Google Scholar 

  15. Filliatre, J.-C.: Finite automata theory in Coq: a constructive proof of Kleene’s theorem. Ecole Normale Supérieure de Lyon Research Report (1997)

    Google Scholar 

  16. Van Heijenoort, J.: From Frege to Godel: A Source Book in Mathematical Logic, 1879–1931. Harvard University Press (1967)

    Google Scholar 

  17. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation, 3rd edn. Addison Wesley, Boston (2007)

    MATH  Google Scholar 

  18. Jaffe, J.: A necessary and sufficient pumping lemma for regular languages. ACM SIGACT News 10(2), 48–49 (1978)

    Article  MathSciNet  Google Scholar 

  19. Krauss, A., Nipkow, T.: Proof pearl: regular expression equivalence and relation algebra. J. Autom. Reasoning 49(1), 95–106 (2012)

    Article  MathSciNet  Google Scholar 

  20. Kreitz, C.: Constructive automata theory implemented with the Nuprl proof development system. Computer Science Technical Reports (1986)

    Google Scholar 

  21. Li, E.: Formalizing block pumpable language theory. Capstone Final Report for BSc. (Honours) in Mathematical, Computational and Statistical Sciences, Yale-NUS College (2019)

    Google Scholar 

  22. Martin-Löf, P.: An intuitionistic theory of types. Twenty-Five Years of Constructive Type Theory (1998)

    Google Scholar 

  23. Nerode, A.: Linear automaton transformations. Proc. Am. Math. Soc. 9(4), 541–544 (1958)

    Article  MathSciNet  Google Scholar 

  24. Nijholt, A.: An annotated bibliography of pumping. Bull. EATCS 17, 34–53 (1982)

    Google Scholar 

  25. Nipkow, T., Traytel, D.: Unified decision procedures for regular expression equivalence. Interact. Theorem Proving, 450–466 (2014)

    Google Scholar 

  26. Ramos, M.V.M., de Queiroz, R.J.G.B., Moreira, N., Almeida, J.C.B.: On the formalization of some results of context-free language theory. In: Väänänen, J., Hirvonen, Å., de Queiroz, R. (eds.) WoLLIC 2016. LNCS, vol. 9803, pp. 338–357. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-52921-8_21

    Chapter  MATH  Google Scholar 

  27. Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Studies in Logic (Mathematical logic and foundations) (2015). 978-1-84890-166-7

    Google Scholar 

  28. Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. s2(30), 264–286 (1930)

    Article  MathSciNet  Google Scholar 

  29. Sommerhalder, R.: Classes of languages proof against regular pumping. RAIRO Informatique théorique 14, 169–180 (1980)

    Article  MathSciNet  Google Scholar 

  30. Turing, A.M.: On computable numbers, with an application to the entscheidungsproblem: a correction. Proc. London Math. Soc. 43(6), 544–546 (1937)

    MathSciNet  MATH  Google Scholar 

  31. Varricchio, S.: A pumping condition for regular sets. SIAM J. Comput. 26(3), 764–771 (1997)

    Article  MathSciNet  Google Scholar 

  32. Wu, C., Zhang, X., Urban, C.: A formalisation of the myhill-nerode theorem based on regular expressions (proof pearl). In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 341–356. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_25

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Yale-NUS College, Singapore, Singapore

    Aquinas Hobor & Elaine Li

  2. School of Computing, National University of Singapore, Singapore, Singapore

    Aquinas Hobor & Frank Stephan

  3. Department of Mathematics, National University of Singapore, Singapore, Singapore

    Frank Stephan

Authors
  1. Aquinas Hobor
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elaine Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frank Stephan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Elaine Li .

Editor information

Editors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Anthony Widjaja Lin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Hobor, A., Li, E., Stephan, F. (2019). Pumping, with or Without Choice. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34175-6_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34174-9

  • Online ISBN: 978-3-030-34175-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics