************
 論理型言語
************

==========================
 理想的な論理型言語の特徴
==========================

* 宣言的なプログラミングが可能。

  * プログラムは動作の手順ではなく、データ間の関係を記述する。
  * データ間の関係に方向性はないため、入力と出力を決めずに、片方を与えればもう片方を計算するようにできる。

* 非決定的なアルゴリズムが書ける（実際の処理系ではバックトラックにより決定的に実行することが多い）。

========
 Prolog
========

一階述語論理に基づく。プログラムの実行は、定理の証明に対応する。

プログラム
----------

プログラムは、ホーン節の集合である。

* ホーン節は、次のような形をした論理式。ただし :math:`P, Q_1, \cdots, Q_n` は原子論理式。

  .. math::

     P \leftarrow Q_1 \wedge Q_2 \wedge Q_3 \wedge \cdots \wedge Q_n

  * 直感的には、「 :math:`P` を証明するには、 :math:`Q_1 \wedge Q_2 \wedge Q_3 \wedge \cdots \wedge Q_n` を証明せよ」ということ。
  * n>0の場合を規則、n=0の場合を事実と呼ぶ。
  
.. admonition:: 「人間は死ぬ」と「ソクラテスは人間である」

   .. code-block:: prolog

      mortal(X) :- human(X).
      human(socrates).

   * 変数名は大文字、関数記号名（定数のようなもの）は小文字で始める。

質問
----

Prolog 処理系は、質問を入力すると、それがプログラムから証明できるかどうかを出力する。

* 質問は、ゴール節という次のような形をした論理式。ただし :math:`Q_1, \cdots, Q_n` は原子論理式。

  .. math::

     \neg Q_1 \vee \neg Q_2 \vee \neg Q_3 \vee \cdots \vee \neg Q_n

  プログラムと同じ形で書こうとすると次のようになる（矢印の左辺に何もないので、正しい論理式ではないが）。

  .. math::
     
     \leftarrow Q_1 \wedge Q_2 \wedge Q_3 \wedge \cdots \wedge Q_n

* 質問に変数が含まれていると、証明可能な具体例に対する変数の値が表示される。

.. admonition:: 「ソクラテスは死ぬか？」

   .. code-block:: prolog

      ?- mortal(socrates).

.. admonition:: 「死ぬのは誰か？」

   .. code-block:: prolog

      ?- mortal(X).

もう少し複雑な例
----------------

リストの結合を表わす ``append`` という述語を定義するプログラム。

* ``[]`` は空リスト
* ``[ A | B ]`` は最初の要素が ``A`` で残りが ``B`` のリスト。

.. code-block:: prolog
		
   append([], Y, Y).
   append([H | X], Y, [H | Z]) :- append(X, Y, Z).

``[a, b]`` と ``[c, d]`` を結合すると ``[a, b, c, d]`` か？

.. code-block:: prolog

   ?- append([a, b], [c, d], [a, b, c, d]).
       yes

``[a, b]`` と ``[c, d]`` を結合すると何になるか？

.. code-block:: prolog

   ?- append([a, b], [c, d], Z).
       Z = [a, b, c, d]

``[a, b]`` と何を結合すると ``[a, b, c, d]`` か？

.. code-block:: prolog

   ?- append([a, b], Y, [a, b, c, d]).
       Y = [c, d]

何と ``[c, d]`` を結合すると ``[a, b, c, d]`` か？

.. code-block:: prolog

   ?- append(X, [c, d], [a, b, c, d]).
       X = [a, b]

==============
 理論的な基礎
==============

導出(resolution)という自動定理証明アルゴリズムを使用する。

1. 質問 ``?- Q`` はゴール節の形で書くと :math:`\neg Q` となる。
2. :math:`\neg Q` とプログラム :math:`P` から矛盾の導出を試みる。
3. 必要に応じて :math:`\neg Q` の具体例 :math:`\neg Q'` を作る。
4. :math:`\neg Q'` が :math:`P` と矛盾するならば、背理法により :math:`Q'` が証明できる。
5. この時に :math:`\neg Q` から :math:`\neg Q'` を作るために使った変数への代入が出力される。

=================
 Prolog の問題点
=================

導出の順序
----------

宣言的なプログラムであるためには、導出に使われるプログラム節とリテラルは非決定的に選択しなければならない。しかし、多くの Prolog 処理系では、上から下、左から右へ順番に選択していく(処理系を単純にするのと、この規則を利用してプログラマに効率の良いプログラムを書かせるため)ので、プログラムを書く順序によっては無限ループに陥ってしまう。

.. admonition:: 順序によって無限ループになる例
   
   ``parent`` という関係が定義されているとき、それを推移的に適用して ``ancestor`` という関係を定義したい。ところが、次のように書くと無限ループになる。

   .. code-block:: prolog

      ancestor(X, X).
      ancestor(X, Y) :- ancestor(Z, Y), parent(X, Z).

   正しくは、こう。

   .. code-block:: prolog

      ancestor(X, X).
      ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).

否定
----

あるゴール節 :math:`Q` がプログラムの論理的帰結でないとき、 :math:`\neg Q` が成り立つと考えることを閉世界仮説(closed world assumption)と呼ぶ。これに基づいて、Prolog では、あるゴール節 :math:`Q` の証明の探索が失敗したとき、 :math:`\neg Q` が成り立つと考える。これを失敗を否定と見なす規則(negation as failure)と呼ぶ。

.. admonition:: 太郎は死なない

   太郎が人間であるという情報がプログラムに含まれていないと、閉世界仮説から太郎は死なないという結論が導かれる。

   .. code-block:: prolog

      mortal(X) :- human(X).
      human(socrates).

      ?- mortal(taro).
        no

      ?- not(mortal(taro)).
        yes