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.