meta.tex

\chapter{Metaprogramiranje}

U ovom poglavlju dokazat ćemo nekoliko rezultata sa zajedničkom idejom: algoritmi mogu preko kodiranja raditi na raznim tipovima podataka, pa tako mogu raditi i na algoritmima. Recimo, u lemi~\ref{lm:compram}, nismo mi samo dokazali da ako su $\f G_1,\f G_2,\dotsc,\f G_l,\f H\in\mathscr Comp$ (odgovarajućih mjesnosti), tada je i $\f H\circ(\f G_1,\dotsc,G_l)\in\mathscr Comp$ --- već smo doista konstruirali funkciju $compose:\mathscr Prog^+\mspace{-2mu}\times\mathscr Prog\times\N_+\to\mathscr Prog$ koja prima RAM-programe $P_{\f G_1}$, $P_{\f G_2}$,~\ldots, $P_{\f G_l}$ i $P_{\f H}$ što računaju odgovarajuće funkcije (i mjesnost $k$) te od njih sastavlja RAM-program $Q_{\f F}^\flat$ što računa njihovu kompoziciju. Funkcija $compose$ (odnosno $compose_k^{l+1}\!$, jer je parametrizirana mjesnostima) je izračunljiva, i ovdje ćemo to dokazati. Nećemo baš programirati dokaz leme~\ref{lm:compram}, jer on ide preko spljoštenja i funkcijskog makroa, što je komplicirano za izvesti formalno --- ići ćemo "zaobilaznim putom", za koji će se poslije ispostaviti da je zapravo prilično koristan.

\section{Specijalizacija}

Kao što smo već nagovijestili, počet ćemo sa \emph{specijalizacijom}: postupkom kojim u od\-re\-đe\-nom algoritmu fiksiramo jedan (zadnji) ulazni podatak na neki konkretni broj. Dosad smo vidjeli mnoge primjere specijalizacije:

\begin{itemize}
    \item Funkcija $\f{blh}$ iz leme~\ref{lm:blh} dobivena je specijalizacijom funkcije $\f{slh}$, fiksirajući njen zadnji (drugi) argument na $2$. %\\ Skraćeno 
	    Kažemo da je $\f{blh}$ $2$-specijalizacija $\f{slh}$, i pišemo $\f{blh}=\$(2,\f{slh})$.
    \item Operacija $\conc{}$ je $12$-specijalizacija funkcije $\f{sconcat}$ (propozicija~\ref{pp:concprn}).
    %\item Općenito u primitivnoj rekurziji~\eqref{eq:defprb}, baza je zapravo $0$-specijalizacija definirane funkcije: $G=\$(0,G\pr H)$.
    \item Bazu primitivne rekurzije~\eqref{eq:defprb} možemo zapisati kao $\$(0,G\pr H)=G$.
    \item Prema~\eqref{eq:resultdef}, $\f{result}=\$(0,\f{ex})$.
    \item Za svaki konkretni $e\in\N$ i $k\in\N_+$, funkcija $\kf e^k$ je $e$-specijalizacija funkcije $\f{comp}_k$.
    \item Baza $\f G_3$ za funkciju $\f{Tape}$ (lema~\ref{lm:StateHeadTapeprn} --- $0$-specijalizacija $\f{Tape}$) je dobivena specijalizacijom funkcije $\f{Recode}$, fiksirajući njena dva zadnja argumenta na $b'$ i $b$ redom. Vidimo da možemo specijalizirati i s obzirom na više argumenata, što je samo višestruka primjena specijalizacije jednog argumenta.
\begin{equation}\label{eq:multpar}
    \f G_3=\$(0,\f{Tape})=\$(b',b,\f{Recode})=\$\bigl(b',\$(b,\f{Recode})\bigr)
\end{equation}
\end{itemize}

Ideja specijalizacije je time na neki način suprotna ideji dinamizacije, koja iz familije $f^k_i(\vec x),i\in\N$ konstruira $f^{k+1}(\vec x,i)$ --- ovdje iz $f^{k+1}(\vec x,i)$ i konkretnog broja $i_0$ dobijemo funkciju $f^k_{i_0}$, koja preslikava $\vec x$ u $f(\vec x,i_0)$. Iako dinamizacija općenito nije izračunljivo preslikavanje na funkcijama, specijalizacija jest --- i to nam je cilj ovdje dokazati.

U literaturi se za specijalizaciju još koristi naziv \emph{parcijalna evaluacija}, posebno kod algoritamske optimizacije --- jer ako imamo fiksnu vrijednost nekog argumenta, određeni dio izraza možemo izračunati unaprijed i tako pojednostaviti izraz. Sličnu ideju imamo u konkretnoj matematici, povezanu s pojmom \emph{zatvorenog oblika}: npr.\ iako je teško izračunati općenite vrijednosti funkcije $f(n,k):=\sum_{j=1}^n j^k$, za $k=2$ dobivamo formulu $f(n,2)=\frac{n(n+1)(2n+1)}{6}$. U logičkom kontekstu toj ideji odgovara \emph{supstitucija}, kojom iz formule s $k+1$ slobodnih varijabli dobijemo formulu s $k$ slobodnih varijabli, uvrštavajući za neku varijablu neki zatvoreni term (koji u standardnom modelu od PA odgovara upravo nekom fiksnom prirodnom broju). Vidimo da se slična ideja pojavljuje na mnogim mjestima, što upućuje na njenu korisnost.

Sasvim je nesporno (i već smo to dokazali u svim specijalnim slučajevima navedenima na početku ove točke) da specijalizacija čuva izračunljivost. Zbog teorema ekvivalencije, svejedno je kako konkretiziramo tu izračunljivost, a dokaz je najlakši za parcijalnu rekurzivnost.

\begin{propozicija}[{name=[specijalizacija čuva parcijalnu rekurzivnost]}]
    Neka su $k\in\N_+$, $y\in\N$ te $\f f^{k+1}$ parcijalno rekurzivna funkcija.\newline
    Tada je i funkcija $\f g^k:=\$(y,\f f)$, zadana s
%\begin{equation}
    $\f g(\vec x):\simeq\f f(\vec x,y)$,
%\end{equation}
parcijalno rekurzivna.
\end{propozicija}
\begin{proof}
Definiciju od $\f g$ možemo zapisati u simboličkom obliku
\begin{equation}\label{eq:paramcompose}
    \f g=\f f\circ(\f I_1^k,\f I_2^k,\dotsc,\f I_k^k,\f C_y^k)\text,
\end{equation}
što vrijedi jer imamo $\dom{\f g}=\{\vec x\in\N^k\mid(\vec x,y)\in\dom{\f f}\}$ --- a to je upravo domena desne strane jer su sve koordinatne projekcije, kao i konstanta $\f C_y^k$, totalne. Sada tvrdnja slijedi iz zatvorenosti skupa svih parcijalno rekurzivnih funkcija na kompoziciju.
\end{proof}

\begin{korolar}[{name=[specijalizacija čuva (primitivnu) rekurzivnost]}]\label{kor:paramprn}
    Ako je $k\in\N_+$, $y\in\N$ te funkcija $\f f^{k+1}$ (primitivno) rekurzivna,\newline tada je i $\f g^k:=\$(y,\f f)$ (primitivno) rekurzivna.
\end{korolar}
\begin{proof}
Isti kao prethodni --- zapravo lakši, jer ne moramo određivati domenu.
\end{proof}

Ipak, ta tvrdnja nije glavna tema ove točke. Konkretizirajući izračunljivost kroz postojanje indeksa, ona samo kaže da ako $\f f$ ima indeks, tada i $\f g$ ima indeks --- ne kaže, barem ne eksplicitno, kako \emph{izračunati} indeks od $\f g$ pomoću indeksa od $\f f$. Mogli bismo izračunati (neke) indekse od $\f I_i^k,i\in[1\mspace{-1mu}\dd k]$ i $\f C_y^k$ --- te kad bismo imali $\f{compose}$ kao izračunljivu funkciju na indeksima, kao posebni slučaj dobiti i indeks kompozicije~\eqref{eq:paramcompose}. Ipak, lakše je prvo realizirati specijalizaciju u obliku izračunljive funkcije $\f S$%(slovo dolazi od \emph{substitute} ili \emph{specialize}, ovisno o tome pitate li logičare ili programere)%
, a onda $\f{compose}$ pomoću te funkcije.

Na neki način, $\f S=\N \$$, gdje funkcije kodiramo njihovim indeksima kako je detaljno objašnjeno u primjeru~\ref{pr:parcspecind}. Ukratko, $\f S$ prima $y$ i \emph{bilo koji} indeks za $\f f$ te vraća \emph{neki} indeks za $\$(y,\f f)$.

Bilo bi sjajno kada bismo mogli dobiti $\f S$ kao jednu funkciju, neovisnu o mjesnosti $k$ funkcije $\f f$ --- no to, barem ovako kako smo zamislili indekse, nije moguće. Ta funkcija bi trebala primati $y$ i kod RAM-programa $e$, i vraćati kod novog RAM-programa $e'$ takvog da bude $\kf e(\vec x,y)\simeq\kf{e'}(\vec x)$ za sve $\vec x\in\N^k$. No to znači da \emph{registar} ($\reg{k+1}$) u kojem će pisati ulazni podatak $y$ u odgovarajućem RAM-stroju ovisi o $k$, a $k$ ne možemo zaključiti iz samog RAM-programa odnosno njegova koda $e$.

\begin{napomena}[{name=[uniformna verzija teorema o parametru]}]
Zapravo bismo mogli dokazati i "uniformnu" verziju, kad bismo fiksirali argumente s početka a ne s kraja. Tada bi $y$ uvijek išao u $\reg1$, a sve ostale registre (koji se stvarno spominju u programu, što \emph{možemo} zaključiti iz $e$) bismo pomicali za jedno mjesto udesno. To može poslužiti kao osnova za malo ozbiljniji studentski rad, ali je kompliciranije --- a nama će ova verzija biti dovoljna.
\end{napomena}

% \subsection{Teorem o parametru}

\begin{propozicija}[Teorem o parametru]\label{pp:tmpar}
	Za svaki $k\in\N_+$ postoji primitivno rekurzivna funkcija $\f S_k^2:\N^2\to\f{Prog}$, takva da za sve $y,e\in\N$ vrijedi $\kf{\f S_k(y,e)}^k=\$(y,\kf e^{k+1}\mspace{-1mu})$.
\end{propozicija}
Spomenutu funkcijsku jednakost možemo zapisati točkovno:
\begin{equation}\label{eq:Sfunceq}
    \f{comp}_k\bigl(\vec x,\f S_k(y,e)\bigr)\simeq\f{comp}_{k+1}(\vec x,y,e)\text{, za sve }\vec x\in\N^k
\end{equation}
(i to je razlog za "obrnuti" redoslijed pisanja argumenata od $\f S_k^2$).
\begin{proof}
    Kao što smo već rekli, trebamo "hardkodirati" $y$ u registar $\reg{k+1}$, i nakon toga pustiti RAM-program $P$ da računa s ulaznim podacima $\vec x$ (u registrima $\reg1$ do $\reg k$, kao ulazni podaci za $\kf{\f S_k(y,e)}^k$) i $y$ (u registru $\reg{k+1}$). Program $P$ je onaj program čiji je $e$ kod, jedinstven zbog injektivnosti kodiranja. (Poslije ćemo vidjeti što ako nema takvog programa.) % --- no što ako takvog nema, odnosno $e\nin\f{Prog}$?
%Sada promotrimo slučaj kad takav $P$ postoji --- zbog injektivnosti kodiranja programa taj $P$ je jedinstven.
    Trebamo spljoštiti makro-program
\begin{equation}\label{eq:makroprogS}
    Q:=\begin{prog}
        0.&\incr{k+1}\\
        1.&\incr{k+1}\\
        &\vdots\\
        (y-1).&\incr{k+1}\\\hline
        y.&P^*
    \end{prog}
\end{equation}
od dva dijela (razdvojena crtom) --- dakle k\=od spljoštenja bit će dobiven konkatenacijom dva koda. Za gornji dio smo tehniku već vidjeli u primjeru~\ref{pr:kodkonst} --- samo umjesto konstante $\kins{\incr0\!}=6$ imamo konstantu $\kins{\incr{k+1}\!}=\f{codeINC}(k+1)=2\cdot3^{k+2}$ ($k$ je fiksan). Dakle, prvi kod je $\overline{\f G}(y)$, za $\f G:=\f C_{\f{codeINC}(k+1)}$.

Za donji dio, primijenimo algoritam iz definicije~\ref{def:flat}. Kako je jedini makro zadnja instrukcija u $Q$, ne treba provoditi korak~\eqref{korak:renumeriraj}, već samo korake~\eqref{korak:makni} i~\eqref{korak:dodaj}. Drugim riječima, umjesto jedne instrukcije $y.\:P^*$ treba stajati $n_P$ instrukcij\=a samog programa $P$ --- s rednim brojevima i odredištima pomaknutima za $y$. Za redne brojeve pobrinut će se konkatenacija jer je $\f{lh}\bigl(\overline{\f G}(y)\bigr)=y$; trebamo još pomaknuti odredišta.

Kod dokazivanja primitivne rekurzivnosti konkatenacije (lema~\ref{lm:starprn}) vidjeli smo ideju "točkovne definicije konačnog niza"% --- zato je dovoljno objasniti kako pomaknuti odredište pojedine instrukcije
: drugi kod će biti $\overline{\f H}\bigl(y,e,\f{lh}(e)\bigr)$, gdje je $\f H(y,e,t):=\f{Shift}(y,e[t])$, tako da još trebamo definirati funkciju $\f{Shift}$ koja pomiče odredište (ako postoji) instrukcije zadane kodom (drugi argument) za $y$ (prvi argument).

Koristeći komponente $\f{dest}$ i $\f{regn}$ te tipove instrukcija (leme~\ref{lm:regndestprn} i~\ref{lm:InsTYPEprn}), definiramo:
\begin{equation}
    \f{Shift}(y,i):=\begin{cases}
        %\f{codeINC}\bigl(\f{regn}(i)\bigr),
        %&\f{InsINC}(i)\\
        \f{codeDEC}\bigl(\f{regn}(i),\f{dest}(i)+y\bigr),&\f{InsDEC}(i)\\
        \f{codeGOTO}\bigl(\f{dest}(i)+y\bigr),&\f{InsGOTO}(i)\\
        i,&\text{inače}
    \end{cases}\text.
\end{equation}
	Radi totalnosti, trebamo nekako definirati $\f{Shift}$ i kad drugi argument nije u $\f{Ins}$, ali jer ćemo je pozivati samo na $e[t]$ za $e\in\f{Prog}$ i $t<\f{lh}(e)$, zapravo je nebitno kako tamo djeluje --- stavit ćemo taj slučaj zajedno sa slučajem instrukcije tipa $\inc$, koju $\f{Shift}$ mora ostaviti na miru. Tada je $\f{Shift}$ primitivno rekurzivna po teoremu~\ref{tm:grek}, pa je takva i $\f H^3=\f{Shift}\circ\bigl(\f I_1^3,\f{part}\circ(\f I_2^3,\f I_3^3)\bigr)$. $\f G$ je primitivno rekurzivna po propoziciji~\ref{prop:konst}, pa su njihove povijesti $\overline{\f G}$ i $\overline{\f H}$ primitivno rekurzivne po lemi~\ref{lm:povijestrek}. Sada prema lemi~\ref{lm:starprn} % i teoremu~\ref{tm:grek} napokon
 možemo utvrditi primitivnu rekurzivnost funkcije
\begin{equation}
    \f F(y,e):=\kprog{Q^\flat}=\overline{\f G}(y)*\overline{\f H}\bigl(y,e,\f{lh}(e)\bigr)
	\in\f{Prog} \text{ (zbog $Q^\flat\in\mathscr Prog$).}
\end{equation}
Još treba vidjeti da $k$-mjesna funkcija s tim indeksom zadovoljava jednadžbu~\eqref{eq:Sfunceq}, što možemo praćenjem po koracima: gornja razina makro programa~\eqref{eq:makroprogS} je sasvim sekvencijalna. Dakle, za sve $\vec x\in\N^k$ imamo
	\vspace{-1em}
\begin{equation}
    \begin{array}{r@{\;}l|cr@{,\dotsc,\,}lcc|cc}
%\SwapAboveDisplaySkip
        & & \reg0 & \reg1 & \reg k & \reg{k+1} & \reg{k+2}.. & \textsc{pc} & \textsc{ac}\\
        & & 0 & x_1 & x_k & 0 & 0 & 0 & 0\\\hline
        0.&\incr{k+1}& 0 & x_1 & x_k & 1 & 0 & 1 & 0\\
        1.&\incr{k+1}& 0 & x_1 & x_k & 2 & 0 & 2 & 0\\
        &\vdots &0&x_1&x_k&\vdots&0&\vdots & 0\\
        (y-1).&\incr{k+1}& 0 & x_1 & x_k & y & 0 & y & 0\\\hline
        y.&P^* &\kf e(\vec x,y) & ? & ? & ? & ? & y+1=n_Q & 0
    \end{array}\text,
\end{equation}
pa je izlazni podatak doista $\kf e^{k+1}(\vec x,y)\simeq\f{comp}_{k+1}(\vec x,y,e)$ --- ako $P$-iz\-ra\-ču\-na\-va\-nje s $(\vec x,y)$ uopće stane. Ako ne stane, onda ne stane ni $Q$-izračunavanje s $\vec x$, jer zapne na donjoj razini izvršavajući zadnju makro-instrukciju.

	Još smo ostali dužni riješiti slučaj kad ne postoji program $P$, jer $e\nin\f{Prog}$. Prema propoziciji~\ref{prop:computeind}\eqref{it:nprogind} je tada $f:=\kf e^{k+1}=\varnothing^{k+1}$, pa je i $\$(y,f)$ prazna --- formula~\eqref{eq:domkomp} kaže da funkcija~\eqref{eq:paramcompose} ima praznu domenu. Za povratnu vrijednost $\f S_k^2$ nam treba kod nekog RAM-programa koji računa $\varnothing^k$ --- uzmimo $\kprog{\begin{prog}0.&\goto\;0\end{prog}}=\kr{\f{codeGOTO(0)}}=2^{25}=33\,554\,432$. Dakle,
\begin{equation}\label{eq:Skprn}
   \f S_k(y,e):=\begin{cases}
       \f F(y,e),&\f{Prog}(e)\\
        33\,554\,432,&\text{inače}
    \end{cases}\text,
\end{equation}
    što je primitivno rekurzivno po teoremu~\ref{tm:grek}.
\end{proof}

\subsection{Teorem o parametrima}

Jednom kad imamo teorem o parametru, njegovom ponovljenom primjenom možemo specijalizirati i više zadnjih argumenata izračunljive funkcije odjednom. Primjer, ujedno i ideju dokaza, vidjeli smo u~\eqref{eq:multpar}.

\begin{korolar}[{name=[teorem o parametrima]}]\label{kor:pars}
Za sve $k,l\in\N_+$ postoji primitivno rekurzivna funkcija $\f S_k^{l+1}$\\ takva da za sve $\vec x\in\N^k$, za sve $\vec y\in\N^l$, i za sve $e\in\N$, vrijedi
\begin{equation}\label{eq:Sklspec}
    \f{comp}_k\bigl(\vec x,\f S_k(\vec y,e)\bigr)\simeq\f{comp}_{k+l}(\vec x,\vec y,e)\text.
\end{equation}
\end{korolar}
\begin{proof}
    Fiksirajmo $k$, i dokažimo (za taj $k$) tvrdnju indukcijom po $l$. 

	Kako je $l\in\N_+$, baza je $l=1$, i $\f S_k^{1+1}\!=\f S_k^2$ je primitivno rekurzivna po propoziciji~\ref{pp:tmpar}.

	Pretpostavimo sad da za neki $l$ postoji primitivno rekurzivna funkcija $\f S_k^{l+1}$ sa svojstvom~\eqref{eq:Sklspec}. Kako definirati $\f S_k^{l+2}\mspace{1mu}$? Uzmemo proizvoljni $(\vec y,z)\in\N^{l+1}$ i računamo:
\begin{equation}
    \f{comp}_{k+l+1}(\vec x,\vec y,z,e)\simeq
    \f{comp}_{k+l}\bigl(\vec x,\vec y,\f S_{k+l}(z,e)\bigr)\simeq
    \f{comp}_k\bigl(\vec x,\f S_k\bigl(
    \vec y,\f S_{k+l}(z,e)
    \bigr)\bigr)
\end{equation}
--- iz čega slijedi da je najprirodnije definirati
\begin{equation}
    \f S_k^{l+2}(\vec y,z,e):=\f S_k^{l+1}\bigl(\vec y,\f S_{k+l}^2(z,e)\bigr)\text.
\end{equation}
    Dakle, $\f S_k^{l+2}$ je definirana kompozicijom iz $\f S_k^{l+1}$ (primitivno rekurzivne po pretpostavci indukcije), $\f S_{k+l}^2$ (primitivno rekurzivne po propoziciji~\ref{pp:tmpar}) i koordinatnih projekcija (primitivno rekurzivnih jer su inicijalne), pa je i sama primitivno rekurzivna. Time smo proveli korak indukcije, odnosno za sve pozitivne $k$ i $l$ smo definirali funkciju $\f S_k^{l+1}$ i dokazali da je primitivno rekurzivna.
\end{proof}

\begin{primjer}[{name=[specijalizacija zadnja tri od sedam argumenata]}]
	Supskript funkcije $\f S$ govori koliko argumenata naše funkcije $\kf e$ će "preživjeti" specijalizaciju, a prethodnik mjesnosti od $\f S$ kaže koliko ih želimo fiksirati (i moramo navesti njihove vrijednosti prije $e$ u pozivu $\f S$). Recimo, u slučaju da funkciji $\kf{e_1}^7$ želimo fiksirati zadnja tri argumenta redom na brojeve $2$, $8$ i $5$, imali bismo
$
    e_2:=\f S_4^4(2,8,5,e_1)=\f S_4^2\bigl(2,\f S_5^2\bigl(8,\f S_6^2(5,e_1)\bigr)\bigr)
$, i za sve $x,y,z,t\in\N$ bi vrijedilo
	$\kf{e_2}(x,y,z,t)\simeq\kf{e_1}(x,y,z,t,2,8,5)$ --- odnosno $\kf{e_2}^4=\$(2,8,5,\kf{e_1}^7)$.
\end{primjer}

% \subsection{Primjena na elementarne operacije s funkcijama}

Sada možemo i vidjeti da je $\N compose$, barem za fiksne mjesnosti $k$ i $l$, primitivno rekurzivna. Tehnika koju ćemo pritom koristiti može se općenito primijeniti na razne funkcije višeg reda, definirane na funkcijama koje primaju preko indeksa.

Naglasimo da ovdje \emph{ne} govorimo o primitivnoj rekurzivnosti kompozicije (rezultata komponiranja) niti o primitivnoj rekurzivnosti funkcija koje ulaze u kompoziciju. Radi ilustracije uzmimo $k=l=1$: tada nas ne zanima jesu li $\f G$ i $\f H$ (pa time i $\f F:=\f G\circ\f H$) primitivno rekurzivne. Zanima nas da su \emph{parcijalno} rekurzivne, odnosno da imaju indekse (redom ih označimo s $g$, $h$ i $f$). Govorimo o primitivnoj rekurzivnosti funkcije $\f{compose}_1^2$ koja prima $g$ i $h$ te vraća $f$ --- pogledajte primjer~\ref{pr:parcspecind} za detalje.

Ugrubo, \emph{kompilirati} kompoziciju dvije funkcije koje već imamo kompilirane, je daleko "pitomije" nego \emph{izvršiti} (evaluirati) tu kompoziciju. Izvršavanje ne mora stati ako te funkcije nisu totalne --- dok s\=amo kompiliranje kompozicije mora stati.

\begin{propozicija}[{name=[primitivna rekurzivnost komponiranja]}]\label{pp:composeprn}
    Za sve $k,l\in\N_+$ postoji primitivno rekurzivna funkcija $\f{compose}_k^{l+1}$\!, takva da za sve $g_1,g_2,\dotsc,g_l,h\in\N$ vrijedi
    \begin{equation}
        \kf{\f{compose}_k(g_1,\dotsc,g_l,h)}^k=\kf h^l\circ(\kf{g_1}^k,\dotsc,\kf{g_l}^k)\text.
    \end{equation}
\end{propozicija}
\begin{proof}
Programirat ćemo postupak računanja kompozicije u proizvoljnom $\vec x\in\N^k$, ali ga nećemo pokrenuti --- nego ćemo iz njegova indeksa specijalizacijom dobiti indeks same kompozicije.

    Dakle, fiksirajmo pozitivne $k$ i $l$ te definirajmo funkciju $\f F^{k+l+1}$ točkovno s
\begin{equation}\label{eq:defkompcomp}
    \f F(\vec x^k,\vec g^l,h):\simeq
    \f{comp}_l\bigl(
    \f{comp}_k(\vec x,g_1),
    \dotsc,
    \f{comp}_k(\vec x,g_l),
    h\bigr)\text.
\end{equation}
Funkcija $\f F$ je definirana kompozicijom iz parcijalno rekurzivnih funkcija $\f{comp}_k$ i $\f{comp}_l$ te koordinatnih projekcija --- pa je parcijalno rekurzivna. Po korolaru~\ref{kor:pii}, $\f F$ ima indeks; označimo jedan njen indeks s $e$ (sjetite se napomene~\ref{nap:>1ind'}).

    Funkcija $\f{compose}_k^{l+1}$ prima $\f g_1$,~\ldots, $\f g_l$ i $\f h$ te na njih fiksira zadnjih $l+1$ argumenata od $\f F$:
\begin{equation}
    \f{compose}_k^{l+1}(\vec g,h):=\f S_k^{l+2}(\vec g,h,e)\text.
\end{equation}

    Dakle, $\f{compose}_k^{l+1}=\$(e,\f S_k^{l+2})$, pa je primitivno rekurzivna po korolaru~\ref{kor:paramprn}. Sada za sve $\vec x\in\N^k$, za sve $\vec g\in\N^l$ i za sve $h\in\N$ vrijedi
\begin{multline}
    \kf{\f{compose}_k^{l+1}(\vec g,h)}(\vec x)\simeq
    \f{comp}_k\bigl(\vec x,\f{compose}_k(\vec g,h)\bigr)\simeq
    \f{comp}_k\bigl(\vec x,\f S_k^{l+2}(\vec g,h,e)\bigr)
    \simeq{}\\{}\simeq
    \f{comp}_{k+l+1}(\vec x,\vec g,h,e)\simeq
    \kf e^{k+l+1}(\vec x,\vec g,h)\simeq\f F(\vec x,\vec g,h)\simeq{}\\
    {}\simeq\f{comp}_l\bigl(
    \f{comp}_k(\vec x,g_1),
    \dotsc,
    \f{comp}_k(\vec x,g_l),
    h\bigr)\simeq\f{comp}_l\bigl(
    \kf{g_1}(\vec x),
    \dotsc,
    \kf{g_l}(\vec x),
    h\bigr)\simeq{}\\
    {}\simeq\kf h\bigl(
    \kf{g_1}(\vec x),
    \dotsc,
    \kf{g_l}(\vec x)\bigr)\simeq\bigl(\kf h^l\circ(\kf{g_1}^k,\dotsc,\kf{g_l}^k)\bigr)(\vec x)\text,
\end{multline}
što smo trebali dokazati.
\end{proof}

Često se tehnika koju smo upravo koristili ne mora ponovo provoditi, već se rezultat može dobiti primjenom funkcije $\f{compose}_k^{l+1}$ (za neke $k$ i $l$).

\begin{korolar}[{name=[primitivna rekurzivnost zbrajanja funkcija]}]
Za svaki $k\in\N_+$ postoji primitivno rekurzivna funkcija $\f{plus}_k$\\ takva da je za sve $e,f\in\N$, $\f{plus}_k(e,f)$ indeks zbroja funkcija $\kf e^k+\,\kf f^k$.
\end{korolar}
\begin{proof}
	Kako je $F+G$ samo skraćeni zapis za $\f{add}^2\circ(F,G)$, sve što nam treba je odgovarajuća funkcija $\f{compose}$ i neki indeks za $\f{add}^2$. Nije problem, istom tehnikom kao za~\eqref{eq:add3}, napisati RAM-program za $\f{add}^2$,
\begin{equation}
    P_{\f{add}^2}:=\begin{prog}
    0.&\decr13\\
    1.&\incr0\\
    2.&\goto\;0\\
    3.&\decr26\\
    4.&\incr0\\
    5.&\goto\;3
    \end{prog}\text,
\end{equation}
kao niti izračunati njegov kod
\begin{equation*}
	a:=\kr{\kr{1,1,3},\kr{0,0},\kr{2,0},\kr{1,2,6},\kr{0,0},\kr{2,3}}=2^{22\,501}\cdot3^7\cdot5^{25}\cdot7^{\mspace{1mu}8\,437\,501}\cdot11^7\cdot13^{649}\text.
\end{equation*}
    %oveći broj (ima $7\,138\,041$ znamenku), ali ipak sasvim točno određen.
    Sada je $\f{plus}_k(e,f):=\f{compose}_k(e,f,a)$, odnosno $\f{plus}_k^2=\$(a,\f{compose}_k^3)$ je primitivno rekurzivna po korolaru~\ref{kor:paramprn}.
\end{proof}

% \subsection{Što s ostalim elementarnim operacijama?}

Kad smo uspjeli isprogramirati pisanje programa za kompoziciju, zašto ne bismo istu stvar pokušali i za primitivnu rekurziju, ili minimizaciju? Na prvi pogled, sve što nam treba je točkovni zapis izračunavanja pomoću funkcija $\f{comp}$ (odgovarajuće mjesnosti), koji onda predstavlja parcijalno rekurzivnu funkciju, čiji indeks uzmemo i specijaliziramo ga s obzirom na indekse polaznih funkcija. Što može poći po zlu? %Pogledajmo.

Pokušajmo što vjernije slijediti postupak koji nas je doveo do funkcije $\f{compose}_k^{l+1}$, za primitivnu rekurziju. Zanemarimo degenerirani slučaj --- lako možete vidjeti da se u njemu pojavljuje sasvim isti problem.

Dakle, umjesto zadanih mjesnosti $k$ i $l$, ovdje imamo samo zadanu mjesnost $k$. Umjesto $l+1$ polaznih funkcija, ovdje imamo $2$ polazne funkcije, $\f G$ i $\f H$ (još moraju biti totalne, ali to ćemo shvatiti kao parcijalnu specifikaciju --- ako ulazni podaci nisu indeksi totalnih funkcija, rezultat može biti bilo što). Želimo primitivno rekurzivnu funkciju $primRecurse_k$, takvu da za sve indekse totalnih funkcija $g,h\in\N$ vrijedi
\begin{equation}
    \kf{primRecurse_k(g,h)}^{k+1}=\kf g^k\pr\kf h^{k+2}\text.
\end{equation}

Za $\f{compose}$ smo uzeli parcijalnu jednakost~\eqref{eq:defkomp}, i zapisali je pomoću univerzalnih funkcija kao~\eqref{eq:defkompcomp}. Ako to učinimo s definicijom~\ref{def:pr}, dobit ćemo nešto poput
\begin{equation}\label{eq:primRecursegr}
    F_k(\vec x,y,g,h)\simeq\begin{cases}
        \f{comp}_k(\vec x,g),&y=0\\
        \f{comp}_{k+2}\bigl(\vec x,\f{pd}(y),\f{comp}_{k+1}\bigl(\vec x,\f{pd}(y),f\bigr),h\bigr),&\text{inače}
    \end{cases}\text,
\end{equation}
i sad bismo mogli upotrijebiti teorem~\ref{tm:gprek}, da nije jednog malog problema: jednadžba~\eqref{eq:defprk} ima traženu funkciju i s lijeve i s desne strane. Ovaj $f$ koji se nalazi u grani "inače", to je upravo $primRecurse_k(g,h)$ koji želimo odrediti. Dakle, nemamo ga još, pa ga ne možemo koristiti u definiciji od $F_k$.

Ili možemo? Sjetimo se napomene~\ref{nap:blokovi} --- $f$ je upravo "implicitna varijabla" kakve smo rekli da trebamo prenijeti kao argumente. Dakle, na lijevoj strani~\eqref{eq:primRecursegr} zapravo imamo $F_k(\vec x,y,g,h,f)$ --- i po teoremu~\ref{tm:gprek} to je parcijalno rekurzivna funkcija pa ima indeks~\ldots\ i tako dalje. No sad bismo u $F_k^{k+4}$ trebali fiksirati $f$, a to ne znamo kako učiniti jer još uvijek ne znamo koju vrijednost staviti za $f$.

Kad bismo samo znali odrediti $f$, dalje bi bilo lako: $g$ i $h$ bismo specijalizirali na isti način kao kod komponiranja. Sigurno $f$ ne možemo odrediti jednoznačno, naprosto jer nije jedinstven: $\f G\pr\f H$, kao i bilo koja izračunljiva funkcija, ima beskonačno mnogo indeksa --- a svi oni mogu poslužiti kao $f$. No ono što nam može biti bitno je da \emph{funkcija} $\kf f^{k+1}=\kf g^k\pr\kf h^{k+2}$ bude jednoznačno određena.

Zanemarujući $g$ i $h$ (jer njih znamo specijalizirati) i "utapajući" $y$ među $\vec x$ te zovući tako dobivenu funkciju $G_k$, vidimo da je općeniti oblik jednadžbe koju želimo riješiti $\kf f(\vec x)\simeq G_k(\vec x,f)$. Takve \emph{opće rekurzije} tema su iduće točke.

\section{Opće rekurzije}\label{sec:rec}

Vidjeli smo da se u metaprogramiranju, a ponekad i u običnom programiranju, pojavljuje potreba za funkcijama čija simbolička definicija koristi njih same. Recimo, definicija funkcije $\f{factorial}$ koju bismo mogli napisati u programskom jeziku C (zanemarujući iz didaktičkih razloga da za faktorijel postoje jednostavnije implementacije i u jeziku C i u jeziku primitivno rekurzivnih funkcija --- primjer~\ref{pr:factorialprn}),
\begin{equation}
    \begin{minipage}{0.8\textwidth}
\begin{verbatim}
                unsigned factorial(unsigned n)
                    { return n ? n*factorial(n-1) : 1; }
\end{verbatim}
\end{minipage}
\end{equation}
može se točkovno zapisati kao
\begin{equation}\label{eq:factorialrek}
    \f{factorial}(n)=\begin{cases}
        n\cdot\f{factorial}\bigl(\f{pd}(n)\bigr),&n>0\\
        1,&\text{inače}
    \end{cases}
\end{equation}
ili simbolički, kao $\f{factorial}=\IF{\N_+:\f{mul}^2\circ(\f I_1^1,\f{factorial}\circ\f{pd}),\f{Sc}\circ\f Z}$.

Tu jednakost nema smisla zvati \emph{definicijom} od $\f{factorial}$, jer je cirkularna --- ali ona može poslužiti kao funkcijska \emph{jednadžba} koju trebamo riješiti po "nepoznanici" $\f{factorial}$. Osnovna prednost definicija pred jednadžbama sastoji se u tome da (dobra) definicija uvijek jednoznačno određuje definirani objekt, dok jednadžba ne mora imati rješenje, ili ih može imati više.

Još jedan detalj treba uzeti u obzir: u~\eqref{eq:factorialrek} smo koristili znak jednakosti jer otprije znamo da je faktorijel totalna funkcija --- ali opće rekurzije koje koriste samo totalne funkcije mogu kao rješenja imati parcijalne funkcije koje nisu totalne. Recimo,
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
                unsigned h(unsigned n){
                    if(n==0) return 0;
                    else if(n==1) return h(n)+1;
                    else return h(n-2)+1;
                }
\end{verbatim}
\end{minipage}\end{equation}
--- ovakva $\f h$ je definirana samo na parnim  brojevima, i svaki preslikava u njegovu polovinu (usporedite s jezičnom funkcijom $\varphi_h$ iz primjera~\ref{pr:pola}). Ovdje smo za $n=1$ koristili kompoziciju sa sljedbenikom da forsiramo parcijalnost (kao kod Russellove funkcije), ali i da nismo napisali taj \texttt{+1} u slučaju $n=1$, C bi svejedno računao istu parcijalnu funkciju. Ipak, odgovarajuća točkovna funkcijska jednadžba
\vspace{-1em}
\begin{equation}\label{eq:halfmany}
    \f h(n)\simeq\begin{cases}
        0,&n=0\\
        \f h(n),&n=1\\
        \f h(n\dotminus2)+1,&\text{inače}
    \end{cases}
\end{equation}
bi pored tog rješenja (nazovimo ga $\f h_0$) imala i razna druga, čak totalna rješenja. Jedno od njih je
$
    \f h_{42}(n):=\begin{smallcases}
        \f h_0(n),&2\,\mid\,n\\
        42\,+\,\f h_0(n-1),&\text{inače}
    \end{smallcases}
$ --- provjerite!

To samo znači ono što već znamo, da trebamo biti mnogo oprezniji s parcijalnim funkcijama nego s totalnima, pa će nam od posebnog značaja biti one opće rekurzije koje definiraju (isključivo) totalne funkcije.

Dakle, neformalno, \emph{opća rekurzija} je funkcijska jednadžba $F=\mathcal M(\vec G,F)$, kojoj s desne strane stoji neka simbolička definicija koja pored nekih već poznatih funkcija $G_1$, $G_2$,~\ldots\ koristi i funkciju $F$. Kao i obično, konkretnu funkciju $F$ koja zadovoljava tu funkcijsku jednadžbu zovemo \emph{rješenjem} te jednadžbe. Za konkretnu opću rekurziju, zanimat će nas tri pitanja:
\begin{quote}
\begin{labeling}{(Jedinstvenost)}
    \item[(Egzistencija)] Ima li uopće rješenje?
    \item[(Jedinstvenost)] Ako ima, je li jedinstveno?
    \item[(Totalnost)] Ako jest, je li totalno?
\end{labeling}
\end{quote}
Pitanja moramo postavljati tim redom, jer npr.\ totalnost rješenja ne znači mnogo ako ono nije jedinstveno. Recimo, vidjeli smo jednadžbu~\eqref{eq:halfmany} koja ima totalno rješenje $\f h_{42}$, ali svejedno nijedan programski jezik ne bi pronašao to rješenje, već bi računao netotalnu funkciju $\f h_0$.

% \subsection{Opće rekurzije s izračunljivim funkcijama}

Kao i drugdje gdje promatramo funkcijske jednadžbe (recimo, u teoriji običnih diferencijalnih jednadžbi), rijetko se bavimo sasvim općenitim funkcijama. Kod diferencijalnih jednadžbi najčešće nas zanimaju \emph{glatke} funkcije --- ovdje, kod općih rekurzija, zanimaju nas \emph{izračunljive} funkcije. Zbog teorema ekvivalencije, svejedno je kako manifestiramo tu izračunljivost --- uglavnom ćemo to činiti kroz parcijalnu rekurzivnost ili kroz postojanje indeksa.

Dakle, zadane su nam parcijalno rekurzivne funkcije $\f G_1$, $\f G_2$,~\ldots\ preko svojih indeksa $g_1$, $g_2$,~\ldots\ --- i tražimo indeks $f$ funkcije $\f F$ koja zadovoljava opću rekurziju $\f F=\mathcal M(\vec{\f G},\f F)$. Simboličku definiciju $\mathcal M$ je (kao i obično) lakše napisati točkovno: u obliku jedne parcijalno rekurzivne funkcije $\f G$ koja prima ulazne podatke $\vec x$, indekse $\vec g$ i indeks $f$; te vraća vrijednost koja mora biti parcijalno jednaka $\f F(\vec x)\simeq\kf f(\vec x)\simeq\f{comp}(\vec x,f)$.

No ako već pišemo točkovnu definiciju, indeksi $\vec g$ nam ne trebaju --- s obzirom na to da su $\f G_i$ poznate funkcije, možemo ih uklopiti u definiciju funkcije $\f G$. Jedina funkcija s kojom to ne možemo učiniti (jer još nije poznata) je funkcija $\f F$, tako da njen indeks moramo prenijeti kao dodatni argument funkciji $\f G$. Kad $\f G$ želi pozvati $\f F$, na nekim argumentima $\vec y$ (koji će najčešće biti na neki način "manji" od $\vec x$), koristit će izraz $\f{comp}_k(\vec y,f)$.

(Moguće su i "simultane opće rekurzije", gdje imamo \emph{više} nepoznatih funkcija koje sve ovise međusobno na opće-rekurzivan način --- no to se može riješiti metodama koje smo već upoznali u dokazu propozicije~\ref{prop:simultrek}.)

% To motivira sljedeću definiciju.

\begin{definicija}[{name=[opća rekurzija i njeno rješenje]}]
Neka je $k\in\N_+$ te $\f G^{k+1}$ parcijalno rekurzivna funkcija. \emph{Opća rekurzija} je jednadžba (po $e$)
\begin{equation}\label{eq:genrek}
    \f{comp}_k(\vec x,e)\simeq\f G(\vec x,e)\text{, za sve }\vec x\in\N^k\text.
\end{equation}
	Ako konkretni broj $e_0\in\N$ zadovoljava tu jednadžbu, funkciju $\kf{e_0}^k=\$(e_0,\f G)$ zovemo \emph{rješenjem} opće rekurzije.
\end{definicija}

Ponekad i indeks $e_0$ neformalno zovemo "rješenjem", ali jedinstvenošću uvijek smatramo jedinstvenost \emph{funkcije}, ne indeksa. To je bitno jer inače u uobičajenim situacijama (kad $\f G$ koristi argument $e$ samo za pozivanje funkcije $\f F$) \emph{nikad} ne bismo imali jedinstvenost: čim postoji neki $e_0$, svi ostali indeksi funkcije $\kf{e_0}^k$ su također "rješenja", a intuitivno znamo (i~dokazat ćemo u ovom poglavlju) da ih ima beskonačno mnogo.

Pitanje totalnosti tada postaje pitanje \emph{rekurzivnosti} --- jer $\f F$ ima indeks $e_0$, po teoremu ekvivalencije je parcijalno rekurzivna, a takve totalne funkcije zovemo rekurzivnima.

U prethodna dva odlomka, čini se, zanemarili smo pitanje egzistencije, odnosno ponašali smo se kao da indeks $e_0$ koji zadovoljava~\eqref{eq:genrek} uvijek postoji. Važan i netrivijalan \emph{teorem rekurzije} kaže da to doista vrijedi.

Naravno, netrivijalan je samo u formalnom smislu: intuitivno objašnjenje kako izvršavati opću rekurzivnu funkciju (za zadanu funkciju $\f G$) po Church--\!Turingovoj tezi računa parcijalno rekurzivnu funkciju. Ipak, takva intuicija nas može zavarati (prisjetite se funkcije~$\f h_{42}$), a i tvrdnje o jedinstvenosti i rekurzivnosti lakše je dokazivati (najčešće matematičkom indukcijom) jednom kad imamo indeks, nego kad imamo neformalni postupak. Zato je dobro izbjeći Church--\!Turingovu tezu, i doista konstruirati indeks $e_0$ s traženim svojstvom.

\subsection{Teorem rekurzije}

Najvažnije svojstvo funkcije $\f F=\kf e^k$ je da mora "znati svoj indeks", odnosno pozvana s argumentima $\vec x$, mora se ponašati kao funkcija $\f G$ pozvana s $\vec x$ i još indeksom $e$. Drugim riječima, želimo $\kf e^k=\$(e,G)$.

Recimo, u slučaju funkcije \texttt{factorial}, kompajler se pobrine za to da poziv te funkcije u njenom kodu doista pozove nju samu (sa za $1$ manjim argumentom), ali da kojim slučajem kompajler ne podržava rekurziju, mogli bismo (pokazivač na) funkciju \texttt{factorial} prenijeti u samu sebe kao dodatni parametar.

(Naravno, u ovom slučaju to uopće ne rješava problem, jer moramo \emph{imati} funkciju \texttt{factorial} koju ćemo poslati kao argument, ali zasad govorimo samo o specifikaciji.)

\noindent\begin{equation}\label{eq:wishful}
    \begin{minipage}{0.8\textwidth}
\begin{verbatim}
            typedef unsigned funkcija(unsigned n);
            unsigned G(unsigned n, funkcija f)
                { return n ? n*f(n-1) : 1; }
            /* ... nekako definiramo factorial */
            int main(void)
                { return G(5, factorial); } /* ovo vrati 120 */
\end{verbatim}
    \end{minipage}
\end{equation}

Matematički, "pokazivač na funkciju" je njen indeks, što motivira sljedeću definiciju.

\begin{definicija}[{name=[dijagonala parcijalno rekurzivne funkcije]}]
    Neka je $k\in\N_+$ te $\f H^{k+1}$ parcijalno rekurzivna funkcija.
	\emph{Dijagonala} funkcije $\f H$ je $k$-mjesna funkcija $\partial\f H:=\$(h,\f H)$, gdje je $h$ jedan (fiksni) indeks funkcije $\f H$.
\end{definicija}

Kako funkcija može imati više indeksa, može imati i više dijagonal\=a --- odnosno, formalno bismo dijagonalu trebali definirati za \emph{indeks}, a ne za funkciju. No nama će prvenstveno biti bitna prateća funkcija $\f D=\N \partial$, koja je ionako definirana na indeksima.

U "stvarnom životu" nemamo tih problema, jer je praktički jedino što ikad radimo s pokazivačem na funkciju, funkcijski poziv\!. Standard jezika C ne dopušta nikakvu aritmetiku s funkcijskim pokazivačima, ali je neki kompajleri ipak podržavaju. Slično, ovdje bismo mogli $h$ iskoristiti ne samo kao zadnji argument funkcije $\f{comp}_k$, nego raditi razne čudne stvari poput gledanja počinje li "strojni kod" funkcije $\f H$ instrukcijom \inc\ ($\f{InsINC}(h[0])$), i sličnog --- ali najčešće to ne činimo, a dok god $h$ koristimo samo za pozivanje funkcije $\f H$, svejedno je koji njen indeks smo uzeli.

\begin{lema}[{name=[primitivna rekurzivnost dijagonalne funkcije]}]
	Za svaki $k\in\N_+$ postoji primitivno rekurzivna funkcija $\f D_k$ s kodomenom $\f{Prog}$,\\ koja preslikava indeks $h$ funkcije $\f H^{k+1}$ u indeks njene dijagonale $\partial\f H=\$(h,H)$.
\end{lema}
\begin{proof}
	Teorem o parametru kaže da se indeks $\f D_k(h)$ za $\partial\f H=\$(h,\kf h^{k+1}\mspace{-2mu})$ može dobiti kao $\f S_k(h,h)\in\f{Prog}$. Drugim riječima, možemo definirati $\f D_k:=\f S_k^2\circ(\f I_1^1,\f I_1^1)$, što je primitivno rekurzivna funkcija kao kompozicija primitivno rekurzivnih.
\end{proof}

% \subsection{Dokaz teorema rekurzije}

Dijagonaliziranje funkcije, kao što smo vidjeli, još uvijek nije dovoljno da bismo doista dobili rješenje opće rekurzije. U programu~\eqref{eq:wishful} svejedno smo trebali nekako drugačije dobiti \texttt{factorial} koju bismo poslali kao drugi argument funkciji~\texttt{G}. To se čini prilično beskorisnim (jer jednom kad imamo \texttt{factorial}, možemo je odmah pozvati bez petljanja s dijagonalom), ali zapravo je vrlo blizu rješenju.

Luda ideja: funkcije \texttt{factorial} i \texttt{G}, konceptualno gledano, služe istoj svrsi --- računanju faktorijele zadanog broja. Ako nemamo \texttt{factorial}, možemo li umjesto nje upotrijebiti \texttt{G} kao drugi argument od \texttt{G} (efektivno, računati $\partial\texttt G$)?

Doslovno, to neće ići --- tipovi ne pašu. Drugi argument funkcije \texttt{G} trebao bi biti pokazivač na jednomjesnu funkciju, a \texttt{G} je dvomjesna. C-kompajler će nam samo dati \emph{warning}, jer za njega su svi pokazivači ionako samo "ukrašeni prirodni brojevi" --- baš kao i indeksi u svijetu parcijalno rekurzivnih funkcija --- ali u strože tipiziranom jeziku kompajler bi nam odbio prevesti kod, uz poruku o grešci.

C je ovdje izuzetno zanimljiv\!, jer na mnogim kompajlerima, ako zanemarite \emph{warning}, zapravo ćete dobiti ispravno rješenje (provjereno radi na \texttt{gcc} 4.6.3 --- pokušajte na svom omiljenom kompajleru). Kako je to moguće?! Zna li \texttt{gcc} nešto što mi ne znamo?

Ovdje treba znati neke tehničke pojedinosti o kompiliranju jezika C. (Nešto smo već rekli kad smo govorili o funkcijskom makrou.) Kad pozovemo funkciju, njeni argumenti stavljaju se na stog (novi okvir) obrnutim redom, i nakon toga se prenosi kontrola na samu funkciju, koja očekuje argumente na stogu i tamo stavlja povratnu vrijednost. Ovdje smo pozvali funkciju \texttt{G} s dva argumenta: $5$ i \texttt{G}. Unutar koda funkcije \texttt{G}, pokazivač \texttt f pokazuje na funkciju \texttt{G}. Kad smo \texttt f pozvali s jednim argumentom (konkretno, $4$), broj $4$ je stavljen na stog, ali je ispod njega i dalje ostao pokazivač \texttt{G}, koji je funkcija \texttt f veselo koristila kao svoj drugi argument. Dakle, poziv \texttt{f(n-1)} je zapravo interpretiran kao \texttt{f(n-1,G)}. Umjesto broja $4$ jednom će (nakon još nekoliko takvih poziva) na tom mjestu na stogu završiti povratna vrijednost $24$, ali ništa neće dirati ovaj \texttt{G} ispod (cjelobrojno množenje i oduzimanje jednice se obavlja u registrima procesora, ne koristeći stog).

Na procesorima s velikim brojem registara, ponekad se argumenti u funkciju male mjesnosti ne prenose preko stoga nego preko registara --- ali slično razmišljanje funkcionira: poziv \texttt{f(n-1)} dekrementira registar u kojem se prenosi prvi argument, ali registar u kojem se prenosi drugi argument ostaje nepromijenjen, kao da smo pozvali \texttt{f(n-1,G)}.

Možemo li to iskoristiti da bismo eksplicitno napisali taj poziv u kodu, i izbjegli \emph{warning}? Da, jer C nam dopušta da ne specificiramo tipove parametara funkcije.
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
       typedef unsigned funkcija(/* prima bilo što */);
       unsigned G(unsigned n, funkcija f)
           { return n ? n * f(n-1, f) : 1; }
       int main(void)
           { return G(5, G); } /* vrati 120 bez warninga */
\end{verbatim}
\end{minipage}\end{equation}

Ali ako već želimo tako zaobilaziti statičke tipove, jednostavnije je prebaciti se na dinamički tipizirani jezik. U Pythonu, stvari rade točno kako smo zamislili.
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
            >>> def H(n, f): return n * f(n-1, f) if n else 1
            >>> H(7, H)
            5040
\end{verbatim}
\end{minipage}\end{equation}

Refaktorirajmo ovu duplikaciju koda za dijagonaliziranje, u definiciji i pozivu \texttt H:
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
            >>> def d(H):
            ...     def dH(x): return H(x, H)
            ...     return dH
            >>> def H(n, f): return n * d(f)(n-1) if n else 1
            >>> factorial = d(H)
            >>> factorial(7)
            5040
\end{verbatim}
\end{minipage}\end{equation}
Dobra strana toga je da više ne moramo ručno proizvoditi funkciju \texttt H iz funkcije \texttt G. Prethodno smo to napravili tako što smo, tamo gdje je \texttt G pozivala \texttt f, u funkciji \texttt H pozvali $\partial\texttt f$. Sada to možemo formalizirati, tako da definicija od \texttt H pozove \texttt G s $\partial\texttt f$ automatski.
\begin{equation}\label{eq:norec}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
            >>> def G(n, f): return n * f(n-1) if n else 1
            >>> def H(x, f): return G(x, d(f))
\end{verbatim}
\end{minipage}\end{equation}

I to je dokaz teorema rekurzije (za $k=1$)! Ako pažljivo pogledamo, vidjet ćemo da~\eqref{eq:norec} nigdje ne koristi rekurzivne pozive. Sad samo sve to treba napisati matematički.

\begin{teorem}[Teorem rekurzije]\label{tm:rek}
	Neka je $k\in\N_+$ te $\f G^{k+1}$ parcijalno rekurzivna funkcija. \\ Tada postoji $e\in\f{Prog}$ takav da za sve $\vec x\in\N^k$ vrijedi $\kf e^k(\vec x)\simeq\f G(\vec x,e)$.
\end{teorem}
\begin{proof}
	Definiramo funkciju $\f H^{k+1}\mspace{-2mu}$ točkovno s $\f H(\vec x,f):\simeq\f G\bigl(\vec x,\f D_k(f)\bigr)$. Ta funkcija je parcijalno rekurzivna (dobivena je kompozicijom iz $\f G$, $\f D_k$ i koordinatnih projekcija) pa ima indeks: označimo jedan od njih s $h$ (sjetite se napomene~\ref{nap:>1ind'}).

	Tvrdimo da je $\partial\f H$ rješenje opće rekurzije, odnosno njen indeks $e:=\f D_k(h)\in\f{Prog}$ je traženi broj. Doista, za sve $\vec x\in\N^k$ imamo
\begin{equation}
    \kf e(\vec x)\simeq
    \partial\f H(\vec x)\simeq
    \f H(\vec x,h)\simeq
    \f G\bigl(\vec x,\f D_k(h)\bigr)\simeq
    \f G(\vec x,e)\text,
\end{equation}
    odnosno $\kf e^k=\$(e,\f G)$, što smo trebali dokazati.
\end{proof}

\subsection{Ackermannova funkcija}

Sada ćemo vidjeti kako pomoću teorema rekurzije možemo definirati rekurzivne funkcije. Metoda je uvijek ista: funkcijsku jednadžbu koju želimo riješiti (po $F^k$) zapišemo u obliku opće rekurzije (nađemo funkciju $\f G^{k+1}$) te nam teorem rekurzije dade parcijalno rekurzivno rješenje --- štoviše, dade nam njegov indeks $e_0$. Sada je potrebno dokazati dvije stvari (ako vrijede): prvo, da je $\f F_0:=\kf{e_0}^k$ jedinstveno rješenje, i drugo, da je $\f F_0$ totalna funkcija.

I jedno i drugo su univerzalne tvrdnje na prirodnim brojevima --- jedinstvenost kaže da, kad god je $e_1$ "rješenje", za sve $\vec x\in\N^k$ vrijedi $\f{comp}(\vec x,e_1\!)\simeq\f F_0(\vec x)$; totalnost kaže da za sve $\vec x\in\N^k$ vrijedi $\vec x\in\dom{\f F_0}$ --- te ih je uobičajeno dokazivati indukcijom. Didaktički problem je u tome što ako je ta indukcija dovoljno jednostavna, najčešće je programabilna, pa primjerice totalnost ne znači samo rekurzivnost već znači primitivnu rekurzivnost. A tada nam ne treba teorem rekurzije: primitivna rekurzija je dovoljna (kao što je uostalom slučaj i s funkcijom $\f{factorial}$).

Recimo, ako se totalnost od $\f F_0^1$ može dokazati običnom matematičkom indukcijom, to znači da imamo neku ogradu za broj koraka računanja $\f F_0(0)$ te neki izračunljiv način da iz ograde za broj koraka u računanju $\f F_0(n)$ dobijemo takvu ogradu za $\f F_0(n+1)$ --- a to zapravo znači da $\f F_0$ možemo dobiti (degeneriranom) primitivnom rekurzijom, samo trebamo u funkciji $\f{step}$ ograničiti minimizaciju tom nađenom ogradom. Ako umjesto obične indukcije moramo upotrijebiti jaku indukciju, to na isti način znači da se $\f F_0$ može dobiti rekurzijom s poviješću. U slučaju simultane indukcije, imamo simultanu rekurziju, i tako dalje.

Vjerojatno najjednostavniji obrazac indukcije koji nije moguće "uloviti" u teoriji primitivno rekurzivnih funkcija je \emph{ugniježđena} indukcija po dvije varijable, gdje iz pretpostavke da tvrdnja vrijedi za neki $m$ i za \emph{sve} $n$, slijedi da vrijedi za $m+1$ i za sve $n$. Jedan od prvih primjera takve funkcije (čija totalnost zahtijeva takav indukcijski obrazac koji nije formalizabilan primitivnom rekurzijom) dao je Hilbertov asistent Wilhelm Friedrich Ackermann 1928.\ godine.

Ackermann je promatrao niz aritmetičkih operacija: sljedbenik, zbrajanje, množenje, potenciranje,~\ldots\ nekako je jasno da ga možemo i nastaviti na sličan način; sljedeći član --- tetracija --- je čak korisna operacija u nekim kombinatornim situacijama. Mala nepravilnost: sljedbenik je jednomjesna funkcija, a sve ostale su dvomjesne; zato stavimo $\f A_0^2:=\f{Sc}\circ \f I_2^2$. Ostale funkcije označimo na očiti način: $\f A_1^2:=\f{add}^2$, $\f A_2^2:=\f{mul}^2$, $\f A_3^2:=\f{pow}$, i tako dalje. Osnovna ideja --- svaka osim prve funkcije u tom nizu dobivena je iteracijom prethodne --- se može iskazati kao
\begin{equation}\label{eq:A2SSdef}
    \f A_{n+1}(x,y+1)=\f A_n\bigl(x,\f A_{n+1}(x,y)\bigr)\text{, za sve }x,y,n\in\N\text,
\end{equation}
što zapravo znači $\f A_{n+1}=\f G_{n+1}\pr\f A_n\circ(\f I_1^3,\f I_3^3)$; razlikuju se samo početni uvjeti zadani s $\f G_n:=\$(0,\f A_n)$. Prvih nekoliko je doista različito: $\f G_0(x)=\f{Sc}(0)=1$, $\f G_1(x)=x+0=x$, $\f G_2(x)=x\cdot 0=0$, $\f G_3(x)=x^0=1$ --- ali svi kasniji se obično fiksiraju na $1$.

Dakle, za sve $n>1$ vrijedi $\f A_{n+1}:=\f C_1^1\pr\f A_n\circ(\f I_1^3,\f I_3^3)$.

\begin{propozicija}[{name=[primitivna rekurzivnost generaliziranih aritmetičkih operacija]}]\label{pp:Anprn}
    Za svaki $n\in\N$, $\f A_n^2$ je primitivno rekurzivna.
\end{propozicija}
\begin{proof}
Običnom matematičkom indukcijom po $n$. Za $n=0$, to je kompozicija inicijalnih funkcija. Za $n\in\{1,2\}$ to smo već dokazali (primjer~\ref{pr:addmulpow}). Za $n\ge 2$, ako je $\f A_n$ primitivno rekurzivna, tada je $\f A_{n+1}=\f C_1^1\pr\f A_n\circ(\f I_1^3,\f I_3^3)$ simbolička definicija $\f A_{n+1}$, iz koje slijedi da je i ona primitivno rekurzivna.
\end{proof}

Primijetimo sličnost s dokazom propozicije~\ref{prop:konst}. No dok smo dinamizirani (zadan argumentom) broj iteracija operatora $\circ$ mogli shvatiti kao primitivnu rekurziju (primjer~\ref{pr:IdinC}), dinamizirani broj iteracija operatora $\pr$ više ne možemo tako shvatiti. Zato dinamizacija familije $\f A_n,n\in\N$ --- tromjesna funkcija zadana s
\begin{equation}
    \f A(x,y,z):=\f A_z(x,y)%\text,
\end{equation}
{} --- \emph{nije} primitivno rekurzivna. Formalni dokaz je kompliciran, ali ideja je ista kao i ideja dokaza da se npr.\ $\f{add}^2$ ne može dobiti samo kompozicijom iz inicijalnih funkcija: \emph{raste prebrzo}. Svaka kompozicija s inicijalnom funkcijom može u najboljem slučaju povećati bilo koji argument za~$1$, dakle pomoću konačno mnogo operatora $\circ$ možemo dobiti samo funkcije oblika $x+c$, gdje je $c$ konstanta a $x$ jedan od argumenata. No $x+y$ raste brže od toga.

Slično je i ovdje: svaka primjena primitivne rekurzije može povećati $z$ samo za $1$, pa s konačno mnogo operatora $\pr$ možemo postići najviše $\f A_c(x,y)$, gdje je $c$ konstanta. No $\f A^3$ raste brže od toga.

\begin{korolar}[{name=[totalnost Ackermannove funkcije]}]\label{kor:A3tot}
$\f A^3$ je totalna funkcija.
\end{korolar}
\begin{proof}
Neka je $(x,y,z)\in\N^3$ proizvoljna. Kako je $\f A_z$ primitivno rekurzivna po propoziciji~\ref{pp:Anprn}, ona je totalna, pa je $\dom{\f A_z}=\N^2$. Specijalno je $(x,y)\in\dom{\f A_z}$, pa izraz $\f A_z(x,y)$ ima vrijednost --- označimo je s $t$. No tada je i $\f A(x,y,z)=t$, dakle izraz $\f A(x,y,z)$ također ima vrijednost, pa je $(x,y,z)\in\dom{\f A^3}$.
\end{proof}

Kako je svaka $\f A_n^2$ izračunljiva, i funkcija $\f A^3$ je intuitivno izračunljiva: ako nam netko dade $(x,y,z)$ i traži od nas da izračunamo $\f A(x,y,z)$, zapravo traži da izračunamo $\f A_z(x,y)$, a to sigurno (za konkretni $z$) znamo učiniti. Po Church--\!Turingovoj tezi $\f A^3$ bi trebala biti parcijalno rekurzivna, dakle rekurzivna po korolaru~\ref{kor:A3tot}, ali možemo li to dokazati bez primjene Church--\!Turingove teze? Da --- korištenjem teorema rekurzije.

\begin{napomena}[{name=[dvomjesna Ackermannova funkcija]}]
Često se pojednostavljena, dvomjesna funkcija $\f A^2$, zadana s
\begin{align}
%\SwapAboveDisplaySkip
    \f A(0,n)&:=n+1\text,\\
    \f A(m+1,0)&:=\f A(m,1)\text,\\
    \f A(m+1,n+1)&:=\f A\bigl(m,\f A(m+1,n)\bigr)\text,
\end{align}
	u literaturi navodi pod imenom "Ackermannova funkcija", iako su je zapravo smislili R\'osza P\'eter i Raphael Mitchel Robinson. Iako s manje specijalnih slučajeva i zato lakša za proučavanje, ta funkcija je daleko manje motivirana i teško je objasniti zašto joj definicija izgleda baš tako. Može se, iako nije baš jednostavno, dokazati~\cite{Ackermann} da za sve $m,n\in\N$ vrijedi
\begin{equation}
    \f A(m,n)=\f A(2,n+3,m)\dotminus3\text,
\end{equation}
	iz čega slijedi da kad bi $\f A^3$ bila primitivno rekurzivna, takva bi bila i $\f A^2$. No $\f A^2$ nije primitivno rekurzivna (dokaz možete vidjeti u~\cite[dodatak]{skr:Vuk} --- ukratko, svaka primitivno rekurzivna funkcija je dominirana jednim retkom tablice Ackermannove funkcije) pa kontrapozicijom slijedi da ni $\f A^3$ nije primitivno rekurzivna.
\end{napomena}

\subsection{Rekurzivnost Ackermannove funkcije}

\begin{propozicija}[{name=[rekurzivnost Ackermannove funkcije]}]
    $\f A^3$ je rekurzivna funkcija.
\end{propozicija}
\begin{proof}
Prvo skupimo na jedno mjesto sve jednadžbe kojima je $\f A^3$ definirana. Osnovna jednadžba je~\eqref{eq:A2SSdef}, sada u obliku~\eqref{eq:A3SSdef}, koja kazuje što činiti kad su i drugi i treći argument pozitivni. Ako je treći argument $0$, imamo definiciju $\f A_0$ preko sljedbenika drugog argumenta~\eqref{eq:A3y0def}, a u preostalim slučajevima imamo početni uvjet~\eqref{eq:A30Sdef}, jednak prvom argumentu za zbrajanje, nuli za množenje, a jedinici za ostale operacije.
\begin{align}
\label{eq:A3SSdef}
    \f A(x,y+1,z+1)&=\f A\bigl(x,\f A(x,y,z+1),z\bigr)\\
\label{eq:A3y0def}
    \f A(x,y,0)&=y+1\\[-5mm]
\label{eq:A30Sdef}
    \f A(x,0,z)&=\f{Astart}(x,z):=\begin{cases}
        x,&z=1\\
        0,&z=2\\
        1,&\text{inače}
    \end{cases}
\end{align}

Slučaj kad su i drugi i treći argument $0$ tako je pokriven i sa~\eqref{eq:A3y0def} i sa~\eqref{eq:A30Sdef}, ali to nije problem, jer je po obje te jednadžbe $\f A(x,0,0)=1$.

Sada zapišimo taj sustav u obliku opće rekurzije. Prvo skupimo sve te jednadžbe u jedno grananje (koristit ćemo znak $=$ jer imamo korolar~\ref{kor:A3tot}, ali općenito, trebali bismo koristiti $\simeq$ dok još ne znamo je li funkcija totalna):
\begin{equation}
    \f A(x,y,z)=\begin{cases}
        \;\f A\bigl(x,\f A\bigl(x,\f{pd}(y),z\bigr),\f{pd}(z)\bigr),&y>0\land z>0\\
        \;y+1,&z=0\\
        \;\f{Astart}(x,z),&\text{inače}
    \end{cases}\text,
\end{equation}
a zatim to napišimo u obliku opće rekurzije $\f{comp}_k(x,y,z,e)=\f G(x,y,z,e)$, gdje je $k=3$, $e$ je traženi indeks, a funkcija $\f G^4$ je zadana s
\begin{equation}
    \f G(x,y,z,e):\simeq\begin{cases}
        \;\f{comp}_3\bigl(x,\f{comp}_3\bigl(x,\f{pd}(y),z,e\bigr),\f{pd}(z),e\bigr),&y\in\N_+\land z\in\N_+\\
        \;\f{Sc}(y),&z=0\\
        \;\f{Astart}(x,z),&\text{inače}
    \end{cases}
\end{equation}
    (sad smo morali upotrijebiti znak \enquote*{$\simeq$}, jer $\f G$ nije totalna --- npr.\ $(0,1,1,0)\notin\dom{\f G}$).

Po teoremu~\ref{tm:gprek}, $\f G$ je parcijalno rekurzivna. Po teoremu~\ref{tm:rek}, postoji prirodni broj $a$ takav da za sve $x,y,z\in\N$ vrijedi $\kf a(x,y,z)\simeq\f G(x,y,z,a)$. Tvrdimo da je $\kf a^3=\f A^3$, odnosno da je rješenje jedinstveno.

Točkovno, trebamo dokazati $\kf a(x,y,z)\simeq\f A(x,y,z)$ za sve $x,y,z\in\N$, i to činimo ugniježđenom indukcijom: vanjskom po $z$, unutarnjom po $y$.

Vanjska baza: za $z=0$ vrijedi (za sve $x,y\in\N$)
\begin{equation}
    \kf a(x,y,0)\simeq\f G(x,y,0,a)=y+1=\f A(x,y,0)\text.
\end{equation}

Vanjska pretpostavka: pretpostavimo da za $z=t$, za sve $x,y\in\N$, vrijedi
\begin{equation}
    \kf a(x,y,t)\simeq\f A(x,y,t)\text.
\end{equation}

Vanjski korak: neka je sada $z=t+1$. Dokazujemo da za sve $x,y\in\N$ vrijedi\\ $\kf a(x,y,t+1)\simeq\f A(x,y,t+1)$, unutarnjom indukcijom po $y$.

Unutarnja baza: za $y=0$ vrijedi (za sve $x\in\N$)
\begin{equation}
    \kf a(x,0,t+1)\simeq\f G(x,0,t+1,a)\simeq\f{Astart}(x,t+1)\text,
\end{equation}
što je u slučaju $t=0$ jednako $\f{Astart}(x,1)=x=x+0=\f A_1(x,0)=\f A(x,0,1)$,\\ u slučaju $t=1$ je jednako $\f{Astart}(x,2)=0=x\cdot0=\f A_2(x,0)=\f A(x,0,2)$, a\\ u svim ostalim slučajevima ($t\ge2$) je jednako $\f{Astart}(x,t+1)=1=\f A_{t+1}(x,0)=\f A(x,0,t+1)$. Dakle, uvijek je $\kf a(x,0,t+1)\simeq\f A(x,0,t+1)$, pa je unutarnja baza dokazana.

Unutarnja pretpostavka: pretpostavimo da za $y=s$, za sve $x\in\N$, vrijedi
\begin{equation}
    \kf a(x,s,t+1)\simeq\f A(x,s,t+1)\text.
\end{equation}

Unutarnji korak: neka je sada $y=s+1$, i $x\in\N$ proizvoljan.\\ Moramo dokazati $\kf a(x,s+1,t+1)\simeq\f A(x,s+1,t+1)$. Krenimo raspisivati s lijeve strane:
\begin{multline}
    \kf a(x,s+1,t+1)\simeq\f G(x,s+1,t+1,a)\simeq
    \f{comp}_3\bigl(x,\f{comp}_3\bigl(x,\f{pd}(s+1),t+1,a\bigr),\f{pd}(t+1),a\bigr)\simeq{}\\
    \f{comp}_3\bigl(x,\f{comp}_3(x,s,t+1,a),t,a\bigr)\simeq
	\f{comp}_3\bigl(x,\kf a(x,s,t+1),t,a\bigr)\simeq
	\f{comp}_3\bigl(x,\f A(x,s,t+1),t,a\bigr)\\
	{}\simeq\kf a\bigl(x,\f A(x,s,t+1),t\bigr)\simeq
	\f A\bigl(x,\f A(x,s,t+1),t\bigr)\simeq\f A(x,s+1,t+1)\text.
\end{multline}
Time su oba koraka provedena, pa tvrdnja vrijedi. To znači da $\f A$ ima indeks $a$, pa je parcijalno rekurzivna, odnosno zbog korolara~\ref{kor:A3tot} rekurzivna funkcija.
\end{proof}

% Upravo provedeni dokaz predstavlja određenu "šablonu" pomoću koje možemo za razne rekurzivno zadane funkcije dokazati da su doista rekurzivne u precizno definiranom smislu (imaju indeks, i totalne su). Ključno je da moramo na neki "vanjski" način zaključiti totalnost, jer inače bismo zapravo mogli zaključiti da je promatrana funkcija primitivno rekurzivna.

\section{Ekvivalentnost indeksa}

Teorem rekurzije može se shvatiti na još jedan način, na koji je prvotno bio dokazan. Fenomen smo već vidjeli na početku ovog poglavlja: teorem o parametru (propozicija~\ref{pp:tmpar}) se prirodno može dobiti iz propozicije~\ref{pp:composeprn}, jer po~\eqref{eq:paramcompose} možemo staviti
\begin{equation}\label{eq:paramcomposeind}
    \f S_k'(y,e):=\f{compose}_k\bigl(i_1,\dotsc,i_k,\overline{\f C_6}(y),e\bigr)\text,
\end{equation}
gdje je $i_n:=\kr{\f{codeDEC}(n,3),\f{codeINC}(0),\f{codeGOTO}(0)}$ indeks funkcije $\f I_n^k$, a (primjer~\ref{pr:kodkonst}) $\overline{\f C_6}(y)$ indeks funkcije $\f C_y^k$ --- ali s obzirom na to da je lakše dokazati teorem o parametru, išli smo u suprotnom smjeru.

% \subsection{Relacije \texorpdfstring{$\approx_k$}{k-ekvivalentnosti}}

Slično je i ovdje: jednakost $\kf e=\$(e,\f G)$ iz teorema rekurzije možemo shvatiti kao relaciju među indeksima $e\approx\f S_k(e,g)$, gdje je $g$ neki indeks za $\f G$. Ta "približna jednakost" ne može doista biti jednakost ni u kojem zanimljivom slučaju, jer za $g\in\f{Prog}$ uvijek vrijedi $\f S_k(e,g)>e$ (zgodna je vježba dokazati to). Što je onda relacija $\approx$?

Ukratko, vrijeme je da malo preciznije formaliziramo ideju ekvivalentnih RAM-programa iz definicije~\ref{def:ekvprog}: ono što bismo htjeli reći nije da su $e$ i $\f S_k(e,g)=:\f F(e)$ jednaki \emph{brojevi}, već da su $\kf e^k$ i $\kf{\f F(e)}^k$ jednake \emph{funkcije}. Nažalost, kao i u slučaju specijalizacije, imat ćemo različite relacije $\approx_k,k\in\N_+\!$ --- nećemo ih moći upotrebljivo objediniti u jednu relaciju, jer u RAM-programu nigdje ne piše intendirana mjesnost.

\begin{definicija}[{name=[$k$-ekvivalentnost]}]
Neka je $k\in\N_+$ te $e,f\in\N$.\\ Kažemo da su $e$ i $f$ \emph{$k$-ekvivalentni}, i pišemo $e\approx_kf$, ako vrijedi $\kf e^k=\kf f^k$.
\end{definicija}

\begin{primjer}[{name=[neke lagane $k$-ekvivalentnosti]}]\label{pr:alef0ind}
Za svaki $k\in\N_+$, za sve $e,f\in\f{Prog}\kompl$ vrijedi $e\approx_kf$ (jer svi brojevi izvan $\f{Prog}$ su indeksi prazne funkcije).
Također, za svaki $e\in\f{Prog}$, za sve $j,k\in\N_+$, vrijedi $e*\kr{\f{codeINC}(j)}\approx_ke$ (dodavanje instrukcije $\incr j$ na kraj programa neće promijeniti uvjet zaustavljanja, a ni izlaznu vrijednost jer je $j>0$).
\end{primjer}

\begin{propozicija}[{name=[struktura kvocijentnog skupa relacije $k$-ekvivalentnosti]}]
    Za svaki $k\in\N_+$, $\approx_k$ je relacija ekvivalencije, \\ s prebrojivo mnogo klasa ekvivalencije koje su sve prebrojive.
\end{propozicija}
\begin{proof}
Refleksivnost, simetričnost i tranzitivnost su trivijalne: recimo, $e\approx_kf\approx_kg$ znači $\kf e^k=\kf f^k=\kf g^k$, pa je $\kf e^k=\kf g^k$, iz čega $e\approx_kg$. Inače, u refleksivnosti se, kroz samu oznaku $\kf e^k$, krije korolar~\ref{kor:ram1fun} koji kaže da za fiksni $k$, svaki RAM-program računa jedinstvenu $k$-mjesnu funkciju.

Prebrojivost kvocijentnog skupa slijedi iz činjenice da postoji prebrojivo mnogo izračunljivih funkcija (teorem~\ref{tm:alef0izr}). Konkretno, za svaki $k\in\N_+$ su sve funkcije $\f C_y^k,y\in\N$, različite, pa je (primjer~\ref{pr:kodkonst}) $\overline{\f C_6}(y)\napprox_k\overline{\f C_6}(z)$ za sve $y\ne z$. Iz toga slijedi da različitih klasa ima beskonačno, a ne može ih biti neprebrojivo jer su neprazni disjunktni podskupovi od $\N$ (recimo, $\min:\N/_{\!\approx_k\!}\to\N$, koja svakoj klasi ekvivalencije pridružuje njen najmanji element, je injekcija, pa je $\card\,\bigl(\N/_{\!\approx_k\!}\bigr)\le\card\N=\aleph_0$).

Prebrojivost svake klase slijedi iz primjera~\ref{pr:alef0ind}: neka je $e\in\N$ proizvoljan. Ako je $e\in\f{Prog}\kompl$, tada je čitav $\f{Prog}\kompl$ u njegovoj klasi. Na primjer, $n\mapsto 2n+3$ je injekcija s $\N$ u $\f{Seq}\kompl\subseteq\f{Prog}\kompl\subseteq[e]_{\approx_k}\subseteq\N$, pa je $[e]_{\approx_k}$ prebrojiva. Ako je pak $e\in\f{Prog}$, tada je $\f F:\N_+\!\to[e]_{\approx_k}$, zadana s $\f F(j):=e*\kr{\f{codeINC}(j)}$, injekcija --- jer $j$ možemo rekonstruirati iz $f:=\f F(j)$ kao $\f{regn}\bigl(\f{rpart}(f,0)\bigr)$.
\end{proof}

Možda malo više iznenađujuća činjenica vezana uz familiju relacija $\approx_k,k\in\N_+$ je da je ona \emph{padajuća}: vrijedi $(\approx_1)\supset(\approx_2)\supset(\approx_3)\supset\dotsb$. Da bismo to dokazali, prvo trebamo jedno tehničko svojstvo funkcij\=a $\f S_k$.

\begin{lema}[{name=[nula je lijevi neutralni element za $\f S_k$]}]\label{lm:0nSk}
	Za svaki $e\in\f{Prog}$ i za svaki $k\in\N_+$ vrijedi $\f S_k(0,e)=e$.
\end{lema}
\begin{proof}
%Direktnim uvrštavanjem u definiciju. %Nulto, ako je $e\in\f{Prog}\kompl$, tada je po~\eqref{eq:Skprn} $\f S_k(y,e)=e$ za sve $y\in\N$, pa tako i za $y=0$. Još treba dokazati tvrdnju za $e\in\f{Prog}$.

Prvo, rastavom na slučajeve vidimo da je $\f{Shift}(0,i)=i$ za sve $i\in\N$. Recimo, za $i\in\f{InsDEC}$, postoje $j,l<i$ takvi da je $i=\f{codeDEC}(j,l)=\kr{1,j,l}$. No to znači da je $j=i[1]=\f{regn}(i)$ i $l=i[2]=\f{dest}(i)$, pa je $\f{Shift}(0,i)=\f{codeDEC}(j,l+0)=i$. Ostali slučajevi su još lakši.

Drugo, sada je $\f H(0,e,t)=\f{Shift}(0,e[t])=e[t]=\f{part}(e,t)$, pa je desni operand operacije $*$ u~\eqref{eq:Skprn} jednak $\overline{\f H}\bigl(0,e,\f{lh}(e)\bigr)=\overline{\f{part}}\bigl(e,\f{lh}(e)\bigr)=e$ jer iz $\f{Prog}(e)$ slijedi $\f{Seq}(e)$. Lijevi operand iste operacije je $\overline{\f G}(0)=1$ jer je svaka povijest u nuli jednaka $\kr{}=1$.

I treće, to onda znači da je (za $e\in\f{Prog}$) $\f S_k(0,e)=1*e$, što je jednako $e$ prema~\eqref{eq:starG} i~\eqref{eq:star}, jer vrijedi $\f{lh}(1)=0$ i $\f{Seq}(e)$.
\end{proof}

\begin{korolar}[{name=[dodavanje nul\=a na kraj ulaza ne mijenja RAM-izračunavanje]}]\label{kor:0nSk}
Za sve $k,l\in\N_+$, za sve $\vec x\in\N^k$ i za sve $e\in\N$, vrijedi 
	$\kf e^{k+l}(\vec x^k,\vec 0^l)\simeq\kf e^k(\vec x)$.
\end{korolar}
\begin{proof}
	Ako $e\notin\f{Prog}$, tvrdnja vrijedi jer ni lijeva ni desna strana nemaju vrijednost po propoziciji~\ref{prop:computeind}\eqref{it:nprogind}. Za $e\in\f{Prog}$, prvo indukcijom po $l$, prateći dokaz korolara~\ref{kor:pars} i koristeći lemu~\ref{lm:0nSk} u svakom koraku, dokažemo $\f S_k^{l+1}(\vec 0,e)=e$. Iz toga onda slijedi
\begin{equation}
    \kf e^{k+l}(\vec x,\vec 0)\simeq\kf{\f S_k^{l+1}(\vec 0,e)}(\vec x)\simeq\kf e^k(\vec x)\text,
\end{equation}
što smo i trebali dokazati.
\end{proof}
Na neformalnoj razini tvrdnja korolara~\ref{kor:0nSk} je očita: za bilo koji RAM-program $P$, $P$-izračunavanje s $\vec x$ je \emph{isto} (isti niz istih konfiguracija) kao i $P$-izračunavanje s $(\vec x,\vec 0)$, za bilo koji broj dodanih nula na kraj ulaza --- jer je izračunavanje deterministično, a početna konfiguracija $c_0=(0,\vec x,0,0,\dotsc)$ je ista. Samo smo rekli da će još $l$ registara nakon $\reg k$ biti postavljeno na nule, no oni bi ionako bili postavljeni na nule u izračunavanju s $\vec x^k$, jer u tom izračunavanju nisu ulazni.

\begin{propozicija}[{name=[niz relacija $k$-ekvivalentnosti strogo pada]}]
Za sve $k,l\in\N_+$ takve da je $k>l$ vrijedi $(\approx_k)\subset(\approx_l)$.
\end{propozicija}
\begin{proof}
Označimo $m:=k-l\in\N_+$. Za $(\subseteq)$, neka je $e\approx_kf$.
	
	Tada je $\kf e^k=\kf f^k$ (a $k=l+m$), pa je prema prethodnom korolaru, za sve $\vec x\in\N^l$,
\begin{equation}
    \kf e^l(\vec x)\simeq\kf e^{l+m}(\vec x^l,\vec 0^m)\simeq\kf f^{l+m}(\vec x,\vec 0)\simeq\kf f^l(\vec x)\text.
\end{equation}
Dakle vrijedi i $\kf e^l=\kf f^l$, pa je $e\approx_lf$.

Za $(\ne)$, moramo naći dva RAM-programa koji jesu ekvivalentni za sve moguće $l$-torke ulaznih podataka, ali kad počnemo stavljati ulaze i u registre od $\reg{l+1}$ do $\reg k$, više nisu. Za to nam mogu poslužiti $1$ kao indeks nulfunkcije, i $i_k$ kao indeks $k$-te koordinatne projekcije --- pogledajte tekst nakon~\eqref{eq:paramcomposeind} za preciznu definiciju.

Tada je $1\approx_l i_k$, jer za svaki $\vec x\in\N^l$ vrijedi
\begin{equation}
    \kf{i_k}^l(\vec x)\simeq\kf{i_k}^{l+m}(\vec x,\vec 0)=\f I_k^k(\vec x,\vec 0)=0=\f C_0^l(\vec x)=\kf1^l(\vec x)\text;
\end{equation}
	ali za $\vec y:=(\vec 0^{k-1},1)\in\N^k$ vrijedi
\begin{equation}
    \kf{i_k}^k(\vec y)=\f I_k^k(\vec 0,1)=1\ne0=\f C_0^k(\vec y)=\kf1^k(\vec y)\text,
\end{equation}
iz čega slijedi $1\napprox_ki_k$.
\end{proof}

%\subsection{Teorem o fiksnoj točki}

Kao što rekosmo na početku, indeks $e$ iz teorema rekurzije možemo shvatiti kao neku vrstu "fiksne točke" primitivno rekurzivne funkcije $\f F^1$ zadane s $\f F(e):=\f S_k(e,g)$, gdje je $g$ neki (fiksni) indeks funkcije $\f G$ čiji poziv stoji na desnoj strani opće rekurzije. Dakle, da imamo teorem koji nam kaže da svaka primitivno rekurzivna jednomjesna funkcija ima fiksnu točku, mogli bismo pomoću njega dokazati teorem rekurzije. Ipak, kako zasad stvari stoje, teorem rekurzije smo već dokazali, pa pokušajmo pomoću njega dokazati teorem o fiksnoj točki. Za početak ga pokušajmo formulirati što općenitije.

Prvo, sasvim je jasno da ne možemo tražiti $e=\f F(e)$ --- već za inicijalnu $\f F=\f{Sc}$ takav $e$ ne postoji. % funkcija, ali ne postoji $e$ takav da je $e=\f{Sc}(e)$ (to smo koristili kod Russellove funkcije).
Ipak možemo tražiti $e\approx_k\f F(e)$ za bilo koji fiksirani $k\in\N_+$ (takav $e$ će ovisiti o $k$; "uniformna" verzija, koja bi imala jedan $e$ za sve $k$, ne vrijedi).

Drugo, $\f F$ ne mora biti primitivno rekurzivna --- vidjet ćemo da je dovoljno da bude rekurzivna. Tada teorem vrijedi i za primitivno rekurzivne funkcije, zbog korolara~\ref{kor:prnrek}. Napomenimo da ne možemo još oslabiti pretpostavku zahtijevajući da je $\f F$ parcijalno rekurzivna: $\varnothing^1=\mu\,\emptyset^2$ je parcijalno rekurzivna prema primjeru~\ref{pr:varnothingprek}, a ne može postojati $e\in\N$ takav da su $e$ i $\varnothing(e)$ $k$-ekvivalentni, jer izraz $\varnothing(e)$ nema vrijednost ni za koji $e$.

Treće, smijemo tražiti da $e$ bude u $\f{Prog}$: dobit ćemo ga iz teorema rekurzije, a on daje samo sintaksno ispravne programe (preko dijagonalne funkcije).

Četvrto, $\f F$ mora biti jednomjesna: broj $k$ je mjesnost funkcije $\kf e^k$, jednake funkciji $\kf{\f F(e)}^k$. Mjesnost od $\f F$ mora biti $1$ jer želimo u nju uvrstiti $e\in\N^1$.

I peto, $\f F$ mora biti izračunljiva: nije dovoljno zahtijevati samo totalnost. Recimo, promotrimo karakterističnu funkciju klase ekvivalencije $E\mspace{-1mu}mp:=[0]_{\approx_1}$. Kad bi postojao broj $e$ takav da je $e\approx_1\chi_{E\mspace{-1mu}mp}(e)$, tada bi $e\in E\mspace{-1mu}mp$ povlačilo s jedne strane $e\approx_10$, a s druge $e\approx_1\chi_{E\mspace{-1mu}mp}(e)=1$, pa bi po tranzitivnosti bilo $0\approx_1\!1$, kontradikcija. (Izraz $\kf0(0)$ nema vrijednost po propoziciji~\ref{prop:computeind}\eqref{it:nprogind}, a $\kf1(0)=\f Z(0)=0$, pa $\kf0(0)\nsimeq\kf1(0)$, dakle $\kf0^1\!\ne\kf1^1$.) No $e\notin E\mspace{-1mu}mp$ je također kon\-tra\-dik\-ci\-ja, jer bi to značilo $e\approx_1\chi_{E\mspace{-1mu}mp}(e)=0$, dakle $e\in[0]_{\approx_1}\!=E\mspace{-1mu}mp$. Zaključujemo da $\chi_{E\mspace{-1mu}mp}$ nema fiksnu točku, iako je (kao i svaka karakteristična funkcija) totalna.

Primijetite sličnost upravo provedenog razmišljanja s Russellovim paradoksom. Iz toga će slijediti, jednom kad dokažemo teorem o fiksnoj točki, da skup $E\mspace{-1mu}mp$ nije rekurzivan. No zapravo će to biti samo jedna posljedica Riceova teorema, koji ćemo dokazati kasnije.

\begin{lema}[Teorem o fiksnoj točki]\label{lm:tmfix}
Neka je $k\in\N_+$ te $\f F^1$ rekurzivna funkcija.\\
	Tada postoji $e\in\f{Prog}$ takav da je $e\approx_k\f F(e)$.
\end{lema}
\begin{proof}
Zapišimo traženi uvjet pomoću univerzalne funkcije:
	\begin{equation}\label{eq:fpor}
    \f{comp}_k(\vec x,e)\simeq\f{comp}_k\bigl(\vec x,\f F(e)\bigr)\text{, za sve }\vec x\in\N^k\text.
\end{equation}
	To je opća rekurzija. Na desnoj strani je $\f G^{k+1}$ zadana s $\f G(\vec x,e):\simeq\f{comp}_k\bigl(\vec x,\f F(e)\bigr)$, dakle dobivena kompozicijom iz parcijalno rekurzivne $\f{comp}_k$, rekurzivne $\f F$ i inicijalnih koordinatnih projekcija, pa je parcijalno rekurzivna. Po teoremu~\ref{tm:rek}, postoji $e\in\f{Prog}$ koji zadovoljava tu funkcijsku jednadžbu. Jer je $\f F$ rekurzivna, dakle totalna, postoji i $f:=\f F(e)\in\N$ ($f$ naravno ne mora biti iz $\f{Prog}$). Sada se~\eqref{eq:fpor} može zapisati kao $\kf e(\vec x)\simeq\kf f(\vec x)$ za sve $\vec x\in\N^k$, odnosno $\kf e^k=\kf f^k$, dakle $e\approx_k f=\f F(e)$, što smo i trebali.
\end{proof}

\section{Invarijantnost}

% \subsection{Skupovi indeksa}

Vidjeli smo u prethodnoj točki da iz teorema o fiksnoj točki zapravo možemo zaključiti da klasa ekvivalencije $E\mspace{-1mu}mp=[0]_{\approx_1}$ nije rekurzivna: njena karakteristična funkcija ne može imati fiksnu točku, jer to vodi na paradoks vrlo sličan Russellovu. Međutim, taj rezultat je "kap u moru" općenitog rezultata koji kaže da \emph{nijedna} klasa ekvivalencije nijedne relacije $\approx_k$ nije rekurzivna --- štoviše, nijedna \emph{unija} takvih klas\=a ekvivalencije nije rekurzivna, osim trivijalnih unij\=a $\bigcup\emptyset=\emptyset$ (unija nijedne klase) i $\bigcup(\N/_{\!\approx_k\!})=\N$ (unija svih klasa).

O čemu se tu zapravo radi? Reći da je neki broj $e$ element klase $E\mspace{-1mu}mp$, zapravo znači reći da je $e\approx_10$, odnosno $\kf e^1=\kf0^1=\varnothing^1$. Drugim riječima, $E\mspace{-1mu}mp$ je upravo skup svih indeksa prazne jednomjesne funkcije. Ako uzmemo neku drugu izračunljivu funkciju, dobit ćemo neku drugu klasu (svih njenih indeksa), i obrnuto, neka druga klasa $[e]_{\approx_k}\!$ će biti skup svih indeksa funkcije $\kf e^k$.

Neka unija klasa $S:=\bigcup_{e\in A}[e]_{\approx_k}$ tada će odgovarati nekom \emph{skupu} izračunljivih $k$-mjesnih funkcija $\mathcal F:=\{\kf e^k\mid e\in A\}\subseteq\mathscr Comp_k$, i to tako da će praznom skupu $S$ odgovarati prazni skup $\mathcal F$, a skupu $S=\N$ odgovarat će $\mathcal F=\mathscr Comp_k$. Kako je to preslikavanje injekcija, ostalim skupovima brojeva ($\emptyset\subset S\subset\N$) odgovarat će ostali skupovi funkcija ($\emptyset\subset\mathcal F\subset\mathscr Comp_k$). Vrijeme je da to formaliziramo.

\begin{definicija}[{name=[skup indeksa]}]
Neka je $k\in\N_+$. Za svaki $\mathcal F\subseteq\mathscr Comp_k$ definiramo \emph{skup indeksa} %\\ (ili \emph{skup $k$-indeksa}, ako želimo naglasiti $k$)
	kao
\begin{equation}
    \kins{\mathcal F\,}:=\{e\in\N\mid\kf e^k\in\mathcal F\,\}\,\text.
\end{equation}
%(U oznaci nigdje ne spominjemo $k$, jer se može rekonstruirati iz $\mathcal F$ ako je $\mathcal F$ neprazan --- a $\kins{\emptyset}=\emptyset^1$ bez obzira na $k$.)
Oznaka ne spominje $k$ jer se $k$ može rekonstruirati iz nepraznog $\mathcal F$, a $\kins\emptyset=\emptyset^1$ za sve $k$.
\end{definicija}

Primijetite sličnost s definicijom~\eqref{eq:kodLdef} --- kao što smo tamo kodirali riječi zapisom u bazi, ovdje kodiramo funkcije njihovim indeksima. Već smo rekli da relacija $index\subseteq\N\times\N_+\times\mathscr Comp$, zadana s $index(e,k,\f F)\Longleftrightarrow\kf e^k=\f F$, nema funkcijsko svojstvo po prvoj varijabli: ne možemo govoriti o jedinstvenom indeksu neke konkretne funkcije --- ali zato možemo govoriti o skupu indeksa nekog skupa funkcija.

\begin{lema}[{name=[različiti skupovi funkcija imaju različite skupove indeksa]}]\label{lm:kodCompinj}
Za svaki $k\in\N_+$, preslikavanje $\kins{\cdots}:\mathcal P(\mathscr Comp_k)\to\mathcal P(\N)$ je injekcija.
\end{lema}
Štoviše, iz dokaza će slijediti da $\kins{\cdots}$ strogo raste: $\mathcal F\subset\mathcal G$ povlači $\kins{\mathcal F\,}\subset\kins{\mathcal G}$.
\begin{proof}
Neka su $\mathcal F,\mathcal G\subseteq\mathscr Comp_k$ različiti. Tada postoji funkcija $\f F$ takva da je (bez smanjenja općenitosti) $\f F\in\mathcal G$, ali $\f F\notin\mathcal F$. Tada $\f F\in\mathcal G\subseteq\mathscr Comp_k$ znači da je $\f F$ RAM-izračunljiva, pa postoji RAM-program $P$ koji je računa. Tada je po propoziciji~\ref{prop:computeind}\eqref{it:progind} $e:=\kprog P$ indeks funkcije $\f F$, odnosno $\kf e^k\in\mathcal G$, pa je $e\in\kins{\mathcal G}$.

	No kad bi bilo i $e\in\kins{\mathcal F\,}$, to bi značilo $\kf e^k\in\mathcal F$, što je nemoguće jer $\f F\notin\mathcal F$. Drugim riječima, $e\in\kins{\mathcal G}\setminus\kins{\mathcal F\,}$, odnosno $\kins{\mathcal F\,}\ne\kins{\mathcal G}$.
\end{proof}

Na neki način, do na neprebrojivost skupa $\mathcal P(\mathscr Comp_k)$, čini se da imamo "kodiranje" skupova izračunljivih funkcija. Onda bismo mogli reći, po uzoru na točku~\ref{sec:Todl}, da $\mathcal F$ ima neko svojstvo izračunljivosti ako karakteristična funkcija $\chi_{\kins{\mathcal F\,}}$ ima to svojstvo. Čak možemo reći, neko \emph{svojstvo} $\wp$ izračunljivih $k$-mjesnih funkcija je \emph{odlučivo} ako je skup $\kins{\{\f F\in\mathscr Comp_k\mid\wp(\f F)\}}$ rekurzivan. Ali zbog Riceova teorema, takva definicija bi bila sasvim beskorisna: \emph{jedini} rekurzivni skupovi indeksa su $\emptyset$ i $\N$, odnosno jedina odlučiva svojstva izračunljivih funkcija su trivijalna svojstva $\bot$ i $\top$.

% \subsection{Invarijantnost}

Kako je to moguće? Pa $\N$ ima hrpu rekurzivnih podskupova. Uzmimo za primjer %skup parnih brojeva $2\N$. Nije li to skup indeksa nekog netrivijalnog skupa funkcija? Nije, jer se može vidjeti da \emph{svaka} funkcija ima (neki) parni indeks: prazna funkcija ima indeks $0\in2\N$, nulfunkcija ima indeks $\kprog{[0.\;\incr1]}=\kr{\f{codeINC}(1)}=2^{19}\in2\N$, a sve ostale RAM-izračunljive funkcije imaju \emph{samo} parne indekse, jer ih računaju neprazni RAM-programi oblika $(I_0,I_1,\dotsc)$ čiji kodovi su sigurno djeljivi s $2^{\kins{I_0\!}\,+1}$. Drugim riječima, ovo svojstvo izračunljivih funkcija je trivijalno svojstvo $\top$.
%
%Dobro, uzmimo onda neki manji skup, recimo
jednočlani skup $\{1\}$. On je rekurzivan po lemi~\ref{lm:r1prn}, ali nije skup indeksa. Recimo, za $k=1$, u odgovarajućem skupu $\mathcal F$ bila bi funkcija $\f Z$, ali skup svih njenih indeksa je daleko veći od $\{1\}$ --- iz primjera~\ref{pr:alef0ind} vidimo da je beskonačan. Čim smo stavili broj~$1$ unutra, morali smo staviti i čitavu klasu $\kins{\{\f Z\}}=[1]_{\approx_1}$.

Dakle, skupovi indeksa nisu bilo kakvi podskupovi od $\N$. Oni moraju biti \emph{invarijantni} na neku relaciju $\approx_k$: ako sadrže $e$, tada moraju sadržavati i sve $f$ takve da je $e\approx_k f$. Na neki način, u takvom skupu se nalaze (kodirani) RAM-programi, ali skup je "neovisan o implementaciji" konkretnog algoritma.

\begin{primjer}[{name=[sortiranje kao jedna funkcija s raznim implementacijama]}]
    Recimo, mogli bismo zamisliti funkciju $\f{sort}^1\!:\f{Seq}\to\f{Seq}$ koja sortira konačne nizove zadane kodovima. Na primjer (\emph{unit test}), $\f{sort}(\kr{2,9,0,2})=\kr{0,2,2,9}$. Nije preteško pokazati da je $\f{sort}$ parcijalno rekurzivna, ali pritom moramo odabrati koji algoritam za sortiranje ćemo koristiti. \emph{Selection sort} bi izgledao ovako nekako:
\begin{align}
    \f{tail}(s)&:\simeq\mu t(\kr{s[0]}*t=s)\qquad
	\f{min}(s):\simeq\mu n\bigl(\exists i<\f{lh}(s)\bigr)(s[i]=n)\\
    %\f{count}(s,x)&:=\bigl(\num i<\f{lh}(s)\bigr)(s[i]=x)\\
    \f{up}(s,x)&\simeq\begin{cases}
        \kr{},&s=\kr{}\\
        \f{up}\bigl(\f{tail}(s),x\bigr),&\f{Seq'}(s)\land s[0]\le x\\
        \kr{s[0]}*\f{up}\bigl(\f{tail}(s),x\bigr),&\f{Seq'}(s)\land s[0]>x
    \end{cases}\\
    \f{sort}(s)&\simeq\begin{cases}
        \kr{},&s=\kr{}\\
	    \overline{\f I_1^2}\bigl(\f{min}(s),\bigl(\num i<\f{lh}(s)\bigr)\bigl(s[i]=\f{min}(s)\bigr)\bigr)*\f{sort}\bigl(\f{up}\bigl(s,\f{min}(s)\bigr)\bigr),&\f{Seq}'(s)
    \end{cases}
\end{align}
(funkcije $\f{up}$ i $\f{sort}$ definirane su općim rekurzijama), dok bi \emph{quicksort} bio nešto poput
\begin{align}
    \f{dn}(s,x)&\simeq\begin{cases}
        \kr{},&s=\kr{}\\
        \f{dn}\bigl(\f{tail}(s),x\bigr),&\f{Seq'}(s)\land s[0]>x\\
        \kr{s[0]}*\f{dn}\bigl(\f{tail}(s),x\bigr),&\f{Seq'}(s)\land s[0]\le x
    \end{cases}\\
    \f{sort}(s)&\simeq\begin{cases}
        \kr{},&s=\kr{}\\
        \f{sort}\bigl(\f{dn}\bigl(\f{tail}(s),s[0]\bigr)\bigr)*\kr{s[0]}*\f{sort}\bigl(\f{up}\bigl(\f{tail}(s),s[0]\bigr)\bigr),&\f{Seq}'(s)
    \end{cases}
\end{align}
--- što će nakon kompiliranja (i korištenja teorema rekurzije na nekoliko mjesta) rezultirati jako različitim RAM-programima, odnosno indeksima funkcije $\f{sort}$. Ako sa $ss$ označimo indeks za \emph{selection sort}, a s $qs$ označimo indeks za \emph{quicksort}, tada vrijedi $ss\approx_1\!qs$, jer što se specifikacije tiče, i jedan i drugi računaju istu funkciju: sortiraju konačan niz.

Možete se zabaviti pišući razne druge algoritme za sortiranje u jeziku parcijalno rekurzivnih funkcija~\ldots\ dobit ćete raznorazne implementacije, odnosno indekse, za jednu te istu matematičku funkciju, i svi su oni u istoj klasi ekvivalencije $\kins{\{\f{sort}\}}$. Ako bismo prije navedeni \emph{unit test} htjeli napisati u obliku jednadžbe po indeksu,
\begin{equation}\label{eq:unittest}
    \kf e(\kr{2,9,0,2})=\kr{0,2,2,9}\text,
\end{equation}
tada je jasno da i $ss$ i $qs$, i svi drugi indeksi iz $\kins{\{\f{sort}\}}$, moraju zadovoljavati tu jednadžbu. Iako taj \emph{unit test} ni izdaleka nije dovoljan za specifikaciju funkcije $\f{sort}$, svejedno ga možemo gledati kao neko svojstvo koje izračunljive funkcije mogu a i ne moraju imati: $\wp(\f F):\Longleftrightarrow\f F(810\,152\,280)=272\,386\,847\,250
$. Važno je naglasiti da to svojstvo ne ovisi o implementaciji funkcije $\f F$, već samo ovisi o funkciji samoj.
\end{primjer}

\begin{definicija}[{name=[$k$-invarijantnost]}]
Neka je $k\in\N_+$. Za skup $S\subseteq\N$ kažemo da je \emph{$k$-invarijantan} ako za sve $e,f\in\N$, iz $e\in S$ i $e\approx_k f$ slijedi $f\in S$.
\end{definicija}

Invarijantnost karakterizira skupove indeksa brojevno, bez pozivanja na skupove funkcija.

\begin{lema}[{name=[$k$-invarijantnost karakterizira skupove indeksa]}]\label{lm:kinv=sind}
Neka je $k\in\N_+$ te $S\subseteq\N$.

	Tada je $S$ $k$-invarijantan ako i samo ako je $S=\kins{\mathcal F\,}$ za neki $\mathcal F\subseteq\mathscr Comp_k$.
\end{lema}
\begin{proof}
	Za smjer ($\Leftarrow$), neka je $f\approx_k e\in S=\kins{\mathcal F\,}$. Tada je po definiciji $\kf f^k=\kf e^k\in\mathcal F$, pa je i $f\in\kins{\mathcal F\,}=S$. Za smjer ($\Rightarrow$), pretpostavimo da je $S$ $k$-invarijantan, i tražimo $\mathcal F$. Očiti kandidat je $\mathcal F:=\{\kf e^k\mid e\in S\}$. Dakle, trebamo dokazati da je $\kins{\mathcal F\,}=S$.

	Za inkluziju ($\supseteq$), po definiciji $\mathcal F$ iz $e\in S$ slijedi $\kf e^k\in\mathcal F$, dakle $e\in\kins{\mathcal F\,}$.

	Za inkluziju ($\subseteq$), iz $f\in\kins{\mathcal F\,}$ slijedi da postoji $\f F^k\in\mathcal F$ takva da je $\kf f^k=\f F$. No $\f F\in\mathcal F$ po definiciji $\mathcal F$ znači da postoji $e\in S$ takav da je $\kf e^k=\f F$. Sada $\kf e^k=\f F=\kf f^k$ znači $e\approx_k f$, pa jer je $S$ $k$-invarijantan i $e\in S$, zaključujemo $f\in S$, što smo trebali.
\end{proof}

Još je jedna stvar tu na prvi pogled čudna: zašto svojstvo~\eqref{eq:unittest} nije parcijalno rekurzivno? Čini se da je njegova karakteristična funkcija dobivena kompozicijom iz primitivno rekurzivne funkcije $\chi_=$, parcijalno rekurzivne funkcije $\f{comp}_1$ te konstanti $\f C^1_{\kr{2,9,0,2}}$ i $\f C^1_{\kr{0,2,2,9}}$. Ipak, to nije istina, jer prema marljivoj evaluaciji, ta kompozicija nikako ne može biti totalna (jer $\f{comp}_1$ nije totalna), dok bi karakteristična funkcija morala biti totalna. Isti problem smo već imali prije --- pogledajte napomenu~\ref{nap:parc=}.

% \subsection{Riceov teorem}

\begin{teorem}[Riceov teorem]\label{tm:Rice}
Neka je $k\in\N_+$, i $S\subseteq\N$ rekurzivan $k$-invarijantan skup.\\
	Tada je $S=\emptyset$ ili $S=\N$.
\end{teorem}

Ideja dokaza je vrlo slična onom što smo napravili za $E\mspace{-1mu}mp$ --- samo, dok nam je tamo Russellov paradoks bio "serviran"\!, ovdje ćemo morati namjestiti scenu za njega.

\begin{proof}
Pretpostavimo da je $S$ rekurzivan, i da $S$ nije ni $\emptyset$ ni $\N$. $S\ne\emptyset$ znači da postoji broj $s\in S$, a $S\ne\N$ znači da postoji $n\in S\kompl=\N\setminus S$. Tada je funkcija $F^1$, zadana s
\begin{equation}
    F(x):=\begin{cases}
        n,&x\in S\\
        s,&\text{inače}
    \end{cases}\text,
\end{equation}
    rekurzivna po teoremu~\ref{tm:grek} (rekurzivna verzija) --- simbolički, $F=\IF{S:\f C_n^1,\f C_s^1}$.

Jer je $F$ rekurzivna, ima fiksnu točku: postoji broj $e\in\N$ takav da je $e\approx_k F(e)$. No to je nemoguće: ako je $e\in S$, tada je po $k$-invarijantnosti i $F(e)\in S$ --- što je u kontradikciji s činjenicom da je $F(e)=n$ za $e\in S$. Ako pak $e\notin S$, tada je $F(e)=s\in S$, a zbog simetričnosti relacije $\approx_k$ imamo i $F(e)\approx_k e$. No to bi značilo da $S$ nije $k$-invarijantan, jer smo našli $s\in S$ takav da je $s\approx_k e$, ali $e$ nije u $S$.

U oba slučaja došli smo do kontradikcije, pa pod pretpostavkom da je $S$ rekurzivan, jedino je moguće da je $S=\emptyset$ ili $S=\N$.
\end{proof}

\subsection{Sintaksna i semantička svojstva RAM-programa}

Riceov teorem smo izrekli u "pozitivnom" obliku --- no on se češće koristi "negativno".

\begin{korolar}[{name=[nerekurzivnost netrivijalnog $k$-invarijantnog skupa brojeva]}]\label{kor:Rice!rek}
Neka je $S\subset\N$ neprazan i $k$-invarijantan za neki $k\in\N_+$. Tada $S$ nije rekurzivan.
\end{korolar}
\begin{proof}
Ovo je samo obrat po kontrapoziciji teorema~\ref{tm:Rice}.
\end{proof}

\begin{korolar}[{name=[neodlučivost netrivijalnog skupa izračunljivih funkcija]}]\label{kor:Rice!odl}
Neka je $k\in\N_+$ te $\emptyset\subset\mathcal F\subset\mathscr Comp_k$. Tada $\mathcal F$ nije odlučiv\!.
\end{korolar}
\begin{proof}
	Označimo $S:=\kins{\mathcal F\,}$. Prema lemi~\ref{lm:kinv=sind}, skup $S$ je $k$-invarijantan. S druge strane, po lemi~\ref{lm:kodCompinj} je $S\ne\kins{\emptyset}=\emptyset$ i $S\ne\kins{\mathscr Comp_k\!}=\N$ (svaki prirodni broj je indeks neke $k$-mjesne funkcije). Po korolaru~\ref{kor:Rice!rek} $S$ nije rekurzivan, što znači da $\mathcal F$ nije odlučiv\!.
\end{proof}

\begin{korolar}[{name=[neodlučivost netrivijalnih semantičkih svojstava]}]
Neka je $k\in\N_+$ te neka je $\wp$ bilo koje netrivijalno svojstvo $k$-mjesnih izračunljivih funkcija. Tada nijedan algoritam ne može točno odrediti, za proizvoljnu $\f F\in\mathscr Comp_k$, ima li $\f F$ svojstvo $\wp$.
\end{korolar}
\begin{proof}
Budući da je $\wp$ netrivijalno svojstvo, postoji neka $k$-mjesna funkcija koja ima to svojstvo, a postoji i neka druga $k$-mjesna funkcija koja ga nema. To znači da za skup $\mathcal F:=\{\f F\in\mathscr Comp_k\mid\wp(\f F)\}$ vrijedi $\emptyset\subset\mathcal F\subset\mathscr Comp_k$. Kad bi takav algoritam postojao, morao bi primati funkciju u nekom obliku (točkovna definicija, simbolička definicija, RAM-program, Turingov stroj,~\ldots) --- a svaki od njih znamo, neformalnim algoritmom, pretvoriti u indeks. Štoviše, imamo i (neformalne) algoritme pretvorbe u suprotnom smjeru, što znači da algoritam kojim bismo htjeli odlučiti $\wp$ mora raditi za \emph{sve} indekse traženih funkcija.
%Ovo vjerojatno treba mnogo bolje raspisati.
Po Church--\!Turingovoj tezi, to znači da bi taj algoritam računao $\chi_{\kins{\!\mathcal F\,}}$, što je u kontradikciji s korolarom~\ref{kor:Rice!odl}.
\end{proof}

Za zadani RAM-program možemo postaviti mnoga pitanja: ima li više od milijun instrukcija, stane li s ulazom $(2,5)$, je li mu registar $\reg{15}$ relevantan, sadrži li instrukciju tipa $\goto$, računa li totalnu funkciju, dekrementira li ikad u toku izračunavanja registar $\reg7$, je li dobiven kompiliranjem simboličke definicije neke primitivno rekurzivne funkcije, zapiše li Turingov stroj dobiven njegovim transpiliranjem ikad prazninu na traku, može li se dobiti spljoštenjem makro-programa koji sadrži barem jedan funkcijski makro, napravi li paran broj koraka prije zaustavljanja s ulazom $27$, i tako dalje.

Mnoga od tih svojstava (ali ne nužno sva) prirodno svrstavamo u dvije grupe: nazovimo ih \emph{sintaksna} i \emph{semantička} svojstva. Sintaksna svojstva su ona vezana uz konkretni "programski jezik" kojim je RAM-program pisan: govore o instrukcijama, registrima, ili o raznim sintaksnim postupcima pretvorbe (npr.\ iz makro-programa, ili u Turingov stroj) te o sintaksnim svojstvima tih drugih nositelja izračunavanja.

Semantička svojstva su ona vezana uz RAM-izračunavanje: govore o zaustavljanju, totalnosti, funkcijama koje se računaju, njihovim domenama, slikama, grafovima, i sličnom. Važno okvirno pravilo koje pruža dobru intuiciju je: \textbf{sintaksna svojstva su uglavnom odlučiva, semantička svojstva su uglavnom neodlučiva}.

Dobru empirijsku potvrdu prvog dijela pravila vidjeli smo u poglavlju~\ref{ch:univ}, gdje smo hrpu sintaksnih svojstava pokazali odlučivima, i razvili alate koji nam omogućavaju za još veću hrpu to pokazati bez muke. Recimo, $\reg{15}$ je relevantan za RAM-program $P$ ako i samo ako vrijedi
$\bigl(\exists i<\f{lh}(e)\bigr)\bigl(\f{regn}(e[i])\ge15\bigr)$, što je primitivno rekurzivno svojstvo od $e=\kprog P$.

S druge strane, Riceov teorem pruža dobar uvid u drugi dio tog pravila. Među semantičkim svojstvima izdvajaju se ona koja govore \emph{samo} o računanoj funkciji, bez ikakvog spominjanja konkretne implementacije. Recimo, "$P$-izračunavanje s $(2,5)$ stane" se može tako zapisati, jer zapravo kaže $(2,5)\in\dom{\f F}$, gdje je $\f F$ funkcija koju $P$ računa. Riceov teorem kaže da su sva takva svojstva sigurno neodlučiva --- osim dva trivijalna, naravno. Primjerice, svojstvo "ovaj RAM-program rješava \emph{halting problem}" jest odlučivo: za svaki RAM-program vratimo $\mathit{false}$. Također, "ovaj RAM-program računa parcijalno rekurzivnu funkciju" jest odlučivo: uvijek vratimo $\mathit{true}$.

S druge strane, parnost broja koraka ne možemo tako napisati. Najlakši način da se to vidi je invarijantnost: za svaki RAM-program koji napravi paran broj koraka prije zaustavljanja s ulazom $27$, postoji RAM-program koji računa istu funkciju, ali napravi neparan broj koraka prije zaustavljanja s ulazom $27$. Standardni trik dodavanja instrukcije $\incr1$ na kraj programa, viđen u primjeru~\ref{pr:alef0ind}, "upalit" će i ovdje.

Svakako postoje i mnoga "hibridna" svojstva, za utvrđivanje čije odlučivosti je potrebna detaljna analiza --- ali Riceov teorem s jedne i Church--\!Turingova teza s druge strane pružaju dobar dio odgovora na takva pitanja.

Iako Riceov teorem govori samo o skupovima indeksa (dakle invarijantnim podskupovima od~$\N$), svođenjem možemo dokazati i razne druge neodlučivosti odnosno nerekurzivnosti: sjetite se korolara~\ref{kor:nrek<nrek}. Neko sasvim općenito uputstvo za korištenje Riceova teorema moglo bi se napisati u sljedećem obliku:

\begin{enumerate}
    \item Utvrdimo da trebamo dokazati da neki skup $S$ nije rekurzivan.
    \item\label{korak:skupfun} Pomoću skupa $S$ nađemo skup $\mathcal F$ u kojem se nalaze izračunljive funkcije neke fiksne mjesnosti $k$.
    %\item
	    Skup svih indeksa svih funkcija iz $\mathcal F$ označimo s $T:=\kins{\mathcal F\,}$.
    \item\label{korak:elemT} Nađemo neki element od $T$ (najčešće tako da nađemo neku jednostavnu funkciju iz $\mathcal F\!$, napišemo RAM-program koji je računa, i nađemo njegov k\=od).
    \item Analogno, nađemo neki element od $T\kompl$. Skupa s korakom~\ref{korak:elemT} sada imamo $\emptyset\subset T\subset\N$.
    \item Dokažemo da je $T$ $k$-invarijantan, gdje je $k$ mjesnost koju smo fiksirali u koraku~\ref{korak:skupfun}.
    \item Formalno svedemo $T\!\preceq S$, pišući $\chi_T$ kao kompoziciju $\chi_S$ s nekim rekurzivnim funkcijama.
    \item Zaključimo da kad bi $S$ bio rekurzivan, bio bi takav i $T$, što je kontradikcija s Riceovim teoremom.
\end{enumerate}

\begin{primjer}[{name=[neodlučivost $k$-mjesnog brojevnog problema zaustavljanja]}]
    Za svaki $k\in\N_+$, skup $Halt_k$ nije rekurzivan. Naime, ako definiramo $T(e):\Longleftrightarrow Halt_k(\vec 0,e)$, skup $T=\kins{\{\f f\in\mathscr Comp_k\mid\vec 0\in\dom{\f f}\}}$ je $k$-invarijantan po lemi~\ref{lm:kinv=sind} te vrijedi $0\notin T$ i $1\in T$. Dakle $T$ nije rekurzivan, pa zbog $T\preceq Halt_k$ niti $Halt_k$ nije rekurzivan.
\end{primjer}