Definizioni
Predicati
Con il nostro linguaggio per il momento non abbiamo la possibilità
di parlare di oggetti come i numeri naturali. Inoltre vorremmo essere in grado
di parlare di proprietà o di relazioni tra oggetti, ovvero
vorremmo avere i cosidetti predicati.
Per esempio, una proprietà di un numero intero è il fatto
di essere primo: 5 è primo. Un esempio di relazione tra
numeri è il fatto che un numero è maggiore di un altro:
5 è maggiore di 3.
Aggiungiamo la possibilità di avere predicati dentro il nostro
linguaggio formale usando una notazione applicativa:
- (Prime 5) rappresenterà il fatto che 5 è primo;
- (Greater 5 3) rappresenterà il fatto che 5 è maggiore di 3.
Quando un predicato è applicato su tutti i suoi argomenti diventa
una proposizione.
Funzioni
Nello stesso modo vorremmo parlare di funzioni. Le funzioni sono diverse
dai predicati nel senso che prendono oggetti e restituiscono oggetti.
Un esempio di funzione è la somma di numeri.
Come per i predicati, usiamo la notazione applicativa per rappresentare
le nostre funzioni:
- (Plus 5 3) rappresenterà la somma di 5 e 3.
È importante notare che non c'è differenza fra
(Plus 5 3) e 8, in quanto sono solo due modi diversi di
parlare dello stesso oggetto. La caratteristica di 8 è
quella di essere la forma
più semplice, ovvero la cosidetta forma normale.
Variabili
Negli esempi abbiamo utilizzato senza dirlo la nozione di costante:
5 e 8 sono delle costanti e rappresentano due
oggetti di tipo numero intero. Oltre alle costanti, abbiamo
le variabili. Per le variabili usiamo tipicamente i nomi:
x, y, z....
Per esempio, (Greater (Plus x y) x) rappresenta il fatto
che la somma dell'oggetto x e dell'oggetto y è
maggiore dell'oggetto x.
Con le variabili è associata la nozione di sostituzione
che permette di rimpiazzare una variabile con una espressione:
F[x <- E] significa che dentro la formula F,
x è stata rimpiazzata con E.
Se F è la formula precedente, si ha che
F[x <- (Plus 3 z)] vale (Greater (Plus (Plus 3 z) y) (Plus 3 z)).
Quantificatori
Quantificatore universale
Il quantificatore universale permette di costruire formule che sono vere
per tutti gli oggetti.
Per esempio ∀x. (P x x) rappresenta il fatto che per ogni
x, x è in relazione con se stesso tramite P,
ovvero P è una relazione riflessiva.
Quantificatore esistenziale
Il quantificatore esistenziale permette di costruire formule che sono vere
per almeno un oggetto.
Per esempio, ∀n. ∃p. (Greater p n) ∧
(Prime p) esprime il fatto che per ogni numero n esiste un
numero p maggiore di n tale che p sia un numero
primo, ovvero l'insieme dei numeri primi è infinito.
Variabile libera e variabile legata
Una variabile è legata se si trova sotto un quantificatore
con lo stesso nome. Se non è il caso, la variabile è libera.
Per esempio, nella formula ∃x. (P x y), x è legata
ed y è libera.
Una variabile è legata con il quantificatore più prossimo.
Per esempio, nella formula ∃x. ∀x. (P x) la variabile x dentro
(P x) è legata al quantificatore universale.
Il nome delle variabili legate non è significativo:
∀x. ∃y. (P x y) è equivalente a ∀z. ∃t. (P z t).
Ovviamente la sostituzione rispetta i quantificatori.
Per esempio, ((P x) ∧ (∀x. (Q x x)))[x <- a] vale
((P a) ∧ (∀x. (Q x x))).
Implementazione
Per l'implementazione delle variabili legate, si utilizzano gli indici
di deBruijn. Una variabile legata è rappresentata da un numero
intero che indica quanti quantificatori bisogna attraversare nella
struttura ad albero della formula per trovare quello che lega la variabile.
Per esempio, la formula ∀n. ∃p. (Greater p n) ∧
(Prime p) viene rappresentata come (FORALL (EX (AND (Greater (VAR 0) (VAR 1)) (Prime (VAR 0))))).
Esercizi
F1. Scrivere la formula che rappresenta il
fatto che un predicato P è simmetrico.
F2. Scrivere la formula che rappresenta il
fatto che un predicato P è transitivo.
F3. Scrivere la formula che rappresenta il
fatto che una funzione f con un parametro è iniettiva. Si può
supporre l'esistenza di un predicato d'uguaglianza scritto x=y.
F4. Scrivere la formula che rappresenta il
fatto che una funzione f con un parametro è suriettiva.
Laurent Théry
Last modified: Thu May 23 23:15:07 MEST 2002