es10 



guess è una funzione con due argomenti.

All'interno del corpo l'argomento "is" è applicato  al predicato "null?" e alla funzione "car", quindi è una lista (queste 

sono funzioni che lavorano sulle liste). Possiamo dire anche che "is" è una lista di liste a qualunque livello di 

annidamento perché nella chiamata ricorsiva "car is" viene dato come argomento a guess, quindi anche la testa di "is" può 

essere una lista.

"is" sarà una lista a qualsiasi livello di annidamento di numeri, in quanto applichiamo (car is) al predicato "number?".

"what" invece è un predicato e lo si deduce dal fatto che è presente in una delle espressioni booleane che distinguono i 

vari casi del "cond".

Quindi guess è una funzione che prende un predicato ed una lista a qualunque livello di annidamento e restituisce una 

lista (questo lo capiamo dal fatto che il caso base restituisce la lista vuota e il caso ricorsivo restituisce il "cons" 

di qualcosa). La lista restituita ha lo stesso numero di elementi di quella iniziale perché in nessun caso viene eliminato 

qualche elemento, viene semplicemente "fatto" qualcosa  su ogni elemento della lista.

Facciamo un esempio:

(define (H? n)

           ( = n 3 ))

 e valutiamo l'espressione

(guess H? ((2 3) 5) )

vediamo informalmente cosa produce la valutazione di questa espressione

(cons (guess H? (2 3) ) (guess H? (5) ))

(cons (cons 2  (guess H? (3) )) (guess H? (5) ))

(cons (cons 2  (0) ) (guess H? (5) ))

(cons (cons 2  (0) ) (5))

((2 0 ) 5)

 

Si nota subito che la ricorsione è fatta sulle liste in quanto si ha o (guess what (car is)) oppure (guess what (cdr is)).

Qual è la relazione di precedenza ben fondata utilizzata per fare ricorsione?

Ne indichiamo due possibili:

1)    l  <1  l'     sse    l ha un livello di annidamento minore di l' oppure se a parità di livello di annidamento, 

il numero di elementi numerici e liste vuote è minore.

Questa è ben fondata in quanto è una relazione di precedenza lessicografica su due relazioni di precedenza ben fondate.

oppure più formalmente:

<1 =  <lex  (<' <'')

dove   l <' l'  sse  ann( l ) < ann( l' )   
   (dove ann ( l ) è il livello di annidamento della lista l)

      l <'' l'  sse  #( l ) < # ( l' )   
   (dove  #( l) è il numero di interi o di liste vuote presente in l)

 

2)  l  <1  l'    sse   il numero totale di liste ed elementi numerici presenti nella lista l è minore di quello della 

lista l'.


Ora dobbiamo dimostrare che per ogni elemento del dominio (cioè per tutte le possibili liste) vale il predicato:

P:  "La funzione guess restituisce una lista uguale a quella data in input tranne per gli elementi che verificano 

il predicato "what"(essi vengono cambiati in 0)"

Lo si dimostra per induzione:

- L'elemento base è   '( ) :

     (guess what '( ))  =  '( )    =>  il predicato è vero

-Ipotesi induttiva:

Consideriamo l'elemento generico  "is" e supponiamo che per tutti gli elementi più piccoli di  "is"  il predicato sia vero.

Allora si ha che guess sugli argomenti (car is) e (cdr is) produce sicuramente delle liste uguali a queste,

dove, però, i numeri che verificano il predicato what sono stati cambiati in 0.

 

guess  sull'argomento  is  non fa altro che applicare il cons del (car is) "già sistemato" (per ipotesi induttiva) 

e del (cdr is) "già sistemato" (per ipotesi induttiva), quindi produce la lista che volevamo.