microkanren

microkanren 是一个嵌入式Python的miniKanren风格关系编程语言实现。求解器以μKanren[^1]风格实现。它提供了一个扩展语言的框架，以及cKanren[^2]风格的差异性和有限域约束的基本实现。

由于Python与参考实现语言（Scheme、Racket）之间的差异，有必要对典型的miniKanren API进行一些调整。目标是捕捉miniKanren语言家族的精神，而不是确切的API。

• 安装
• 使用方法
  • 基本使用
  • 合取和析取
  • 结果类型和多个顶级变量
  • 定义目标构造函数
    • 递归目标构造函数和 snooze (Zzz)
• 开发microkanren

安装

pip install microkanren

使用方法

基本使用

基本目标构造函数是 eq。 eq 接受两个项作为参数，并返回一个目标，如果项可以统一，则成功，否则失败。

>>> from microkanren import eq
>>> eq("🍕", "🍕")
<microkanren.core.Goal object at 0x7f07d85cced0>

要运行目标，请使用以下提供的接口之一：run、run_all 或 irun。 run 接受两个参数

1. 一个整数，要返回的最大结果数；以及
2. 一个带有位置参数的可调用对象，每个参数都将接收一个新的逻辑变量。

run_all 和 irun 只接受一个参数，即新的变量接收器。

>>> from microkanren import run
>>> run(1, lambda x: eq(x, "🍕"))
['🍕']

run 和 run_all 的返回类型是（可能为空）的结果列表。如果列表为空，则没有满足目标的结果。 irun 返回一个生成器，它产生单个结果。

>>> from microkanren import irun
>>> rs = irun(lambda x: eq(x, "😁"))
>>> next(rs)
'😁'
>>> next(rs)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
StopIteration

合取和析取

连接和析取操作由变量参数函数 conj 和 disj 提供。Goal 对象支持使用 | 和 & 运算符进行组合，它们对应于 conj 和 disj。

>>> from microkanren import run_all
>>> run_all(lambda x: disj(eq(x, "α"), eq(x, "β"), eq(x, "δ")))
['α', 'β', 'δ']
>>> run_all(lambda x: eq(x, "α") | eq(x, "β") | eq(x, "δ"))
['α', 'β', 'δ']
>>> run_all(lambda x: eq(x, "ω") & eq(x, "ω"))
['ω']
>>> run_all(lambda x: conj(eq(x, "ω"), eq(x, "ω")))
['ω']

结果类型和多个顶级变量

如果提供给接口的新变量接收器具有 1 个参数，则结果将是单个元素。如果它具有大于 1 的参数，则结果将是一个值元组，每个值按位置映射到接收器的参数。

>>> run_all(lambda x, y: eq(x, "foo") & eq(y, "bar") | eq(x, "hello") & eq(y, "world"))
[('foo', 'bar'), ('hello', 'world')]

定义目标构造函数

在顶层程序中调用目标构造函数很快就会变得难以管理。为了减轻这一点，您可以定义自己的目标构造函数。

目标构造函数是一个接受零个或多个参数并返回一个 Goal（或实现 GoalProto 的某个对象）的函数。

Goal 是一个可调用对象，它接受一个 State 并返回一个 State 对象的 Stream。

Stream 是以下之一：

• 空的（mzero）；
• 一个无参数的可调用对象，它返回一个 Stream（一个延迟计算）；或者
• 一个元组，(State, Stream)。

>>> def likes_pizza(person, out):
...     return eq(out, (person, "likes 🍕"))
...
>>> run_all(lambda q: likes_pizza("Jane", q) | likes_pizza("Bill", q))
[('Jane', 'likes 🍕'), ('Bill', 'likes 🍕')]

如上例所示，根据其他目标的组合来定义目标可能很方便。但是，如果您需要访问当前状态，您可以显式地定义由目标构造函数返回的目标。

def my_constructor(x):
    def _my_constructor(state):
        if there_is_something_about(x):
            return unit(state)
        return mzero

    return Goal(_my_constructor)

将您的目标包装在 Goal 中意味着它可以与其他目标使用 | 和 & 进行组合。

递归目标构造函数和 snooze (Zzz)

如果您的目标构造函数是直接递归的，它将永远不会终止。

>>> def always_pizza(x):
...     return eq(x, "🍕") | always_pizza(x)
...
>>> run(1, lambda x: always_pizza(x))
...
RecursionError: maximum recursion depth exceeded while calling a Python object

我们提供了 snooze 来延迟目标的构建，直到需要时。使用 snooze，我们可以将 always_pizza 固定为返回无限流披萨。

>>> def always_pizza(x):
...     return eq(x, "🍕") | snooze(always_pizza, x)
...
>>> rs = irun(lambda x: always_pizza(x))
>>> next(rs)
'🍕'
>>> next(rs)
'🍕'
>>> next(rs)
'🍕'
>>> next(rs)
'🍕'

开发microkanren

microkanren 当前需要 Python 3.11。

1. git clone git@github.com:jams2/microkanren.git
2. pip install -e .[dev,testing]

使用 pytest 运行测试。

使用 black 和 ruff 格式化代码。

black .
ruff check --fix src tests

[^1]: μKanren: A Minimal Functional Core for Relational Programming (Hemann & Friedman, 2013) [^2]: cKanren: miniKanren with constraints (Alvis et al, 2011) [^3]: 这里修改了 μKanren 论文中原始的 fives 示例，以提供更多披萨