Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2019: Intelligent Computer Mathematics pp 77–92Cite as

Variadic Equational Matching

  • Conference paper
  • First Online:

  • 486 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11617))

Abstract

In this paper we study matching in equational theories that specify counterparts of associativity and commutativity for variadic function symbols. We design a procedure to solve a system of matching equations and prove its soundness and completeness. The complete set of incomparable matchers for such a system can be infinite. From the practical side, we identify two finitary cases and impose restrictions on the procedure to get an incomplete terminating algorithm, which, in our opinion, describes the semantics for associative and commutative matching implemented in the symbolic computation system Mathematica.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • 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

Learn about institutional subscriptions

Notes

  1. 1.

    It is also possible to modify \({\mathfrak {M}}\) so that it terminates and computes a finite representation of the infinite set of matchers with the help of regular expressions over substitution composition. For associative (flat) matching, an implementation of such a procedure can be found at https://www3.risc.jku.at/people/tkutsia/software.html.

  2. 2.

    Roughly, the canonical order orders symbols alphabetically and extends to trees with respect to left-to-right pre-order.

References

  1. Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 445–532. Elsevier and MIT Press (2001)

    Google Scholar 

  2. Benanav, D., Kapur, D., Narendran, P.: Complexity of matching problems. J. Symb. Comput. 3(1/2), 203–216 (1987). https://doi.org/10.1016/S0747-7171(87)80027-5

    Article  MathSciNet  MATH  Google Scholar 

  3. Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4(4), 470–504 (2006). https://doi.org/10.1016/j.jal.2005.10.006

    Article  MathSciNet  MATH  Google Scholar 

  4. Cirstea, H., Kirchner, C., Kopetz, R., Moreau, P.E.: Anti-patterns for rule-based languages. J. Symb. Comput. 45(5), 523–550 (2010). https://doi.org/10.1016/j.jsc.2010.01.007

    Article  MathSciNet  MATH  Google Scholar 

  5. Coelho, J., Florido, M.: CLP(Flex): constraint logic programming applied to XML processing. In: Meersman, R., Tari, Z. (eds.) OTM 2004. LNCS, vol. 3291, pp. 1098–1112. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30469-2_17

    Chapter  Google Scholar 

  6. Dundua, B., Kutsia, T., Reisenberger-Hagmayer, K.: An overview of P\(\rho \)Log. In: Lierler, Y., Taha, W. (eds.) PADL 2017. LNCS, vol. 10137, pp. 34–49. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51676-9_3

    Chapter  Google Scholar 

  7. Eker, S.: Single elementary associative-commutative matching. J. Autom. Reason. 28(1), 35–51 (2002). https://doi.org/10.1023/A:1020122610698

    Article  MathSciNet  MATH  Google Scholar 

  8. Eker, S.: Associative-commutative rewriting on large terms. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 14–29. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44881-0_3

    Chapter  MATH  Google Scholar 

  9. Horozal, F.: A framework for defining declarative languages. Ph.D. thesis, Jacobs University Bremen (2014)

    Google Scholar 

  10. Horozal, F., Rabe, F., Kohlhase, M.: Flexary operators for formalized mathematics. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 312–327. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_23

    Chapter  MATH  Google Scholar 

  11. Hullot, J.: Associative commutative pattern matching. In: Buchanan, B.G. (ed.) Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI 1979, Tokyo, Japan, 20–23 August 1979, 2 Volumes, pp. 406–412. William Kaufmann (1979)

    Google Scholar 

  12. International Organization for Standardization: Information technology—Common Logic (CL)—a framework for a family of logic-based languages. International Standard ISO/IEC 24707:2018(E) (2018). https://www.iso.org/standard/66249.html

  13. Krebber, M., Barthels, H., Bientinesi, P.: Efficient pattern matching in python. In: Schreiber, A., Scullin, W., Spotz, B., Thomas, R. (eds.) Proceedings of the 7th Workshop on Python for High-Performance and Scientific Computing. ACM (2017)

    Google Scholar 

  14. Kutsia, T.: Solving and proving in equational theories with sequence variables and flexible arity symbols. RISC Report Series 02–09, RISC, Johannes Kepler University Linz (2002)

    Google Scholar 

  15. Kutsia, T.: Unification with sequence variables and flexible arity symbols and its extension with pattern-terms. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds.) AISC/Calculemus -2002. LNCS (LNAI), vol. 2385, pp. 290–304. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45470-5_26

    Chapter  MATH  Google Scholar 

  16. Kutsia, T.: Solving equations with sequence variables and sequence functions. J. Symb. Comput. 42(3), 352–388 (2007). https://doi.org/10.1016/j.jsc.2006.12.002

    Article  MathSciNet  MATH  Google Scholar 

  17. Kutsia, T.: Flat matching. J. Symb. Comput. 43(12), 858–873 (2008). https://doi.org/10.1016/j.jsc.2008.05.001

    Article  MathSciNet  MATH  Google Scholar 

  18. Kutsia, T., Marin, M.: Solving, reasoning, and programming in Common Logic. In: Voronkov, A., et al. (eds.) 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, Timisoara, Romania, 26–29 September 2012, pp. 119–126. IEEE Computer Society (2012). https://doi.org/10.1109/SYNASC.2012.27

  19. Kutsia, T., Marin, M.: Regular expression order-sorted unification and matching. J. Symb. Comput. 67, 42–67 (2015). https://doi.org/10.1016/j.jsc.2014.08.002

    Article  MathSciNet  MATH  Google Scholar 

  20. Marin, M., Kutsia, T.: On the implementation of a rule-based programming system and some of its applications. In: Konev, B., Schmidt, R. (eds.) Proceedings 4th International Workshop on the Implementation of Logics, WIL 2003, pp. 55–68 (2003)

    Google Scholar 

  21. Marin, M., Tepeneu, D.: Programming with sequence variables: the Sequentica package. In: Proceedings of the 5th International Mathematica Symposium on Challenging the Boundaries of Symbolic Computation, pp. 17–24. World Scientific (2003)

    Google Scholar 

  22. Wolfram, S.: The Mathematica Book, 5th edn. Wolfram Media (2003)

    Google Scholar 

Download references

Acknowledgments

This research has been partially supported by the Austrian Science Fund (FWF) under the project 28789-N32 and the Shota Rustaveli National Science Foundation of Georgia (SRNSFG) under the grant YS-18-1480.

Author information

Authors and Affiliations

  1. CTE, International Black Sea University, Tbilisi, Georgia

    Besik Dundua

  2. VIAM, Ivane Javakhishvili Tbilisi State University, Tbilisi, Georgia

    Besik Dundua

  3. RISC, Johannes Kepler University, Linz, Austria

    Temur Kutsia

  4. West University of Timişoara, Timişoara, Romania

    Mircea Marin

Authors
  1. Besik Dundua
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Temur Kutsia
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mircea Marin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Temur Kutsia .

Editor information

Editors and Affiliations

  1. University of Innsbruck, Innsbruck, Austria

    Cezary Kaliszyk

  2. University of St. Andrews, St. Andrews, UK

    Edwin Brady

  3. University of Applied Sciences, Neu-Ulm, Germany

    Andrea Kohlhase

  4. University of Bologna, Bologna, Italy

    Claudio Sacerdoti Coen

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

Dundua, B., Kutsia, T., Marin, M. (2019). Variadic Equational Matching. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds) Intelligent Computer Mathematics. CICM 2019. Lecture Notes in Computer Science(), vol 11617. Springer, Cham. https://doi.org/10.1007/978-3-030-23250-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-23250-4_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-23249-8

  • Online ISBN: 978-3-030-23250-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation