Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Aniello Murano » 5.Definizione Induttiva di Domini


Riassunto delle lezioni precedenti

Prima Lezione: Introduzione e motivazioni del corso; Sintassi e semantica di ARITHM
Seconda lezione: Sintassi e semantica operazionale del linguaggio imperativo IMP
Terza lezione: Tecniche di prova per induzione:

  • Induzione matematica (ipotesi induttiva su numeri precedenti).
  • Induzione strutturale (ipotesi induttiva su sottotermini).
  • Induzione ben fondata (include i precedenti).
  • Induzione su derivazione (ipotesi induttiva su sottoderivazioni).

Introduzione

  • In questa lezione analizzeremo la teoria degli insiemi definiti induttivamente.
  • Un esempio di tale insieme è il linguaggio IMP definito induttivamente dalle regole sintattiche e semantiche introdotte nelle precedenti lezioni.
  • Questa teoria permette di provare proprietà degli insiemi in modo efficiente, utilizzando le regole che definiscono l’insieme (induzione sulle regole).
  • Per esempio, è possibile dimostrare che un insieme definito induttivamente tramite regole è il minimo insieme chiuso rispetto alle regole date.
  • Dunque, l’induzione sulle regole è largamente utilizzata nella costruzione dei linguaggi (come vedremo per IMP) e se applicata alle regole semantiche del linguaggio permette di ragionare sulla sua semantica operazionale.

Definizione induttiva di insiemi

  • Nelle lezioni precedenti abbiamo già visto insiemi definiti induttivamente(Aexp, !Com, ecc.). Queste definizioni includono regole sintattiche (grammatiche) per la definizione sintattica e regole semantiche per la definizione degli alberi di derivazione.
  • Una definizione induttiva di un insieme è una collezione di regole che include assiomi e regole di inferenza. Un assioma x indica che x è un elemento dell’insieme per default. Una regola di inferenza {x1,…,xn/}/x mostra che x è un elemento dell’insieme se x1,…, xn lo sono.
  • Per esempio, l’insieme dei numeri naturali N è un insieme definito induttivamente, la cui definizione consiste nelle seguenti due regole (vedi figura).

Principio di induzione sulle regole descrizione informale

  • Il principio di induzione sulle regole si basa sulla seguente idea:
    • “se una proprietà è preservata nel passaggio dalle premesse alle conclusioni di tutte le regole utilizzate in una derivazione allora la proprietà vale anche per la conclusione della derivazione”
  • Se questo è vero per tutte le regole, allora la proprietà è vera per tutti gli elementi dell’insieme definito dalle regole.

Principio di induzione sulle regole

  • Sia R un insieme di regole (insieme di assiomi e regole di inferenza) e I l’insieme delle istanze delle regole di R.
  • Con IR indichiamo l’insieme di tutti gli elementi x ottenuti da I per cui esiste una derivazione consistente con R.
  • Formalmente 
    • IR = {x | ╟  R x}
  • Per esempio, si consideri la seguente regola e una sua istanza (vedi figura 1).
  • <2 x 3, σ> → 12 non è un elemento di IR perché l’istanza è corretta, ma non è derivabile con le regole di R.
Figura 1

Figura 1

Figura 2

Figura 2


Definizione di insieme (R-)chiuso

  • Un insieme Q è R-chiuso rispetto alle istanze delle regole R sse ogni volta che le premesse di una istanza di una regola appartengono a Q allora anche le conclusioni appartengono a Q.
  • Formalmente: Q è R-chiuso rispetto alle istanze delle regole R sse per ogni istanza di regola (X/y), si ha quanto riportato in figura 1.
Figura 1

Figura 1

Figura 2

Figura 2


Minimo insieme chiuso


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion