Abstract

This entry provides a basic library for many-sorted terms and algebras. We view sorted sets just as partial maps from elements to sorts, and define sorted set of terms reusing the data type from the existing library of (unsorted) first order terms. All the existing functionality, such as substitutions and contexts, can be reused without any modifications. We provide predicates stating what substitutions or contexts are considered sorted, and prove facts that they preserve sorts as expected.

BibTeX

@article{Sorted_Terms-AFP,
  author  = {Akihisa Yamada and René Thiemann},
  title   = {Sorted Terms},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Sorted_Terms.html},
             Formal proof development},
  ISSN    = {2150-914x},
}