Importanza McCarthy 91 funzione in Computer Science

Question

Mentre ricorsione imparare mi sono imbattuto in funzione McCarthy 91 che restituisce il valore 91 per tutti gli argomenti interi n < = 101 e n - 10 per n> 101.

int McCarthy(int n) 
{ 
    if (n > 100) 
    return n - 10; 
    return McCarthy(McCarthy(n+11)); 
} 

int main() 
{ 
    printf(" %d ", McCarthy(45)); 
    return 0; 
} 

Ero solo curioso di sapere qual è il suo significato in Informatica? L'articolo Wikipedia afferma che è utilizzato come test case per la verifica formale. Cosa significa.?

Qualcuno può semplificare il suo utilizzo per me?

Answer 1

Immagina di scrivere un compilatore C, che accetta programmi come quello che hai scritto e produce codice eseguibile. Vuoi verificare che il tuo compilatore funzioni correttamente. Esegui un test case che è la definizione ricorsiva della funzione come lo hai scritto, e asserisci che quando si esegue il codice compilato si ottiene il risultato di facile calcolo (in questo caso il programma dovrebbe produrre 91). Casi di test difficili come questo sarebbero particolarmente utili se si stanno iniziando a scrivere ottimizzazioni per la compilazione di chiamate ricorsive.

Immagine che invece di scrivere un compilatore, si sta scrivendo un programma che tenta di scrivere una prova, come si scriverebbe in una classe matematica. Gli input per il programma potrebbero essere un insieme di trasformazioni come le leggi di algebra che usi per scrivere una dimostrazione e una dichiarazione che il programma tenta di dimostrare. Questo ramo dell'informatica è chiamato verifica formale. Le dichiarazioni relative alla funzione McCarthy 91 sono difficili da dimostrare. Ad esempio (per tutti x < = 100, M (x) == 91) sarebbe molto difficile da dimostrare. Questo sarebbe un problema molto difficile per il tuo programma di scrittura di prove e trasformazioni per produrre una prova di.