{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,16]],"date-time":"2026-05-16T06:50:20Z","timestamp":1778914220069,"version":"3.51.4"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            A\n            <jats:italic>pattern<\/jats:italic>\n            <jats:italic>t<\/jats:italic>\n            , i.e., a term possibly with variables, denotes the set (language)\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mo>\u301a<\/mml:mo>\n                    <mml:mi>t<\/mml:mi>\n                    <mml:mo>\u301b<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            of all its\n            <jats:italic>ground instances<\/jats:italic>\n            . 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\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi mathvariant=\"normal\">\u03a3<\/mml:mi>\n                    <mml:mo>\u21a6<\/mml:mo>\n                    <mml:msup>\n                      <mml:mi mathvariant=\"normal\">\u03a3<\/mml:mi>\n                      <mml:mo>#<\/mml:mo>\n                    <\/mml:msup>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            that enriches the types of\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"normal\">\u03a3<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            . 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.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0415-5","type":"journal-article","created":{"date-parts":[[2017,2,7]],"date-time":"2017-02-07T08:23:47Z","timestamp":1486455827000},"page":"423-452","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Equational formulas and pattern operations in initial order-sorted algebras"],"prefix":"10.1145","volume":"29","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Champaign, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Skeirik","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Champaign, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.006"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1056"},{"key":"e_1_2_1_2_3_2","unstructured":"Clavel M Dur\u00e1n F Eker S Meseguer J Lincoln P Mart\u00ed-Oliet N Talcott C (2007) All about Maude. In: LNCS vol 4350. Springer Berlin"},{"key":"e_1_2_1_2_4_2","unstructured":"Comon H Dauchet M Gilleron R L\u00f6ding C Jacquemard F Lugiez D Tison S Tommasi M (2007) Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata. Release 12 Oct 2007"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80017-3"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Comon H (1990) Equational formulas in order-sorted algebras. In: Proceedings of the ICALP\u201990. LNCS vol 443. Springer Berlin pp 674\u2013688","DOI":"10.1007\/BFb0032066"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.5555\/577099"},{"key":"e_1_2_1_2_8_2","volume-title":"CafeOBJ Report","author":"Futatsugi K","year":"1998"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1998.0203"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_2_1_2_12_2","unstructured":"Guttag J (1975) The specification and application to programming of abstract data types. Ph.D. thesis University of Toronto. Computer Science Department Report CSRG-59"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Goguen J Winkler T Meseguer J Futatsugi K Jouannaud JP (2000) Introducing OBJ. In: Software engineering with OBJ: algebraic specification in action. Kluwer Dordrecht pp 3\u2013167","DOI":"10.1007\/978-1-4757-6541-0_1"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hudak P Hughes J Peyton Jones SL Wadler P (2007) A history of haskell: being lazy with class. In: Proceedings of the third ACM SIGPLAN history of programming languages conference (HOPL-III). ACM New york pp 1\u201355","DOI":"10.1145\/1238844.1238856"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lassez JL Maher M Marriott K (1991) Elimination of negation in term algebras. In: Mathematical foundations of computer science. Springer Berlin pp 1\u201316","DOI":"10.1007\/3-540-54345-7_44"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/33031.33036"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Maher MJ (1988) Complete axiomatizations of the algebras of finite rational and infinite trees. In: Proceedings of the LICS\u201988. IEEE Computer Society Silver Spring pp 348\u2013357","DOI":"10.1109\/LICS.1988.5132"},{"key":"e_1_2_1_2_18_2","unstructured":"Maher MJ (1988) Complete axiomatizations of the algebras of finite rational and infinite trees. Technical report IBM T. J. Watson Research Center"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Meseguer J (1998) Membership algebra as a logical framework for equational specification. In: Proceedings of the WADT\u201997. In: LNCS vol 1376. Springer Berlin pp 18\u201361","DOI":"10.1007\/3-540-64299-4_26"},{"key":"e_1_2_1_2_21_2","unstructured":"Meseguer J (2016) Variant-based satisfiability in initial algebras. In: Artho C \u00d6lveczky PC (eds) proc. FTSCS 2015. Springer CCIS 596 pp 1\u201332"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1016\/S0747-7171(89)80036-7","article-title":"Order-sorted unification.","volume":"8","author":"Jos\u00e9 Meseguer","year":"1989","journal-title":"J Symb Comput"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Meseguer J Palomino M Mart\u00ed-Oliet N (2008) Equational abstractions. Theor Comput Sci 403(2\u20133):239\u2013264","DOI":"10.1016\/j.tcs.2008.04.040"},{"key":"#cr-split#-e_1_2_1_2_24_2.1","doi-asserted-by":"crossref","unstructured":"Meseguer J Skeirik S (2015) Equational formulas and pattern operations in initial order-sorted algebras. In: Falaschi M","DOI":"10.1007\/978-3-319-27436-2_3"},{"key":"#cr-split#-e_1_2_1_2_24_2.2","unstructured":"(ed) Proceedings of the LOPSTR 2015. LNCS vol 9527. Springer Berlin pp 36-53"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00583-2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Tajine M (1993) The negation elimination from syntactic equational formula is decidable. In: Proceedings of the RTA-93. LNCS vol 690. Springer Berlin pp 316\u2013327","DOI":"10.1007\/3-540-56868-9_24"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","DOI":"10.1142\/3163","volume-title":"Language prototyping: an algebraic specification approach","author":"van Deursen A","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0415-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0415-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0415-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0415-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:26Z","timestamp":1641538586000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0415-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-017-0415-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0415-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}