kanren

使用miniKanren在Python中进行逻辑/关系编程。

安装

使用pip

pip install miniKanren

使用conda

conda install -c conda-forge miniKanren

开发

首先获取项目源代码

git clone git@github.com:pythological/kanren.git
cd kanren

安装开发依赖项

$ pip install -r requirements.txt

设置pre-commit钩子

$ pre-commit install --install-hooks

可以使用提供的Makefile运行测试

make check

动机

逻辑编程是一种通用的编程范式。然而，此实现特别旨在作为Python计算机代数系统的算法核心，以及数值软件的自动生成和优化。领域特定语言、代码生成和编译器最近一直是科学Python社区的热门话题。《kanren》旨在成为这些项目的底层核心。

这些要点——以及kanren示例——在论文"miniKanren as a Tool for Symbolic Computation in Python"中进行了介绍。

示例

kanren允许用户以目标的形式表达复杂的关联，并生成满足这些关联的值。以下代码是逻辑编程的“Hello, world!”；它请求逻辑变量 x的值，使得x == 5

>>> from kanren import run, eq, membero, var, lall
>>> x = var()
>>> run(1, x, eq(x, 5))
(5,)

可以同时使用多个逻辑变量和目标。以下代码请求一个包含 x 和 z 值的列表，使得 x == z 且 z == 3

>>> z = var()
>>> run(1, [x, z], eq(x, z),
                   eq(z, 3))
([3, 3],)

kanren 使用 统一 来匹配表达式树中的形式。以下代码请求满足 (1, 2) == (1, x) 的 x 值

>>> run(1, x, eq((1, 2), (1, x)))
(2,)

上述示例使用了 eq：一个 目标构造函数，用于在两个对象之间创建统一目标。其他目标构造函数，如 membero(item, coll)，表示更复杂的关联，通常由像 eq 这样的简单函数构建。更具体地说，membero 表明 item 是集合 coll 的成员。

以下示例使用 membero 请求所有满足条件的 x 值，即 x 是 (1, 2, 3) 和 (2, 3, 4) 的成员。

>>> run(0, x, membero(x, (1, 2, 3)),  # x is a member of (1, 2, 3)
              membero(x, (2, 3, 4)))  # x is a member of (2, 3, 4)
(2, 3)

上述示例隐式使用了目标构造函数 lall 和 lany，分别代表目标的 合取 和 析取。仅使用 lall、lany 和 eq 就可以表达许多有用的关系，但在 kanren 中，也可以轻松利用宿主语言并显式创建任何可以用 Python 表达的关系。

表示知识

kanren 以表示术语之间关系的公理的形式存储数据。以下代码创建了一个父子关系，并使用它来陈述关于辛普森一家中谁是谁的父亲的事实

>>> from kanren import Relation, facts
>>> parent = Relation()
>>> facts(parent, ("Homer", "Bart"),
...               ("Homer", "Lisa"),
...               ("Abe",  "Homer"))

>>> run(1, x, parent(x, "Bart"))
('Homer',)

>>> run(2, x, parent("Homer", x))
('Lisa', 'Bart')

我们可以使用中间变量进行更复杂的查询。例如，谁是巴特的外祖父？

>>> grandparent_lv, parent_lv = var(), var()
>>> run(1, grandparent_lv, parent(grandparent_lv, parent_lv),
                           parent(parent_lv, 'Bart'))
('Abe',)

我们可以通过创建一个目标构造函数将祖孙关系表达为不同的关系

>>> def grandparent(x, z):
...     y = var()
...     return lall(parent(x, y), parent(y, z))

>>> run(1, x, grandparent(x, 'Bart'))
('Abe,')

约束

kanren 提供了一个完整的约束系统，允许用户限制统一和对象类型

>>> from kanren.constraints import neq, isinstanceo

>>> run(0, x,
...     neq(x, 1),  # Not "equal" to 1
...     neq(x, 3),  # Not "equal" to 3
...     membero(x, (1, 2, 3)))
(2,)

>>> from numbers import Integral
>>> run(0, x,
...     isinstanceo(x, Integral),  # `x` must be of type `Integral`
...     membero(x, (1.1, 2, 3.2, 4)))
(2, 4)

图关系

kanren 带有适合基本符号代数运算的图关系操作支持。请参阅 doc/graphs.md 中的示例。

扩展 kanren

kanren 使用 multipledispatch 和 logical-unification 库 来支持用户定义类型的模式匹配。基本上，可以统一的数据类型可以与大多数 kanren 目标一起使用。请参阅 logical-unification 项目的示例，了解如何将任意类型转换为可统一。

关于

本项目是 logpy 的分支。

参考

• 维基百科上的逻辑编程
• miniKanren，这是一个基于此库的 Scheme 库，用于关系编程。更多信息可以在 威廉·伯德的论文 中找到。