SpringerLink
Log in

System Description: A Theorem-Prover for Subregular Systems: The Language Toolkit and Its Interpreter, Plebby

  • Conference paper
Functional and Logic Programming (FLOPS 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14659))

Included in the following conference series:

  • 122 Accesses

Abstract

We introduce here a domain-specific language, PLEB. The Piecewise-Local Expression Builder interpreter (plebby) is an interactive system for defining, manipulating, and classifying regular formal languages. The interactive theorem-proving environment provides a generalization of regular expressions with which one can intuitively construct languages via constraints. These constraints retain their semantics upon extension to larger alphabets. The system allows one to decide implications and equalities, either at the language level (with a specified alphabet) or at the logical level (across all possible alphabets). Additionally, one can decide membership in a number of predefined classes, or arbitrary algebraic varieties. With several views of a language, including multiple algebraic structures, the system provides ample opportunity to explore and understand properties of languages.

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
EUR 32.99 /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
EUR 29.95
Price includes VAT (Thailand)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 55.63
Price includes VAT (Thailand)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 64.99
Price excludes VAT (Thailand)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    At https://github.com/vvulpes0/Language-Toolkit-2/tree/develop one finds the latest unstable version of the software, and full stable releases can be found at https://hackage.haskell.org/package/language-toolkit.

  2. 2.

    In ascii, the word boundaries are %| (left) and |% (right), while angle-brackets are represented by less-than and greater-than signs. Other equivalences are given in Table 2 on page 302.

  3. 3.

    Available at https://hackage.haskell.org/package/finite-semigroups.

  4. 4.

    Available at https://github.com/vvulpes0/amalgam.

References

  1. Allauzen, C., Riley, M., Schalkwyk, J., Skut, W., Mohri, M.: OpenFst: a general and efficient weighted finite-state transducer library. In: Holub, J., Ždárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 11–23. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-76336-9_3

    Chapter  Google Scholar 

  2. Beauquier, D., Pin, J.-E.: Factors of words. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 63–79. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0035752

    Chapter  Google Scholar 

  3. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964). https://doi.org/10.1145/321239.321249

    Article  MathSciNet  Google Scholar 

  4. Brzozowski, J.A., Simon, I.: Characterizations of locally testable events. Discret. Math. 4(3), 243–271 (1973). https://doi.org/10.1016/S0012-365X(73)80005-6

    Article  MathSciNet  Google Scholar 

  5. Caron, P.: LANGAGE: a maple package for automaton characterization of regular languages. In: Wood, D., Yu, S. (eds.) WIA 1997. LNCS, vol. 1436, pp. 46–55. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0031380

    Chapter  Google Scholar 

  6. Carpenter, B.: The Logic of Typed Feature Structures. Cambridge Tracts in Theoretical Computer Science, vol. 32. Cambridge University Press (1992). https://doi.org/10.1017/CBO9780511530098

  7. Chandlee, J.: Strictly local phonological processes. Ph.D. thesis, University of Delaware (2014). https://chandlee.sites.haverford.edu/wp-content/uploads/2015/05/Chandlee_dissertation_2014.pdf

  8. Chen, K.T., Fox, R.H., Lyndon, R.C.: Free differential calculus IV. The quotient groups of the lower central series. Ann. Math. 68(1), 81–95 (1958). https://doi.org/10.2307/1970044

    Article  MathSciNet  Google Scholar 

  9. Chomsky, N.: On certain formal properties of grammars. Inf. Control 2(2), 137–167 (1959). https://doi.org/10.1016/S0019-9958(59)90362-6

    Article  MathSciNet  Google Scholar 

  10. Clifford, A.H., Preston, G.B.: The Algebraic Theory of Semigroups, Mathematical Surveys and Monographs, vol. 7. American Mathematical Society, Providence (1961)

    Google Scholar 

  11. Edlefsen, M., Leeman, D., Myers, N., Smith, N., Visscher, M., Wellcome, D.: Deciding strictly local (SL) languages. In: Breitenbucher, J. (ed.) Proceedings of the 2008 Midstates Conference for Undergraduate Research in Computer Science and Mathematics, pp. 66–73 (2008)

    Google Scholar 

  12. Eilenberg, S.: Automata, Languages, and Machines, vol. B. Academic Press, New York (1976)

    Google Scholar 

  13. Eilenberg, S., Schützenberger, M.P.: On pseudovarieties. Adv. Math. 19(3), 413–418 (1976). https://doi.org/10.1016/0001-8708(76)90029-3

    Article  MathSciNet  Google Scholar 

  14. Haines, L.H.: On free monoids partially ordered by embedding. J. Comb. Theory 6(1), 94–98 (1969). https://doi.org/10.1016/s0021-9800(69)80111-0

    Article  MathSciNet  Google Scholar 

  15. Heinz, J.: Inductive learning of phonotactic patterns. Ph.D. thesis, University of California, Los Angeles (2007)

    Google Scholar 

  16. Heinz, J., Rawal, C., Tanner, H.G.: Tier-based strictly local constraints for phonology. In: Proceedings of the 49th Annual Meeting of the Association for Computational Linguistics: Short Papers, Portland, Oregon, vol. 2, pp. 58–64. Association for Computational Linguistics (2011). https://aclanthology.org/P11-2011

  17. de la Higuera, C.: Grammatical Inference: Learning Automata and Grammars. Cambridge University Press (2010). https://doi.org/10.1017/CBO9781139194655

  18. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley (1979)

    Google Scholar 

  19. Hulden, M.: Finite-state machine construction methods and algorithms for phonology and morphology. Ph.D. thesis, The University of Arizona (2009). https://hdl.handle.net/10150/196112

  20. Hulden, M.: Foma: a finite-state compiler and library. In: Proceedings of the Demonstrations Session at EACL 2009, Athens, Greece, pp. 29–32. Association for Computational Linguistics (2009). https://aclanthology.org/E09-2008

  21. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, Annals of Mathematics Studies, vol. 34, pp. 3–42. Princeton University Press (1956). https://doi.org/10.1515/9781400882618-002

  22. Krebs, A., Lodaya, K., Pandya, P.K., Straubing, H.: Two-variable logics with some betweenness relations: expressiveness, satisfiability, and membership. Logical Methods Comput. Sci. 16(3), 1–41 (2020). https://doi.org/10.23638/LMCS-16(3:16)2020

    Article  MathSciNet  Google Scholar 

  23. Lambert, D.: Relativized adjacency. J. Logic Lang. Inform. 32(4), 707–731 (2023). https://doi.org/10.1007/s10849-023-09398-x

    Article  MathSciNet  Google Scholar 

  24. Lothaire, M.: Combinatorics on Words. Cambridge University Press, New York (1983)

    Google Scholar 

  25. MacCormick, J.: What Can Be Computed? A Practical Guide to the Theory of Computation. Princeton University Press (2018)

    Google Scholar 

  26. McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biol. 5, 115–133 (1943). https://doi.org/10.1007/bf02478259

    Article  MathSciNet  Google Scholar 

  27. McNaughton, R., Papert, S.A.: Counter-Free Automata. MIT Press, Cambridge (1971)

    Google Scholar 

  28. Mitchell, J., et al.: Semigroups – GAP Package, 5.1.0 edn. (2022). https://doi.org/10.5281/zenodo.592893

  29. Pin, J.-E.: Syntactic semigroups. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 679–746. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-59136-5_10

    Chapter  Google Scholar 

  30. Pin, J.E., Weil, P.: Polynomial closure and unambiguous product. Theory Comput. Syst. 30(4), 383–422 (1997). https://doi.org/10.1007/bf02679467

    Article  MathSciNet  Google Scholar 

  31. van der Poel, S., et al.: MLRegTest: a benchmark for the machine learning of regular languages (2023). https://doi.org/10.48550/ar**v.2304.07687

  32. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114–125 (1959). https://doi.org/10.1147/rd.32.0114

    Article  MathSciNet  Google Scholar 

  33. Rawal, C., Tanner, H.G., Heinz, J.: (Sub)regular robotic languages. In: 2011 19th Mediterranean Conference on Control & Automation (MED), pp. 321–326 (2011). https://doi.org/10.1109/MED.2011.5983140

  34. Reiterman, J.: The Birkhoff theorem for finite algebras. Algebra Universalis 14, 1–10 (1982). https://doi.org/10.1007/BF02483902

    Article  MathSciNet  Google Scholar 

  35. Rogers, J., et al.: On languages piecewise testable in the strict sense. In: Ebert, C., Jäger, G., Michaelis, J. (eds.) MOL 2007/2009. LNCS (LNAI), vol. 6149, pp. 255–265. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14322-9_19

    Chapter  Google Scholar 

  36. Rogers, J., Lambert, D.: Extracting subregular constraints from regular stringsets. J. Lang. Model. 7(2), 143–176 (2019). https://doi.org/10.15398/jlm.v7i2.209

    Article  Google Scholar 

  37. Rogers, J., Lambert, D.: Some classes of sets of structures definable without quantifiers. In: Proceedings of the 16th Meeting on the Mathematics of Language, Toronto, Canada, pp. 63–77. Association for Computational Linguistics (2019). https://doi.org/10.18653/v1/W19-5706

  38. Romero, J.: Pyformlang: an educational library for formal language manipulation. In: Proceedings of the 52nd ACM Technical Symposium on Computer Science Education, pp. 576–582. Association for Computing Machinery, New York (2021). https://doi.org/10.1145/3408877.3432464

  39. Schützenberger, M.P.: On finite monoids having only trivial subgroups. Inf. Control 8(2), 190–194 (1965). https://doi.org/10.1016/s0019-9958(65)90108-7

    Article  MathSciNet  Google Scholar 

  40. Simon, I.: Piecewise testable events. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 214–222. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_23

    Chapter  Google Scholar 

  41. Sipser, M.: Introduction to the Theory of Computation, 3rd edn. Cengage Learning, Boston (2013)

    Google Scholar 

  42. Thomas, W.: Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25, 360–376 (1982). https://doi.org/10.1016/0022-0000(82)90016-2

    Article  MathSciNet  Google Scholar 

  43. Thompson, K.: Programming techniques: regular expression search algorithm. Commun. ACM 11(6), 419–422 (1968). https://doi.org/10.1145/363347.363387

    Article  Google Scholar 

Download references

Acknowledgments

The system described in this work owes its creation to the wonderful Theory of Computation course taught by Jim Rogers at Earlham College. Further enhancements arose from work with Jeffrey Heinz at Stony Brook University. And much gratitude is extended to the anonymous reviewers for their helpful suggestions.

Author information

Authors and Affiliations

  1. Université Jean Monnet Saint-Étienne, CNRS, Institut d Optique Graduate School, Laboratoire Hubert Curien, UMR 5516, 42023, Saint-Étienne, France

    Dakotah Lambert

Authors
  1. Dakotah Lambert
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dakotah Lambert .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Wolfson Building, Oxford University, Oxford, UK

    Jeremy Gibbons

  2. Campus de l’École Polytechnique, Inria Saclay, Palaiseau, France

    Dale Miller

Ethics declarations

Disclosure of Interests

The authors have no competing interests to declare that are relevant to the content of this article.

Appendix

Appendix

This appendix contains selected worked exercises from various textbooks.

1.1 Exercise 2.1 from McNaughton and Papert [27]

“Decide whether each of the Figures 2.2–2.8 represents a locally testable event. Decide further whether it is locally testable in the strict sense.” We cover only figures 2.4, 2.7 and 2.8. These figures are represented by the following at &t files, named mp-2-1-4.att, mp-2-1-7.att and mp-2-1-8.att, respectively.

figure o
figure p

Here, the tool directly answers the exercises, even providing additional information regarding the factor size \(k\) for the language locally testable in the strict sense.

1.2 5.1 Exercises from Sipser [41]

In the third edition of “Introduction to the Theory of Computation”, Sipser [41] asks students to construct state diagrams for various regular languages. Exercise 1.4 focuses on intersections, 1.5 on complements, and 1.6 has assorted other languages. We select a small sample to cover here, all over the alphabet \(\varSigma =\{a,b\}\):

  • 1.4e \(\{w|w\text { starts with an a and has at most one b}\}\)

  • 1.5c \(\{w|w\text { contains neither the substrings ab nor ba}\}\)

  • 1.6n All strings except the empty string

As an aside, exercise 1.6 uses \(\varSigma =\{0,1\}\) in the original.

figure q
Fig. 2.
figure 2

State diagrams for Sipser, with node labels omitted.

Full size image

Figure 2 depicts the results. Rejecting sink states are omitted from the display and must be filled in by hand.

Rights and permissions

Reprints and permissions

Copyright information

© 2024 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

About this paper

Cite this paper

Lambert, D. (2024). System Description: A Theorem-Prover for Subregular Systems: The Language Toolkit and Its Interpreter, Plebby. In: Gibbons, J., Miller, D. (eds) Functional and Logic Programming. FLOPS 2024. Lecture Notes in Computer Science, vol 14659. Springer, Singapore. https://doi.org/10.1007/978-981-97-2300-3_16

Download citation

  • DOI: https://doi.org/10.1007/978-981-97-2300-3_16

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-97-2299-0

  • Online ISBN: 978-981-97-2300-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation