Clausole di Horn e Prolog

Cosa sono le clausole di Horn? La definizione formale di una clausola di horn
è: una clausola di Horn è una disgiunzione di letterali con al più un letterale
positivo, che nella sintassi Lisp (sotto forma di liste innestate) si scrive così:

(or (not x1) (not x2) ... (not xn) y)

Cerchiamo di chiarire le parole grosse usate in questa definizione che possono
confondere. La disgiunzione è semplicemente un OR logico (AND è detto invece
congiunzione). Un letterale è una formula atomica come x1, x2, ..., xn, y
oppure la sua negazione come (not x1) o (not y). Il letterale positivo è y,
positivo significa semplicemente che il letterale non è negato.

Notiamo che l'implicazione X -> Y, avente la seguente tabella di verità:

X Y | X -> Y
----+-------
F F |   V
F V |   V
V F |   F
V V |   V

è equivalente alla seguente disgiunzione, che è una semplice clausola di Horn,
come dimostrato dalla sua tabella della verità:

X Y | (not X) | (or (not X) Y)
----+---------+---------------
F F |    V    |       V
F V |    V    |       V
V F |    F    |       F
V V |    F    |       V

La cosa si vede subito se si pensa che l'implicazione è falsa solo quando
l'operando di sinistra (X, o proposizione "antecendente") è vero e il risultato
(operando di destra o proposizione "conseguente") è falsa, ed è appunto questo
l'unico caso in cui (or (not X) Y) è falso.

Se ora applichiamo il teorema di De Morgan per calcolare la negata di una
disgiunzione di termini tutti negativi:

(or (not x1) (not x2) ... (not xn))

viene fuori (or diventa and e i not spariscono):

(and x1 x2 ... xn)

Combinando queste due osservazioni possiamo ora riprendere una clausola di Horn:

(or (not x1) (not x2) ... (not xn) y)

e vederla come un'implicazione equivalente. Infatti è equivalente a :

(or (or (not x1) (not x2) ... (not xn)) y)

che è della forma

(or (not z) y)

dove

z = (not (or (not x1) (not x2) ... (not xn)))

Ma abbiamo visto che

(or (not z) y)

è equivalente a:

z -> y

Quindi anche la clausola di horn è equivalente a:

(not (or (not x1) (not x2) ... (not xn))) -> y

che applicando ancora il teorema di De Morgan si può semplificare in:

(and x1 x2 ... xn) -> y

quest'ultima allora è un modo logicamente del tutto equivalente di definire o
scrivere una clausola di Horn.

Cosa hanno a che fare queste clausole di Horn con la programmazione in pratica?
Considerate il linguaggio Prolog, un linguaggio di programmazione logica e
quindi di stile dichiarativo. Una regola in Prolog ha il formato:

testa :- coda.

Quel :- sta per <-. Nella notazione della logica si dovrebbe scrivere:

testa <- coda

oppure

coda -> testa

Data allora una clausola di Horn nella sintassi con l'implicazione:

(and x1 x2 ... xn) -> y

questa si scrive in Prolog in questo modo:

y <- (and x1 x2 ... xn)

y :- (and x1 x2 ... xn)

y :- x1, x2, ..., xn.

Dal momento che tutte le clausole devono essere terminate con un . e la virgola
rappresenta come sapete l'operazione logica di AND. Anche una clausola di tipo
fatto, semplicemente:

y.

è equivalente ad una banale clausola di Horn:

true -> y

o nella sintassi con disgiunzione:

(or y)

Quindi un programma Prolog non è altro che una lista di clausole di Horn, per
quanto grande possa essere questa lista, non c'è nient'altro. In altri termini,
programmando in Prolog, si programma con le clausole di Horn!

Nota: siccome una clausola di Horn deve contenere al più un letterale positivo,
potrebbe non averne alcuno, quindi se non c'è y, anche questa è una clausola di
Horn in accordo con la definizione:

(or (not x1) (not x2) ... (not xn))

come si scrive questa come implicazione? Dal momento che è equivalente a questa
(avendo posto Y=false):

(or (not x1) (not x2) ... (not xn) false)

l'implicazione equivalente sarà:

(and x1 x2 ... xn) -> false

che equivale nella notazione del Prolog a una regola "senza testa" o con testa false:

false :- x1, x2, ..., xn.

:- x1, x2, ..., xn.

Questa rappresenta un goal, in particolare il goal che risolve il problema.

Family rules

A specialty of Prolog are genealogical databases aka family trees.

For the sake of simplicity we assume that do not need to represent couples without children. Therefore we can choose these three fundamental relations to build our tree: 'male', 'female' and 'parent'.

Here's an example from the Bible:

                      amram
                     jochebed
             ___________|________
            /           |        \
         moses        aaron    miriam
        zipporah     elisheba
        /      \        |
     gershom eliezer  nadab

male(amram).
male(aaron).
male(moses).
male(gershom).
male(eliezer).
male(nadab).

female(jochebed).
female(miriam).
female(zipporah).
female(elisheba).

parent(amram,moses).
parent(jochebed,moses).
parent(amram,aaron).
parent(jochebed,aaron).
parent(amram,miriam).
parent(jochebed,miriam).

parent(moses,gershom).
parent(zipporah,gershom).
parent(moses,eliezer).
parent(zipporah,eliezer).

parent(aaron,nadab).
parent(elisheba,nadab).

All the other family relationships can be defined in terms of these three fundamental predicates. The following definitions are all optmized for the first argument being a constant and the second being a variable:

% profile -,+

father(X,Y) :- parent(X,Y), male(X).
mother(X,Y) :- parent(X,Y), female(X).

% The inverse of parent
child(X,Y) :- parent(Y,X).

son(X,Y) :- parent(Y,X), male(X). 
% just the same
%son(X,Y) :- child(X,Y), male(X).
daughter(X,Y) :- parent(Y,X), female(X).

% Siblings have the same parents.
sibling(X,Y) :- father(Z,Y), mother(W,Y), parent(Z,X), parent(W,X), X \== Y.
% unoptmized version:
%sibling(X,Y) :- father(Z,Y), mother(W,Y), father(Z,X), mother(W,X), X \== Y.

% A brother is a male sibling.
brother(X,Y) :- sibling(X,Y), male(X).
% A sister is a female sibling.
sister(X,Y) :- sibling(X,Y), female(X).

% Here we assume that one only marries once.
husband(X,Y) :- mother(Y,Z), father(X,Z), !.
wife(X,Y) :- father(Y,Z), mother(X,Z), !.

grandparent(X,Y) :- parent(Z,Y), parent(X,Z).
grandmother(X,Y) :- parent(Z,Y), mother(X,Z).
% just the same
%grandmother(X,Y) :- grandparent(X,Y), female(X).
grandfather(X,Y) :- parent(Z,Y), father(X,Z).

cousin(X,Y) :- parent(Z,Y), sibling(W,Z), parent(W,X).

% An aunt is a parent's sister.
aunt(X,Y) :- parent(Z,Y), sister(X,Z).
% An uncle is a parent's brother.
uncle(X,Y) :- parent(Z,Y), brother(X,Z).

Note that if we define siblings as:

sibling(X,Y) :- parent(Z,X), parent(Z,Y), X \== Y.

we have a problem. We get each sibling twice:

?- sibling(X,moses).
X = aaron ;
X = aaron ;
X = miriam ;
X = miriam ;
false.

Can you see why? If not, a little bit of debug output will help you:

sibling(X,Y) :- parent(Z,X), parent(Z,Y), X \== Y, write(Z).

Example queries:

?- father(X,miriam).
X = amram ;
false.

?- sibling(X,moses).
X = aaron ;
X = miriam ;
false.

?- wife(X,moses).
X = zipporah.

?- grandparent(X,gershom).
X = amram ;
X = jochebed ;
false.

?- grandmother(X,eliezer).
X = jochebed ;
false.

?- cousin(X,nadab).
X = gershom ;
X = eliezer ;
false.

?- aunt(X,eliezer).
X = miriam ;
false.

Exercises

Make that of your own family! If you want to use full names the syntax is 'Name Surname'. Add rules for nephew (sibling's son), niece (sibling's daughter), descendant (a child or a descendant's child) and ancestor (the inverse of descendant). The definition of aunt given before is incomplete: "an aunt is a person who is the sister or sister-in-law of a parent". Similarly, mark uncle.