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 one of the most common data structure in programming, the finite multiset of some wpo. There are two natural orders one can define on the set of finite multisets $M(X)$ of a partial order $X$: the multiset embedding and the multiset ordering, for which $M(X)$ remains a wpo when $X$ is. Though the maximal order type of these orders is already known, the 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.
翻译:良拟序及其用于度量的序数不变量,在集合论、程序验证、证明论以及计算机科学与数学的许多其他领域中具有重要意义。本文重点关注编程中最常见的数据结构之一——某个良拟序的有限多重集。对于偏序集$X$的有限多重集集合$M(X)$,可以定义两种自然序:多重集嵌入序和多重集序,当$X$为良拟序时,$M(X)$仍是良拟序。尽管这些序的最大序型已知,但其他序数不变量仍大多未知。我们的主要贡献是:给出组合计算多重集嵌入序的宽度和多重集序的高度的表达式。此外,我们提供了一个新的序数不变量,用于刻画多重集序的宽度。