4个版本 (1个稳定版)

新版本 1.0.0 2024年8月10日
0.1.2 2024年7月10日
0.1.1 2024年7月9日
0.1.0 2024年7月9日

#195 in 数学

Download history 381/week @ 2024-07-08 4/week @ 2024-07-15 20/week @ 2024-07-29 96/week @ 2024-08-05

134次每月下载

MIT/Apache

135KB
2.5K SLoC

遗传有限集

定义了遗传有限集的数据类型,以及该类型上的许多标准数学操作。这可以视为ZFC(减去无穷公理)的实现。

简介

策梅洛-弗兰克尔集合论中,唯一的数学对象类型是集合。因此,集合只能包含更多的集合,而这些集合又可以包含更多的集合,以此类推。这种递归的最底层是空集,这是唯一一个不包含任何元素的集合。

当集合是有限的,并且它的所有元素也都是遗传有限的时,这个集合是遗传有限集。这个crate中的主要数据类型允许在合理的内存和时间约束下表示任何遗传有限集。

实现

crate中最基本的数据类型是Mset,它被简单地定义为

struct Mset(Vec<Mset>);

这是遗传有限多重集合的类型,与集合相同,但允许重复元素。元素在多重集合中出现的次数称为它的“多重性”。多重集合的多重集合也可以被视为一个根树

集合上的许多基本操作也实现了多重集合,尽管它们有时定义有所不同。例如,两个多重集合的并集取两个集合中每个元素的最大多重性,交集则取最小多重性。

Set只是一个包装在Mset上的包装器,条件是没有任何两个元素是相等的,并且每个元素也是一个集合。这个条件不是静态检查的,实际上,它被处理得与unsafe trait一样,即允许不安全代码假设这个不变性。然而,可以通过Mset::into_set或类似函数将Mset安全地转换为Set,但这会有性能损失。

我们还实现了Class,表示一个可能无限的。这只是一个对Set的包装迭代器。

优化

19世纪的数学基础并不适合计算机。每个非空集合都需要单独的堆分配,因此即使是适度的集合也可能在声明时很慢。确定集合相等或成员资格是非平凡的任务,这扩展到更复杂的操作,如取并集或交集。一个简单的集合比较算法可能具有指数级复杂性或更坏。

正是AHU算法使我们能够在合理的时间内执行这些操作。算法中的多个步骤被实现为我们内部Levels类型中的不同方法。随着更多集合关系被编码,这些函数的确切不变性和执行的过程将变得更加明确。

我们努力使每个函数在输入和输出的大小上都是“近似线性的”。确切的复杂性非常复杂,在许多情况下,“线性”是最坏的情况。例如,两个深层嵌套的集合如果不具有相同的基数,则它们的相等性几乎可以立即确定。对于浅层和大型集合,这可能会看起来更像是O(n log(n))。

所有这些都说了,瓶颈实际上在于数学本身。对于15这个只有4位的数字,需要16384个分配来表示。数字31将消耗你大部分甚至所有的RAM,而63可能永远超出了计算机的范畴。

更极端的例子是冯·诺伊曼等级将集合宇宙划分为层次。在这个序列中,只有V6这个集合已经包含了265536个元素;说它不在这个宇宙中是大大低估了。

总的来说:如果你只想测试小集合的构建,这个crate非常适用,否则则毫无用处。

为什么?

创建这个crate的主要动机是展示ZFC的荒谬。通过这个,我并不是说ZFC是坏的,甚至不是它没有用,而是如果你真正将其付诸实践,它会有非常荒谬的后果。如果你声称2和3是集合,通过冯·诺伊曼,有序对是集合,通过库拉托夫斯基,函数是有序对的集合,那么你必须主张从2到3的函数集合是

{{{{{}}}, {{{}, {{}}}, {{{}}}}}, {{{{}}}, {{{{}}}}}, {{{{}}}, {{{{}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{}, {{}}}}, {{{}, {{}}}, {{{}}}}}, {{{{}}, {{}, {{}}}}, {{{{}}}}}, {{{{}}, {{}, {{}}}}, {{{{}}}, {{{}}, {{}, {{}}}}}}, {{{{}}, {{}, {{}, {{}}}}}, {{{}, {{}}}, {{{}}}}}, {{{{}}, {{}, {{}, {{}}}}}, {{{{}}}}}, {{{{}}, {{}, {{}, {{}}}}}, {{{{}}}, {{{}}, {{}, {{}}}}}}}

你可以使用这个crate直接与这些集合等互动,而不仅仅是它们是某种数学抽象。这些示例可能为你提供了尝试构建的指导。

同样,这个代码库也是对有限主义的捍卫。很容易将其整个哲学视为一种疯狂的理论,不相信计数数集合的存在。但事实上,在计算机的有限范围内仍然可以做很多事情(尽管这实际上并不是最好的方法)。

依赖关系

~1.3–1.8MB
~43K SLoC