end0tknr's kipple - web写経開発

太宰府天満宮の狛犬って、妙にカワイイ

kanren for python による論理プログラミング (数式の照合)

https://www.oreilly.co.jp/books/9784873118727/

上記url の 6章の写経。

「数式の照合」として、数式の変数(a,b,c)の値を算出します。

論理プログラミングというと、prologの方が記述しやすいと思いますが、 pythonの場合、算出後のデータ加工等が容易な為、 今回、 kanren for python を使用しています。

ただ、複雑な論理プログラミングは、prolog の方が良い気がします。

kanren for python は日本語の情報も少ないようですので

#!/usr/local/python3/bin/python3
# -*- coding: utf-8 -*-
from kanren import run, var, fact   # https://pypi.org/project/kanren/
import kanren.assoccomm as la


def main():
    add = 'addition' 
    mul = 'multiplication'

    # 交換法則(commutative)と結合法則(associative)の事実を定義
    
    ## 交換法則 : 2x4=4x2 のように順番を交換可
    fact(la.commutative, mul)
    fact(la.commutative, add)
    ## 結合法則 : (3×6)×2=3×(6×2) のように、()をどこにつけても結果は同じ
    fact(la.associative, mul)
    fact(la.associative, add)

    # 変数を定義
    a, b, c = var('a'), var('b'), var('c')

    # 0) ↓ 3x(-2) + (1+2+3) x (-1)
    expression_orig = (add, (mul, 3, -2), (mul, (add, 1, (mul, 2, 3)), -1))

    # 1) ↓ (1+2xa) x b + 3xc
    expression1 = (add, (mul, (add, 1, (mul, 2, a)), b), (mul, 3, c))
    # 2) ↓ cx3 x b x (2xa+1)
    expression2 = (add, (mul, c, 3), (mul, b, (add, (mul, 2, a), 1))) 
    # 3) ↓ (((2xa) x b) + b) + 3xc
    expression3 = (add, (add, (mul, (mul, 2, a), b), b), (mul, 3, c)) 

    # 数式の照合
    print(run(0, (a, b, c), la.eq_assoccomm(expression1, expression_orig)))
    print(run(0, (a, b, c), la.eq_assoccomm(expression2, expression_orig)))
    print(run(0, (a, b, c), la.eq_assoccomm(expression3, expression_orig)))

    
if __name__ == '__main__':
    main()

上記のように書くと、上記の式0と式1-3を比較し、同一式である場合、 変数a,b,cの値が算出されます。

$ ./foo.py 
((3, -1, -2),)
((3, -1, -2),)
()