Connecting Constrained Constructor Patterns and Matching Logic

Xiaohong Chen; Dorel Lucanu; Grigore Roşu

doi:10.1007/978-3-030-63595-4_2

Connecting Constrained Constructor Patterns and Matching Logic

Xiaohong Chen, Dorel Lucanu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers
Editors	Santiago Escobar, Narciso Martí-Oliet
Publisher	Springer
Pages	19-37
Number of pages	19
ISBN (Print)	9783030635947
DOIs	https://doi.org/10.1007/978-3-030-63595-4_2
State	Published - 2020
Event	13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 - Virtual, Online Duration: Oct 20 2020 → Oct 22 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12328 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020
City	Virtual, Online
Period	10/20/20 → 10/22/20

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-030-63595-4_2

Library availability

Discover UIUC Full Text

Cite this

Chen, X., Lucanu, D., & Roşu, G. (2020). Connecting Constrained Constructor Patterns and Matching Logic. In S. Escobar, & N. Martí-Oliet (Eds.), Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers (pp. 19-37). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12328 LNCS). Springer. https://doi.org/10.1007/978-3-030-63595-4_2

Connecting Constrained Constructor Patterns and Matching Logic. / Chen, Xiaohong; Lucanu, Dorel; Roşu, Grigore.
Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers. ed. / Santiago Escobar; Narciso Martí-Oliet. Springer, 2020. p. 19-37 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12328 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Chen, X, Lucanu, D & Roşu, G 2020, Connecting Constrained Constructor Patterns and Matching Logic. in S Escobar & N Martí-Oliet (eds), Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12328 LNCS, Springer, pp. 19-37, 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020, Virtual, Online, 10/20/20. https://doi.org/10.1007/978-3-030-63595-4_2

Chen X, Lucanu D, Roşu G. Connecting Constrained Constructor Patterns and Matching Logic. In Escobar S, Martí-Oliet N, editors, Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers. Springer. 2020. p. 19-37. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-63595-4_2

Chen, Xiaohong ; Lucanu, Dorel ; Roşu, Grigore. / Connecting Constrained Constructor Patterns and Matching Logic. Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers. editor / Santiago Escobar ; Narciso Martí-Oliet. Springer, 2020. pp. 19-37 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e9cc94fc23f24837bd79d2c305e0992b,

title = "Connecting Constrained Constructor Patterns and Matching Logic",

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.",

author = "Xiaohong Chen and Dorel Lucanu and Grigore Ro{\c s}u",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020 ; Conference date: 20-10-2020 Through 22-10-2020",

year = "2020",

doi = "10.1007/978-3-030-63595-4_2",

language = "English (US)",

isbn = "9783030635947",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "19--37",

editor = "Santiago Escobar and Narciso Mart{\'i}-Oliet",

booktitle = "Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers",

address = "Germany",

}

TY - GEN

T1 - Connecting Constrained Constructor Patterns and Matching Logic

AU - Chen, Xiaohong

AU - Lucanu, Dorel

AU - Roşu, Grigore

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85099049469&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85099049469&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-63595-4_2

DO - 10.1007/978-3-030-63595-4_2

M3 - Conference contribution

AN - SCOPUS:85099049469

SN - 9783030635947

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 19

EP - 37

BT - Rewriting Logic and Its Applications - 13th International Workshop, WRLA 2020, Revised Selected Papers

A2 - Escobar, Santiago

A2 - Martí-Oliet, Narciso

PB - Springer

T2 - 13th International Workshop on Rewriting Logic and Its Applications, WRLA 2020

Y2 - 20 October 2020 through 22 October 2020

ER -

Connecting Constrained Constructor Patterns and Matching Logic

Abstract

Publication series

Conference

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this