Avatar Hypergraph Rewriting

带有象征区分的符号的重写超图系统

基于论文 Avatar Hypergraph Rewriting。

象征可以在重写规则的左侧使用，以控制超图演变中节点符号区分。它们可以应用于任何超边。

示例：Wolfram 与 Avatar

use avatar_hypergraph_rewriting::*;

use Expr::*;

fn main() {
    // `{0,0}`
   let a = vec![Nat(0), Nat(0)];

    // `{1,2} -> {}`
    let wolfram_rule = Rule(vec![Nat(1), Nat(2)], vec![]);
    // prints `{}` because `{0,0}` is reduced.
    println!("{}", format(&wolfram_rule.parallel(&a)));

    // `{a'(1),b'(2)} -> {}`
    let avatar_rule = Rule(vec![ava("a", 1), ava("b", 2)], vec![]);
    // prints `{0,0}` because avatars "a" and "b" must be different nodes.
    println!("{}", format(&avatar_rule.parallel(&a)));
}

动机

Avatar Hypergraph Rewriting (AHR) 是寻找满足论文 Consciousness in Wolfram Models 中假设的 Wolfram 模型的一种 Avatar Extension。

Wolfram 模型用于 Wolfram Physics Project，该项目试图使用超图重写系统解释基本物理学。

Wolfram 模型对应于带有 直觉主义命题逻辑 (IPL) 的定理证明，可以推广到同伦型理论。更多信息，请参阅 Xerxes D. Arsiwalla 和 Jonathan Gorard 的这篇论文 this paper。

IPL 是类型理论和现代数学基础的基础。IPL 比 命题逻辑 (PL) 弱。

• PL 被称为“经典”逻辑，满足布尔代数
• IPL 被称为“构造性”逻辑，满足 Heyting 代数

然而，在 Path Semantics 中，有一种甚至更弱的逻辑称为路径语义直觉主义命题逻辑 (PSI)。

PSI 比IPL和PL更少为人所知，但对数学语言设计的哲学相关。PSI与IPL不同之处在于，一个质量运算符 ~~ 提升了带有符号区分的双条件（质量是部分等价）。

与PSI密切相关的研究主题是 Avatar Extensions。

这个超图重写系统结合了符号区分的特性与象征。象征是一种设计选择，用于高效地表达符号区分。