7.4 Costrutti per il controllo

A differenza del Prolog, che usa la regola di computazione che seleziona sempre il letterale più a sinistra, il Gödel ha una regola di computazione flessibile che può selezionare un letterale diverso da quello leftmost. Le ragioni per desiderare una regola di computazione flessibile sono molteplici: permette di ottenere la correttezza, agevolare la terminazione, aumentare l'efficienza e controllare il pruning.

Dal momento che la semantica procedurale del Gödel è data dalla risoluzione SLDNF, la regola di computazione utilizzata deve essere safe nel senso che dei letterali negativi solo quelli ground possono essere selezionati. In questo caso, ogni risposta calcolata SLDNF è corretta rispetto alla semantica del completamento. Tale regola è built-in nel sistema Gödel.

Il programmatore Gödel può modificare la regola di computazione per mezzo delle dichiarazioni di controllo DELAY, che fanno rimandare la selezione di sottogoal finché questi ultimi non siano sufficientemente istanziati.

La regola di computazione flessibile permette di aumentare l'efficienza nel caso di coroutining; consideriamo il seguente esempio di schema generate-and-test:

PREDICATE   Permutation : List(alpha) $\ast$ List(alpha). 


DELAY          Permutation(x,y) UNTIL NONVAR(x) $\vee$ NONVAR(y).    





Permutation([],[]).    


Permutation ([x$\mid$ y],[u$\mid$ v]) $\leftarrow$ 


Delete(u,[x$\mid$ y],z)  $\&$ 


Permutation(z,v).    





PREDICATE Sorted : List(Integer).  


DELAY  Sorted([]) UNTIL TRUE; 


Sorted([_]) UNTIL TRUE; 


Sorted([x,y$\mid$ _]) UNTIL NONVAR(x) $\&$ NONVAR(y).  





PREDICATE Slowsort : List(Integer) $\ast$ List(Integer).   


Slowsort(x,y) $\leftarrow$ 


Sorted(y) $\&$ 


Permutation(x,y).  

La valutazione di un goal del tipo

$\leftarrow$ Slowsort([1,3,4,2],x)

sarà molto più efficiente con la definizione data di Slowsort rispetto a quella che si sarebbe avuta se non fossero state disponibili le dichiarazioni di DELAY. Infatti, i due letterali presenti nel corpo della definizione di Slowsort sarebbero dovuti apparire nell'ordine inverso e quindi Permutation avrebbe dovuto calcolare una permutazione completa. Invece il DELAY Sorted([x,y$\mid$ _]) UNTIL NONVAR(x) $\&$ NONVAR(y) fa in modo che, appena Permutation ha calcolato i primi due elementi della nuova permutazione, si verifichi se sono ordinati.

Un altro uso importante del DELAY è quello che permette di evitare cicli infiniti. Considerando il predicato Delete

PREDICATE Delete : alpha $\ast$ List(alpha) $\ast$ List(alpha). 


DELAY 		 Delete(_,y,z) UNTIL NONVAR(y) $\vee$ NONVAR(z). 




Delete(x,[x $\mid$ y],y). 


Delete(x,[y $\mid$ z],[y $\mid$ w]) $\leftarrow$ 


Delete(x,z,w).

Con la regola leftmost senza i DELAY visti la valutazione del goal $\leftarrow$ Permutation(x,[1,2,3]). porterebbe al calcolo di una soluzione e poi, col backtracking, si cadrebbe in un ciclo infinito. Con i DELAY si calcolano solo le sei risposte e poi il goal fallisce.

Il Gödel ha la capacità di risolvere vincoli nel dominio degli interi e dei razionali. Per esempio anche un semplice goal del tipo

$${\tt 3 \ast x + 5 \ast y = 16 \ \& \ 11 \ast x - y =2. }$$

richiede del coroutining tra i goal e ciò viene realizzato dal sistema stesso senza impegno da parte del programmatore.

L'ultimo strumento di controllo disponibile nel Gödel è l'operatore di pruning. In Prolog l'operatore di pruning è il cut che ha però una serie di problemi semantici, il primo dei quali è che il programmatore inserendo dei cut può sfruttarne la natura sequenziale per effettuare dei "test". Il problema a questo punto è che la componente logica del programma non può essere ottenuta semplicemente rimuovendo i cut. Inoltre in presenza di negazione l'uso del cut può dar luogo a risposte non corrette rispetto al completamento del programma. Infine la classe dei programmi contenenti cut non è chiusa rispetto alle trasformazioni di programmi.

Quindi il Gödel adotta un diverso operatore di pruning, detto commit che si rifà al commit dei linguaggi concorrenti. Il significato procedurale del commit, che si indica con $\mid \$, è che è trovata una sola soluzione della formula alla sua sinistra e tutti gli altri rami scaturiti dalle altre clausole della definizione del predicato che contiene il commit vengono tralasciati.

Chiaramente, avendo solo una semantica procedurale, l'uso del commit si allontana dal fine principale del Gödel che è quello di avere programmi con la semantica dichiarativa migliore possibile. D'altra parte è possibile eliminare tutti i commit per ottenere la componente logica dei programmi, e inoltre il commit è corretto.

Il commit può essere usato per evitare computazioni inutili:

p $\leftarrow$ q $\mid$ r

p $\leftarrow$ s $\mid$ t

considerando il goal $\leftarrow$ p, se il sottogoal q ottenuto dopo un passo di derivazione ha successo, si eviterà di unificare con la seconda clausola.

Più in generale il commit one solution permette di tralasciare risposte: tale commit, scritto $\{ \ldots \}$, calcola una sola soluzione alla formula contenuta tra le parentesi. Per esempio, il goal

$${\tt\leftarrow \{Permutation([1,2,3],x)\}.}$$

avrà un'unica risposta calcolata. Tale commit può essere anche usato nel corpo di clausole del programma.

Il seguente esempio mette in luce come i due tipi di commit finora visti diano luogo a programmi non chiusi rispetto a trasformazioni di programma, per esempio l'unfolding; considerando:

p $\leftarrow$ m $\&$ l

p $\leftarrow$ n

m $\leftarrow$ q $\mid$ r

m $\leftarrow$ s $\mid$ t

n $\leftarrow$ u $\mid$ v

facendo l'unfolding su m e n otteniamo:

p $\leftarrow$ q $\mid$ r $\&$ l

p $\leftarrow$ s $\mid$ t $\&$ l

p $\leftarrow$ u $\mid$ v

Tale programma non è corretto perché la portata del commit nelle prime due clausole è diversa da quella del commit nella terza.

Per ovviare a questo problema, in Gödel è presente un terzo tipo di commit, scritto $\{ \ldots \} _{l}$, dove $l$ è una etichetta (intero positivo). Con questa notazione, il programma precedente sarà

p $\leftarrow$ m $\&$ l

p $\leftarrow$ n

m $\leftarrow \{$q$\}_{1} \&$ r

m $\leftarrow \{$s$\}_{1} \&$ t

n $\leftarrow \{$u$\}_{1} \&$ v

che darà luogo, con l'unfolding, al programma corretto

p $\leftarrow \{$q$\}_{1} \&$ r $\&$ l

p $\leftarrow \{$s$\}_{1} \&$ t $\&$ l

p $\leftarrow \{$u$\}_{2} \&$ v