Strategie generali di prova per mostrare la correttezza delle funzioni ricorsive?

Question

Mi chiedo se esiste una regola/schema per procedere con la correttezza dell'algoritmo di dimostrazione? Per esempio abbiamo una funzione $ F $ definita sui numeri naturali e definito di seguito:

function F(n,k) 
begin 
    if k=0 then return 1 
    else if (n mod 2 = 0) and (k mod 2 = 1) then return 0 
    else return F(n div 2, k div 2); 
end; 

dove $ n \ \ text {div} \ 2 = \ left \ lfloor \ frac {n} {2} \ right \ rfloor $

il compito è dimostrare che $ F (n, k) = \ begin {casi} 1 \ Leftrightarrow {n \ choose k} \ \ text {mod} \ 2 = 1 \ 0 \ text {altrimenti} \ end {casi} $

Non sembra molto complicato (mi sbaglio?), ma non so come dovrebbe essere strutturato questo tipo di prova. Sarei molto grato per l'aiuto.

Answer 1

La correttezza degli algoritmi ricorsivi è spesso dimostrata da mathematical induction. Questo metodo consiste di due parti: in primo luogo, si stabilisce la base e quindi si utilizza un passo induttivo.

Nel tuo caso, la base è tutti i casi in cui k = 0, o quando k è dispari ma n è pari.

Il passo induttivo richiede dimostrando che quando f(n,k) è corretto, f(2*n,2*k), f(2*n+1,2*k), f(2*n,2*k+1) e f(2*n+1,2*k+1) sono tutti corretti.

Answer 2

In linea generale, si tenta di dimostrare per induzione la correttezza. Ciò funziona molto bene quando si dimostra la correttezza delle funzioni ricorsive, dal momento che è possibile provare direttamente il caso base, e quindi utilizzare il fatto che la funzione funzioni per input "più piccoli" per dimostrare che funziona per il prossimo input più grande.

In questo caso, tenterei una dimostrazione con induzione ben fondata. In particolare, proverei che

1. La funzione è corretta per tutti gli input del modulo (n, 0).
2. Supponendo che per tutti gli input (n ', k') tale che (n ', k') sia lessicograficamente minore di (n, k), la funzione sia corretta, dimostrare che è corretta per (n, k) .

Le specifiche di questa prova dovrebbero sfruttare le specifiche della funzione e il bahvaior dei coefficienti binomiali, ma il modello generale è come sopra.

Spero che questo aiuti!

Answer 3

Al di fuori di dimostrare matematicamente la logica (esempio: inductive proof), ci sono alcuni risultati nella scienza dell'informatica relativa a questo.

si può iniziare qui per una descrizione dei soggetti: Correctness
Per il vostro caso particolare, si sarebbe interessata alla correttezza parziale per dimostrare che la risposta è quello previsto. Quindi totale correttezza per mostrare che il programma termina.

Hoare logic può risolvere la vostra correttezza parziale.

quanto riguarda la risoluzione di questo problema particolare:

If (n% 2 == 0 e k% 1 == 1) o (k == 0) il programma termina, altrimenti recurses al n/2, k/2 caso.
Utilizzando strong induction su k, possiamo mostrare che il programma raggiunge sempre uno dei nodi terminali dove k == 0. (Potrebbe terminare prima nella prima clausola ma abbiamo solo bisogno di mostrare che termina del tutto, cosa che fa)

Quindi ho lasciato a voi la prova della correttezza parziale (perché non conosco quella roba)