Sorted Terms

Akihisa Yamada 📧 and René Thiemann 🌐

May 27, 2024

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.

We further provide algorithms for computing emptyness, finiteness and cardinality of sorts.

License

BSD License

History

November 7, 2025
added algorithms for computing emptyness, finiteness and cardinality of sorts (revision 000650ad3ece)

Topics

Related publications

  • Thiemann, R., & Yamada, A. (2024). A Verified Algorithm for Deciding Pattern Completeness. In J. Rehof (Ed.), LIPIcs, Volume 299, FSCD 2024 (No.27; Vol. 299, pp. 27:1–27:17). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.FSCD.2024.27

Session Sorted_Terms

Depends on

Used by

Cite

× 
@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},
}
Download

Download

× Download latest

Older releases: