Abstract
A pattern t, i.e., a term possibly with variables, denotes the set (language) \(\llbracket t \rrbracket \) 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 \(\varSigma \mapsto \varSigma ^{\#}\) that enriches the types of \(\varSigma \). 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Theorem 4 holds for \(\varSigma \) finite and regular because any such \(\varSigma \) can be transformed into a semantically equivalent signature with no ad-hoc overloading (by symbol renaming) and with each connected component having a top sort (added when missing).
References
Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., MartÃ-Oliet, N., Talcott, C.: All About Maude. LNCS, vol. 4350. Springer, Heidelberg (2007)
Comon, H., Lescanne, P.: Equational problems and disunification. J. Symbol. Comput. 7, 371–425 (1989)
Comon, H.: Equational formulas in order-sorted algebras. In: Comon, H. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 674–688. Springer, Heidelberg (1990)
Comon, H., Delor, C.: Equational formulae with membership constraints. Inf. Comput. 112(2), 167–216 (1994)
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1, vol. 6. Springer, Heidelberg (1985)
Fernández, M.: Negation elimination in empty or permutative theories. J. Symb. Comput. 26(1), 97–133 (1998)
Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)
Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)
Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theo. Comput. Sci. 105, 217–273 (1992)
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action, pp. 3–167. Kluwer (2000)
Lassez, J.-L., Maher, M., Marriott, K.: Elimination of negation in term algebras. In: Tarlecki, Andrzej (ed.) MFCS 1991. LNCS, vol. 520, pp. 1–16. Springer, Heidelberg (1991)
Lassez, J.L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason. 3(3), 301–317 (1987)
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. In: Proceedings of LICS 1988, pp. 348–357. IEEE Computer Society (1988)
Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. Technical report, IBM T. J. Watson Research Center (1988)
Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Technical Report, University of Illinois at Urbana-Champaign, June 2015. http://hdl.handle.net/2142/78055
Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, Francesco (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)
Meseguer, J., Goguen, J., Smolka, G.: Order-sorted unification. J. Symbolic Comput. 8, 383–413 (1989)
Pichler, R.: Explicit versus implicit representations of subsets of the Herbrand universe. Theo. Comput. Sci. 290(1), 1021–1056 (2003)
Tajine, M.: The negation elimination from syntactic equational formula is decidable. In: Kirchner, Claude (ed.) RTA 1993. LNCS, vol. 690, pp. 316–327. Springer, Heidelberg (1993)
Acknowledgements
Partially supported by NSF Grant CNS 13-19109. We thank the referees for their excellent suggestions to improve the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Meseguer, J., Skeirik, S. (2015). Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras. In: Falaschi, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2015. Lecture Notes in Computer Science(), vol 9527. Springer, Cham. https://doi.org/10.1007/978-3-319-27436-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-27436-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27435-5
Online ISBN: 978-3-319-27436-2
eBook Packages: Computer ScienceComputer Science (R0)