Document Open Access Logo

Ordinal Measures of the Set of Finite Multisets

Author Isa Vialard

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.87.pdf
  • Filesize: 0.8 MB
  • 15 pages

Document Identifiers

Author Details

Isa Vialard
  • Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190, Gif-sur-Yvette, France

Cite As Get BibTex

Isa Vialard. Ordinal Measures of the Set of Finite Multisets. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 87:1-87:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.MFCS.2023.87

Abstract

Well-partial orders, and the ordinal invariants used to measure them, are relevant in set theory, program verification, proof theory and many other areas of computer science and mathematics. In this article we focus on a common data structure in programming, finite multisets of some well partial order. There are two natural orders one can define on the set of finite multisets of a partial order: the multiset embedding and the multiset ordering. Though the maximal order type of these orders is already known, other ordinal invariants remain mostly unknown. Our main contributions are expressions to compute compositionally the width of the multiset embedding and the height of the multiset ordering. Furthermore, we provide a new ordinal invariant useful for characterizing the width of the multiset ordering.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Logic and verification
  • Theory of computation → Proof theory
  • Theory of computation → Program reasoning
Keywords
  • Well-partial order
  • finite multisets
  • termination
  • program verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. U. Abraham and R. Bonnet. Hausdorff’s theorem for posets that satisfy the finite antichain property. Fund. Math., 159(1):51-69, 1999. URL: https://doi.org/10.4064/fm-159-1-51-69.
  2. H. J. Altman. Intermediate arithmetic operations on ordinal numbers. Mathematical Logic Quarterly, 63(3-4):228-242, 2017. URL: https://doi.org/10.1002/malq.201600006.
  3. M. Aschenbrenner and Wai Yan Pong. Orderings of monomial ideals. Fundamenta Mathematicae, 181(1):27-74, 2004. Google Scholar
  4. A. Blass and Y. Gurevich. Program termination and well partial orderings. ACM Trans. Computational Logic, 9(3):1-26, 2008. URL: https://doi.org/10.1145/1352582.1352586.
  5. R. Bonnet, A. Finkel, S. Haddad, and F. Rosa-Velardo. Ordinal theory for expressiveness of well-structured transition systems. Information and Computation, 224:1-22, 2013. URL: https://doi.org/10.1016/j.ic.2012.11.003.
  6. D. H. J. de Jongh and R. Parikh. Well-partial orderings and hierarchies. Indag. Math., 39(3):195-207, 1977. URL: https://doi.org/10.1016/1385-7258(77)90067-1.
  7. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979. URL: https://doi.org/10.1145/359138.359142.
  8. M. Džamonja, S. Schmitz, and Ph. Schnoebelen. On ordinal invariants in well quasi orders and finite antichain orders. In P. Schuster, M. Seisenberger, and A. Weiermann, editors, Well Quasi-Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends in Logic, chapter 2, pages 29-54. Springer, Berlin/Heidelberg, Germany, 2020. URL: https://doi.org/10.1007/978-3-030-30229-0_2.
  9. D. Figueira, S. Figueira, S. Schmitz, and Ph. Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s lemma. In Proc. 26th IEEE Symp. Logic in Computer Science (LICS 2011), Toronto, Canada, June 2011, pages 269-278. IEEE Comp. Soc. Press, 2011. URL: https://doi.org/10.1109/LICS.2011.39.
  10. G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326-336, 1952. URL: https://doi.org/10.1112/plms/s3-2.1.326.
  11. I. Kříž and R. Thomas. Ordinal types in Ramsey theory and well-partial-ordering theory. In J. Nešetřil and V. Rödl, editors, Mathematics of Ramsey Theory, volume 5 of Algorithms and Combinatorics, pages 57-95. Springer, Berlin/Heidelberg, Germany, 1990. URL: https://doi.org/10.1007/978-3-642-72905-8_7.
  12. J. B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Trans. Amer. Math. Soc., 95(2):210-225, 1960. URL: https://doi.org/10.2307/1993287.
  13. D. Schmidt. Well-partial orderings and their maximal order types. In P. Schuster, M. Seisenberger, and A. Weiermann, editors, Well Quasi-Orders in Computation, Logic, Language and Reasoning, volume 53 of Trends in Logic, chapter 12, pages 351-391. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-30229-0_13.
  14. S. Schmitz. The parametric complexity of lossy counter machines. In Proc. 46th Int. Coll. Automata, Languages, and Programming (ICALP 2019), Patras, Greece, July 2019, volume 132 of Leibniz International Proceedings in Informatics, pages 129:1-129:15, Dagstuhl, Germany, 2019. Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.129.
  15. J. Van der Meeren, M. Rathjen, and A. Weiermann. Well-partial-orderings and the big Veblen number. Archive for Mathematical Logic, 54(1-2):193-230, 2015. URL: https://doi.org/10.1007/s00153-014-0408-5.
  16. I. Vialard. On the cartesian product of well-orderings. arXiv:2202.07487 [cs.LO], February 2022. Submitted for publication to Order. URL: https://arxiv.org/abs/2202.07487.
  17. A. Weiermann. Proving termination for term rewriting systems. In Proc. 5th Workshop on Computer Science Logic (CSL '91), Berne, Switzerland, Oct. 1991, volume 626 of Lecture Notes in Computer Science, pages 419-428. Springer, 1991. URL: https://doi.org/10.1007/BFb0023786.
  18. A. Weiermann. A computation of the maximal order type of the term ordering on finite multisets. In Proc. 5th Conf. Computability in Europe (CiE 2009), Heidelberg, Germany, July 2009, volume 5635 of Lecture Notes in Computer Science, pages 488-498. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03073-4_50.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact