*******************
 Logic Programming
*******************

================================================
 Feature of an ideal logic progarmming language
================================================

* Declarative programming

  * Programs describe rules to get the result instead of step-by-step instractions.
  * Rules can be written in any order.

* Non-deterministic behavior

  * You may explore several possibilities for a single input.

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

Prolog is a language based on the first-order predicate logic (cf. `First-Order Logic in Artificial Intelligence - GeeksforGeeks <https://www.geeksforgeeks.org/artificial-intelligence/first-order-logic-in-artificial-intelligence/>`_).  Execution of a program corresponds to the proof of a theorem.

Program
-------

A rule is of the form:

.. code-block:: prolog

   p :- q1, q2, ... , qn.

where each of p, q1, q2, ..., qn is of the form ``pred(arg1, arg2, ..., argn)``.

* It means "To show p, show q1, q2, ..., qn".

* In case of n=0, it is called a fact.

A program is a set of rules (and facts).

.. admonition:: "Human is mortal" and "Socrates is a human"

   .. code-block:: prolog

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

Query
-----

A query is of the form:

.. code-block:: prolog

   ?- q1, q2, ... , qn.

If all of q1, q2, ... , qn can be shown from the given program, the output is "Yes"; otherwise "No".

.. admonition:: Is Socrates mortal?

   .. code-block:: prolog

      ?- mortal(socrates).
      Yes

If the query contains variables, the output displays assignments to the variables that make the query true.

.. admonition:: Who is mortal?

   .. code-block:: prolog

      ?- mortal(X).
      X = socrates

More complicated example
------------------------

The predicate ``append`` appends two lists into one.

* ``[]`` is an empty list.
* ``[ A | B ]`` denotes a list whose first element is ``A`` and the remaining part is ``B``.

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

Does appending ``[a, b]`` and ``[c, d]`` result in ``[a, b, c, d]`` ?

.. code-block:: prolog

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

What is the result of appending ``[a, b]`` and ``[c, d]`` ?

.. code-block:: prolog

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

Appending ``[a, b]`` and what result in ``[a, b, c, d]`` ?

.. code-block:: prolog

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

Appending what and ``[c, d]`` result in ``[a, b, c, d]`` ?

.. code-block:: prolog

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

========================
 Theoretical foundation
========================

Logical formula
---------------

A rule corresponds to a logical formula called *Horn clause*:

.. math::

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

which is equivalent to:

.. math::

   P \vee \neg Q_1 \vee \neg Q_2 \vee \neg Q_3 \vee \dots \vee \neg Q_n

A query corresponds to a logical formula called *Goal clause*:

.. math::
     
   {\rm False} \leftarrow Q_1 \wedge Q_2 \wedge Q_3 \wedge \cdots \wedge Q_n

which is equivalent to:

.. math::

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

Proof
-----

In order to show Q is true, a proof by contradiction is used.

1. We give a query ``?- Q`` which is equivalent to :math:`\neg Q`.
2. An automated theorem proving algorithm called *resolution* is used to derive a contradiction from :math:`\neg Q` and the program :math:`P`.

   * :math:`\neg Q'` (an instance of :math:`\neg Q`) is produced when necessary.

3. If contradiction can be derived, we can say :math:`Q'` is true.

   * We also get the assignment to variables that is used to produce :math:`\neg Q'`.

====================
 Issues with Prolog
====================

Derivation order
----------------

To implement declarative programming, it is required to choose derivation steps in non-deterministic manner.  However, Prolog adopts deterministic way of choosing next steps (top to bottom, left to right) because of simplicity and efficiency.  So, a program may fall into an infinite loop depending on the order of rules.

.. admonition:: Order sensitive program
   
   When the predicate ``parent`` is defined, we want to apply it transitively to define a new predicate ``ancestor``.

   The following program falls into an infinite loop:

   .. code-block:: prolog

      ancestor(X, X).
      ancestor(X, Y) :- ancestor(Z, Y), parent(X, Z).
      parent(alice, bob).
      parent(bob, charlie).

      ?- ancestor(alice, charlie).

   It should be:

   .. code-block:: prolog

      ancestor(X, X).
      ancestor(X, Y) :- parent(X, Z), ancestor(Z, Y).
      parent(alice, bob).
      parent(bob, charlie).

      ?- ancestor(alice, charlie).

Negation
--------

The resolution algorithm only deal with Horn clauses, so there should be no negative literal in the body part of a rule.  We need some tricks to use ``not`` operator in a program.

The *closed-world assumtion* is the assumption that all the true statements are known to be true.  Therefore, what is not known to be true is false.

In Prolog, based on the closed-world assumption, if we cannot prove :math:`Q`, we think :math:`\neg Q` is true.  This method is called *negation as failure*.

.. admonition:: Alice is not mortal

   If the program does not contain information about Alice, the computer concludes Alice is not mortal based on the closed-world assumption.

   .. code-block:: prolog

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

      ?- mortal(alice).
      no

      ?- not(mortal(alice)).
      yes