Church, tesi di

Church, tesi di

Church, tesi di tesi elaborata dal logico statunitense A. Church; afferma che ogni funzione calcolabile è una funzione ricorsiva e, viceversa, ogni funzione ricorsiva è una funzione calcolabile. Ciò comporta che se per una funzione esiste una procedura algoritmica che permette di calcolarne il valore in modo deterministico e in un tempo finito (funzione calcolabile), allora è possibile costruire tale funzione secondo gli schemi di una funzione ricorsiva, cioè partendo dalle funzioni base e applicando gli schemi di composizione, ricorsione e minimalizzazione. La tesi di Church afferma, pertanto, che il modello di calcolo fornito dalle funzioni ricorsive traduce in modo rigoroso il concetto intuitivo di funzione calcolabile. Nessun formalismo di descrizione esaustiva dell’insieme delle funzioni calcolabili ha mai contraddetto la tesi di Church, che rimane tuttavia una tesi non dimostrabile; infatti esprimendo con un qualsiasi formalismo l’idea di → calcolabilità, si riesce a dimostrare soltanto l’equivalenza fra le funzioni ricorsive e le funzioni calcolabili secondo quel formalismo. La tesi di Church è comunque verificata da tutti i formalismi finora conosciuti. È stata per esempio dimostrata l’equivalenza fra l’insieme delle funzioni ricorsive, l’insieme delle funzioni calcolabili con una macchina di Turing e l’insieme delle funzioni rappresentabili nel λ-calcolo.