Part of the book series:Lecture Notes in Computer Science ((LNTCS,volume 12328))
Included in the following conference series:
181Accesses
Abstract
Constrained constructor patterns are pairs of a constructor term pattern and a quantifier-free first-order logic constraint, built from conjunction and disjunction. They are used to express state predicates for reachability logic defined over rewrite theories. Matching logic has been recently proposed as a unifying foundation for programming languages, specification and verification. It has been shown to capture several logical systems and/or models that are important for programming languages, including first-order logic with fixpoints and order-sorted algebra. In this paper, we investigate the relationship between constrained constructor patterns and matching logic. The comparison result brings us a mutual benefit for the two approaches. Matching logic can borrow computationally efficient proofs for some equivalences, and the language of the constrained constructor patterns can get a more logical flavor and more expressiveness.
This is a preview of subscription content,log in via an institution to check access.
Access this chapter
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
- Chapter
- JPY 3498
- Price includes VAT (Japan)
- eBook
- JPY 5719
- Price includes VAT (Japan)
- Softcover Book
- JPY 7149
- Price includes VAT (Japan)
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
This answers a question asked by Jacques Carette on themathoverflow site (https://mathoverflow.net/questions/16180/formalizing-no-junk-no-confusion) ten years ago: Are there logics in which these requirements (“no junk, no confusion”) can be internalized?
- 2.
This is an informal notation because\([\![u| \varphi ]\!]\subseteq \bigcup _{i\in I}[\![v_i|\psi _i ]\!]\) is not exactly a formula.
References
Arusoaie, A., Lucanu, D.: Unification in matching logic. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 502–518. Springer, Cham (2019).https://doi.org/10.1007/978-3-030-30942-8_30
Chen, X., Roşu, G.: Applicative matching logic. Technical report (2019).http://hdl.handle.net/2142/104616. University of Illinois at Urbana-Champaign
Chen, X., Rosu, G.: Matching\(\mu \)-logic. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), Vancouver, Canada, pp. 1–13. IEEE (2019).https://doi.org/10.1109/LICS.2019.8785675
Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebraic Program.81(7–8), 898–928 (2012).https://doi.org/10.1016/j.jlap.2012.01.002
Futatsugi, K.: Fostering proof scores inCafeOBJ. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 1–20. Springer, Heidelberg (2010).https://doi.org/10.1007/978-3-642-16901-4_1
Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. Technical report. RC 6487, IBM Res. Rep (1976). See also Current Trends in Programming Methodology, vol. 4: Data Structuring, R. T. Yeh, Ed. Englewood Cliffs, NJ: Prentice-Hall1978, 80–149 (1976)
Meseguer, J.: Variant-based satisfiability in initial algebras. Sci. Comput. Program.154, 3–41 (2018).https://doi.org/10.1016/j.scico.2017.09.001
Meseguer, J.: Generalized rewrite theories, coherence completion, and symbolic methods. J. Log. Algebraic Methods Program.110 (2020).https://doi.org/10.1016/j.jlamp.2019.100483
Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebraic Program.81(7), 721–781 (2012).https://doi.org/10.1016/j.jlap.2012.06.003
Roşu, G.: Matching logic. Log. Methods Comput. Sci.13(4), 1–61 (2017)
Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. In: Fioravanti, F., Gallagher, J.P. (eds.) LOPSTR 2017. LNCS, vol. 10855, pp. 201–217. Springer, Cham (2018).https://doi.org/10.1007/978-3-319-94460-9_12
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math.5(2), 285–309 (1955)
Author information
Authors and Affiliations
University of Illinois at Urbana-Champaign, Champaign, USA
Xiaohong Chen & Grigore Roşu
Alexandru Ioan Cuza University of Iai, Iai, Romania
Dorel Lucanu
- Xiaohong Chen
You can also search for this author inPubMed Google Scholar
- Dorel Lucanu
You can also search for this author inPubMed Google Scholar
- Grigore Roşu
You can also search for this author inPubMed Google Scholar
Corresponding author
Correspondence toXiaohong Chen.
Editor information
Editors and Affiliations
Valencian Research Institute for Artificial Intelligence, Universitat Politècnica de València, Valencia, Spain
Santiago Escobar
Facultad de Informática, Universidad Complutense de Madrid, Madrid, Spain
Narciso Martí-Oliet
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Chen, X., Lucanu, D., Roşu, G. (2020). Connecting Constrained Constructor Patterns and Matching Logic. In: Escobar, S., Martí-Oliet, N. (eds) Rewriting Logic and Its Applications. WRLA 2020. Lecture Notes in Computer Science(), vol 12328. Springer, Cham. https://doi.org/10.1007/978-3-030-63595-4_2
Download citation
Published:
Publisher Name:Springer, Cham
Print ISBN:978-3-030-63594-7
Online ISBN:978-3-030-63595-4
eBook Packages:Computer ScienceComputer Science (R0)
Share this paper
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative