• Autore:   Elia Argentieri
  • Ultima modifica:   6 mag 2022 18:07
  • Redazione:   17 gen 2022 23:02
  • Sorgente di questa pagina
  • Tempo di lettura:   3 minuti

Torniamo a dimostrare teoremi che ci porteranno ad avere una visione più formale di Turing-equivalenza, quella proprietà di un formalismo che ci garantisce la possibilità di calcolare tutte le funzioni calcolabili, compresa la MdT universale.

Iniziamo con il cosidetto teorema del parametro o teorema s-m-n, considerando prima il caso m = 1 e n = 1. Informalmente, il teorema dice che, dato un programma che prenda in entrata m+n variabili, esiste un algoritmo ricorsivo che fornisce in uscita un programma di n variabili che fornisce gli stessi risultati del primo e che codifica le altre m variabili.

Teorema del parametro

Teorema: esiste una funzione calcolabile totale (iniettiva) \(s^1_1\) con due argomenti, tale che:

$$\forall i,x \quad \varphi_{s_1^1(i,x)} = \lambda z.\varphi_i(x,z)$$

La funzione \(s^1_1\) ha apice 1 e pedice 1 perché nella versione s-m-n sarà \(s^m_n\) , avrà m + 1 parametri e restituirà l’indice di una funzione a n parametri. Considerando il caso m = 1 e n = 1, omettiamo sia l’apice che il pedice e consideriamo s a 2 parametri e che restituisce l’indice di una funzione a 1 parametro.

Per esempio sia \(\varphi_i(x,z) = x \times f(z)\) . Dato i qualunque e posto x = 2, mediante s trovo in modo effettivo l’indice del programma che calcola la funzione \(\lambda z.\>2 \times f(z)\) .

La tecnica di valutazione parziale utilizzata in alcuni linguagi di programmazione (tipo OCaml, Clojure e molti altri) si basa proprio sul teorema del paramentro.

Dimostrazione (intuitiva): per calcolare \(\varphi_{s(i,x)}(z)\) trova \(M_i\) grazie al teorema di enumerazione, predisponi lo stato iniziale di \(M_i(x,z)\) con x fissato in anticipo (in termini di programmi si aggiunge un assegnamento x:=k all’inizio del programma per fissare il valore di x). L’algoritmo delineato, per la tesi di Church-Turing, calcola una funzione che è proprio la funzione \(s = s_1^1\) che stavamo cercando. Ci manca da dimostrare che la s esiste iniettiva. Basta costruire s strettamente crescente e questo è possibile perché ci sono \(\#(\mathbb{N})\) MdT che calcolano s(i,x). Quindi s deve essere tale che se la codifica delle coppie \((i_0, x_0) < (i_1, x_1) \implies s(i_0, x_0) < s(i_1, x_1)\) .

Implementazione del teorema s-1-1 in lisp:

(defun s11 (f x)
	(list 'lambda '(y) (list f x 'y)))

(defun myf (x y)
	(+ x y))

(s11 myf 3)
=> (lambda (y) (myf 3 y))

Teorema del parametro s-m-n

Teorema: esiste una funzione calcolabile totale iniettiva \(s_n^m\) con m + 1 argomenti tale che:

$$\forall x,y_1,...,y_m \quad \varphi^{(n)}_{s^m_n(x,y_1,...,y_m)} = \lambda z_1,...,z_n. \> \varphi_x^{(m + n)}(y_1,...,y_m,z_1,...,z_n)$$

Notiamo che \(s_n^m\) prende m + 1 parametri e restituisce l’indice di una funzione a n parametri. Notiamo anche che \(\varphi_x^{m+n}\) ha m+n parametri.

Come viene spiegato su Wikipedia, se prendiamo una funzione con m+n variabili e numero di Gödel z:

$$ \varphi_z(x_1,...,x_n,y_1,...,y_m) $$
Esiste una funzione ricorsiva primitiva \(s_n^m\) di m + 1 variabili che fornisce il numero di Gödel \(g_n\) di una procedura delle restanti variabili che dia lo stesso risultato.
$$ \forall z,x_1,...,x_n,y_1,...,y_m \;\;\; \varphi_z^{(m+n)}(x_1,...,x_n,y_1,...,y_m) = \varphi_{s_n^m(z,y_1,...,y_m)}^{(n)}(x_1,...,x_n) $$
e φ è una funzione parziale.

Il teorema di enumerazione e del parametro, in un certo senso, sono l’uno l’inverso dell’altro in quanto il primo “innalza” un indice alla posizione di argomento, mentre il secondo “abbassa” un argomento alla posizione di indice.

Teorema di espressività

Teorema: un formalismo è Turing equivalente (calcola tutte e sole le funzioni T-calcolabili, è universale) se e solamente se