python邏輯編程之kanren

https://github.com/logpy/logpy

https://pypi.org/project/kanren/

 https://www.yiibai.com/ai_with_python/ai_with_python_logic_programming.html

kanren

python邏輯編程

示例：

KANEN是關系的表達式和滿足他們的價值的搜索。下列代碼就是邏輯編程的"Hello, world!" ，最簡單的示例。他請求一個數 x，如x ==5

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

多個變量和多個目標可以同時使用。下列代碼請求一個數x，如 x==z，同時z==3

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

KANN使用統一模式匹配的高級形式來匹配表達式樹。下列代碼請求一個數 X，如（1, 2）=（1，x）。

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

 

前面的例子中使用的 eq，表述的是兩個表達式相等。membero(item, coll) 表示 item  是 coll集合中的一個成員。下面例子使用 兩次 membero去請求 x 的2個值，

>>> run(2, x, membero(x, (1, 2, 3)),  # x is a member of (1, 2, 3) #x是（1,2,3）的成員之一
              membero(x, (2, 3, 4)))  # x is a member of (2, 3, 4) #x是（2,3,4）的成員之一   
#2 表示求兩個解，則，變量x，可能的解為 （2,3）

(2, 3)

 

邏輯變量

下面例子中，z = var() 創建一個邏輯變量.  您還可以選擇為變量命名，以方便后面調試：

>>> z = var('test')
>>> z
~test

也可以用  vars() 帶一個整形參數一次創建一組邏輯變量:

>>> a, b, c = vars(3)
>>> a
~_1
>>> b
~_2
>>> c
~_3

 

Representing Knowledge

知識表達

kanren存儲兩個條件之間的狀態關系的數據。

kanren stores data as facts that state relationships between terms.、

下面代碼創建一個親緣關系，並且使用它來判斷誰是 Simpsons家庭的父親。

The following code creates a parent relationship and uses it to state facts about who is a parent of whom within the Simpsons family.

>>> 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')

我們可以使用中間變量來進行更復雜的查詢。Bart的祖父是誰？

We can use intermediate variables for more complex queries. Who is Bart's grandfather?

>>> y = var()
>>> run(1, x, parent(x, y),
              parent(y, 'Bart'))
('Abe',)

 

 

我們可以分別表達祖父關系。在這個例子中，我們使用CONDE，一個用於邏輯和/或OR的目標構造函數。

We can express the grandfather relationship separately. In this example we use conde, a goal constructor for logical and and or.

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

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

 

數據結構

kanren 依賴 functions, tuples, dicts, and generators. 可以很容易融入以往的代碼。

Extending kanren to other Types

kanren uses Multiple Dispatch and the unification library to support pattern matching on user defined types. Also see unification (wikipedia). Types which can be unified can be used for logic programming. See the project examples for how to extend the collection of unifiable types to your use case.

Install

With pip or easy_install

pip install kanren

From source

git clone [e-mail]:logpy/logpy.git
cd logpy
python setup.py install

Run tests with tox

tox

支持

kanren supports Python 2.7+ and Python 3.3+ with a common codebase. It is pure Python and requires no dependencies beyond the standard library, toolz, multipledispatch, and unification.

簡而言之，它是一種輕量級的依賴。

作者

Matthew Rocklin

License

New BSD license. See LICENSE.txt

Motivation

Logic programming is a general programming paradigm. This implementation however came about specifically to serve as an algorithmic core for Computer Algebra Systems in Python and for the automated generation and optimization of numeric software. Domain specific languages, code generation, and compilers have recently been a hot topic in the Scientific Python community. kanren aims to be a low-level core for these projects.

References

• Logic Programming on wikipedia
• miniKanren, a Scheme library for relational programming on which this library is based. More information can be found in the thesis of William Byrd.
• core.logic a popular implementation of miniKanren in Clojure.

如果涉及到某些函數不會用，不知道做啥用的，直接下載源代碼，查看里面的各個文件，都有詳細的解釋。

解決難題

邏輯編程可用於解決許多問題，如8拼圖，斑馬拼圖，數獨，N皇后等。在這里，舉例說明斑馬拼圖的變體如下 -

有五間房子。
英國人住在紅房子里。
瑞典人有一只狗。
丹麥人喝茶。
綠房子在白房子的左邊。
他們在綠房子里喝咖啡。
吸Pall Mall的人有鳥。
吸Dunhill在的人黃色房子里。
在中間的房子里，他們喝牛奶。
挪威人住在第一宮。
那個抽Blend的男人住在貓屋旁邊的房子里。
在他們有一匹馬的房子旁邊的房子里，他們吸Dunhill煙。
抽Blue Master的人喝啤酒。
德國人吸Prince煙。
挪威人住在藍房子旁邊。
他們在房子旁邊的房子里喝水，在那里吸Blend煙。

Text

在Python的幫助下解決誰有斑馬的問題。
導入必要的軟件包 -

from kanren import *
from kanren.core import lall
import time

 

Python

現在，我們需要定義兩個函數 - left()和next()來查找哪個房屋左邊或接近誰的房子 -

def left(q, p, list):
   return membero((q,p), zip(list, list[1:]))
def next(q, p, list):
   return conde([left(q, p, list)], [left(p, q, list)])

 

Python

現在，聲明一個變量:houses，如下 -

houses = var()

 

Python

需要在lall包的幫助下定義規則如下。

有5間房子 -

rules_zebraproblem = lall(
   (eq, (var(), var(), var(), var(), var()), houses),     #5個var（）分別代表 人、煙、飲料、動物、屋子顏色

   (membero,('Englishman', var(), var(), var(), 'red'), houses),
   (membero,('Swede', var(), var(), 'dog', var()), houses),
   (membero,('Dane', var(), 'tea', var(), var()), houses),
   (left,(var(), var(), var(), var(), 'green'),
   (var(), var(), var(), var(), 'white'), houses),
   (membero,(var(), var(), 'coffee', var(), 'green'), houses),
   (membero,(var(), 'Pall Mall', var(), 'birds', var()), houses),
   (membero,(var(), 'Dunhill', var(), var(), 'yellow'), houses),
   (eq,(var(), var(), (var(), var(), 'milk', var(), var()), var(), var()), houses),
   (eq,(('Norwegian', var(), var(), var(), var()), var(), var(), var(), var()), houses),
   (next,(var(), 'Blend', var(), var(), var()),
   (var(), var(), var(), 'cats', var()), houses),
   (next,(var(), 'Dunhill', var(), var(), var()),
   (var(), var(), var(), 'horse', var()), houses),
   (membero,(var(), 'Blue Master', 'beer', var(), var()), houses),
   (membero,('German', 'Prince', var(), var(), var()), houses),
   (next,('Norwegian', var(), var(), var(), var()),
   (var(), var(), var(), var(), 'blue'), houses),
   (next,(var(), 'Blend', var(), var(), var()),
   (var(), var(), 'water', var(), var()), houses),
   (membero,(var(), var(), var(), 'zebra', var()), houses)
)

 

Python

現在，用前面的約束運行解算器 -

solutions = run(0, houses, rules_zebraproblem)

 

Python

借助以下代碼，可以提取解算器的輸出 -

output_zebra = [house for house in solutions[0] if 'zebra' in house][0][0] 

Python

以下代碼將打印解決方案 -

print ('\n'+ output_zebra + 'owns zebra.') 

Python

上述代碼的輸出如下 -

German owns zebra.