Avalog

Avalog是一个使用类似Prolog语法的Avatar逻辑的实验性实现。

=== Avalog 0.7 ===
Type `help` for more information.
> parent'(alice) : mom
> (bob, parent'(alice))
> prove mom(bob) => parent'(alice)
parent'(alice) : mom
(bob, parent'(alice))
----------------------------------
mom(bob) => parent'(alice)

OK

要从终端运行Avalog，请输入

cargo install --example avalog_repl avalog

然后，要运行

avalog_repl

基于论文Avatar Binary Relations。

动机

Avatar Logic试图创建一种满足“avatars”的正式语言，类似于Avatar Extensions。Avatar Extensions是Path Semantics中的一种抽象泛化技术，Path Semantics是一种非常适用于数学编程的高度表达性语言。

在更高维度的编程中，如Path Semantics，人们希望同时泛化多个维度的抽象，而无需为每个维度编写公理。

如果常规编程是二维的，那么Path Semantics中的常规路径就是三维的。Avatar Extensions试图超越三维编程到任意高维度。Avatar Logic是讨论Avatar Graphs的解释的一个深刻结果，它将笛卡尔组合学的变体与图、群作用和拓扑联系起来。

示例：奶奶爱丽丝

uniq parent
parent'(alice) : mom
grandparent'(alice) : grandma
parent'(bob) : dad
(bob, parent'(alice))
(carl, parent'(bob))
(X, grandparent'(Z)) :- (X, parent'(Y)), (Y, parent'(Z)).

这可以用来证明以下目标

grandma(carl) => grandparent'(alice)

第一个语句uniq parent表示1-avatar parent应该表现出独特性。基本上，这意味着一个人最多只能有一个妈妈和一个爸爸。

当这个特性关闭时，人们只能说例如“鲍勃有一个名叫爱丽丝的妈妈”，但不能说“鲍勃的妈妈是爱丽丝”，因为鲍勃可能有多个妈妈。

从形式上讲，mom(bob) => parent'(alice)（具有）与mom(bob) = parent'(alice)（是）。

语句parent'(alice) : mom表示Alice有一个1-化身“parent”，被分配了“mom”的角色。化身逻辑“知道”Alice和Alice作为parent是同一个人，但与Alice的关系是普遍的，而作为parent的关系则取决于上下文。

关系(bob, parent'(alice))没有指定Bob和Alice作为parent如何相关联，因为这是从分配给Alice作为parent的角色中推断出来的。这对于编程的高维度逻辑大大简化了逻辑。

(a, b)

p(a, b)         b : p           p(a) = b
p(a, q'(b))     q'(b) : p       p(a) = {q'(_)} ∈ q'(b)

p(a) = q'(b)