Corrispondenza tra Induzione e Ricorsione: un cenno

 

Abbiamo in precedenza accennato [FBg] al fatto che dimostrare e programmare (descrivere computazioni) siano essenzialmente ed intrinsecamente la stessa cosa.

Qual e' allora il processo computazionale corrispondente alle dimostrazioni per induzione? [VS]

Il procedimento dimostrativo di una formula ∀n.φ(n) per induzione matematica consiste nel dimostrare φ(0) e nel dimostrare, preso un m generico, che vale φ(m) utilizzando l'ipotesi che valga φ(m-1).
Il suo corrispettivo computazionale e' la programmazione di funzioni su numeri naturali utilizzando una particolare forma di ricorsione: si descrive l'algoritmo per il calcolo della funzione specificando quanto vale la funzione per 0 e specificando quanto vale la funzione per un generico m supponendo di conoscere il risultato del calcolo della funzione su m-1.
Utilizziamo, per fare degli esempi, il semplice linguaggio di programmazione funzionale descritto nella Sezione 2 di [VS] (in pratica e' un piccolo sottoinsieme del linguaggio Haskell).
Il seguente programma sommadazeroa calcola la somma dei numeri da 0 al numero dato in input:

sommadazeroa 0 = 0             
                
          // specifichiamo il valore dell'output per l'input 0

sommadazeroa n = (somma (n-1)) + n             

          // specifichiamo il valore dell'output per un input generico n
          // (diverso da 0) supponendo di conoscere il risultato 
          // del calcolo per l'input (n-1)

Il procedimento dimostrativo di una formula ∀n.φ(n) per induzione completa consiste invece nel dimostrare φ(0) e nel dimostrare, preso un m generico, che vale φ(m) utilizzando (non necessariamente tutte) le ipotesi φ(m-1), φ(m-2),... e φ(1), (che quindi corrisponde a dimostrare (∀1≤q≤m.φ(q)) → φ(m) ).

Il suo corrispettivo computazionale e' la programmazione di funzioni attraverso una particolare laseguente forma di ricorsione: si descrive l'algoritmo per il calcolo della funzione specificando quanto vale la funzione per 0 e specificando quanto vale la funzione per un generico m supponendo di sapere il conoscere il risultato del calcolo della funzione per i numeri da 1 ad m-1.

Vediamo un esempio di programma ricorsivo che utilizza tale forma di ricorsione per restituire, dato in input n, l'n-esimo numero di Fibonacci:

fib 0 = 1                                       
         // specifichiamo il valore dell'output per l'input 0

fib n = if (n==1) then 1 else (fib (n-1) + fib (n-2)) 
 
         // specifichiamo il valore dell'output per un input generico n
         // (diverso da 0) supponendo di conoscere il risultato 
         // del calcolo per tutti gli input da 1 ad (n-1) (anche se
         // ci serve poi solo il valore per n-1 ed n-2)

L'induzione e la ricorsione appena viste considerano solo il dominio dei numeri naturali. Esiste una generalizzazione dei principi di induzione matematica e completa che permette di dimostrare proprieta' quantificate universalmente su insiemi ben fondati: l'induzione ben fondata (vedi [VS]).
Il procedimento dimostrativo di una formula ∀s∈ S.φ(n) per induzione ben fondata, dove (S, ∠) e' un insieme ben fondato, consiste nel dimostrare φ(m) per tutti gli elementi minimali di S e nel dimostrare, preso un q generico non minimale, che vale φ(p) utilizzando l'ipotesi che valga φ(q) per tutti gli q che precedono p (che quindi corrisponde a dimostrare ∀p∈(S-M).((∀q∠p.φ(q)) → φ(p)), dove M e' l'insieme degli elementi minimali di S).
Il suo corrispettivo computazionale e' la programmazione di funzioni attraverso la ricorsione generale su input appartenenti ad insiemi ben fondati: si descrive l'algoritmo per il calcolo della funzione specificando quanto vale la funzione per tutti gli elementi minimali e specificando quanto vale la funzione per un generico p non minimale supponendo di conoscere il valore della funzione su tutti gli elementi "piu' piccoli" di p (rispetto la relazione di precedenza).

Vediamo un esempio di programma ricorsivo che utilizza tale forma di ricorsione per restituire, data in input una lista di numeri, la sua lunghezza:

sommanums [] = 0

sommanums (n:listnum) = n + (sommanums listnum)

(ricordiamo che [] denota la lista vuota e che l'operatore infisso ':' concatena un numero ad una lista di numeri)

In questo caso l'insieme ben fondato su cui applichiamo il procedimento ricorsivo e'

dove la relazione di precedenza ∠ e' definita nel modo seguente: Ovviamente ∠ e' una relazione ben fondata su ListeDiNumeri.

Che la definizione ricorsiva di lungh sia corretta si poteva capire immediatamente, poiche' tale definizione riflette il procedimento induttivo di definizione dell'insieme ListeDiNumeri.

Un insieme e' definito induttivamente quando si forniscono gli elementi "piu' semplici" appartenenti all'insieme (nel nostro caso la lista vuota []) e poi si mostra come qualsiasi altro elemento dell'insieme possa essere "costruito" a partire da altri elementi dell'insieme (nel nostro caso una lista non vuota si "costruisce" concatenando un numero ad una lista di numeri).
Un esempio di insieme definito induttivamente e' quello degli Alberi Binari Localmente Completi (ABLC): l'ABLC piu' semplice e' un nodo (che possiamo indicare con '•' e chiamare Node); tutti gli altri ABLC sono costruiti aggiungendo un nodo radice a due ABLC:

Possiamo chiamare AggRad l'operazione di aggiungere un nodo radice a due ADLC

(in Haskell e' molto semplice definire tipi di dato induttivi, per esempio il tipo di dato ABLC si puo' elegantemente definire nel modo seguente

data ABLC =  Node |  AggRad ABLC ABLC 

dove il simbolo '|' si puo' leggere come "oppure". Quindi la definizione e' come se dicesse: un ABLC e' Node (l'elemento piu' semplice), oppure si ottiene da due ABLC attraveso l'operatore AggRad).

Per esempio l'espressione

 (AggRad (AggRad (AggRad Node Node) Node) Node)

corrisponde all'ABLC seguente:

              •
             / \
            •   • 
           / \
          •   •
         / \
        •   •

E' immediato vedere come la relazione "_ e' un elemento con cui si e' costruito _ " sia la relazione di precedenza associata al procedimento induttivo di costruzione degli ABLC, e sia ben fondata. Per esempio abbiamo che rispetto a tale relazione

                                                • 
            •                                  / \
           / \            precede             •   • 
          •   •                              / \
         / \                                •   •
        •    •                             / \      
                                          •   •

e che

                                            • 
                                           / \
         •           precede              •   • 
                                         / \
                                        •   •
                                       / \      
                                      •   •

Il seguente programma ricorsivo calcola l'altezza di un ABLC:

altezza Node = 1

altezza (AggRad ablc1 ablc2) =  1 + (max (altezza ablc1) (altezza ablc2))

dove max e' una funzione predefinita che calcola il massimo di due numeri.

La relazione rispetto alla quale viene utilizzata la ricorsione e' banalmente ben fondata, poiche' e' esattamente la relazione associata al procedimento induttivo di costruzione degli ABLC: infatti
ablc1 "e' un ABLC con cui si e' costruito" (AggRad ablc1 ablc2)
e
ablc2 "e' un ABLC con cui si e' costruito" (AggRad ablc1 ablc2)

Il programma altezza definisce il valore da restituire nel caso in cui l'input sia l'ABLC piu' piccolo e poi, per un generico ABLC composto, descrive il valore da restituire supponendo di conoscere il valore restituito per gli elementi con cui e' costruito l'input.

Ci sono pero' definizioni ricorsive che utilizzano relazioni di precedenza che sono molto differenti dalla relazione associata al procedimento induttivo di costruzione del tipo di dato. E spesso e' quindi non banale capire qual e' la relazione utilizzata per la ricorsione e vedere che sia ben fondata.

Consideriamo un programma ricorsivo snums che prende in input liste di numeri e restituisce la somma dei numeri presenti nella lista di input, ma che utilizza un algoritmo differente da quello utilizzato da sommanums

snums [] = 0

snums (0:listanum) = snums listanums

snums (n:listanum) = 1 + (snums ((n-1):listanums))

ora, quale relazione di precedenza ben fondata esiste sia tra
(0:listanum) e listanum
che tra
(n:listanum) e ((n-1):listanums) ?

Di certo non e' la relazione "e' un elemento con cui si e' costruito".

Qual e' allora?

E' la relazione ∠ definita come segue: dove |L| e' la lunghezza della lista L e fst e' la funzione che restituisce il primo elemento di una lista.
Si puo' dimostrare che (ListeDiNum, ∠) e' un insieme ben fondato.
Si puo' vedere anche come la relazione di precedenza ∠ corrisponda ad una versione della precedenza lessicografica utilizzata nella Definizione 1.50 in [AAG], che e' ben fondata. E come sia in particolare una versione della definizione di precedenza lessicografica definita in [VS] (Esercizio 1.16), ovviamente considerando che ListeDiNum x ListediNum e' isomorfo a ListeDiNum.

Quanto detto ci fa capire come sia naturale che proprieta' di programmi scritti in linguaggi funzionali, o programmi ricorsivi in generale, si possano dimostrare utilizzando i principi di induzione.