Teorema di ricorsione di Kleene

Nella teoria della computabilità, i teoremi di ricorsione di Kleene sono due fondamentali risultati riguardanti l'applicazione di funzioni calcolabili a loro stesse. I teoremi furono dimostrati per la prima volta da Stephen Kleene nel 1938.

I due teoremi di ricorsione possono essere applicati per costruire punti fissi di certe operazioni su funzioni calcolabili, per generare quine, e per costruire funzioni definite mediante definizione ricorsiva.

Il secondo teorema di ricorsione

Il secondo teorema di ricorsione è strettamente legato alle definizioni di funzioni calcolabili date tramite ricorsione. Poiché è più conosciuto del primo teorema di ricorsione, è semplicemente chiamato teorema di ricorsione. La sua tesi fa riferimento alla numerazione standard di Gödel φ delle funzioni parziali ricorsive, in cui la funzione corrispondente all'indice e è $\varphi _{e}$.

Secondo teorema di ricorsione: Se F è una funzione ricorsiva allora c'è un indice e tale che $\varphi _{e}\simeq \varphi _{F(e)}$.

Dove $\varphi _{e}\simeq \varphi _{F(e)}$ significa che, per ogni n, sia $\varphi _{e}(n)$ che $\varphi _{F(e)}(n)$ sono definite, ed i loro valori sono gli stessi, oppure entrambe sono non definite.

Esempio

Supponiamo che g e h siano funzioni totali ricorsive che sono usate per la definizione ricorsiva di una funzione f:

$f(0,y)\simeq g(y)$

$f(x+1,y)\simeq h(f(x,y),x,y)$

Questa definizione ricorsiva può essere convertita in una funzione calcolabile F(e) che prende l'indice di un programma e e restituisce un indice F(e) tale che

$\varphi _{F(e)}(0,y)\simeq g(y)$

$\varphi _{F(e)}(x+1,y)\simeq h(\varphi _{e}(x,y),x,y)$

In questo contesto, un punto fisso di F è un indice e tale che $\varphi _{e}\simeq \varphi _{F(e)}$; la funzione calcolata da un tale e sarà una soluzione dell'equazione ricorsiva originale. Il teorema di ricorsione stabilisce l'esistenza di un tale punto fisso, supponendo che F sia calcolabile, ed è talvolta chiamato teorema del punto fisso (di Kleene) per tale ragione. Il teorema non garantisce che e sia l'indice per il più piccolo punto fisso dell'equazione ricorsiva; questo è compito del primo teorema di ricorsione, descritto sotto.

Applicazione alle quine

Un'interpretazione informale del secondo teorema di ricorsione è che ogni funzione parziale ricorsiva possa fornire un indice di sé stessa. Questo segue dal seguente corollario del teorema.

Corollario. Per ogni funzione parziale ricorsiva Q(x,y) esiste un indice p tale che $\varphi _{p}\simeq \lambda y.Q(p,y)$.

Il corollario si dimostra ponendo $F(p)$ una funzione che restituisce un indice per $\lambda y.Q(p,y)$.

Il corollario mostra che per ogni funzione calcolabile Q di due argomenti, c'è un programma che prende un argomento e calcola Q con tale programma come primo argomento ed il parametro passato come secondo. Si noti che questo programma è in grado di generare il suo indice a partire dalle informazioni contenute nel programma stesso; non necessita nessuna risorsa esterna per trovare l'indice.

Un classico esempio è la funzione Q(x,y) = x. Il corrispondente indice p in questo caso produce una funzione calcolabile che ha come output il suo stesso indice per ogni valore a cui si applichi. Quando intesi come programmi per computer, tali indici sono chiamati quine.

Funzioni senza punti fissi

Una funzione F tale che $\varphi _{e}\not \simeq \varphi _{F(e)}$ per ogni e è detta senza punti fissi. Il teorema di ricorsione mostra che nessuna funzione calcolabile è senza punti fissi, ma ci sono molte funzioni non calcolabili senza punti fissi. Il criterio di completezza di Arslanov afferma che l'unico insieme ricorsivamente enumerabile (nella teoria della calcolabilità) che calcola una funzione senza punti fissi è l'insieme dei programmi che terminano su sé stessi (K).

Bibliografia

• Kleene, Stephen, "On notation for ordinal numbers," The Journal of Symbolic Logic, 3 (1938), 150-155.
• Rogers, H. The Theory of Recursive Functions and Effective Computability, MIT Press. ISBN 0-262-68052-1; ISBN 0-07-053522-1

Voci correlate

• Semantiche denotazionali, in cui un altro teorema di minimo punto fisso è usato per lo stesso scopo del primo teorema di ricorsione.
• Combinatori di punti fissi, che sono usati nel lambda calcolo per alcuni scopi come il primo teorema di ricorsione.

Collegamenti esterni

• (EN) Piergiorgio Odifreddi e S. Barry Cooper, Recursive Functions, in Edward N. Zalta (a cura di), Stanford Encyclopedia of Philosophy, Center for the Study of Language and Information (CSLI), Università di Stanford, 2012..