Esempio: A*

• Contesto: Parole su un alfabeto A

• Consideriamo un linguaggio L con due sorte: A e A*

• Def Induttiva di parola di A*

• Le clausole base e passo si applicano per generare per strati le parole

• La clausola di chiusura lavora al contrario e si usa per verificare l'appartenenza di una parola ad A*

$$ Assiomi\ di\ diversità \\ Div:\forall x:A\forall p :A^(xp\ne\epsilon) \\ Inj:\forall x_1:A \forall x_2:A\forall p_1:A^\forall p_2:A^*(x_1p_1=x_2p_2\rightarrow(x_1=x_2\wedge p_1=p_2)) $$

• Gli assiomi di chiusura e di diversità consentono inoltre di provare ¬A per ogni proposizione atomica (unico predicato nel linguaggio L è il =) A falsa. (es: Atomica (aba≠ab) si può provare assumendo aba = ab e arrivando ad un assurdo)

Principio di induzione su A*

Il principio di induzione è, come abbiamo detto prima, associato alla definizione induttiva.

<aside> 💡 L'assioma di chiusura è troppo debole per catturare la clausola di chiusura nel caso di enunciati più complessi delle atomiche.

</aside>

• Per catturare appieno la clausola di chiusura occorre introdurre il principio di induzione, che è più forte del solo assioma di chiusura.
• Si ragiona su proprietà quindi, per ogni fbf. H(x) (con libere(H) = {x}), se valgono

$$ Base: H(\epsilon) \\ Passo: \forall x:A\forall q: A^* (H(q)\rightarrow H(xq)) $$

• Allora vale ∀p: A* H(p)