【LPN】2 Unification and Proof Search

* 2 Unification and Proof Search
 - Unificationっていまいちつかめてないんだよなぁ。
   やってることはわかるんだけど、なんでそれを
   Unificationと呼ぶのというところが釈然としない。
   PAIPでも引掛った記憶が。
 - websterによると、、、
   unify: to make into a unit or a coherent whole
   あ、このa coherent wholeの方の意味のだったら納
   得できる！
** 1 Unification
 - PrologはUnificationするだけでなく、variablesに
   ついてUnificationが成功するようなinstantiations
   を実施してそれをプログラマに返却する。
 - Unifyの定義。
 - =/2の導入。=/2が、まんまUnifyの実装なんだ。

?- =(aka,aka).
true.

?- =(aka,hoge).
fail.

 - お、Prologってinfixで書いてもいいんだ。

?- aka = aka.
true.

?- aka = hoge.
fail.

 - Prologでのsymbolsはcharactersのこと。なので、an
   atomはsymbolsから構成される。Common Lispとは違う。

 - 一応Unifyの定義の構造を書いておく。
   - Clause 1: a constantとa constantのunify。
   - Clause 2: a variableとa termのunify。付随して、
     a variableとa variableのunify。
   - Clause 3: a complex termとa complex termの
     unify。
   - Clause 4: ufifyの定義は上記3つで必要十分であ
     ることの言明。

 - k(s(g),t(k)) = k(X,t(Y)).がunify可能かどうか。
   - complex termsなのでClause 3。
    - functorとarityは同じである。
    - よって、argumentsがそれぞれunifyして
      instansiationsに一貫性があるならばok。
     - ひとつめのargument。
      - 一方がa variableなのでClause 2。
      - X = s(g)でinstatiationsにてunify。。
     - ふたつめのarguments。
      - complex termsなのでClause 3。
       - functorとarityは同じである。
       - よって、the argumentがunifyして
         instantiationsに一貫性があるならok。
        - the argument。
         - 一方がa variableなのでClause 2。
         - Y = kでinstatiationsにてunify。
        - instansiationsに一貫性があるのでok。
    - instansiationsに一貫性があるのでok。
 - loves(X,X) = loves(marcellus,mia).がunify可能か
   どうか。
   - complex termsなのでClause 3。
    - functorとarityは同じである。
    - よって、argumentsがそれぞれunifyして
      instantiationsに一貫性があるならok。
     - ひとつめのargument。
      - 一方がa variableなのでClause 2。
      - X = marcelluslでinstantiationsにてunify。
     - ふたつめのarugumet。
      - 一方がa variableなのでClause 2。
      - X = miaでinstantiationsにてunify。
    - instatiationsに一貫性が無いのでunifyしない。

*** The occurs check

 - Unificationは計算機科学の様々な分野で使われてい
   て、徹底的に研究されつくしている。Unificationに
   関するアルゴリズムもたくさんある。
 - Prologはそれらstandard algorithmsを使用していな
   い。
 - standard alogrithmsでは、

   father(X) = X.

   はunifyしない。functorの数をかぞえるとすると、
   左側の方が常に1多いと考えるから。
 - Prologのlunificationはこれをunifyすると考える。
   これはClause 2による。そしてXはfather(X)だから、
   Xはfather(father(X))であり、さらに、Xは
   father(father(father(X)))であり、という終りがな
   い展開を実行する。
 - 実行するとどうなるかは処理系による。out of
   memoryになるものもある。やってみよう。

?- father(X) = X.
X = father(**).

?- 

   あり？ なんか対処がなされているようだ
   (SWI-prolog)。

 - たぶん、father(**)は無限回のfatherの入れ子を表
   わすのだろう。そうすれば、

   father(father(**)) = father(**).

   だ。これやってみよう。
 
?- father(father(**)) = father(**).
fail.

?- 

   なんですとぉ！

   そうか。**がatomと認識されているんだな。

?- =(**,**).
true.

?- =(X,**).
X = **.

?-

   読み書き不変性をもっていないのだと推測。

   ちょっと遊んでみる。

?- father(Y) = X, mother(X) = Y .
Y = mother(father(**)),
X = father(mother(**)).

?- X = father(X), Y = father(Y), X = Y .
X = father(**),
Y = father(**).

?- 

 - standard alogorithmsはvariablesによる自己言及を
   禁止している、ということかなぁ。それがoccurs
   checkであると。
 - Prologはoccurs checkをしない。それがshort cut。
   そしてoptimisitc(楽観的)であるという所以。
 - 安全性はプログラマが自分で確保せよ、と。
 - Prologにもstandard unificationはあるよ。

?- unify_with_occurs_check(father(X),X).
fail.

?- 

 - しかしPrologが対象として無限そのものも扱える、と
   いうのは凄いな。

*** Programming with unification
 - horizontalとverticalの例。Unificationすごい。。。
   パワフルだ。
 - unificationを利用したプログラミングスタイルは、
   対象領域の概念がhierarchical(階層制、階級制)で
   あるときに有効である。

** 2 Proof Search
 - a queryがsatisfiedである(満足する、充足する)か
   どうか、a knowledge baseを探索することをproof
   searchと呼ぶ。
 - choice points。Prologは探索にあたって、他の選択
   肢がありえるところをchoice pointsとして保持して
   いる。ある枝にて探索が失敗した場合、choice
   pointsに戻ってやり直すことをbacktrackingという。
 - ;はPrologに、the last choice pointにバックトラッ
   クして探索することを指示するものだ。
 - Prologの探索木(search tree)の概念の説明。
 - Prologのfactsは消費されない。

** 3 Exercises

 - Exercise 2.1.
  - 1. bread = bread.
    unify.
  - 2. 'Bread' = bread.
    not unify.
  - 3. 'bread' = bread.
    unify.
  - 4. Bread = bread.
    unify.
    instantiations: Bread = bread.
  - 5. bread = sausage.
    not unify.
  - 6. food(bread) = bread.
    not unify.
  - 7. food(bread) = X.
    unify.
    instantiations: X = food(bread).
  - 8. food(X) = food(bread).
    unify.
    instantiations: X = bread.
  - 9. food(bread,X) = food(Y,sausage)
    unify.
    instantiations: X = sausage, Y = bread.
  - 10. food(bread,X,beer) = food(Y,sausage,X).
    not unify.
  - 11. food(bread,X,beer) = food(Y,kahuna_burger).
    not unify.
  - 12. food(X) = X.
    unify.
    instantiations: X = food(**). (swi-prolog)
  - 13. meal(food(bread),drink(beer)) = meal(X,Y).
    unify.
    instantiations: X = food(bread), Y = drink(beer).
  - 14. meal(food(bread),X) = meal(X,drink(beer)).
    not unify.

 - Exercise 2.2.
  - 1. ?- magic(house_elf).
    fail.
  - 2. ?- wizard(harry).
    fail.
  - 3. ?- magic(wizard).
    fail.
  - 4. ?- magic('McGonagall').
    true.
    (inner?)instantiations: X = 'McGonagall'.
  - 5. ?- magic(Hermione).
    Hermione = dobby;
    Hermione = hermione;
    Hermione = 'McGonagall';
    Hermione = rita_skeeter.
    true.

 - Exercise 2.3.
  - query
   sentence(D1,N1,V,D2,N2).
  - instantiations
     a criminal eats a criminal
     a criminal eats a 'big kahuna burger'
     a criminal eats every criminal
     a criminal eats every 'big kahuna burger'
     a criminal likes a criminal
     a criminal likes a 'big kahuna burger'
     a criminal likes every criminal
     a criminal likes every 'big kahuna burger'
     a 'big kahuna burger' eats a criminal
     a 'big kahuna burger' eats a 'big kahuna burger'
     a 'big kahuna burger' eats every criminal
     a 'big kahuna burger' eats every 'big kahuna burger'
     a 'big kahuna burger' likes a criminal
     a 'big kahuna burger' likes a 'big kahuna burger'
     a 'big kahuna burger' likes every criminal
     a 'big kahuna burger' likes every 'big kahuna burger'
     every criminal eats a criminal
     every criminal eats a 'big kahuna burger'
     every criminal eats every criminal
     every criminal eats every 'big kahuna burger'
     every criminal likes a criminal
     every criminal likes a 'big kahuna burger'
     every criminal likes every criminal
     every criminal likes every 'big kahuna burger'
     every 'big kahuna burger' eats a criminal
     every 'big kahuna burger' eats a 'big kahuna burger'
     every 'big kahuna burger' eats every criminal
     every 'big kahuna burger' eats every 'big kahuna burger'
     every 'big kahuna burger' likes a criminal
     every 'big kahuna burger' likes a 'big kahuna burger'
     every 'big kahuna burger' likes every criminal
     every 'big kahuna burger' likes every 'big kahuna burger'

 - Exercise 2.4.

word(astante, a,s,t,a,n,t,e).
word(astoria, a,s,t,o,r,i,a).
word(baratto, b,a,r,a,t,t,o).
word(cobalto, c,o,b,a,l,t,o).
word(pistola, p,i,s,t,o,l,a).
word(statale, s,t,a,t,a,l,e).

crossword(V1,V2,V3,H1,H2,H3) :-
        word(V1,V11,V12,V13,V14,V15,V16,V17),
        word(V2,V21,V22,V23,V24,V25,V26,V27),
        word(V3,V31,V32,V33,V34,V35,V36,V37),
        word(H1,H11,H12,H13,H14,H15,H16,H17),
        word(H2,H21,H22,H23,H24,H25,H26,H27),
        word(H3,H31,H32,H33,H34,H35,H36,H37),
        V12 = H12, V14 = H22, V16 = H32,
        V22 = H14, V24 = H24, V26 = H34,
        V32 = H16, V34 = H26, V36 = H36.

** 4 Practical Session
 - うーん。swi-prolog、notrace.でデバッグモードか
   ら戻れない。

こつこつ。