\chapter{Prolog}


It may be useful to first have a look at the "Logic programming" section of 
\href{\gitLAAITwo}{\texttt{Languages and Algorithms for AI (module 2)}}.


\section{Syntax}

\begin{description}
    \item[Term] \marginnote{Term}
        Following the first-order logic definition, a term can be a:
        \begin{itemize}
            \item Constant (\texttt{lowerCase}).
            \item Variable (\texttt{UpperCase}).
            \item Function symbol (\texttt{f(t1, \dots, tn)} with \texttt{t1}, \dots, \texttt{tn} terms).
        \end{itemize}

    \item[Atomic formula] \marginnote{Atomic formula}
        An atomic formula has form:
        \[ \texttt{p(t1, \dots, tn)} \]
        where \texttt{p} is a predicate symbol and \texttt{t1}, \dots, \texttt{tn} are terms.

        Note: there are no syntactic distinctions between constants, functions and predicates.

    \item[Clause] \marginnote{Horn clause}
        A Prolog program is a set of horn clauses:
        \begin{descriptionlist}
            \item[Fact] \texttt{A.}
            \item[Rule] \texttt{A :- B1, \dots, Bn.} (\texttt{A} is the head and \texttt{B1, \dots, Bn} the body)
            \item[Goal] \texttt{:- B1, \dots, Bn.}
        \end{descriptionlist}
        where:
        \begin{itemize}
            \item \texttt{A}, \texttt{B1}, \dots, \texttt{Bn} are atomic formulas.
            \item \texttt{,} represents the conjunction ($\land$).
            \item \texttt{:-} represents the logical implication ($\Leftarrow$).
        \end{itemize}

        \begin{description}
            \item[Quantification] \marginnote{Quantification} \phantom{}
                \begin{description}
                    \item[Facts] 
                        Variables appearing in a fact are quantified universally.
                        \[ \texttt{A(X).} \equiv \forall \texttt{X}: \texttt{A(X)}  \]
                    \item[Rules] 
                        Variables appearing in the body only are quantified existentially.
                        Variables appearing in both the head and the body are quantified universally.
                        \[ \texttt{A(X) :- B(X, Y).} \equiv \forall \texttt{X}, \exists \texttt{Y} : \texttt{A(X)} \Leftarrow \texttt{B(X, Y)} \]

                    \item[Goals] 
                        Variables are quantified existentially.
                        \[ \texttt{:- B(Y).} \equiv \exists \texttt{Y} : \texttt{B(Y)}  \]
                \end{description}
        \end{description}
\end{description}


\section{Semantics}

\begin{description}
    \item[Execution of a program]
        A computation in Prolog attempts to prove the goal.
        Given a program $P$ and a goal \texttt{:- p(t1, \dots, tn)},
        the objective is to find a substitution $\sigma$ such that:
        \[ P \models [\, \texttt{p(t1, \dots, tn)} \,]\sigma \]

        In practice, it uses two stacks:
        \begin{descriptionlist}
            \item[Execution stack] Contains the predicates the interpreter is trying to prove.
            \item[Backtracking stack] Contains the choice points (clauses) the interpreter can try.
        \end{descriptionlist}

    \item[SLD resolution] \marginnote{SLD}
        Prolog uses a SLD resolution with the following choices:
        \begin{descriptionlist}
            \item[Left-most] Always proves the left-most literal first.
            \item[Depth-first] Applies the predicates following the order of definition.
        \end{descriptionlist}

        Note that the depth-first approach can be efficiently implemented (tail recursion)
        but the termination of a Prolog program on a provable goal is not guaranteed as it may loop depending on the ordering of the clauses.

    \item[Disjunction operator]
        The operator \texttt{;} can be seen as a disjunction and makes the Prolog interpreter
        explore the remaining SLD tree looking for alternative solutions.
\end{description}



\section{Arithmetic operators}
\marginnote{Arithmetic operators}

In Prolog:
\begin{itemize}
    \item Integers and floating points are built-in atoms.
    \item Math operators are built-in function symbols.
\end{itemize}
Therefore, mathematical expressions are terms.

\begin{description}
    \item[\texttt{is} predicate]
        The predicate \texttt{is} is used to evaluate and unify expressions:
        \[ \texttt{T is Expr} \]
        where \texttt{T} is a numerical atom or a variable and \texttt{Expr} is an expression without free variables.
        After evaluation, the result of \texttt{Expr} is unified with \texttt{T}.

        \begin{example} \phantom{}
            \begin{lstlisting}[language={}]
    ?- X is 2+3.
        yes X=5
            \end{lstlisting}
        \end{example}

        Note: a term representing an expression is evaluated only with the predicate \texttt{is} (otherwise it remains as is).

    \item[Relational operators]
        Relational operators (\texttt{>}, \texttt{<}, \texttt{>=}, \texttt{=<}, \texttt{==}, \texttt{=/=}) are built-in.
\end{description}



\section{Lists}
\marginnote{Lists}

A list is defined recursively as:
\begin{descriptionlist}
    \item[Empty list] \texttt{[]}
    \item[List constructor] \texttt{.(T, L)} where \texttt{T} is a term and \texttt{L} is a list.
\end{descriptionlist}
Note that a list always ends with an empty list.

As the formal definition is impractical, some syntactic sugar has been defined:
\begin{descriptionlist}
    \item[List definition] \texttt{[t1, \dots, tn]} can be used to define a list.  
    \item[Head and tail] \texttt{[H | T]} where \texttt{H} is the head (term) and \texttt{T} the tail (list) can be useful for recursive calls.
\end{descriptionlist}



\section{Cut}
\marginnote{Cut}

The cut operator (\texttt{!}) allows to control the exploration of the SLD tree.

A cut in a clause:
\[ \texttt{p :- q1, \dots, qi, !, qj, \dots, qn.} \]
makes the interpreter consider only the first choice points for \texttt{q1, \dots, qi}, dropping all the other possibilities.
Therefore, if \texttt{qj, \dots, qn} fails, there won't be backtracking and \texttt{p} fails.

\begin{example} \phantom{}\\[0.5em]
    \begin{minipage}{0.5\textwidth}
        \begin{lstlisting}
    p(X) :- q(X), r(X).
    q(1).
    q(2).
    r(2).

    ?- p(X).
        yes X=2
        \end{lstlisting}
    \end{minipage}
    \begin{minipage}{0.5\textwidth}
        \begin{lstlisting}
    p(X) :- q(X), !, r(X).
    q(1).
    q(2).
    r(2).

    ?- p(X).
        no
        \end{lstlisting}
    \end{minipage}

    In the second case, the cut drops the choice point \texttt{q(2)} and only considers \texttt{q(1)}.
\end{example}

\begin{description}
    \item[Mutual exclusion]
        A cut can be useful to achieve mutual exclusion.
        In other words, to represent a conditional branching:
        \[ \texttt{if a(X) then b else c} \]
        a cut can be used as follows:
        \begin{lstlisting}
    p(X) :- a(X), !, b.
    p(X) :- c.
        \end{lstlisting}

        If \texttt{a(X)} succeeds, other choice points for \texttt{p} will be dropped and only \texttt{b} will be evaluated.
        If \texttt{a(X)} fails, the second clause will be considered, therefore evaluating \texttt{c}.
\end{description}



\section{Negation}

\begin{description}
    \item[Closed-world assumption] \marginnote{Closed-world assumption}
        Only what is stated in a program $P$ is true, everything else is false:
        \[ \texttt{CWA}(P) = P \cup \{ \lnot A \mid A \text{ is a ground atomic formula and } P \cancel{\models} A \} \]

        \begin{description}
            \item[Non-monotonic inference rule]
                Adding new axioms to the program may change the set of valid theorems. 
        \end{description}

        As first-order logic is undecidable, the closed-world assumption cannot be directly applied in practice.

    \item[Negation as failure] \marginnote{Negation as failure}
        A negated atom $\lnot A$ is considered true iff $A$ fails in finite time:
        \[ \texttt{NF}(P) = P \cup \{ \lnot A \mid A \in \texttt{FF}(P) \} \]
        where $\texttt{FF}(P) = \{ B \mid P \cancel{\models} B \text{ in finite time} \}$ 
        is the set of atoms for which the proof fails in finite time.
        Note that not all atoms $B$ such that $P \cancel{\models} B$ are in $\texttt{FF}(P)$.

    \item[SLDNF] \marginnote{SLDNF}
        SLD resolution with NF to solve negative atoms.
        
        Given a goal of literals \texttt{:- L$_1$, \dots, L$_m$}, SLDNF does the following:
        \begin{enumerate}
            \item Select a positive or ground negative literal \texttt{L$_i$}:
                \begin{itemize}
                    \item If \texttt{L$_i$} is positive, apply the normal SLD resolution.
                    \item If \texttt{L$_i$} = $\lnot A$, prove that $A$ fails in finite time. 
                \end{itemize}
            \item Solve the remaining goal \texttt{:- L$_1$, \dots, L$_{i-1}$, L$_{i+1}$, \dots,  L$_m$}.
        \end{enumerate}

        \begin{theorem}
            If only positive or ground negative literal are selected during resolution, SLDNF is correct and complete.
        \end{theorem}

        \begin{description}
            \item[Prolog SLDNF] 
                Prolog uses an incorrect implementation of SLDNF where the selection rule always chooses the left-most literal.
                This potentially causes incorrect deductions.

                \begin{proof}
                    When proving \texttt{:- \char`\\+capital(X).}, the intended meaning is:
                    \[ \exists \texttt{X}: \lnot \texttt{capital(X)}  \]

                    In SLDNF, to prove \texttt{:- \char`\\+capital(X).}, the algorithm proves \texttt{:- capital(X).}, which results in:
                    \[ \exists \texttt{X}: \texttt{capital(X)}  \]
                    and then negates the result, which corresponds to:
                    \[ \lnot (\exists \texttt{X}: \texttt{capital(X)}) \iff \forall \texttt{X}: (\lnot \texttt{capital(X)}) \]

                \end{proof}

                \begin{example}[Correct SLDNF resolution]
                    Given the program:
                    \begin{lstlisting}[language={}, mathescape=true]
    capital(rome).
    region_capital(bologna).
    city(X) :- capital(X).
    city(X) :- region_capital(X).

    ?- city(X), \+capital(X).
                    \end{lstlisting}
                    its resolution succeeds with \texttt{X=bologna} as \texttt{\char`\\+capital(X)} is ground by the unification of \texttt{city(X)}.
                    \begin{center}
                        \includegraphics[width=0.75\textwidth]{img/_sldnf_correct_example.pdf}
                    \end{center}
                \end{example}

                \begin{example}[Incorrect SLDNF resolution] 
                    Given the program: \\
                    \begin{minipage}{0.45\textwidth}
                        \begin{lstlisting}[language={}, mathescape=true]
    capital(rome).
    region_capital(bologna).
    city(X) :- capital(X).
    city(X) :- region_capital(X).

    ?- \+capital(X), city(X).
                        \end{lstlisting}
                    \end{minipage}
                    \begin{minipage}{0.5\textwidth}
                        \includegraphics[width=0.7\linewidth]{img/_sldnf_incorrect_example.pdf}
                    \end{minipage}

                    its resolution fails as \texttt{\char`\\+capital(X)} is a free variable and 
                    the proof of \texttt{capital(X)} is ground with \texttt{X=rome} and succeeds, therefore failing \texttt{\char`\\+capital(X)}.
                    Note that \texttt{bologna} is not tried as it does not appear in the axioms of \texttt{capital}.
                \end{example}
        \end{description}
\end{description}



\section{Meta predicates}

\begin{description}
    \item[\texttt{call/1}] \marginnote{\texttt{call/1}}
        Given a term \texttt{T}, \texttt{call(T)} considers \texttt{T} as a predicate and evaluates it.
        At the time of evaluation, \texttt{T} must be a non-numeric term.

        \begin{example} \phantom{}
            \begin{lstlisting}
    p(X) :- call(X).
    q(a).

    ?- p(q(Y)).
        yes Y=a
            \end{lstlisting}
        \end{example}

    \item[\texttt{fail/0}] \marginnote{\texttt{fail/0}}
        The evaluation of \texttt{fail} always fails, forcing the interpreter to backtrack.

        \begin{example}[Implementation of negation as failure] \phantom{}
            \begin{lstlisting}[language={}]
    not(P) :- call(P), !, fail.
    not(P).
            \end{lstlisting}
        \end{example} 
        \vspace*{-1.5em}
        Note that the cut followed by \texttt{fail} (\texttt{!, fail}) is useful to force a global failure.

    \item[\texttt{bagof/3} and \texttt{setof/3}] \phantom{}
        \begin{description}
            \item[\texttt{bagof/3}]  \marginnote{\texttt{bagof/3}}
                The predicate \texttt{bagof(X, P, L)} unifies \texttt{L} with a list of the instances of \texttt{X} that satisfy \texttt{P}.
                Fails if none exists.
            \item[\texttt{sefof/3}]  \marginnote{\texttt{sefof/3}}
                The predicate \texttt{setof(X, P, S)} unifies \texttt{S} with a set of the instances of \texttt{X} that satisfy \texttt{P}.
                Fails if none exists.
                
                In practice, for computational reasons, a list (with repetitions) might be computed.
        \end{description}
        
        \begin{example} \phantom{}
            \begin{lstlisting}[language={}]
    p(1).
    p(2).
    p(1).

    ?- setof(X, p(X), S).
        yes S=[1, 2] X=X

    ?- bagof(X, p(X), S).
        yes S=[1, 2, 1] X=X
            \end{lstlisting}
        \end{example}

        \begin{description}
            \item[Quantification] 
                When solving a goal, the interpreter unifies free variables with a value.
                This may cause unwanted behaviors when using \texttt{bagof} or \texttt{setof}.
                The \texttt{X\textasciicircum} tells the interpreter to not (permanently) bind the variable \texttt{X}.

                \begin{example} \phantom{}\\
                    \begin{minipage}{0.5\textwidth}
                        \begin{lstlisting}[language={}]
father(giovanni, mario).
father(giovanni, giuseppe).
father(mario, paola).

?- setof(X, father(X, Y), S).
    yes X=X Y=giuseppe S=[giovanni];
        X=X Y=mario    S=[giovanni];
        X=X Y=paola    S=[mario]
                        \end{lstlisting}   
                    \end{minipage}
                    \begin{minipage}{0.5\textwidth}
                        \begin{lstlisting}[language={}]
father(giovanni, mario).
father(giovanni, giuseppe).
father(mario, paola).

?- setof(X, Y^father(X, Y), S).
    yes S=[giovanni, mario] X=X Y=Y
                        \end{lstlisting}   
                    \end{minipage}
                \end{example}
        \end{description}

    \item[\texttt{findall/3}] \marginnote{\texttt{findall/3}}
        The predicate \texttt{findall(X, P, S)} unifies \texttt{S} with a list of the instances of \texttt{X} that satisfy \texttt{P}.
        If none exists, \texttt{S} is unified with an empty list.
        Variables in \texttt{P} that do not appear in \texttt{X} are not bound (same as the \texttt{Y\textasciicircum} operator).

        \begin{example} \phantom{}
                \begin{lstlisting}[language={}]
    father(giovanni, mario).
    father(giovanni, giuseppe).
    father(mario, paola).

    ?- findall(X, father(X, Y), S).
        yes S=[giovanni, mario] X=X Y=Y
                \end{lstlisting}   
        \end{example}

    \item[\texttt{var/1}] \marginnote{\texttt{var/1}}
        The predicate \texttt{var(T)} is true if \texttt{T} is a variable.    

    \item[\texttt{nonvar/1}] \marginnote{\texttt{nonvar/1}}
        The predicate \texttt{nonvar(T)} is true if \texttt{T} is not a free variable.    

    \item[\texttt{number/1}] \marginnote{\texttt{number/1}}
        The predicate \texttt{number(T)} is true if \texttt{T} is a number.    

    \item[\texttt{ground/1}] \marginnote{\texttt{ground/1}}
        The predicate \texttt{ground(T)} is true if \texttt{T} does not have free variables.    

    \item[\texttt{=../2}] \marginnote{\texttt{=../2}}
        The operator \texttt{T =.. L} unifies \texttt{L} with a list where 
        its head is the head of \texttt{T} and the tail contains the remaining arguments of \texttt{T}
        (i.e. puts all the components of a predicate into a list).
        Only one between \texttt{T} and \texttt{L} can be a variable.

        \begin{example} \phantom{} \\
            \begin{minipage}{0.5\textwidth}
                \begin{lstlisting}[language={}]
    ?- foo(hello, X) =.. List.
        List = [foo, hello, X]
                \end{lstlisting}   
            \end{minipage}
            \begin{minipage}{0.5\textwidth}
                \begin{lstlisting}[language={}]
    ?- Term =.. [baz, foo(1)].
        Term = baz(foo(1))
                \end{lstlisting} 
            \end{minipage}
        \end{example}

    \item[\texttt{clause/2}] \marginnote{\texttt{clause/2}}
        The predicate \texttt{clause(Head, Body)} is true if it can unify \texttt{Head} and \texttt{Body} with an existing clause.
        \texttt{Head} must be initialized to a non-numeric term. \texttt{Body} can be a variable or a term.

        \begin{example} \phantom{}
            \begin{lstlisting}[language={}]
    p(1).
    q(X, a) :- p(X), r(a).
    q(2, Y) :- d(Y).

    ?- clause(p(1), B).
        yes B=true

    ?- clause(p(X), true).
        yes X=1
    
    ?- clause(q(X, Y), B).
        yes X=_1 Y=a B=p(_1), r(a);
            X=2 Y=_2 B=d(_2)
            \end{lstlisting}  
        \end{example}

    \item[\texttt{assert/1}] \marginnote{\texttt{assert/1}}
        The predicate \texttt{assert(T)} adds \texttt{T} in an unspecified position of the clauses database of Prolog.
        In other words, it allows to dynamically add clauses.
        \begin{descriptionlist}
            \item[\texttt{asserta/1}] \marginnote{\texttt{asserta/1}}
                As \texttt{assert(T)}, with insertion at the beginning of the database.
            \item[\texttt{assertz/1}] \marginnote{\texttt{assertz/1}}
                As \texttt{assert(T)}, with insertion at the end of the database.
        \end{descriptionlist}

        Note that \texttt{:- assert((p(X)))} quantifies \texttt{X} existentially as it is a query.
        If it is not ground and added to the database as is, 
        it becomes a clause and therefore quantified universally: $\forall \texttt{X}: \texttt{p(X)}$.

        \begin{example}[Lemma generation] \phantom{}
            \begin{lstlisting}[language={}]
    fib(0, 0) :- !.
    fib(1, 1) :- !.
    fib(N, F) :- N1 is N-1, fib(N1, F1),
                 N2 is N-2, fib(N2, F2),
                 F is F1+F2,
                 generate_lemma(fib(N, F)).

    generate_lemma(T) :- clause(T, true), !.
    generate_lemma(T) :- assert(T).
            \end{lstlisting} 

            The custom defined \texttt{generate\_lemma/1} allows to add to the clauses database all the intermediate steps to compute the Fibonacci sequence
            (similar concept to dynamic programming).
        \end{example}

    \item[\texttt{retract/1}] \marginnote{\texttt{retract/1}}
        The predicate \texttt{retract(T)} removes from the database the first clause that unifies with \texttt{T}.

    \item[\texttt{abolish/2}] \marginnote{\texttt{abolish/2}}
        The predicate \texttt{abolish(T, n)} removes from the database all the occurrences of \texttt{T} with arity \texttt{n}.
\end{description}



\section{Meta-interpreters}

\begin{description}
    \item[Meta-interpreter] \marginnote{Meta-interpreter}
        Interpreter for a language $L_1$ written in another language $L_2$.

    \item[Prolog vanilla meta-interpreter] \marginnote{Vanilla meta-interpreter}
        The Prolog vanilla meta-interpreter is defined as follows:
        \begin{lstlisting}[language={}]
    solve(true) :- !.
    solve( (A, B) ) :- !, solve(A), solve(B).
    solve(A) :- clause(A, B), solve(B).
        \end{lstlisting}

        In other words, the clauses state the following:
        \begin{enumerate}
            \item A tautology is a success.
            \item To prove a conjunction, we have to prove both atoms.
            \item To prove an atom \texttt{A}, 
                we look for a clause \texttt{A :- B} that has \texttt{A} as conclusion and prove its premise \texttt{B}.
        \end{enumerate}
\end{description}