Axiomatic

Axiomatic 是一个逻辑框架，它接受事实和规则的声明，并提供一种机制来运行查询，以确定一个语句是否为真，如果是，在什么条件下为真。Axiomatic 构建在统一框架 Gluey 之上，并通过定义树状统一类型以及适用于逻辑编程的查询系统来扩展它。Axiomatic 密切基于逻辑编程语言 Prolog 以及 Horn 子句 的数学概念。

逻辑编程不是要求你编写一个逐步的算法来解决问题，而是要求你提供一组事实和规则。例如，我们可以从给出“草是绿色的”这个事实 color(grass, green) 和 “绿色的东西很棒”这个规则 awesome(X) :- color(X, green) 开始，然后查询 “草是否真的很棒” ?- awesome(grass)。请注意，“grass” 和 “green” 的顺序并不重要，只要我们在内部保持一致即可。逻辑编程不仅仅让我们问是或否的问题，我们还可以要求它找到所有符合我们约束条件的可能解决方案。

考虑以下事实和规则 (表示为一个 Prolog 程序)

parent(matt, jaden).
parent(tuesday, jaden).
parent(debbie, matt).
parent(dennis, matt).
parent(liz, tuesday).
parent(mike, tuesday).

grandparent(A, B) :- parent(A, X), parent(X, B).

我们可以很容易地查询 Jaden 的祖父母是谁，?- grandparent(G, jaden)，得到的响应是 G 是 Debbie、Dennis、Liz 或 Mike，正如我们所预期的那样。

逻辑编程提供了一个非常简单的机制来找到可以从一组规则中轻松推导出的答案。无需担心枚举所有可能的匹配项，甚至无需自己回溯，因为框架会处理所有这些。

Term（项）是 Axiomatic 提供的最原始的逻辑类型。本质上，它允许您定义原子（atoms），例如 jaden 和 green，以及复杂的复合项（compound terms），例如 awesome(jaden) 或 triangle(point(0, 0), point(1, 1), point(0, 1))。项（Terms）由一个 name（名称）以及 0 个或多个 arguments（参数）组成。虽然名称必须是字面值（literal value），但参数可以是变量。例如，color(X, purple) 讨论的是所有紫色的东西！

let s = Term(name: "cool", arguments: [.Literal(Term(atom: "swift"))])  // cool(swift).
let p = Term(name: "cool", arguments: [.Literal(Term(atom: "prolog"))]) // cool(prolog).

请注意，Term 的每个参数的类型都是 Unifiable<Term>，因此您必须指定参数是 Unifiable.Literal(Term) 还是 Unifiable.Variable(Binding)。作为提醒，Binding 是 Gluey 定义的一种类型，可以与同一类型的其他实例进行统一。它用于表示此框架内的变量，因为它们通过统一过程绑定在一起，并且通常位于不同项中的两个变量应该引用相同的值。

子句（Clauses）声明 X 蕴含 Y 形式的语句。其中 Y 称为子句的 head（头部），它由单个项组成，而 X 称为子句的 tail（尾部），它由一组项组成，当这些项都为真时，意味着头部为真。tail 为空的特殊情况称为事实（fact），因为它是不容置疑的真理。否则，子句称为规则（rule），因为尾部定义了头部被认为是真的充分条件。

作为提醒，Clause 完全由我们的 Term 组成。例如，子句 happy(monkey) :- eating(monkey, banana) 表示，只要术语 eating(monkey, banana) 为真，则术语 happy(monkey) 为真。但是，这并不意味着相反的情况，因为可能存在另一个子句说，如果猴子在荡秋千，它也会很高兴。

子句可以而且经常使用带有变量参数的术语来指定条件真理。这是通过声明一个 Binding 并将其用作子句中一个或多个术语中一个或多个参数中的变量来完成的。请注意，在单独子句中的多个变量之间共享同一个 Binding 是非法的，但不会被检查，这样做会导致未定义的行为。

// awesome(X) :- color(X, green).
let x = Binding<Term<String>>()
let c = Clause(
     rule: Term(name: "awesome", arguments: [
          .Variable(x)
     ]),
     conditions: [
          Term(name: "color", arguments: [
               .Variable(x),
               .Literal(Term(atom: "green"))
          ])
     ]
)

现在你可能在想，哇，这对于这样一个简单的 Prolog 查询来说，是一个非常冗长的定义，你是对的。Axiomatic 并非旨在“开箱即用”地构建程序，而是旨在用作依赖逻辑的程序的基础。此外，在 Axiomatic 之上提供一个抽象，使其适用于特定的用例，相对容易且直接。

一旦你随心所欲地定义了子句，你终于准备好用它们做一些事情了。System 提供了一个初始化器，它接受一系列子句，并构建一个可以轻松查询的逻辑系统。让我们看看上面我们的祖父母示例作为一个 Axiomatic 系统是什么样的！

let system = System(clauses: [
    // parent(matt, jaden).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Matt")),
        .Literal(Term(atom: "Jaden"))
    ])),
    // parent(tuesday, jaden).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Tuesday")),
        .Literal(Term(atom: "Jaden"))
    ])),
    // parent(debbie, matt).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Debbie")),
        .Literal(Term(atom: "Matt"))
    ])),
    // parent(dennis, matt).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Dennis")),
        .Literal(Term(atom: "Matt"))
    ])),
    // parent(liz, tuesday).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Liz")),
        .Literal(Term(atom: "Tuesday"))
    ])),
    // parent(mike, tuesday).
    Clause(fact: Term(name: "parent", arguments: [
        .Literal(Term(atom: "Mike")),
        .Literal(Term(atom: "Tuesday"))
    ])),
    // grandparent(A, B) :- parent(A, X), parent(X, B).
    Clause{ A, B, X in (
        rule: Term(name: "grandparent", arguments: [.Variable(A), .Variable(B)]),
        conditions: [
            Term(name: "parent", arguments: [.Variable(A), .Variable(X)]),
            Term(name: "parent", arguments: [.Variable(X), .Variable(B)])
        ]
    )}
])

该死，这太长了！好吧，别担心。正如我们所说，句法简洁从来都不是目标！那么我们刚刚做了什么？我们定义了一个逻辑事实和规则的 System，我们以后可以查询它。

请注意，我们的祖父母规则的初始化程序接受一个 lambda？好吧，Axiomatic 为 Clause 定义了这些便利的初始化程序，因此你可以定义规则，而无需单独声明 Binding。只需将一个 lambda 传递给 Clause 的初始化程序，该 lambda 接受你想要的任意数量的 Binding 参数（最多 6 个），并返回它通常期望的参数元组。如果你感到困惑，请不要担心，这只是一种语法上的便利；你仍然可以在外部作用域中单独声明你的绑定。

那么我们如何查询这个系统呢？好吧，有一个名为 enumerateMatches 的奇特小函数专门用于此！

let G = Binding<Term<String>>()
let query = Term(name: "grandparent", arguments: [.Variable(G), .Literal(Term(atom: "Jaden"))])
try system.enumerateMatches(query) {
    print(G) // -> Debbie -> Dennis -> Liz -> Mike
}

当当当当！很简单，对吧？请注意，我们必须使用 try 调用该函数。这是因为我们的查询可能根本无法统一。此外，你不能保证每个 Binding 在回调中都有一个非 nil 值。如果逻辑系统对变量的限制不足，则可能会在没有找到实际具体值的情况下统一该变量。

默认情况下，enumerateMatches 将为每个可能的匹配调用回调。如果你想在任何给定的匹配后返回，只需抛出 SystemException.Break，系统将停止统一过程。

你不能保证变量的统一状态在你从回调返回后仍然存在。因此，请确保记录你可能需要在回调内部知道的任何信息。

那么这个花哨的 enumerateMatches 函数是如何工作的呢？好吧，它使用一个称为 统一 的过程，通过该过程枚举和尝试所有可能的匹配项，在成功时递归查询子句的依赖项，在失败时回溯。我们将更详细地查看该算法。如果你只是想使用此库，请随意跳过本节。

第一步是，给定一个目标，确定我们可能能够统一的可能的子句。任何与我们的子句具有相同函子（functor）（名称和元数）的子句都是统一的潜在候选者。幸运的是，System 存储了一个 [Functor : [Clause]] 类型的字典，因此查找与给定术语兼容的子句列表非常有效。

对于每个合适的候选者，我们将尝试将子句的头部与我们的查询统一。如果统一失败，我们已经确定它们是不兼容的，然后我们进入下一个子句。如果与头部的统一成功，我们已经确定该子句提供了对此查询的见解。回想一下，只有当其主体的每个术语也为真时，子句的头部才为真。因此，如果我们能够统一其主体，我们可以认为该查询已与此子句统一。因此，我们必须在其主体的每个术语上递归调用 enumerateMatches。

如果我们能够统一主体中的所有这些术语，那么我们应该调用回调。为此，我们将第一个术语的回调设置为统一第二个术语，并将该术语的回调设置为统一第三个术语，依此类推。最终术语的回调将调用原始传入的 lambda，因此将在主体中的所有术语都已统一后调用它。

如果在任何时候失败，我们都会回溯到最后一个选择点并从那里继续。同样，在将成功的匹配项通知给调用者之后，我们会模拟一个错误的发生，这样我们就可以再次回溯到最后一个选择点，以便找到下一个匹配项。请注意，此回溯涉及弹出调用堆栈和恢复先前的统一状态。前者使用 Swift 的有效异常处理来完成，而后者通过在选择点保存统一状态快照并在稍后捕获发生的异常以恢复该快照来完成。

总的来说，寻找匹配项的过程非常简单！只需查看查询可能匹配的所有子句，尝试将其与子句的头部统一，然后与子句的主体统一。如果所有这些都成功了，我们就找到了匹配项！如果不是，继续寻找！如果想了解更多信息，请查看 源代码！

如果你有兴趣了解如何执行两个单个术语的统一，你应该首先阅读 Gluey 的文档，因为它只是该模块提供的功能的次要扩展。事实上，Axiomatic 唯一的修改是引入了一个 Term 类型，它是一个树状数据结构。由于 Gluey 中的 Unifiable 值已经支持递归统一，因此当两个术语统一时，它只是尝试统一它们的每个参数。超级简单！如果你不相信我，这里是 源代码中的定义！

希望这篇文档能很好地介绍了逻辑编程和 Axiomatic 框架。 如果你仍然感到困惑，请浏览一下 源代码，查看一些 测试用例，也许还可以阅读文档。 如果你仍然迷路，请随时 发推给我！ :)