Programmazione Logica -- Lezione 1: Sintassi e Semantica Dichiarativa

Introduzione

La programmazione logica e' nata dall'ideale di avere un linguaggio di programmazione il piu' possibile dichiarativo, in cui cioe' il compito del programmatore sia unicamente quello di specificare il problema da risolvere. Parafrasando Kowalski, uno dei padri fondatori della programmazione logica, si puo' dire che in generale un qualsiasi algoritmo si compone di due parti: la parte logica, cioe' la struttura del problema, e la parte di controllo, cioe' la sequenza dei passi da risolvere:
Algoritmo = Logica + Controllo
Nei linguaggi di programmazione tradizionali (imperativi) le due parti sono entrambe compito del programmatore. L'ideale della programmazione logica e' quella di definire un linguaggio in cui la parte di controllo sia demandata all'interprete, e al programmatore non resti quindi che definire la struttura logica del problema.

Esistono vari linguaggi "reali" basati sulla programmazione logica. In questo corso vedremo il linguaggio attualmente piu' diffuso, che e' il Prolog (Programming in logic). Questo linguaggio fu ideato e implementato per la prima volta da Colmerauer e Roussel nel 1972.

Sintassi

La programmazione logica e' un sottoinsieme della logica del primo ordine (FOL: First Order Logic), e si compone delle cosiddette Clausole di Horn (dal nome del loro inventore). Come per ogni sistema logico, avremo quindi un Alfabeto, che nel nostro caso e' composto da:
Var
Un insieme di simboli di variabili, x, y, z,....
Costr
Un insieme di simboli di costruttori, ciascuno con una determinata arieta'. Chiameremo costanti (Const) i costruttori con arieta' 0, e li indicheremeo con a, b, c,... . Chiameremo funzioni (Fun) quelli con arieta' maggiore di 0, e li indicheremo con f, g, h,... . Notare che questa e' solo una terminologia di comodo: queste non sono funzioni nel senso generale del termine, ma solo simboli usati per costruire il dominio dei dati (cioe' costruttori, appunto).
Pred
Un insieme di simboli di predicato, ciascuno con una determinata arieta', che indicheremo con p, q, r,...
Spec
Due simboli speciali corrispondenti a connettivi della logica classica: <- , (implicazione da destra a sinistra) e and (congiunzione).
Definiamo adesso l'insieme dei termini Term, che indicheremo con t, u, ..., tramite la seguente grammatica:
Term ::= Var | Const | Fun(Term,..., Term)
I termini che non contengono variabili sono detti termini ground e costituiscono il cosiddetto Universo di Herbrand. Alcuni esempi di termini sono: x , a , f(a,x) , f(g(a), b) , f(g(y), y). Di questi, solo a e f(g(a), b) sono ground.

Definiamo adesso l'insieme dei atomi Atom, che indicheremo con A, H, B, ..., tramite la seguente grammatica:

Atom ::= Pred(Term,..., Term)
Gli atomi che non contengono variabili sono detti atomi ground e costituiscono la cosiddetta Base di Herbrand. Alcuni esempi di atomi sono: p(a,x) , q(f(g(a), b)) , p(g(y), y). Di questi, solo q(f(g(a), b)) e' ground.

Possiamo adesso finalmente definire l'insieme delle Clausole di Horn:

HClause ::= Atom <- Atom and ... and Atom | <- Atom and ... and Atom
Il primo tipo di clausola e' detto clausola definita. La parte a sinistra della freccia e' detta head (testa) e la parte a destra e' detta body (corpo). Quando il corpo e' vuoto, scriveremo semplimente solo la testa. (Il corpo vuoto sta per il valore logico True e H <- True corrisponde quindi a H ). Una clausola con corpo vuoto e' detta anche fatto.

Il secondo tipo di clausola e' detto clausola negativa o goal. La testa vuota sta per il valore logico False e False <- B corrisponde quindi alla negazione di B .

Un programma logico P e' un insieme di clausole definite.

Esempio
Il seguente programma logico definisce il predicato "somma di numeri naturali" (sum). I numeri sono rappresentati tramite i costruttori 0 e s (successore).
sum(0,y,y)
sum(s(x),y,s(z)) <- sum(x,y,z)

Note sintattiche

In Prolog al posto di and si usa il simbolo ",". Inoltre al posto di <- si usa il simbolo ":-" nelle clausole definite, e "?-" nei goals. I simboli di variabile , costruttori e predicati possono essere nomi qualsiasi, ma le variabili devono cominciare con una maiuscola. Infine, ogni clausola e' terminata da un punto ("."). In queste note, useremo entrambe le notazioni, a seconda di cosa risulta di volta in volta piu' comodo.

Semantica dichiarativa

Un programma logico si puo' vedere come una particolare teoria della FOL, che definisce il significato di certi predicati (quelli che compaiono nelle teste delle clausole definite). Computare, in programmazione logica, significa effettuare una deduzione logica, cioe' provare che una certa proprieta' (espressa dal body di un goal) e' conseguenza logica del programma.

Ci si puo' chiedere fino a che punto le clausole di Horn siano un sottoinsieme della FOL, cioe' "quante" teorie si riescano ad esprimere con clausole di Horn. A questo proposito, e' utile ricordare il seguente teorema della logica classica:

Teorema
Una qualsiasi teoria FOL T si puo' riscrivere in un insieme di clausole (generali) T' tale che T e T' sono equivalenti dal punto di vista della soddisfacibilita'.
Una clausola generale e' una clausola della forma
A1 or ... or Am <- B1 and ... and Bn
dove or rappresenta la disgiunzione logica. Una clausola Horn e' quindi un caso particolare di clausola, in cui m vale 0 o 1.

Essere equivalenti dal punto di vista della soddisfacibilita' significa che T e' soddisfacibile (ha almeno un modello) se e solo se T' e' soddisfacibile. Questa e' una relazione molto forte, infatti la proprieta' di essere conseguenza logica di una teoria si puo' caratterizzare in termini di (in)soddisfacibilita':

Proposizione
Una formula F e' conseguenza logica di una teroria T se e solo se T unita a not(F) e' insoddisfacibile.
Quindi, in generale, il problema di determinare se una formula e' conseguenza logica di una teoria si puo' esprimere in forma clausale. Le clausole di Horn sono pero' un sottoinsieme stretto delle clausole generali, e si puo' vedere facilmente che esistono teorie che non si possono esprimere con clausole di Horn. Ad esempio, la teoria
insetto(x) or uccello(x) or pipistrello(x) <- vola(x)
non si puo' formulare con clausole di Horn.

Il motivo per cui la programmazione logica si restringe alle clausole di Horn e' essenzialmente l'efficienza: vedremo infatti che per i programmi logici e' possibile definire un metodo di prova molto piu' efficiente di quanto sia possibile fare per la FOL in generale.

Anche dal punto di vista della teoria dei modelli, comunque, le clausole Horn godono di interessanti proprieta'. In particolare, per ogni programma logico esiste un modello, detto minimo modello di Herbrand, che rappresenta, in un certo senso, tutti gli altri modelli, e si puo' quindi considerare la semantica dichiarativa del programma. Vediamo piu' formalmente cosa significa. Nota: nel seguito, supporremo sempre che l'alfabeto di riferimento sia quello determinato da tutti e soli i simboli che compaiono nel programma. Quindi Universo e Base di Herbrand sono determinati dal programma.

Definizione
Una Interpretazione di Herbrand e' un qualsiasi sottoinsieme I della Base di Herbrand. La relazione di soddisfacibilita', per gli atomi ground, e' definita da:
I |= A sse A appartiene ad I
Le interpretazioni di Herbrand sono interpretazioni nel senso logico del termine, il loro insieme di supporto e' l'universo di Herbrand, e la funzione d'interpretazione e' semplicemente quella che mappa ogni simbolo in se stesso. Sono interpretazioni cosiddette "sintattiche".

I modelli di Herbrand di un programma logico P (o piu' in generale di una teoria P in forma clausale) sono semplicemente le interpretazioni di Herbrand che soddisfano tutte le clausole di P, viste come formule logiche. Per definire formalmente questo concetto, ricordiamo che una istanziazione sigma e' una funzione dalle variabili all'Universo di Herbrand, (cioe' una sostituzione di variabili con termini ground). Indicheremo l'applicazione di una istanziazione sigma ad un atomo A con A sigma.

Definizione
Dato un programma P, un Modello di Herbrand per P e' una qualsiasi interpretazione di Herbrand M tale che, per ogni clausola H <- B1,...,Bn in P, e per ogni istanziazione sigma, se M |= B1 sigma, ... , M |= Bn sigma, allora vale anche M |= H sigma.
Teorema
Dato un insieme di clausole Horn, se esso ammette un modello, allora ammette un modello minimo di Herbrand. In particolare, un programma logico (insieme di clausole definite) P, ammette sempre un modello di Herbrand minimo, che indicheremo con M(P)
Questo teorema e' molto importante perche' implica che nei programmi logici le conseguenze logiche sono caratterizzate dal modello minimo. Ossia: se vogliamo vedere se un atomo ground A e' conseguenza logica P, basta controllare se A appartiene o meno a P.
Esercizio
Dimostrare una forma debole della prima parte di questo teorema, ossia che se un insieme di clausole Horn ammette un modello di Herbrand, allora ammette un modello di Herbrand minimo.
Esercizio
Dimostrare che un programma logico ammette sempre un modello di Herbrand.
Esercizio
Esibire una teoria in forma clausale che abbia modelli di Herbrand ma non ne abbia uno minimo.

Costruzione del modello minimo di Herbrand

Si puo' vedere facilmente che c'e un'ovvia analogia fra la nozione di programma logico ed una nozione studiata approfonditamente in passato: quella di definizione induttiva. Un'insieme di clausole definite P, infatti, si puo' tradurre in una definizione induttiva D(P) facendo corrispondere, ad ogni clausola della forma
H <- B1,...,Bn
una metaregola della forma:
B1 , ... , Bn
-----------------
H
dove le metavariabili sono le variabili della clausola, e l'universo di istanziazione e' l'Universo di Herbrand.
Esempio
Il programma visto prima che definisce la somma di numeri naturali si puo' tradurre nella seguente definizione induttiva:
sum(x,y,z)
----------------- --------------------
sum(0,y,y) sum(s(x),y,s(z))
dove x, y e z sono le metavariabili.
E' facile vedere che i modelli di Herbrand di P sono tutti e soli gli insiemi (interpretazioni di Herbrand) chiusi rispetto a D(P). L'esistenza del modello minimo segue quindi dall'esistenza del minimo insieme chiuso rispetto a D(P):
Proposizione
Dato un programma P, un' interpretazione di Herbrand I e' modello di P se e solo se I e' chiuso rispetto a D(P). Il modello minimo M(P) coincide quindi con l'insieme definito da D(P).
Per costruire M(P) si possono quindi applicare le tecniche standard viste per i sistemi induttivi.
Esercizio
Costruire il modello minimo del programma che definisce la somma di numeri naturali.