2013-12-11

core.unify - 単一化をサポートするClojureライブラリ

(この記事はClojure Contrib Library Advent Calendar 2013の11日目の記事です)


概要

core.unifyは「単一化」をClojureで扱うためのライブラリです。作者は『Joy of Clojure』の著者の一人、Fogusさんです。

単一化はPrologなど論理プログラミングなどで使われる処理で、与えられた条件から未知の値を推論する仕組みです。単一化自体について詳しく説明するのは私には難しいので、詳しくはWikipedia等で調べて下さい;−)

ユニフィケーション - Wikipedia

抽象度が高いライブラリなので利点が分かりにくいですが、同じくFogusさんの作ったcore.constractsで使われているそうです。

fogus: Using unification to write readable Clojure macros?



Clojure Contirib Libraryにはcore.logicという論理プログラミングをするためのライブラリがあり、そちらでも単一化の機能は提供してます。ではなんでcore.unifyがあるんでしょう?
READMEを読むとcore.logicとの違いについて次のように書いてあります。

Differences from core.logic
===========================

core.unify provides a la carte unification facilities that are not deeply tied into the operation of a logic engine. While core.logic does provide a similar simple unifier interface with support for specifying fine-grained constraints, if you have no need for a logic programming system, core.unify may be a better fit.

core.unifyは、論理プログラミングをバリバリ使いたい人ではなく、単一化の機能だけを使いたい人を対象に作られてるようですね。

core.unifyは次の機能を提供します
  • 単一化の束縛を作る、置き換え、単一化を行なう関数のファクトリー関数(occur-check有り/無し)
  • 上記の処理をパッケージ化し、"?"が接頭辞になるシンボルを置き換え用の値として解釈するしくみ
※occur-checkは後述


インストール

現在の最新安定版は0.5.5です。

leiningenを使う場合は:dependenciesに以下を追加してください。

[org.clojure/core.unify "0.5.5"]

今後の最新情報&Mavenでのインストールは公式のREADME.mdを参照して下さい。


使い方

core.cljは240行程度がライブラリ本体で、あとは使用例がcommentマクロで書いてあります。

core.unify/src/main/clojure/clojure/core/unify.clj at master · clojure/core.unify

"PUBLIC API"というコメント文の下に幾つか関数が並んでますが、基本的には次の3+2個の関数を知ってればOKのようです。

  • unify, unify-
  • subst
  • unifier, unifier- 

substはsubstitute(置き換え)の略。
unify-,unifier-については後述します。


まずは単純な例から。

(require '[clojure.core.unify :as uf])

;; ?から始まるシンボルを単一化の対象として、置き換え用のマップを返す
(uf/unify '(?a ?b) '(1 2))
;=> {?b 2, ?a 1}

(uf/unify '(?a ?b) '([1 2 3] [4 5 6]))
;=> {?b [4 5 6], ?a [1 2 3]}

;; 単一化結果の置き換えマップを引数で指定することも可能
(uf/unify '(?a ?b) '(1 ?b) {'?b 9})
;=> {?a 1, ?b 9}


;; unifyで返される形式のマップで第一引数の式を置き換える
(uf/subst '(?a ?b) {'?a 1, '?b 2})
;=> (1 2)

;; 置き換え後に未知の値があったら可能な限り置き換える
(uf/subst '(?a ?b) {'?a 2, '?b '(+ 3 ?a)})
;=> (2 (+ 3 2))


;; 式の未確定の値を第二引数から単一化して置き換えたものを返す
(uf/unifier '(?a ?b) '(1 2))
;=> (1 2)

(uf/unifier '(?a ?b) '([1 2 3] [4 5 6]))
;=> ([1 2 3] [4 5 6])

(uf/unifier '(?a ?b) '(1 ?b) {'?b 9}) ; 置き換えマップを指定
;=> (1 9)

これだけだと「これ知ってる、パターンマッチングってやつじゃね?」となりそうなのでちょっと違う例を出してみます。

(uf/unify '(?a ?b) '(1 ?a))
;=> {?b 1, ?a 1}

ちゃんと「?aと?bは同じ」という単一化をしてくれてますね。 パターンマッチングとの違いについては作者Fogusさんのこのブログ記事が詳しいです。

fogus: Unification versus Pattern Matching… to the death!



「単一化ってのはなんとなく分かったけど、なんか嫌な予感がする」とおもう人もいるでしょう。その予感は正しいです。上記のように値が確定するまで推論を展開していくのなら、つぎのコードはどうなってしまうでしょう?

(uf/unify '(?a ?b) '([?a 2 3] [4 5 6]))


まず{?a [?a 2 3]}と単一化されますが、そのさきの?aをいくら単一化しても無限ループに入ってしまいます。なので実行すると「循環がありますよ」という例外が発生します。

(uf/unify '(?a ?b) '([?a 2 3] [4 5 6]))
;=> IllegalStateException Cycle found in the path [?a 2 3]  clojure.core.unify/var-unify (unify.clj:95)

この「単一化したあとにも?aのような未知な値が残っているか」というチェックをoccur-checkと呼んでいるみたいです。


しかし途中まででいいから単一化した結果が欲しい場合もあるでしょう。そういう場合には"without occur-check"な関数である"unify-","unifier-"を使います。

(uf/unify- '(?a ?b) '([?a 2 3] [4 5 6]))
;=> {?b [4 5 6], ?a [?a 2 3]}

(uf/unifier- '(?a ?b) '([?a 2 3] [4 5 6]))
;=> StackOverflowError   clojure.lang.AFn.applyToHelper (AFn.java:155)


あれれ? "unifier-"なら"([?a 2 3] [4 5 6])"を返してくれると思ったんですが、そうなりませんね。
正しい挙動なのか良くわからないので、気になる人はコードを追ってみてください。





unifyを使って簡単なデータベースを作ってみます。

(def database [[:Superman :is :ClarkKent]
               [:Batman :is :BruceWayne]
               [:Conan :is :Shinichi]
               [:AnpanMan :is :AnpanMan]
               [:Batman :fought :Joker]
               [:AnpanMan :fought :BaikinMan]])

(defn query [q]
  (filter (fn [m] (not (nil? m)))
          (map #(uf/unify % q) database)))

;; バットマンの正体は誰?
(query '[:Batman :is ?who])
;=> ({?who :BruceWayne})

;; ヒーロー名と正体が同じ人は?
(query '[?who :is ?who])
;=> ({?who :AnpanMan})

;; ヒーローの敵はだれ?
(query '[_ :fought ?enemy])
;=> ({?enemy :Joker} {?enemy :BaikinMan})

;; コナンは(略
(query '[:Conan :is ?who])
;=> ({?who :Shinichi})

いまいち単一化が必要な例じゃないですが、まぁこんな感じでも使えます。

もう少し実用的なのはこちらのFogusさんの記事を見て下さい。core.constracts内で、substを簡易マクロのように使ってるみたいです。



まとめ

  • 単一化の処理を提供するcore.unifyライブラリを紹介しました
  • unify、subst、unifierを知っておけば大丈夫
  • 単一化は循環する場合があるから気をつけてね
    • その場合はunify-,unifier-(?)を使ってね
  • 実用的な例を作りたかったけど思いつかなかった(´・ω・`)


次回12日の発表者はまだ決まってないようです athosさんです。

カレンダーはまだ何日か空いてるようなので誰か書いてみませんか?(個人的にはcore.unifyつながりでcore.constractsが気になるなぁ)

Clojure Contrib Library Advent Calendar 2013 - connpass

0 件のコメント: