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 $I$. Sia $a\in I$ una lettera predicativa per ogni simbolo di $I$, una formula $\phi$ è:

• $a(x)$: il predicato $a$ applicato ad una variabile
• $x<y$
• $\neg \phi$: negazione logica della formula
• $\phi \wedge \phi$: congiunzione (and booleano) di due formule
• $\forall x(\phi )$: quantificatore universale

Dove il dominio delle variabili è un sottoinsieme finito di $\mathbb{N}$ da pensare come posizioni, e $<$ corrisponde alla relazione di minore tra le posizioni.

Dati $w\in I^{+}$ e $V_1$ insieme delle variabili, un assegnamento è una funzione $v_1:V_1\to \{0,1,\cdots ,\mid w|-1\}$.

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

Tip

Definiamo alcune relazioni:

$$\begin{array}{rl}{\phi }_1\vee {\phi }_2& \equiv \neg (\neg {\phi }_1\wedge \neg {\phi }_2)\\ {\phi }_1\Rightarrow {\phi }_2& \equiv \neg {\phi }_1\vee {\phi }_2\\ \exists x(\phi )& \equiv \neg \forall x(\neg \phi )\\ x=y& \equiv \neg (x<y)\wedge \neg (x>y)\\ x\le y& \equiv \neg (y<x)\end{array}$$

Definiamo inoltre:

• Costante $0$: $x=0\equiv \forall y(\neg (y<x))$
• Funzione successore $S(x)$: $s(x)=y\equiv (x<y)\wedge \neg \exists z(x<z\wedge z<y)$
• Costanti $1,2,\cdots$: rispettivamente $S(0),S(S(O)),\cdots$

Da qui possiamo definire le seguenti abbreviazioni:

• $y=x+kk\in \mathbb{N},k>1$ equivale a $y=\underset{k\text{ volte}}{\underbrace{S}}(x)$. Da qui possiamo anche definire $y=x-kk\in \mathbb{N},k>1$ che equivale a $x=\underset{k\text{ volte}}{\underbrace{S}}(x)$.
• $\text{last}(x)$ equivale a $\neg \exists y(y<x)$, mentre $\text{first}(x)$ equivale a $\neg \exists y(x<y)$.

Si ha che $a(x)$ è vera se e solo se l’$x$-esimo elemento di una parola $w\in I^{\ast }$ è $a$.

Definiamo il linguaggio definito da una formula come:

$$L(\phi )=\{w\in I^{+}\mid \exists v:w,v\models \phi \}$$

con $\phi$ 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 $\ast$ 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 $\exists X(\phi )$ con $X$ 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 $\mathbb{N}$.

L’assegnamento di variabili del secondo ordine (insieme $V_2$) è una funzione $v_2:V_2\to \wp (\{0,1,\cdots ,\mid w|-1\})$.

Definiamo le seguenti formule utili:

$$\begin{array}{rl}\text{First}(x,P)& :=P(x)\wedge \forall y(y<x\Rightarrow \neg P(y))\\ \text{Last}(x,P)& :=P(x)\wedge \forall y(x<y\Rightarrow \neg P(y))\\ \text{Next(x,y,P)}& :=P(x)\wedge P(y)\wedge (x<y)\wedge \forall z((x<z\wedge z<y)\Rightarrow \neg P(z))\\ \text{Odd}(Q,P)& :=\forall x(Q(x)\iff (\text{First}(x,P)\vee \exists y\exists z(\text{Next}(z,x,P)\wedge \text{Next}(y,z,P)\wedge Q(y)))\\ \text{OddCard}(P)& :=\exists Q(\text{Odd}(Q,P)\wedge \forall x(\text{Last}(x,P)\Rightarrow Q(x))\wedge \exists P(x))\end{array}$$

Teorema di Büchi-Elgot-Trakhtenbrot

Note

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

Per convertire da FSA a MSO seguo il seguente approccio:

• Per ogni $q\in Q$ del FSA definiamo una variabile $X_q$, che rappresenta l’insieme di posizioni di una stringa accettata dove l’automa si trova in $q$. L’automa non è in due stati contemporaneamente, quindi per ogni coppia $X_i$ e $X_j$ abbiamo $\neg \exists y(y\in X_1\wedge y\in X_j)$
• L’FSA parte da $q_0$, cioè $\forall x(x=0\Rightarrow x\in X_{q_0})$ delle posizioni dei caratteri letti dall’FSA partendo da $q$.
• Ogni transizione $\delta (q_i,a)=q_j$ diventa $\forall x,y(y=x+1\Rightarrow (x\in X_i\wedge a(x)\wedge y\in X_j))$
• L’accettazione tramite $\delta (q_i,a)\in F$ diventa $\forall x(\text{last}(x)\Rightarrow {\bigvee }_{\delta (q_i,a)\in F}(x\in X_i\wedge a(x)))$

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 $P$) affinché sia vero un insieme di fatti (postcondizioni) dopo l’esecuzione.