LogicKit

Build Status

LogicKit 是一种类似 Prolog 的语言，以 Swift 嵌入式领域特定语言 (EDSL) 的形式分发。

简短论文：LogicKit：将逻辑编程引入 Swift

动机

Prolog 是一种通用的逻辑编程语言。程序以关系的形式表达，而计算则以对这些关系的查询形式表达。逻辑编程的美妙之处在于，我们不再需要告诉计算机如何计算结果，而只需描述它应该遵守的约束。例如，以下 Prolog 代码片段查找所有和为 2 的操作数对。

add(zero, Y, Y).
add(succ(X), Y, Z) :-
  add(X, succ(Y), Z).

?- add(X, Y, succ(succ(zero))).

以这种方式编写程序可以说非常有趣。然而，正如任何其他范例一样，逻辑编程并非万能解决方案。例如，以命令式方式轻松表达的算法，通常被证明难以用函数式逻辑编程风格编写。这就是为什么大多数现代编程语言（如 Swift）都关于混合范例。

那么为什么不也将逻辑编程引入其中呢！借助 LogicKit，上面的 Prolog 示例可以完全用 Swift 重写

let zero: Term = "zero"
let x: Term = .var("x")
let y: Term = .var("y")
let z: Term = .var("z")

let kb: KnowledgeBase = [
   .fact("add", zero, y, y),
   .fact("add", .fact("succ", x), y, z) |-
     .fact("add", x, .fact("succ", y), z),
]

var answers = kb.ask(.fact("add", x, y, .fact("succ", .fact("succ", zero))))
for result in answers.prefix(3) {
  print(result)
}

入门指南

以下是一个快速入门指南，介绍了 LogicKit 的安装和使用，仅对该库进行了粗略介绍。您可能需要参考用户手册以获取更多详细信息。

快速教程

与 Prolog 类似，LogicKit 围绕知识库（或数据库）展开，可以对其进行查询。LogicKit 中有四个构造

知识库只不过是这些构造的集合

let kb: KnowledgeBase = [
  .fact("is effective against", .fact("water"), .fact("fire")),
  .fact("is effective against", .fact("fire"), .fact("grass")),
  .fact("is effective against", .fact("grass"), .fact("water")),

  .fact("has type", .fact("Bulbasaur"), .fact("grass")),
  .fact("has type", .fact("Squirtle"), .fact("water")),
  .fact("has type", .fact("Charmander"), .fact("fire")),
]

上面的知识库仅使用事实和命题。例如，它声明水对火有效，或者杰尼龟的类型是水。可以按如下方式查询此类知识库

var answers = kb.ask(.fact("has type", .fact("Squirtle"), .fact("water")))

由于单个查询可能存在多个答案，因此 Knowledge.ask(_:logger:) 不会返回单个是/否答案。相反，它返回一个序列，其每个元素表示一个正确答案。如果序列为空，则没有任何解决方案。

print("Squirtle has type water:", answers.next() != nil)
// Prints "Squirtle has type water: true"

能够以这种方式查询我们的知识库很好，但只能到此为止。更有趣的是使用 LogicKit 进行推演。让我们向我们的知识库添加一条规则

.rule("is stronger", .var("x"), .var("y")) {
  .fact("has type", .var("x"), .var("tx")) &&
  .fact("has type", .var("y"), .var("ty")) &&
  .fact("is effective against", .var("tx"), .var("ty"))
}

此规则声明，如果 x 的类型对 y 的类型有效，则宝可梦 x 比宝可梦 y 更强大。现在我们可以问这样的问题

var answers = kb.ask(.fact("is stronger", .fact("Charmander"), .fact("Bulbasaur")))

甚至更有趣的

var answers = kb.ask(.fact("is stronger", .var("a"), .var("b")))

请注意，由于查询涉及变量，我们不仅对它是否可满足感兴趣，而且还对 a 和 b 的哪些绑定感兴趣。嗯，事实上，Knowledge.ask(_:logger:) 返回的序列的每个元素都表示这样的绑定

for binding in answers {
  let a = binding["a"]!
  let b = binding["b"]!
  print("\(a) is stronger than \(b)")
}
// Prints "Bulbasaur is stronger than Squirtle"
// Prints "Squirtle is stronger than Charmander"
// Prints "Charmander is stronger than Bulbasaur"

请注意，由于 LogicKit 是 EDSL，因此没有任何东西阻止我们使用 Swift 的全部功能来使我们的定义更具可读性

let bulbasaur: Term = "Bulbasaur"
let squirtle: Term = "Squirtle"
let charmander: Term = "Charmander"

infix operator !>
func !>(lhs: Term, rhs: Term) -> Term {
  return .fact("is stronger", lhs, rhs)
}

let kb: KnowledgeBase = [
  bulbasaur  !> squirtle,
  squirtle   !> charmander,
  charmander !> bulbasaur,
]

var answers = kb.ask(bulbasaur !> squirtle)

LogicKit 提供了许多语法糖，以提高代码的可读性。请务必查看用户手册以获取全面的文档。

内置类型

以下是您可以直接在 LogicKit 中使用的内置类型列表

内置类型 构造函数 运算符 助手
Nat zero succ(_:) add(_:_:_:), sub(_:_:_:), mul(_:_:_:)
div(_:_:_:), mod(_:_:_:)
greater(_:_:), greaterOrEqual(_:_:)
smaller(_:_:), smallerOrEqual(_:_:)		 Nat.from(_:)
asSwiftInt(_:)
isNat(_:)
List empty cons(_:_:) count(list:count:)
contains(list:element:)
concat(_:_:_:)		 List.from<Collection>(elements:)
isList(_:)

关于如何使用 List.from 的示例

let list = List.from(elements: [1,2,3].map(Nat.from))
// Or
let list = List.from(elements: [Nat.from(1), Nat.from(2), Nat.from(3)])

原生谓词

原生谓词是一项实验性功能，允许 Swift 函数充当逻辑谓词。虽然它们不能用于推断逻辑变量的值，但它们可以用于检查特定绑定是否满足某些属性。一种常见的模式是使用原生谓词来定义规则的主体，以便可以使用 Swift 谓词来定义它

let isTextOutputStream = "isTextOutputStream"/1
let a: Term = .var("a")
let kb: KnowledgeBase = [
  isTextOutputStream(a) |- .native { t in
    t["a"]?.extractValue() is TextOutputStream
  }
]

安装

LogicKit 以 Swift 包的形式分发，并且可以与 Swift Package Manager 集成。

首先创建一个新包（除非您已经有一个）

mkdir MyLogicProgram
cd MyLogicProgram
swift package init --type executable

然后从您的 Package.swift 文件中将 LogicKit 添加为包的依赖项

import PackageDescription

let package = Package(
  name: "MyLogicProgram",
  dependencies: [
    .package(url: "https://github.com/kyouko-taiga/LogicKit", .branch("master")),
  ],
  targets: [
    .target(name: "MyLogicProgram", dependencies: ["LogicKit"]),
  ]
)

LogicKit 的 master 分支始终指向 LogicKit 的最新稳定版本，因此使用 .branch("master") 指定依赖项位置可保证您始终拉取最新版本。有关替代配置，请参阅 Swift Package Manager 的文档。

确保 Swift Package Manager 能够使用以下命令正确下载、编译和链接 LogicKit

swift build

如果一切顺利，您应该能够将 LogicKit 导入到您自己的 Swift 源代码中

import LogicKit

// Your code here ...

对于 Xcode 用户：您可以使用 Swift Package Manager 创建一个 Xcode 项目。一旦您添加了 LogicKit 作为依赖项并至少编译过一次您的项目，请输入命令

swift package generate-xcodeproj

它将创建一个 MyLogicProgram.xcodeproj 目录，您可以使用 Xcode 编辑它。自动生成的包的方案可能需要一些手动配置。请参阅 Xcode 的文档以获取有关该方面的更多信息。

许可证

LogicKit 根据 MIT 许可证获得许可。