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.