TY - GEN
T1 - Equational formulas and pattern operations in initial order-sorted algebras
AU - Meseguer, José
AU - Skeirik, Stephen
N1 - Funding Information:
Partially supported by NSF Grant CNS 13-19109. We thank the referees for their excellent suggestions to improve the paper.
PY - 2015
Y1 - 2015
N2 - A pattern t, i.e., a term possibly with variables, denotes the set (language) 〚t〛 of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation Σ↦Σ# that enriches the types of Σ. We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted (i.e., simply typed) algebra. This yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.
AB - A pattern t, i.e., a term possibly with variables, denotes the set (language) 〚t〛 of all its ground instances. In an untyped setting, symbolic operations on finite sets of patterns can represent Boolean operations on languages. But for the more expressive patterns needed in declarative languages supporting rich type disciplines such as subtype polymorphism untyped pattern operations and algorithms break down. We show how they can be properly defined by means of a signature transformation Σ↦Σ# that enriches the types of Σ. We also show that this transformation allows a systematic reduction of the first-order logic properties of an initial order-sorted algebra supporting subtype-polymorphic functions to equivalent properties of an initial many-sorted (i.e., simply typed) algebra. This yields a new, simple proof of the known decidability of the first-order theory of an initial order-sorted algebra.
KW - Initial decidability
KW - Order-sorted logic
KW - Pattern operations
UR - http://www.scopus.com/inward/record.url?scp=84952783919&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84952783919&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-27436-2_3
DO - 10.1007/978-3-319-27436-2_3
M3 - Conference contribution
AN - SCOPUS:84952783919
SN - 9783319274355
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 36
EP - 53
BT - Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers
A2 - Falaschi, Moreno
PB - Springer
T2 - 25th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2015
Y2 - 13 July 2015 through 15 July 2015
ER -