next up previous Sommario
Next: 8.1 Una sessione al Up: tesi Previous: 7.8 Stato dell'implementazione   Sommario

8. Il progetto

Qui di seguito sono riportati alcuni esempi di utilizzo dei moduli che realizzano gli operatori di base e il metodo di negazione che integra NI e NC di Chan.

Il progetto è stato realizzato utilizzando una workstation SUN Sparcstation II con il sistema operativo UNIX X-Window.

Il progetto realizzato in questa tesi è costituito da una serie di moduli organizzati secondo una struttura gerarchica evidenziata nella figura 8.1.

Su alcuni moduli di base, che realizzano, per esempio, gli operatori di unione e di intersezione, la negazione intensionale e alcuni predicati che trattano la negazione di risposte secondo la SLDCNF, sono costruiti, sfruttando il sistema modulare del Gödel, altri moduli che definiscono gli altri operatori e in particolare il metodo di negazione presentato nei capitoli precedenti.

Figure 8.1: moduli del progetto
\begin{figure}\par {\tt\setlength{\unitlength}{0.92pt}\begin{picture}(350,255)
\...
...
\put(140,148){\framebox (80,32){Nega}}
\end{picture}}
\par\par\par\end{figure}

Ogni modulo ha una parte locale, con il codice che realizza ogni singolo predicato, e una parte export che permette di indicare quali tra questi predicati e quali costanti, funzioni ecc. definiti nel modulo vanno ``esportati", cioè messi a disposizione di altri moduli o, solo nel caso di Shell che è l'unico modulo a cui deve fare riferimento l'utente, utilizzati dall'utente stesso.

Per una particolarità presente nella versione di Gödel utilizzata, ma eliminata nella successiva, è stato necessario indicare nella parte export di ogni modulo tutti i moduli da cui il modulo in questione eredita, e non solo quelli da cui eredita direttamente.



Le teorie logiche oggetto di questa tesi sono state rappresentate, nell'ambito della realizzazione del progetto, per mezzo dei moduli Gödel. Ogni teoria è un modulo, con le sue dichiarazioni di tipi, funzioni, costanti e predicati, e con elencate le clausole della teoria. Tali moduli vengono poi compilati con il predicato GetTheory ottenendo così termini di tipo OTheory: in questo modo sono stati disponibili tutti i predicati del Gödel che operano sulla rappresentazione ground; d'altra parte si è riscontrata una non perfetta corrispondenza tra il nostro concetto di teoria e quello di termine di tipo OTheory. Ciò è dovuto al modo in cui è organizzata la rappresentazione ground: in pratica, ogni oggetto è rappresentato da una coppia (nome_della_teoria, indicatore_oggetto). Quando, quindi, si ha a che fare con più teorie, come nel caso dell'Unione o dell'Intersezione, per rappresentare, per esempio, una clausola di una teoria A in un'altra teoria B, è necessario ricavarsi prima la rappresentazione della clausola come stringa per poi ottenere quella come oggetto ground nella teoria B. Questo si traduce inevitabilmente in un appesantimento della computazione, considerando anche il necessario alto numero di tali operazioni.

È d'altra parte comprensibile il motivo che ha spinto gli sviluppatori del Gödel ad adottare tale soluzione: in questo modo si possono utilizzare senza ambiguità nomi uguali per indicare oggetti diversi in teorie differenti, evitando problemi quando si vorrà far ereditare una teoria da un'altra. Quello che si vuole invece intendere facendo, per esempio, l'intersezione di due teorie, è che predicati con lo stesso nome nelle due teorie indicano esattamente lo stesso predicato. È auspicabile, per ottenere livelli di efficienza maggiori in progetti su argomenti simili a quelli qui affrontati, mettere a punto una implementazione della rappresentazione ground che permetta di manipolare più teorie evitando però i problemi prima evidenziati.



Un'altra conseguenza del modo in cui è implementato Gödel è il fatto che è impossibile, o quantomeno non proponibile, realizzare la definizione metainterpretativa degli operatori Unione ed Intersezione. Non si potrebbe, tanto per incominciare,considerando $T1 \cup T2$, rappresentare un goal del tipo

\begin{displaymath}\leftarrow p(x) \wedge q(x) \end{displaymath}

dove $p$ (risp. $q$) è un simbolo di predicato dichiarato nella prima (risp. seconda) teoria. La soluzione potrebbe essere quella di ottenere una rappresentazione del goal in una teoria che ha le dichiarazioni di T1 e T2, ma ciò non si accorda sicuramente con l'obbiettivo di avere una definizione metainterpretativa. È anche non proponibile il pensare di rappresentare il primo letterale del goal in T1 e il secondo in T2 perchè il problema si ripresenterebbe quando si dovrà applicare la sostituzione di risposta calcolata del primo letterale al nuovo sottogoal ottenuto.



Nella implementazione del modulo Theory disponibile non è possibile che un modulo oggetto (cioè che verrà compilato con GetTheory) importi da un altro modulo. Ciò ha portato dei problemi non sostanziali ma che per esempio hanno impedito di utilizzare negli esempi la rappresentazione dei naturali come cifre: la usuale rappresentazione per mezzo della costante Zero e della funzione Succ comporta un appesantimento della notazione per indicare numeri solo poco superiori ad alcune unità.



Subsections
next up previous Sommario
Next: 8.1 Una sessione al Up: tesi Previous: 7.8 Stato dell'implementazione   Sommario
Roberto Giungato 2001-03-14