Equational Formulas and Pattern Operations in Initial Order-Sorted Algebras

  • José Meseguer
  • Stephen SkeirikEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9527)


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.


Pattern operations Initial decidability Order-Sorted logic 



Partially supported by NSF Grant CNS 13-19109. We thank the referees for their excellent suggestions to improve the paper.


  1. 1.
    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)zbMATHGoogle Scholar
  2. 2.
    Comon, H., Lescanne, P.: Equational problems and disunification. J. Symbol. Comput. 7, 371–425 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    Comon, H., Delor, C.: Equational formulae with membership constraints. Inf. Comput. 112(2), 167–216 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1, vol. 6. Springer, Heidelberg (1985)CrossRefzbMATHGoogle Scholar
  6. 6.
    Fernández, M.: Negation elimination in empty or permutative theories. J. Symb. Comput. 26(1), 97–133 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Futatsugi, K., Diaconescu, R.: CafeOBJ Report. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  8. 8.
    Goguen, J., Burstall, R.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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) CrossRefGoogle Scholar
  12. 12.
    Lassez, J.L., Marriott, K.: Explicit representation of terms defined by counter examples. J. Autom. Reason. 3(3), 301–317 (1987)CrossRefzbMATHGoogle Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Maher, M.J.: Complete axiomatizations of the algebras of finite, rational and infinite trees. Technical report, IBM T. J. Watson Research Center (1988)Google Scholar
  15. 15.
    Meseguer, J., Skeirik, S.: Equational formulas and pattern operations in initial order-sorted algebras. Technical Report, University of Illinois at Urbana-Champaign, June 2015.
  16. 16.
    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) CrossRefGoogle Scholar
  17. 17.
    Meseguer, J., Goguen, J., Smolka, G.: Order-sorted unification. J. Symbolic Comput. 8, 383–413 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Pichler, R.: Explicit versus implicit representations of subsets of the Herbrand universe. Theo. Comput. Sci. 290(1), 1021–1056 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    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) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Department of Computer ScienceUniversity of Illinois at Urbana-ChampaignChampaignUSA

Personalised recommendations