Logica matematica

Note

La logica è un formalismo universale alternativo al linguaggio naturale. Ha come vantaggio di non essere ambigua, e ha la possibilità di dimostrare in modo automatico delle proprietà desiderate.

In questo corso useremo la logica per specificare dei linguaggi formali, usando la logica monadica del primo e secondo ordine, e per specificare il comportamento I/O di programmi.

Logica monadica del primo ordine

Note

Consideriamo la logica del primo ordine con predicati su una sola variabile (MFO), questa consente di descrivere parole su un alfabeto . Sia una lettera predicativa per ogni simbolo di , una formula è:

  • : il predicato applicato ad una variabile
  • : negazione logica della formula
  • : congiunzione (and booleano) di due formule
  • : quantificatore universale

Dove il dominio delle variabili è un sottoinsieme finito di da pensare come posizioni, e corrisponde alla relazione di minore tra le posizioni.

Dati e insieme delle variabili, un assegnamento è una funzione .

La MFO permette di descrivere la categoria di linguaggi star-free.

Tip

Definiamo alcune relazioni:

Definiamo inoltre:

  • Costante :
  • Funzione successore :
  • Costanti : rispettivamente

Da qui possiamo definire le seguenti abbreviazioni:

  • equivale a . Da qui possiamo anche definire che equivale a .
  • equivale a , mentre equivale a .

Si ha che è vera se e solo se l'-esimo elemento di una parola è .

Definiamo il linguaggio definito da una formula come: con formula chiusa.

Linguaggi star-free

I linguaggi esprimibili con MFO sono chiusi per unione, intersezione e complemento, tuttavia sono strettamente meno potenti degli FSA, poiché non sono chiusi rispetto alla di Kleene (da cui il nome star-free).

Logica monadica del secondo ordine

Note

La logica monadica del secondo ordine (MSO) permette di quantificare predicati del primo ordine, e quindi ammettiamo formule come con appartenente all'insieme dei predicati monadici. Per convenzione si usano le maiuscole per indicare variabili con domini l'insieme dei predicati monadici, e le minuscole per indicare variabili in .

L'assegnamento di variabili del secondo ordine (insieme ) è una funzione .

Definiamo le seguenti formule utili:

Teorema di Büchi-Elgot-Trakhtenbrot

Note

Data una MSO , si può sempre costruire un FSA che accetta esattamente . La classe dei linguaggi definibili tramite MSO coincide con REG.

Per convertire da FSA a MSO seguo il seguente approccio:

  • Per ogni del FSA definiamo una variabile , che rappresenta l'insieme di posizioni di una stringa accettata dove l'automa si trova in . L'automa non è in due stati contemporaneamente, quindi per ogni coppia e abbiamo
  • L'FSA parte da , cioè delle posizioni dei caratteri letti dall'FSA partendo da .
  • Ogni transizione diventa
  • L'accettazione tramite diventa

Logica come formalismo per definire le proprietà dei programmi

Note

La logica può essere usata come specifica per algoritmi, come algoritmo di ricerca e ordinamento. In generale sono presenti delle precondizioni (insieme di condizioni che devono essere vere prima dell'esecuzione di un programma ) affinché sia vero un insieme di fatti (postcondizioni) dopo l'esecuzione.