10个版本 (5个破坏性更新)

0.6.3 2020年10月26日
0.6.2 2020年10月26日
0.6.1 2020年7月27日
0.5.0 2020年7月27日
0.1.0 2020年7月26日

#1263 in 数学

每月32次下载

MIT许可证

43KB
685

Avatar Graph

Avatar Graphs库。

avatar5-01.png avatar8-02.png avatar3-01.png

Avatar Graph是一种在数学编程中非常有用的特殊图。

Avatar Graph是用于路径语义定理证明技术/工具的图的子类型。

更多信息,请参阅论文Avatar Graphs

示例:Avatar Graphs和超立方体

以下是一个使用Avatar Graphs进行定理证明的示例。

猜想:任何只包含核心候选者的Avatar Graphs都与某个超立方体同构。

如果这个猜想是正确的,那么构建一个“填充”的Avatar Graph所需的节点数是

2^n 其中 n = 0, 1, 2, ...

这个猜想有一个反例

wagner.png

这被称为“Wagner图”。更多信息请见维基百科文章

更容易看出这个图与立方体不同构,如下所示

wagner-mobius.png

然而,即使这个猜想是错误的,那么2^n定律怎么样?Wagner图有8个节点,这是2^3

猜想:每个填充的Avatar Graph中的节点数都是2^n,其中n是某个值。

这个猜想有一个反例

avatar6-03.png

Avatar Graphs简介

avatar16-01.png

四维超立方体。任何超立方体都只包含称为“核心候选者”的节点。

一个更实用的示例:[Rust的新类型惯用法](https://doc.rust-lang.net.cn/rust-by-example/generics/new_types.html)。

  • 为什么这个技术有效?
  • 如何在数学上证明这种技术在一般情况下有效?
  • 这种技术如何进行泛化?

实际上,这种泛化背后存在一种数学模式。这些模式共有的特点是,它们处理对象信息的某种封装,使得对象“扮演不同的角色”,同时与原始对象“整合信息”。

在抽象层面,这种模式表现为一个“分身图”。

分身图首先是洞察和灵感的工具。通常不需要明确表示。这意味着分身图可以揭示数学理论中的一些不明确之处,而这些不明确之处在理论内部是无法看到的。

分身图的图示

原始的数学模型称为“核心自我”或“分身图中的核心”,简称“核心”。分身图用于研究从分身扩展来的核心自我的对称性。

  • 黑色节点:核心自我的候选者
  • 白色节点:N-分身,其中最小的可能的N大于零
  • 黑色边:依赖于核心自我候选者的有向边
  • 灰色/虚线边:从核心自我候选者到最高分身的唯一边

avatar7-01.png

唯一的最高分身

由于从图中移除了所有无关的结构,每个候选核心都有一个相关的唯一最高分身。

这是因为添加同一级别的新的n-分身是微不足道的,因此只有研究具有唯一最高分身的图才是有趣的。

最高分身的选择可能取决于节点的顺序。这种限制对于大多数有趣的图来说大多是不相关的。然而,它极大地简化了分身距离的计算。

分身距离

n-分身中的n在图中也是一种距离,称为“分身距离”。

分身距离计算的是到达核心自我的路径数。

它是通过首先找到所有节点的最短距离,然后通过“放松”子节点的分身距离来构建的。子节点的选择可能取决于节点的顺序。

分身距离的精确值并不重要,除非作为找到相对于核心候选者的最高分身的一种手段。

把它想象成一个需要解决的复杂谜题,而分身距离只是解决这个谜题的技术。

分身距离与最短距离的语义不同。具有相等最短距离的两个节点可以有不同的分身距离。

分身连通性

同一级别的分身不允许进行通信。

1-分身只能将信息传递给核心自我。

2-分身只能将信息传递给两个1-分身。

3-分身可以将信息传递给3x1-分身或2+1-分身。

n-分身可以将信息传递给任何较低分身的子集。

不可收缩性

当一个分身相对于最短距离只有一个子节点时,它是可收缩的,但相对于核心候选者是不允许的。

核心自我不被计入收缩性的子节点。这意味着1-分身没有子节点,因此不是只有一个子节点。人们也可以将其视为1-分身是规则的例外。

半收缩性

由于不可收缩性规则使用最短距离而不是分身距离,因此存在一些情况下分身是半收缩性的。

avatar8-04.png

具有半收缩性的图的示例。

半收缩性发生在分身可以通过分身距离收缩但无法通过最短距离收缩时。

半收缩性意味着同一级别的两个分身需要就如何整合信息达成一致。他们使用彼此作为子节点,这取决于图中节点的顺序。

此属性允许使用,否则在拓扑结构包含类似于莫比乌斯带的特征的案例中,头像图将不会是对称的。

通用可达性

在从最高头像走向核心候选者时,所有图节点都必须是可达的,且移动距离不得超过最短路径所给的距离。

换句话说,从最高头像到任何节点都存在某些路径,同时要么更靠近核心候选者,要么保持距离不变。

从另一个角度思考此属性,即对于从最高头像到核心的合适路径,可以访问任何节点。

此属性在有选择需求且希望避免退化的系统中很有益处。

无运行时依赖