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 -