univ.tex

\chapter{Univerzalna izračunljivost}\label{ch:univ}

%\section{Kodiranje}

Sada već možemo i prilično komplicirane funkcije dokazati primitivno rekurzivnima. Sljedeći veliki zalogaj koji ćemo uzeti je kodiranje konačnih nizova prirodnih brojeva (skupa $\N^*\mspace{-2mu}$).

Zašto baš to kodiranje? Dva su razloga. Prvo, trebat će nam za opis rada RAM-stroja, tako da možemo raditi s konfiguracijama i izračunavanjima kao s ulaznim podacima. Recimo, implementirat ćemo funkciju $\f U$ koja prima izračunavanje koje je stalo i vraća njegov izlazni podatak. Ubuduće ćemo često tako neformalno govoriti: "funkcija prima izračunavanje", ili "funkcija vraća RAM-program", misleći  pritom na kanonsko kodiranje izračunavanja odnosno RAM-programa. Znamo da su RAM-programi konačni nizovi instrukcija, a izračunavanja koja stanu se također mogu pamtiti samo do završne konfiguracije kao konačni nizovi konfiguracija. Same pak konfiguracije također se mogu pamtiti kao konačni nizovi --- vrijednost programskog brojača i sadržaj samo relevantnih registara. Vidjet ćemo da se mnogi objekti koje ćemo željeti kodirati mogu prikazati kao konačni nizovi drugih objekata, tako da ako već imamo kodiranje tih jednostavnijih objekata, kodiranje $\N^*$ dat će nam odmah mogućnost kodiranja složenih objekata.

Drugi razlog je preciznost specifikacije. Kodiranja su zapravo opisana algoritmima, čiji izlazni podaci su prirodni brojevi, a ulazni podaci su \emph{nešto drugo} osim prirodnih brojeva. Općenito može biti komplicirano specificirati takav algoritam, jer on praktički po definiciji ne može biti formalni algoritam (recimo, RAM-algoritam) --- ulazni podaci mu nisu prirodni brojevi, a da bismo ih prikazali kao prirodne brojeve, trebamo upravo kodiranje koje pokušavamo implementirati! Kodiranje $\N^*$ pruža izlaz iz tog začaranog kruga, jer imamo formalizaciju algoritama koji primaju konačne nizove prirodnih brojeva: za fiksnu duljinu niza ($k$-torke) to su jednostavno $k$-mjesni algoritmi, a za proizvoljnu duljinu niza to su familije algoritama $\mathcal A^k,k\in\N_+$ (i eventualno konstanta $\mathcal A^0$). Naše kodiranje je upravo takva familija $\f{Code}^k,k\in\N_+$, s konstantom $1$ koja igra ulogu $\f{Code}^0$. Prvo preciznije definirajmo općenita kodiranja.

\begin{definicija}[{name=[kodiranje]}]
	Neka je $\mathcal K$ neki skup (koji ne sadrži prirodne brojeve nego neku drugu vrstu objekata). \emph{Kodiranje skupa $\mathcal K$} je izračunljiva totalna injekcija $\N\mathcal K:\mathcal K\to\N$, kojoj je slika $\im{\N\mathcal K}$ (skup svih kodova, gledan kao jednomjesna brojevna relacija) rekurzivna, a parcijalni inverz (lijevi inverz s obzirom na kompoziciju) $\NKmj:\N\rightharpoonup\mathcal K$, s domenom $\dom{\NKmj}=\im{\N\mathcal K}$, je također izračunljiva funkcija.
\end{definicija}

Napominjemo da ${\N\mathcal K}$ i $\NKmj$ jesu izračunljive, dakle imamo (neformalne) algoritme za njih --- ali to nisu brojevne funkcije, pa te algoritme nemamo u formalnom smislu (recimo, ne možemo reći "$\N\mathcal K\in\mathscr Comp$"). Ipak, možemo biti precizni u pogledu izračunljivosti skupa $\im{\N\mathcal K}$: kako je to obični podskup od $\N$, dakle jednomjesna relacija, zahtijevamo da njena karakteristična funkcija bude rekurzivna.

Pokušajmo još malo preciznije odrediti što mislimo pod izračunljivošću funkcija ${\N\mathcal K}$ i $\NKmj$. Zamislimo da imamo funkciju $g:\mathcal K\rightharpoonup\mathcal K$, za koju želimo utvrditi je li izračunljiva. Tada možemo na $\im{\N\mathcal K}$ definirati tzv\!.\ \emph{prateću} funkciju (\emph{tracking function}) $\N g:={\N\mathcal K}\circ g\circ\NKmj$, koja uzme kod $c$, iz njega odredi jedinstveni $\kappa\in\mathcal K$ takav da je ${\N\mathcal K}(\kappa)=c$, primijeni $g$ na $\kappa$, a rezultat (ako je definiran, odnosno ako je $\kappa\in\dom g$) kodira natrag funkcijom ${\N\mathcal K}$. Prateća je funkcija uvijek brojevna; ako je izračunljiva u nekom smislu (recimo, parcijalno rekurzivna) i kodiranje relativno kanonsko, prirodno je smatrati funkciju $g$ izračunljivom u tom istom smislu. Primijetimo da ${\N\mathcal K}\circ g\circ\NKmj$ ne možemo smatrati simboličkom definicijom prateće funkcije, jer to nije kompozicija brojevnih funkcija. Moramo nekako drugačije, koristeći samo prirodne brojeve, zapisati prateću funkciju. Ako to uspijemo izvesti za velik broj intuitivno izračunljivih funkcija $g$, to je argument za tvrdnju da imamo izračunljivo kodiranje.

Slično možemo činiti za funkcije iz $\mathcal K$ u $\N$ (samo ih komponiramo s $\NKmj$ zdesna), za funkcije iz $\N$ u $\mathcal K$ (samo ih komponiramo s ${\N\mathcal K}$ slijeva --- primijetite da su karakteristične funkcije posebni slučaj pratećih funkcija, za $\N bool(\mathit{false}):=0,\,\N bool(\mathit{true}):=1$), pa čak i za razne "višemjesne" funkcije iz skupova poput $\mathcal K^2\times \mathcal L\times\N$ (gdje je $\mathcal L$ neki drugi skup čije kodiranje $\N\mathcal L$ već imamo): ulaze dekodiramo (ostavivši nepromijenjenima ulaze koji već jesu prirodni brojevi), primijenimo funkciju te kodiramo rezultat ako je definiran. Puna implementacija tog principa odvela bi nas u \emph{objektno programiranje}, gdje je $\mathcal K$ \emph{klasa}, čije razne \emph{metode} kodiramo na opisani način. Često među tim metodama postoji jedna istaknuta surjekcija na $\mathcal K$ (ili više njih čije slike čine particiju od $\mathcal K$) koju onda zovemo \emph{konstruktor}, a koordinatne funkcije njenog inverza (\emph{getters} ili \emph{komponente}) služe kao podloga za sve ostale metode.

\begin{napomena}[{name=[ne možemo kodirati neprebrojive skupove]}]
U još jednoj stvari budimo precizni: \textbf{neprebrojive skupove ne možemo kodirati}! Doista, ako postoji kodiranje kao injekcija s $\mathcal K$ u $\N$, tada mora biti $\card\mathcal K\le\card\N=\aleph_0$. Ovo je izuzetno važno, jer opravdava intuiciju da samo konačni i prebrojivi skupovi imaju \emph{totalnu reprezentaciju}: sve njihove elemente možemo reprezentirati u (po volji velikom) računalu.

Neegzaktnosti tipa \texttt{float}, i raznih drugih tipova koji bi trebali reprezentirati realne brojeve, nisu samo tehnički nedostaci pojedinog standarda (kao što je IEEE\;754): one su fundamentalna posljedica činjenice da $\mathbb R$ kao neprebrojiv skup nema totalnu reprezentaciju. Kako god pokušali~\cite{url:calc}, ne možemo u računalu reprezentirati proizvoljni realni broj --- i to nema veze s ograničenom veličinom naših računala. Ograničenost memorije samo predstavlja razliku između konačnih i prebrojivih skupova; razlika prebrojivih i neprebrojivih skupova mnogo je veća i njen prijelaz zahtijeva sasvim nove paradigme.
\end{napomena}

\section{Kodiranje konačnih nizova}
Sada se možemo pozabaviti samom implementacijom kodiranja $\N^*$. Kako bismo najlakše kodirali $\vec x=(x_1,x_2,\dotsc,x_k)$ kao jedan prirodni broj, iz kojeg se kasnije mogu "izvući" pojedini brojevi $x_i$? U teoriji skupova, za dokaz da je $\N^2$ prebrojiv\!, promatramo injekciju $p(x,y):=2^x\cdot3^y$ te koristimo osnovni teorem aritmetike (rastav na prim-faktore) da bismo iz $p(x,y)$ natrag dobili $x$ i $y$. To možemo proširiti na proizvoljnu mjesnost jer prim-brojeva ima beskonačno mnogo: uzmemo ih dovoljno redom po veličini, potenciramo odgovarajućim eksponentima i pomnožimo --- ali to nije kodiranje skupa $\N^*$. Naime, takvo preslikavanje nije injekcija, jer se primjerice $(1,2,0,0)$ i $(1,2)$ preslikaju u isti broj $2^1\cdot3^2\cdot5^0\cdot7^0=2^1\cdot3^2=18$.

Ipak, mala modifikacija tog postupka dat će nam kodiranje. Zapravo, jedini problem su nule u konačnom nizu --- opisano preslikavanje \emph{jest} kodiranje skupa ${\N_+\!}^*$ konačnih nizova \emph{pozitivnih} prirodnih brojeva. Sada je još samo preostalo komponirati ga s izračunljivom bijekcijom $\f{Sc}$ između $\N$ i $\N_+$, i dobili smo traženo kodiranje.

\begin{definicija}[{name=[kodiranje konačnih nizova prirodnih brojeva]}]
	Označimo prim-brojeve redom s $p_0:=2$, $p_1:=3$, $p_2:=5$,~\dots
%Za $i\in\N$, s $p_i$ označimo $i$-ti po redu prim-broj (počevši od $p_0=2$).

	Definiramo $\langle\rangle:=1$ te za svaki $k\in\N_+$ definiramo 
\begin{equation}\label{eq:Codek}
	\f{Code}^k(x_1,x_2,\dotsc,x_k):=\langle x_1,x_2,\dotsc,x_k\rangle:=2^{x_1+1}\cdot3^{x_2+1}\mathbin{\dotsm}p_{k-1}^{x_k+1}\text{.\quad\qedhere}
\end{equation}
\end{definicija}
Time je definirana funkcija $\langle\cdots\rangle:\N^*\to\N$. To doduše nije brojevna funkcija jer nema fiksnu mjesnost, ali ipak možemo reći da je izračunljiva u istom smislu u kojem su višestruko zbrajanje i množenje izračunljive operacije po lemi~\ref{lm:addmulk}.

\begin{propozicija}[{name=[primitivna rekurzivnost kodiranja konačnih nizova]}]\label{prop:Codekprn}
Za svaki $k\in\N_+$, funkcija $\f{Code}^k$ je primitivno rekurzivna.
\end{propozicija}
\begin{proof}
    Svaki faktor u produktu~\eqref{eq:Codek} možemo prikazati kao kompoziciju potenciranja, konstante, sljedbenika i koordinatne projekcije. Tada kompozicija s $\f{mul}^k$ daje simboličku definiciju
    \begin{equation}\f{Code}^k=\f{mul}^k\circ\bigl(\f{pow}\circ(\f C_2^k,\f{Sc}\circ\f I_1^k),\f{pow}\circ(\f C_3^k,\f{Sc}\circ\f I_2^k),\dotsc,\f{pow}\circ(\f C_{p_{k-1}}^k,\f{Sc}\circ\f I_k^k)\bigr)\text,
    \end{equation}
    iz koje po propozicijama~\ref{prop:konst} i~\ref{prop:symbdef}, primjeru~\ref{pr:addmulpow} te lemi~\ref{lm:addmulk} slijedi tvrdnja.
\end{proof}

Simbolička definicija je napisana kako bi bilo sasvim jasno da nigdje nismo trebali izračunljivost funkcije $n\mapsto p_n$. To svakako vrijedi, i trebat će nam kasnije, ali za pojedinu funkciju $\f{Code}^k$ dovoljno je znati da postoji barem $k$ prim-brojeva te da su konstante s tim vrijednostima izračunljive.

\begin{propozicija}[{name=[injektivnost kodiranja konačnih nizova]}]\label{prop:codeinj}
Preslikavanje $\langle\cdots\rangle:\N^*\to\N$ je injekcija.
\end{propozicija}
\begin{proof}
    Pretpostavimo da su $\vec x^k,\vec y^{l}\in\N^*$ takvi da je $\langle\vec x\rangle=\langle\vec y\rangle$. Ako je $k>l$, tada je $k-1\in\N$, pa je $\langle\vec x\rangle$ djeljiv s $p_{k-1}$, što $\langle\vec y\rangle$ nije ($p_{k-1}\notin\{p_0,p_1,\dotsc,p_{l-1}\}$, pa ne dijeli njihov umnožak), kontradikcija. Analogno ne može biti $k<l$ --- dakle je $k=l$.
	
	Za svaki $i\in[1\mspace{-1mu}\dd k]$, tvrdimo da ne može biti $x_i>y_i$. U suprotnom, k\=od bi bio djeljiv s $p_{i-1}^{y_i+1}\!$, pa bi nakon dijeljenja lijeva strana bila djeljiva s $p_{i-1}$, a desna ne~bi. Analogno se vidi da nije ni $x_i<y_i$, dakle mora biti $x_i=y_i$. Time smo dokazali $\vec x=\vec y$.
\end{proof}

Sljedeće bismo trebali pokazati da je $\im{\langle\cdots\rangle}=:\f{Seq}$ rekurzivan skup te da na tom skupu imamo izračunljivu funkciju koja nam na neki način daje originalni $\vec x$ iz kojeg je pojedini kod dobiven. Za taj dokaz potrebno nam je ponešto teorije brojeva, no prije toga precizirajmo u kakvom obliku tražimo naš inverz.

Naglasimo odmah da tražimo primitivno rekurzivne, dakle totalne funkcije. Njihovo djelovanje bit će parcijalno specificirano na skupu $\f{Seq}$, iako će se napisani algoritmi moći izvršiti na svakom prirodnom broju.

Da bismo odredili konačni niz iz kojeg je dobiven k\=od $c$, moramo prvo odrediti njegovu duljinu. Dakle, tražimo totalnu funkciju $lh$ takvu da za svaki $c\in\f{Seq}$, $lh(c)$ bude duljina konačnog niza čiji je $c$ k\=od. Takvih funkcija ima neprebrojivo mnogo jer je $\f{Seq}\kompl$ beskonačan (recimo, sadrži sve neparne brojeve veće od $3$), a na njemu $lh$ može djelovati proizvoljno --- pa sigurno postoje i neizračunljive takve funkcije. Ipak, dokazat ćemo da postoji takva funkcija $\f{lh}$ koja je primitivno rekurzivna.

Kad smo odredili $\f{lh}(c)=:k$, na prvi pogled imamo tipičnu situaciju algoritma s više izlaza: od jednog broja $c$ trebamo dobiti $k$ njih, pa bismo u skladu s napomenom~\ref{nap:brip} to trebali reprezentirati pomoću koordinatnih funkcija $\f{part}_1,\f{part}_2,\dotsc,\f{part}_k$. Ipak, to nema baš smisla jer broj takvih funkcija ovisi o $c$ (po funkciji $\f{lh}$), a osim toga, ponekad će nam trebati i dinamički određeni indeksi. Recimo, kad budemo pisali funkciju $\f U$, koja k\=od izračunavanja koje stane preslikava u njegov rezultat, bit će potrebno odabrati \emph{posljednju} konfiguraciju u konačnom nizu. A čak i da imamo izračunljive funkcije $\f{part}_i$ za sve $i$, iz toga ne slijedi da je preslikavanje $c\mapsto\f{part}_{\f{lh}(c)}(c)$ izračunljivo (pokušajte napisati simboličku definiciju i vidjet ćete u čemu je problem).

Srećom, ideja dinamizacije i ovdje pomaže: zapravo ćemo imati \emph{dvomjesnu} funkciju $\f{part}^2$, tako da $\f{part}(c,i)$ (skraćena oznaka $c[i]$) bude ono što smo bili nazvali $\f{part}_{i+1}(c)$ --- pomaknuli smo indekse za $1$ jer želimo shvatiti konačne nizove kao polja (\emph{arrays}), koja se u većini modernih programskih jezika indeksiraju od nule. Bitno nam je da to vrijedi samo za $c\in\f{Seq}$ i $i\in[0\dd \f{lh}(c)\rangle$ --- za ostale uređene parove mora biti nekako definirana jer je primitivno rekurzivna, ali nije nam bitno kako točno. Pokazat će se da za $c\in\f{Seq}$ i $i\ge\f{lh}(c)$ vrijedi $c[i]=0$, što će biti korisno u jednom trenutku, ali naglasit ćemo to kad nam bude trebalo.

\begin{napomena}[{name=[strukture kao konačni nizovi fiksne duljine]}]
%Recimo još nekoliko riječi o dinamizaciji ovdje.
    Ako za fiksni $k\in\N_+$ promatramo funkciju $\f{Code}^k$ u jednom smjeru i funkcije $\f{part}_1,\dotsc,\f{part}_k$ u drugom, zapravo modeliramo ono što jezik C zove struktura (\texttt{struct}) s $k$ članova. C ima strukture kao zasebne tipove podataka prvenstveno jer one mogu sadržavati podatke različitih tipova. Kako mi sve kodiramo prirodnim brojevima, to nam neće bitno trebati. %Ipak, jedna prednost struktura je u tome da umjesto indeksa možemo imati lijepa \emph{imena} za članove, što će nam biti korisno u jednom trenutku kasnije, pa ćemo se na ovu ideju vratiti.
\end{napomena}

Kad smo već kod programskog jezika C, vjerojatno znate da se polja u njemu najčešće prenose tako da se u jednom argumentu prenese pokazivač (što u našem slučaju odgovara kodu), a u drugom, zasebnom argumentu duljina polja. Tada bismo mogli kodirati i bez sljedbenika u eksponentu, jer bi duljina do koje gledamo "memoriju" bila posebno zadana. Ipak, većina modernijih programskih jezika drži duljinu zajedno sa sadržajem spremnika (na primjer, Python ima ugrađenu funkciju \texttt{len}) pa je zato i mi kodiramo tako da ju je moguće odrediti iz koda. %Nama će ideja kodiranja bez sljedbenika biti bitna u jednom drugačijem slučaju, kada je duljina nespecificirana --- ali o tome kasnije.

Funkcije $\f{Code}^k$ su prikladne ako imamo fiksnu mjesnost i možemo argumente zadati posebno. Što dobijemo ako primijenimo ideju dinamizacije na tu familiju funkcija? Argumenti su tada zadani nekom funkcijom $G$ te posebni argument $y$ kaže koliko ih ima (usporedite s točkom~\ref{sec:ogrprog}). Operator koji dinamički kodira zadani broj vrijednosti neke funkcije zovemo operatorom \emph{povijesti}, jer često argument $y$ %koji kaže koliko vrijednosti treba kodirati zapravo
predstavlja vrijeme, odnosno broji korake u nekom postupku (konkretno, trebat će nam za brojenje koraka u $P$-izračunavanju s $\vec x$).

\begin{definicija}[{name=[povijest totalne brojevne funkcije]}]
Neka je $k\in\N_+$ i $G^k$ totalna funkcija. Za funkciju $F^k$ zadanu s
\begin{equation}\label{eq:povijest}
    F(\vec x,y):=\langle G(\vec x,0),G(\vec x,1),\dotsc,G(\vec x,y-1)\rangle
\end{equation}
(početak je $F(\vec x,0):=\langle\rangle=1$) kažemo da je \emph{povijest} funkcije $G$ i pišemo $F:=\overline G$.
\end{definicija}

\begin{primjer}[{name=[primorijel kao povijest nulfunkcije]}]\label{pr:primorijel}
$\overline{\f{Code}}(0,2)=\kr{\kr{0,0},\kr{0,1}}=\kr{6,18}=2^7\cdot3^{19}=148\,769\,467\,776$. Također,
\begin{multline}
    \overline{\f{mul}}(2,1,3)=\langle\f{mul}(2,1,0),\f{mul}(2,1,1),\f{mul}(2,1,2)\rangle=\langle2\cdot1\cdot0,2\cdot1\cdot1,2\cdot1\cdot2\rangle=\\
    =\langle0,2,4\rangle=2^{0+1}\cdot3^{2+1}\cdot5^{4+1}=2\cdot27\cdot3125=168\,750.
\end{multline}
Može biti i $k=1$; jedan važni slučaj je $\f G:=\f Z$. Recimo,
\begin{equation}
    \overline{\f Z}(5)=\langle\f Z(0),\f Z(1),\f Z(2),\f Z(3),\f Z(4)\rangle=\langle0,0,0,0,0\rangle=2\cdot3\cdot5\cdot7\cdot11=2\,310.
\end{equation}
Dakle, funkcija $\overline{\f Z}$ je u uskoj vezi s funkcijom tzv\!.\ \emph{primorijel}, definiranom slično kao faktorijel, osim što množi samo prim-brojeve.
\end{primjer}

Sada bismo htjeli dokazati rezultat analogan onom u lemi~\ref{lm:sumprodrek}, samo za operator povijesti. Kao što smo već rekli, to će zahtijevati ponešto teorije brojeva.

\subsection{Potrebni rezultati iz teorije brojeva}\label{sec:teobroj}

Dokazujemo niz rezultata o primitivnoj rekurzivnosti, navodeći uglavnom samo toč\-kov\-ne definicije (koristeći ograničene sume, produkte, brojenje i minimizaciju) te obrazlažući ukratko manje poznate rezultate iz teorije brojeva koje ovdje koristimo.

Sjetimo se napomene~\ref{nap:crtica}: često brojevnoteorijske funkcije nisu definirane u nuli, koju zato zamjenjujemo jedinicom, pišući $n\bump$ za $n$ ako je pozitivan, a $1$ ako je $n=0$.

\begin{propozicija}[{name=[primitivna rekurzivnost dijeljenja s ostatkom]}]\label{prop:divmodprn}
    Cjelobrojno dijeljenje, zadano s $x\div y:=\bigl\lfloor\frac{x}{y\bump\!}\bigr\rfloor$, kao i ostatak cjelobrojnog dijeljenja ($x\bmod y$), primitivno su rekurzivne operacije.
\end{propozicija}
Prije dokaza napomenimo da je nula problematična u operaciji $\div\!$, ali ne i u operaciji $\bmod$: definicija $x\bmod 0:=x$ uobičajena je u modernoj teoriji brojeva.
\begin{proof}
	Cjelobrojno dijeljenje zapravo je ponovljeno oduzimanje, onoliko puta koliko se može. Dakle, za zadane $x$ i $y$, tražimo najveći $t$ takav da je $t\cdot y\le x$. Relacija $t\cdot y\le x$ jest primitivno rekurzivna (korolar~\ref{kor:mj-vj} i primjer~\ref{pr:addmulpow}), ali nemamo operator maksimizacije. S razlogom ga općenito nemamo: ako malo razmislimo, vidjet ćemo da ne postoji općeniti algoritam kojim bismo odredili najveći broj s nekim svojstvom, čak ni ako znamo da taj broj postoji, jer nikad ne znamo jesmo li tražili dovoljno dugo --- u svakom trenutku iznad najvećeg broja koji smo ispitali postoji još beskonačno mnogo kandidata, svaki od kojih može biti traženi broj.

Srećom, naša relacija je \emph{padajuća} po $t$: jednom kad $t\cdot y\le x$ postane laž, ostat će laž za sve veće $t$. Kod takvih relacija, "prva laž" i "posljednja istina" su susjedne, dakle možemo naći prethodnik najmanjeg $t$ za kojeg vrijedi suprotno.

Ipak, to je neograničena minimizacija, koja neće dati primitivno rekurzivnu funkciju --- možemo li je nekako ograničiti? Svakako: $y\bump\ge 1$ znači $t\cdot y\bump\ge t$ za svaki $t$, posebno $(x+1)\cdot y\bump\ge x+1>x$. Dakle, dovoljno je tražiti $t$ do $x+1$ --- odnosno do $x$ uključivo, jer znamo da će ograničena minimizacija tada dati $x+1$ ako ne pronađe nijedan broj s traženim svojstvom u zadanom rasponu. Sve u svemu, tvrdimo da vrijedi
\begin{equation}\label{eq:sslash}
    x\div y=\f{pd}\bigl((\mu t\le x)(t\cdot y>x)\bigr)\text.
\end{equation}
Za $y>0$, samo trebamo formalizirati navedeni argument: označimo $z:=x\div y$. Tada je $zy\le x$ (i $ty\le zy\le x$ za sve $t\le z$), a $(z+1)y>x$, dakle $z+1$ je najmanji $t$ koji pomnožen s $y$ daje broj veći od $x$. S druge strane je $z\le x\div1=x$, pa je $z+1\le x+1$. Ako je $z+1\le x$, tada će ga ograničena minimizacija u~\eqref{eq:sslash} naći, a ako je $z+1=x+1$, tada ga neće naći do uključivo $x$ (isključivo $x+1$), pa će po definiciji vratiti upravo $x+1$. U svakom slučaju vrijednost te ograničene minimizacije bit će $z+1$, pa će njen prethodnik biti $z=x\div y$, što smo trebali.

Za $y=0$, samo trebamo izračunati lijevu i desnu stranu. Na lijevoj je $x\div 0=\bigl\lfloor\frac{x}{1}\bigr\rfloor=x$, a na desnoj je prethodnik minimizacije po $t\le x$, relacije $t\cdot 0=0>x$. Ta relacija je uvijek lažna (nemamo negativnih brojeva), pa minimizacija daje $x+1$, a njen prethodnik onda daje upravo $x$, kao što i treba.

Ostatak: tvrdimo da je
\begin{equation}
    x\bmod y=x\dotminus x\div y\cdot y
\end{equation}
(redoslijed izvođenja operacija je: $\div$, pa $\cdot$, pa $\dotminus$). Za $y>0$ iz teorema o dijeljenju s ostatkom dobijemo da je ostatak $x-z\cdot y$ (sa $z$ smo označili količnik), a iz provedenog razmatranja se vidi da je $z\cdot y\le x$, pa se oduzimanje može ograničiti nulom. Za $y=0$ na lijevoj strani piše $x$, a na desnoj također $x\dotminus x\div0\cdot 0=x\dotminus x\cdot0=x\dotminus0=x$.
\end{proof}

\begin{korolar}[{name=[primitivna rekurzivnost djeljivosti]}]\label{kor:midprn}
Djeljivost je primitivno rekurzivna relacija.
\end{korolar}
\begin{proof}
Svatko tko je ikad provjeravao djeljivost u programiranju zna kako se to radi:
\begin{equation}
    y\mid x\Longleftrightarrow x\bmod y\eq0\text.
\end{equation}
Zaista, za $y>0$, postojanje broja $z$ takvog da je $z\cdot y=x$ (definicija djeljivosti) zapravo znači da je $z=x\div y$, pa je $x\bmod y=x\dotminus z\cdot y=x\dotminus x=0$. U drugom smjeru, ako je $x\dotminus x\div y\cdot y=0$, iz toga slijedi (kao i prije, vrijedi $x\div y\cdot y\le x$) $x=x\div y\cdot y$, pa postoji $z:=x\div y$ takav da vrijedi $x=z\cdot y$, odnosno $y\mid x$.

Za $y=0$, na desnoj strani stoji $x\bmod 0=x=0$, a to stoji i na lijevoj strani jer je jedino $0$ djeljiva nulom --- "postoji $z$ takav da je $0\cdot z=x$" upravo znači da je $x=0$.
\end{proof}

\begin{korolar}[{name=[primitivna rekurzivnost skupa svih prim-brojeva]}]
    Skup $\mathbb P$ svih prim-brojeva je primitivno rekurzivan.
\end{korolar}
\begin{proof}
Prim-brojevi imaju točno dva prirodna djelitelja, a za pozitivne $x$, svaki djelitelj od $x$ je manji ili jednak $x$:
\begin{equation}\label{eq:Pprn}
    x\in\mathbb P\Longleftrightarrow(\num d\le x)(d\mid x)\eq2\text.
\end{equation}
Za nulu će tom metodom ispasti da ima jedan djelitelj (samu sebe), a zapravo ih ima beskonačno mnogo --- ali i tako je $0\notin\mathbb P$. Sada tvrdnja slijedi iz korolara~\ref{kor:midprn} i leme~\ref{lm:brojrek}.
\end{proof}

U "stvarnom životu", provjera je li $x\in\mathbb P$ odvija se drugačije: nulu, jedinicu i dvojku te sve ostale parne brojeve odvojimo kao posebne slučajeve, a onda provjeravamo samo neparne kandidate za djelitelje od 3 do uključivo $\lfloor\!\sqrt{x}\rfloor$. Ipak, to su sve samo praktične optimizacije, koje bitno ubrzavaju algoritam --- ostavljajući ga doduše u istoj klasi složenosti. Početkom ovog stoljeća čak je pronađen \emph{polinomni} algoritam za provjeru je li zadani broj prim-broj, ali je uvelike kompliciraniji. Kako se mi ovdje ne opterećujemo performansama, tražimo samo najelegantniji zapis algoritma, a to je bez sumnje~\eqref{eq:Pprn}.

\begin{propozicija}[{name=[primitivna rekurzivnost enumeracije skupa $\mathbb P$]}]\label{pp:primeprn}
    Niz $(p_i)_{i\in\N}$ (strogo rastući niz čija je slika $\mathbb P$, tzv\!.\ \emph{enumeracija} skupa $\mathbb P$)\\je primitivno rekurzivan.
\end{propozicija}
\begin{proof}
    Zapravo trebamo algoritam za funkciju $\f{prime}^1$, koja svakom broju $n$ pridružuje $p_n$, $n$-ti prim-broj po veličini. Treba nam primitivna rekurzija --- i to degenerirana jer definiramo funkciju mjesnosti $1$. Za inicijalizaciju stavimo samo vrijednost $p_0=2$, a u koraku trebamo funkciju $\f{nextprime}$ koja prima ($n$ i) $p_n$, i mora vratiti $p_{n+1}$. Je li ta funkcija izračunljiva?

	Kako uopće znamo da je $\f{nextprime}$ \emph{totalna}, odnosno da njome možemo graditi primitivnu rekurziju? Prim-brojeva ima beskonačno mnogo: za svaki $p_n$ postoji $q\in\mathbb P$ takav da je $q>p_n$. Štoviše, $p_{n+1}$ je prvi takav $q$, pa ga možemo naći minimizacijom:
\begin{equation}\label{eq:primerek}
    \f{nextprime}(p):=\mu q(q\in\mathbb P\land q>p)\text.
\end{equation}
Upravo napisani izraz zapravo kaže da je $\f{nextprime}^1$ \emph{rekurzivna} funkcija (parcijalno je rekurzivna jer je dobivena minimizacijom konjunkcije dvije rekurzivne relacije, a totalna je zbog beskonačnosti skupa $\mathbb P$), pa je i $\f{prime}$ rekurzivna po korolaru~\ref{kor:F1rek}.

    Za primitivnu rekurzivnost, moramo nekako ograničiti minimizaciju, odnosno moramo "isprogramirati" dokaz da je $\mathbb P$ beskonačan. Uzmimo Euklidov dokaz: ako imamo $p_0,p_1,\dotsc,p_n\in\mathbb P$, novi prim-broj možemo dobiti tako da potražimo prim-djelitelj broja $m:=p_0\cdot p_1\mathbin{\dotsm}p_n+1>1$. Aha! Znamo da je djelitelje pozitivnog broja dovoljno tražiti do samog tog broja, dakle samo trebamo primitivno rekurzivno izračunati $m$ iz $n$ i $p_n$. Tu bismo mogli upotrijebiti primorijel iz primjera~\ref{pr:primorijel} --- konkretno, $m=\f{Sc}\bigl(\overline{\f Z}\bigl(\f{Sc}(n)\bigr)\bigr)$ --- ali nažalost još ne znamo da je funkcija $\overline{\f Z}$ primitivno rekurzivna, jer nismo dokazali da povijest čuva primitivnu rekurzivnost. I to s razlogom: pokazat će se da za tu lemu treba rezultat koji upravo dokazujemo.

    Kako se izvući? Spas je u tome da ne trebamo pomoću $n$ i $p_n$ izračunati baš $m$, nego samo neki broj od kojeg je $m$ manji. Ionako nećemo tražiti njegove prim-djelitelje, nego će nam on samo poslužiti kao gornja granica za traženje sljedećeg prim-broja nakon $p_n$. To znači da umjesto primorijela možemo upotrijebiti faktorijel, za koji znamo da je primitivno rekurzivan (primjer~\ref{pr:factorialprn}), a vrijedi $p_n!\ge p_0\cdot p_1\mathbin{\dotsm}p_n$ jer je $p_n!$ umnožak svih brojeva na desnoj strani i eventualno još nekih --- koji iznose $1$ ili više, pa ne smanjuju umnožak.
\begin{equation}
    \f{nextprime}(p)=(\mu q\le p!+1)(q\in\mathbb P\land q>p)%\text,
\end{equation}
	Dakle $\f{nextprime}^1$ je dobivena ograničenom minimizacijom primitivno rekurzivne relacije do primitivno rekurzivne granice, pa je primitivno rekurzivna po napomeni~\ref{nap:igpk} i propoziciji~\ref{prop:ominprn}. A tada je i $\f{prime}=2\pr\f{nextprime}\circ\f I_2^2$ primitivno rekurzivna po propoziciji~\ref{prop:F1prn}.
\end{proof}

%\section{Lema o povijesti i posljedice}
\begin{lema}[{name=[primitivna rekurzivnost rastava na prim-faktore]}]\label{lm:exprn}
Za $(n,i)\in\N^2$, označimo s $\f{ex}(n,i)$ eksponent prim-broja $p_i$ u rastavu broja $n\bump$ na prim-faktore. Funkcija $\f{ex}^2$ je primitivno rekurzivna.
\end{lema}
Nula nema rastav na prim-faktore, pa je moramo zamijeniti jedinicom --- koja \emph{ima} jedinstveni rastav na prim-faktore: prazni produkt, gdje su svi eksponenti jednaki $0$.
\begin{proof}
Opet, tražimo najveći broj $t$ takav da ${p_i}^t\mid n\bump$. Kao i u dokazu propozicije~\ref{prop:divmodprn}, ta relacija je padajuća po $t$: jednom kad prestane biti istina, ne može ponovo postati istina ni za koji veći $t$. Dakle, isti trik (prethodnik najmanjeg elementa komplementa) prolazi. Također, kako je $\f{prime}$ rastuća funkcija, imamo $n\bump\ge{p_i}^t\ge{p_0}^t=2^t>t$ (Cantorov osnovni teorem za konačne skupove), pa je $t$ dovoljno tražiti do $n\bump$ isključivo, ili do $n$ jer su za $n=0$ ionako svi eksponenti $0$. Sve u svemu, vrijedi
\begin{equation}
    \f{ex}(n,i):=\f{pd}\bigl((\mu t<n)\bigl(\f{pow}(\f{prime}(i),t)\nmid n\bigr)\bigr)\text,
\end{equation}
pa je $\f{ex}$ primitivno rekurzivna.
\end{proof}

Pomoću funkcije $\f{ex}$ napokon možemo dekodirati proizvoljni kod konačnog niza.

\begin{propozicija}[{name=[primitivna rekurzivnost dekodiranja konačnih nizova]}]\label{prop:lhpartprn}
Postoje primitivno rekurzivne funkcije $\f{lh}^1$ i $\f{part}^2$, takve da \\za svaki $\vec x=(x_1,x_2,\dotsc,x_k)\in\N^*$, uz oznaku $c:=\langle\vec x\rangle$ te pokratu $c[i]:=\f{part}(c,i)$ vrijedi:
\begin{enumerate}
    \item\label{stav:lh} $\f{lh}(c)=k$;
    \item\label{stav:part<k} za sve $i<k$, $c[i]=x_{i+1}$;
    \item\label{stav:part=0} za sve $i\ge k$, $c[i]=0$.
\end{enumerate}
\end{propozicija}
%Kao što smo već rekli, $\f{part}(c,i)$ ćemo skraćeno pisati $c[i]$, po uzoru na indeksiranje u brojnim programskim jezicima.
\begin{proof}
Tvrdimo da funkcije zadane s
\begin{align}
%\f{lh}(c)&:=(\num i<c)\bigl(\f{prime}(i)\mid c\bigr)\text,\\
	\f{lh}(c)&:=(\num d\le c)(d\in\mathbb P\land d\mid c)\text,\\
c[i]:=\f{part}(c,i)&:=\f{pd}\bigl(\f{ex}(c,i)\bigr)\text,
\end{align}
zadovoljavaju sve uvjete. Prije svega, primitivno su rekurzivne: $\f{lh}$ je dobivena og\-ra\-ni\-če\-nim brojenjem primitivno rekurzivne relacije do primitivno rekurzivne granice, a $\f{part}=\f{pd}\circ\f{ex}$.

    Što se tiče tvrdnje~\ref{stav:lh}, prema definiciji $\f{lh}$ broji prim-djelitelje od $c$ %(kako je $\f{prime}$ strogo rastuća i $0<p_0$, vrijedi $i<p_i\le c$, pa je dovoljno brojiti do $c$)
	--- a kako je $c=\langle\vec x\rangle=2^{x_1+1}\cdot3^{x_2+1}\mathbin{\dotsm}p_{k-1}^{x_k+1}$ te su svi napisani eksponenti pozitivni, $c$ ima točno $k$ prim-djelitelja.

Za tvrdnju~\ref{stav:part<k}, neka je $i<k$ proizvoljan. Tada je eksponent od $p_i$ u rastavu $c>0$ na prim-faktore upravo $\f{ex}(c,i)=x_{i+1}+1$, pa je $c[i]=\f{pd}(x_{i+1}+1)=x_{i+1}$.

    Za tvrdnju~\ref{stav:part=0}, neka je $i\ge k$ proizvoljan. Jedini prim-djelitelji od $c$ su $p_j,j\in[0\dd k\rangle$, među kojima nije $p_i$. Dakle $(\mu t<c)(p_i^t\nmid c)=1$, pa je $\f{ex}(c,i)=\f{pd}(1)=0$ te je i $c[i]=\f{pd}(0)=0$.
\end{proof}

Funkcija $\f{part}$ je parcijalno specificirana samo po $c$: jednom kad znamo da je $c\in\f{Seq}$, sve vrijednosti $c[i]$ su propisane. Još nam nedostaje dokaz da je $\f{Seq}$ primitivno rekurzivna relacija, no to će slijediti uskoro.

\section{Funkcije definirane kodiranjem konačnih nizova}

\begin{lema}[Lema o povijesti]\label{lm:povijestrek}
	Neka je $k\in\N_+$ i $\f{G}^k$ (primitivno) rekurzivna funkcija.\\ Tada je i $\overline{\f G}$ (primitivno) rekurzivna.
\end{lema}
(Vrijedi i obrat ove leme, ali nam neće biti potreban. Zapravo, i u lemi~\ref{lm:sumprodrek} vrijedi obrat za $\f F_1$, dok za $\f F_2$ ne vrijedi. Zgodna je vježba pokušati to dokazati.)
\begin{proof}
Da bismo zapisali $\overline{\f G}$ primitivno rekurzivno pomoću $\f G$, uvrstimo~\eqref{eq:Codek} u~\eqref{eq:povijest}:
\begin{equation}\label{eq:povijestrek}
    \overline{\f G}(\vec x,y)=\prod_{i<y}\f{pow}\bigl(\f{prime}(i),\f{Sc}\,\bigl(\f{G}(\vec x,i)\bigr)\bigr)\text.
\end{equation}
Ako $i$-ti faktor u~\eqref{eq:povijestrek} označimo s $\f H(\vec x,i)$, tada je $\f{pow}\circ(\f{prime}\circ\f I_k^k,\f{Sc}\circ\f G)$ sim\-bo\-li\-čka definicija od $\f H^k$ kompozicijom iz funkcija za koje je već dokazano da su primitivno rekurzivne, i funkcije $\f G$ koja je (primitivno) rekurzivna po pretpostavci --- pa je $\f H$ (primitivno) rekurzivna. Sada je $\overline{\f G}$ (primitivno) rekurzivna po lemi~\ref{lm:sumprodrek}.
%
%Za drugi smjer, zadana nam je $\overline{\f G}$ i želimo iz nje dobiti $\f G$. Pažljivim gledanjem~\eqref{eq:povijest} vidimo da $\overline{\f G}(\vec x,y)$ kodira prvih $y$ vrijednosti oblika $\f G(\vec x,i)$, među kojima \emph{nije} $\f G(\vec x,y)$. (To je čest \emph{bug} u C-programiranju: u polju deklariranom s \texttt{int a[7];} nema elementa \texttt{a[7]}.) Ako želimo dobiti taj broj, moramo zapravo izračunati $\overline{\f G}$ u nekom broju \emph{većem} od $y$ kao zadnjem argumentu. Dovoljno je uzeti $\overline{\f G}(\vec x,y+1)$: tvrdimo
%\begin{equation}\label{eq:unpovijest}
%    \f G(\vec x,y)=\overline{\f G}\bigl(\vec x,\f{Sc}(y)\bigr)[y]\text,
%\end{equation}
%odakle slijedi (primitivna) rekurzivnost od $\f G$, iz (primitivne) rekurzivnosti od $\overline{\f G}$. Doista, $c:=\overline{\f G}(\vec x,y+1)$ jest kod konačnog niza duljine $y+1$, pa prema propoziciji~\ref{prop:lhpartprn}\eqref{stav:part<k} za svaki $i<y+1$ vrijedi $c[i]=\f G(\vec x,i)$. Specijalno za $i:=y$ imamo jednakost~\eqref{eq:unpovijest}.
\end{proof}

Napokon možemo dokazati primitivnu rekurzivnost slike kodiranja.

\begin{korolar}[{name=[primitivna rekurzivnost slike kodiranja konačnih nizova]}]\label{kor:Seqprn}
    Relacija $\f{Seq}^1:=\,\im{\langle\cdots\rangle}$ je primitivno rekurzivna.
\end{korolar}
\begin{proof}
	Formalno, definicija slike (totalne funkcije) daje
\begin{equation}
    \f{Seq}(c)\Longleftrightarrow(\exists\,\vec x\in\N^*)(c=\langle\vec x\rangle)\text,
\end{equation}
i način za određivanje $\vec x$ je kanonski: pokušamo dekodirati $c$. (To funkcionira i općenito, ali razlog zašto se rekurzivnost slike navodi kao zasebno svojstvo funkcije kodiranja je u tome što ga u slučaju kodiranja nekih drugih objekata možemo provjeriti formalnije nego na ovaj način, koji općenito koristi neformalne algoritme.) Dakle, tvrdimo
\begin{equation}
    \f{Seq}(c)\Longleftrightarrow c\eq\overline{\f{part}}\bigl(c,\f{lh}(c)\bigr)\text;
\end{equation}
pritom smjer $(\Leftarrow)$ odmah slijedi iz činjenice da je \emph{svaka} vrijednost funkcije oblika $\overline{\f G}$ kod konačnog niza.

	Za smjer $(\Rightarrow)$, pretpostavimo da je $c=\langle\vec x\rangle$ za neki $\vec x=(x_1,x_2,\dotsc,x_k)\in\N^k\subset\N^*$. Tada je prema propoziciji~\ref{prop:lhpartprn}\eqref{stav:part<k},
\begin{multline}
    \overline{\f{part}}\bigl(c,\f{lh}(c)\bigr)=\langle c[0],c[1],\dotsc,c[\f{lh}(c)-1]\rangle=\\
    =\langle x_{0+1},x_{1+1},\dotsc,x_{\f{lh}(c)-1+1}\rangle=\langle x_1,x_2,\dotsc,x_k\rangle=\langle\vec x\rangle=c\text.
\end{multline}
Za $c=\langle\rangle=1$, također vrijedi $\overline{\f{part}}\bigl(1,\f{lh}(1)\bigr)=\overline{\f{part}}(1,0)=\langle\rangle=1=c$.

Sada primitivna rekurzivnost slijedi na uobičajeni način: prema propoziciji~\ref{prop:lhpartprn} funkcija $\f{part}$ je primitivno rekurzivna, prema lemi~\ref{lm:povijestrek} je tada i $\overline{\f{part}}$ primitivno rekurzivna, a onda je $\chi_{\f{Seq}}=\chi_\eq\circ\bigl(\f I_1^1,\overline{\f{part}}\circ(\f I_1^1,\f{lh})\bigr)$ simbolička definicija karakteristične funkcije od $\f{Seq}$, iz koje se vidi da je ona primitivno rekurzivna.
\end{proof}

Time smo u potpunosti opisali kodiranje skupa $\N^*$, koje ćemo kasnije koristiti na brojnim mjestima. Što možemo njime? Rekli smo da nam kodiranje omogućuje rad s kodiranim skupom kao \emph{klasom}, gdje konstruktori i komponente čine podlogu za sve ostale metode. Striktno, ulogu konstruktora za $\N^*$ igra familija funkcija $\f{Code}^k,k\in\N_+$, dinamizirana kroz operator povijesti, a ulogu komponenata funkcije $\f{lh}$ i $\f{part}$. Ideju da sad sve metode klase $\N^*$ možemo napisati pomoću tih funkcija, možemo shvatiti kao da je $\N^*$\! \emph{apstraktni tip podataka}, čija konkretna implementacija (umnožak prim-brojeva potenciranih sljedbenicima elemenata niza) nam nije bitna, dok god koristimo $\langle\cdots\rangle$ odnosno $\overline{\cdots}$ te $\f{lh}$ i $\f{part}$ prema njihovoj specifikaciji. Pogledajmo jedan primjer.

\begin{primjer}[{name=[konkatenacija konačnih nizova]}]\label{pr:concat}
\emph{Konkatenacija} je preslikavanje  $concat:\N^*\times\N^*\to\N^*$, zadano s
\begin{equation}
    concat\bigl((x_1,x_2,\dotsc,x_k),(y_1,y_2,\dotsc,y_l)\bigr):=(x_1,x_2,\dotsc,x_k,y_1,y_2,\dotsc,y_l)\text.
\end{equation}
Pomalo neprecizno, ali sasvim jasno, pišemo $concat(\vec x^k,\vec y^{l}):=(\vec x,\vec y)$. I ubuduće ćemo smatrati da su takvi konstrukti "spljošteni" na jednu razinu --- duljina od $(\vec x,\vec y)$ nije $2$, već $k+l$. To smo zapravo već koristili svaki put kad smo napisali npr.\ $\f{f}(\vec x,y)$.
\end{primjer}

Prateća funkcija $\N concat$ definirana je samo na $\f{Seq}\times\f{Seq}$, ali u svrhu primitivne rekurzivnosti, to shvaćamo kao parcijalnu specifikaciju. Također, njeno primitivno rekurzivno proširenje često pišemo infiksno kao operaciju $*$.

\begin{lema}[{name=[primitivna rekurzivnost konkatenacije konačnih nizova]}]\label{lm:starprn}
Postoji primitivno rekurzivna operacija $*$ takva da za sve $\vec x,\vec y\in\N^*\!$ vrijedi
\begin{equation}
    \langle\vec x\rangle*\langle\vec y\rangle=\langle\vec x,\vec y\rangle\text.
\end{equation}
\end{lema}
\begin{proof}
Zapravo, operator povijesti nam daje mogućnost pisanja "točkovne definicije" željenog konačnog niza: samo kažemo koju duljinu želimo i zadamo funkciju koja propisuje elemente. Konkretno, ovdje za duljinu želimo zbroj duljina od $\vec x$ i od $\vec y$ --- a ako operande od $*$ označimo s $x$ i $y$, prvih $k:=\f{lh}(x)$ elemenata trebaju biti dobiveni pomoću $\f{part}$ iz $x$, a preostali elementi iz $y$ (s indeksima pomaknutima za $k$).

Preciznije, definirajmo funkciju $\f G^3$ točkovno po slučajevima:
\begin{align}
    \label{eq:starG}\f G(x,y,i)&:=\begin{cases}
    x[i],&i<\f{lh}(x)\\
    y[i\dotminus\f{lh}(x)],&\text{inače}
    \end{cases}\text,
\shortintertext{i pomoću nje}
\label{eq:star}
x*y&:=\overline{\f G}\bigl(x,y,\f{lh}(x)+\f{lh}(y)\bigr)\text.
\end{align}
Sada sigurno vrijedi da je $x*y\in\f{Seq}$ (jer je vrijednost funkcije dobivene poviješću), vrijedi $t:=\f{lh}(x*y)=\f{lh}(x)+\f{lh}(y)$ te za svaki $i<t$ vrijedi $(x*y)[i]=\f G(x,y,i)$. Kako kod konačnog niza $concat(\vec x,\vec y)$ ima sva ta svojstva, kodiranje je injekcija, a konačan niz je jednoznačno zadan svojom duljinom i elementima, zaključujemo da je $x*y$ upravo $\langle concat(\vec x,\vec y)\rangle=\langle\vec x,\vec y\rangle$.

Jednadžbe~\eqref{eq:starG} i~\eqref{eq:star} mogu poslužiti kao točkovna definicija od $\f G$ i $*$ za sve $x$ i $y$, ne samo za one iz $\f{Seq}$ --- i iz toga slijedi primitivna rekurzivnost funkcije $\f G$ po teoremu~\ref{tm:grek} (primitivno rekurzivna verzija), a onda i funkcije $\overline{\f G}$ po lemi~\ref{lm:povijestrek}, pa tako i operacije $*$ dobivene iz nje kompozicijom.
\end{proof}

Zanimljivo je da smo koristili samo javno sučelje kodiranja konačnih nizova --- isti dokaz funkcionira za liste u Pythonu, koje sigurno imaju drugačiju implementaciju:
\begin{verbatim}
   >>> x, y = [2, 5, 8], [0, 3]
   >>> [x[i] if i<len(x) else y[i-len(x)] for i in range(len(x)+len(y))]
   [2, 5, 8, 0, 3]
\end{verbatim}

\subsection{Primitivna rekurzija kroz prostor i vrijeme}

Primitivna rekurzija nam omogućuje pisanje ograničenih petlji koje prate jedan podatak. Što ako ih želimo pratiti više, recimo $l$ njih? U napomeni~\ref{nap:brip} rekli smo da ćemo više izlaznih podataka reprezentirati kroz više nezavisnih algoritama, i ponekad se to doista može rastaviti: recimo, ako tražimo kumulativni zbroj i umnožak nekog niza, možemo prvo naći zbroj pa onda umnožak, zasebnim primitivnim rekurzijama. No kod kompliciranijih rekurzija algoritmi više nisu odvojivi, jer je zamislivo da sljedeće vrijednosti svih $l$ podataka ovise o prethodnim vrijednostima svih njih.

Važna situacija u kojoj se taj fenomen pojavljuje je simulacija kompliciranih (npr.\ univerzalnih) modela izračunljivosti, primitivnom rekurzijom kroz vrijeme. Recimo, u RAM-stroju moramo pratiti registre i programski brojač. Stanje registara u koraku $n+1$ ovisi o stanju registara u koraku $n$, ali ovisi i o tome koja se instrukcija izvršava, što (za fiksni program) ovisi o vrijednosti programskog brojača. Vrijednost pak programskog brojača u koraku $n+1$ definirana je po slučajevima: najčešće je sljedbenik te vrijednosti u koraku $n$, ali pri izvršavanju instrukcije tipa $\dec$ ovisi i o stanju registra na koji ta instrukcija djeluje, u koraku $n$.

Takva ovisnost zove se \emph{simultana} primitivna rekurzija, jer moramo simultano ra\-ču\-na\-ti svih $l$ vrijednosti --- ali kodiranje $\N^*$ (zapravo samo $\N^l$) omogućuje nam da je implementiramo pomoću obične primitivne rekurzije: umjesto $l$ vrijednosti $\vec a^l$ pratimo jednu vrijednost $\langle\vec a\rangle$. Slikovito, pratimo jedan \texttt{struct} s $l$ članova.

\begin{propozicija}[{name=[o simultanoj rekurziji]}]\label{prop:simultrek}
    Neka su $k,l\in\N_+$ te neka su $\f G_1^k$, $\f G_2^k$,~\ldots, $\f G_l^k$ i $\f H_1^{k+l+1}$, $\f H_2^{k+l+1}$,~\ldots, $\f H_l^{k+l+1}$ (primitivno) rekurzivne funkcije.  Tada su funkcije $\f F_1^{k+1}$, $\f F_2^{k+1}$,~\ldots, $\f F_l^{k+1}$, zadane s
\begin{align}
    %\SwapAboveDisplaySkip
    \label{eq:simultG}\f F_i(\vec x,0)&:=\f G_i(\vec x)\text,\\
    \label{eq:simultH}
    \f F_i(\vec x,y+1)&:=\f H_i\bigl(\vec x,y,\f F_1(\vec x,y),\f F_2(\vec x,y),\dotsc,\f F_l(\vec x,y)\bigr)\text,
\end{align}
	za sve $i\in[1\mspace{-1mu}\dd l]$, također (primitivno) rekurzivne.
\end{propozicija}
\begin{proof}
Kao što smo već rekli, cilj nam je primitivnom rekurzijom prvo dobiti funkciju $\f F:=\f{Code}^l\circ(\f F_1,\f F_2,\dotsc,\f F_l)$, iz koje ćemo onda dobiti svaku $\f F_i$ kompozicijom s funkcijom $\f{part}$. Inicijalizacija: iz~\eqref{eq:simultG} imamo
\begin{equation}\label{eq:simultGd}
    \f F(\vec x,0)=\langle \f F_1(\vec x,0),\dotsc,\f F_l(\vec x,0)\rangle=\langle \f G_1(\vec x),\dotsc,\f G_l(\vec x)\rangle=:\f G(\vec x)\text,
\end{equation}
te je $\f G=\f{Code}^l\circ(\f G_1,\dotsc,\f G_l)$ (primitivno) rekurzivna kao kompozicija takvih.
	
\noindent Korak: iz~\eqref{eq:simultH} je
\begin{multline}\label{eq:simultHd}
\f F(\vec x,y+1)=\langle\f F_1(\vec x,y+1),\dotsc,\f F_l(\vec x,y+1)\rangle=\\
	=\bigl\langle\mspace{1mu}\f H_1\bigl(\vec x,y,\f F_1(\vec x,y),\dotsc,\f F_l(\vec x,y)\bigr),\dotsc,\f H_l\bigl(\vec x,y,\f F_1(\vec x,y),\dotsc,\f F_l(\vec x,y)\bigr)\bigr\rangle=\\
	=\langle\mspace{1mu}
\f H_1(\vec x,y, \f F(\vec x,y)[0], \dotsc, \f F(\vec x,y)[l-1]), \dotsc,
\f H_l(\vec x,y, \f F(\vec x,y)[0], \dotsc, \f F(\vec x,y)[l-1])\rangle\\
=:\f H\bigl(\vec x,y,\f F(\vec x,y)\bigr)
\end{multline}
te je $\f H$ (primitivno) rekurzivna kao kompozicija funkcij\=a $\f{Code}^l$, $\f H_i$, $\f{part}$, konstanti $\f C_0^{k+2}$ do $\f C_{l-1}^{k+2}$, i koordinatnih projekcija.

Jednakosti~\eqref{eq:simultGd} i~\eqref{eq:simultHd} kažu nam da je $\f F=\f G\pr\f H$, dakle funkcija $\f F$ je dobivena primitivnom rekurzijom iz (primitivno) rekurzivnih funkcija, pa je i sama (primitivno) rekurzivna.

	A onda je za svaki $i\in[1\mspace{-1mu}\dd l]$, funkcija $\f F_i$ zadana s $\f F_i(\vec x, y)=\f F(\vec x,y)[i-1]$, simbolički $\f F_i=\f{part}\circ(\f F,\f C_{i-1}^{k+1})$. To znači da su sve $\f F_i$ dobivene kompozicijom iz (primitivno) rekurzivnih funkcija $\f F$, $\f{part}$ i konstanti, pa su (primitivno) rekurzivne.
\end{proof}

\begin{napomena}[{name=[pokrate u točkovnim definicijama]}]
Gdje se u točkovnoj definiciji pojavljuje sintaksno isti izraz više puta, uvodit ćemo pokrate koje će nam omogućiti da kompliciranije izraze zapišemo lakše i preglednije. Recimo, mogli bismo zapisati~\eqref{eq:simultHd} u obliku
\begin{align*}
    \f H(\vec x,y,z)&:=\langle \f H_1(\vec a),\f H_2(\vec a),\dotsc,\f H_l(\vec a)\rangle\text,\\
    \text{uz pokratu } \vec a&:=\bigl(\vec x,y,z[0],z[1],\dotsc,z[l-1]\bigr)\text.
\end{align*}
Treba napomenuti da je to samo kraći \emph{zapis} za~\eqref{eq:simultHd}, ne uvođenje pomoćnih funkcija --- jer tada bi $\vec a$ kao funkcija trebala imati više izlaznih podataka te primati kontekst $\vec x$, $y$ i $z$ kao argumente, što bi uništilo dobar dio kratkoće zapisa.

Analogija u programskom jeziku C je korištenje preprocesora (\verb+#define+). Na neki način, uvodimo "makroe" u funkcijski jezik, ali ih nećemo formalizirati jer nam neće biti potrebni tako često, nećemo uopće koristiti makroe s parametrima (koje C-ov preprocesor podržava), a "grafičko" uvrštavanje izraza na određena mjesta u većem izrazu nije pretjerano zahtjevna operacija --- samo smanjuje preglednost, koja je zapravo jedina motivacija za uvođenje pokrata.
\end{napomena}

Dokazali smo da je moguće u primitivnoj rekurziji simultano graditi $l$ funkcija, tako da svaka sljedeća vrijednost ovisi "prostorno" o prethodnim vrijednostima različitih funkcija. Što dobijemo ako pokušamo dinamizirati taj $l$? Dobit ćemo funkciju koja ovisi o \emph{povijesti} neke druge funkcije, no najzanimljiviji je slučaj kad ovisi "vremenski" o povijesti same sebe --- kad je definirana \emph{rekurzijom s poviješću}, koja može koristiti ne samo neposredno prethodnu vrijednost, nego sve ranije.

Matematički, ako obična primitivna rekurzija odgovara običnom principu matematičke indukcije --- gdje u dokazu $\wp(n+1)$ smijemo koristiti $\wp(n)$, ali još moramo zasebno dokazati bazu $\wp(0)$ --- tada rekurzija s poviješću odgovara principu \emph{jake} indukcije --- gdje u dokazu $\wp(n)$ smijemo koristiti $\wp(m)$ za sve $m<n$, a ne trebamo odvajati bazu kao zasebni slučaj: za $n=0$ ionako nema pretpostavki $\wp(m)$ koje bismo mogli koristiti.

\begin{propozicija}[{name=[o rekurziji s poviješću]}]\label{prop:rekpov}
Neka je $k\in\N_+$ te $\f G^k$ (primitivno) rekurzivna funkcija. Tada je i funkcija $\f F^k$\!, zadana s
\begin{equation}\label{eq:rekpov}
    \f F(\vec x,y):=\f G\bigl(\vec x,\overline{\f F}(\vec x,y)\bigr)\text,
\end{equation}
također (primitivno) rekurzivna.
\end{propozicija}
Po Dedekindovu teoremu rekurzije (pogledajte~\cite[str.\ 60]{skr:VukTS} za detalje; $\overline{\f F}(\vec x,y)$ ovdje kodira $\varphi|_y$) za svaku totalnu funkciju $G^k$ postoji jedinstvena (totalna) funkcija $F^k$ koja zadovoljava jednadžbu~\eqref{eq:rekpov}. Zato u njoj možemo pisati simbol $:=$, odnosno reći da je $\f F$ \emph{definirana} rekurzijom s poviješću.
\begin{proof}
Ideja je slična kao u dokazu propozicije~\ref{prop:simultrek}, samo umjesto kodiranja fiksne mjesnosti $\f{Code}^l$ imamo dinamički operator povijesti. Dakle, trebamo dobiti $\overline{\f F}$ primitivnom rekurzijom (degeneriranom u slučaju $k=1$). Inicijalizacija: svaka povijest počinje kodom praznog niza,
\begin{equation}
    \overline{\f F}(\vec x,0)=\langle\rangle=1\text.
\end{equation}
Za korak, moramo izraziti $\overline{\f F}(\vec x,y+1)$ pomoću $\vec x$, $y$ i $z:=\overline{\f F}(\vec x,y)$ --- iako "kontrolnu varijablu" $y$ zapravo i ne trebamo jer je uvijek možemo dobiti kao $\f{lh}(z)$. Kao što smo, primjerice, operator $\sum$ mogli dobiti iteriranjem operacije $+$~\eqref{eq:sumH1} na početnoj vrijednosti $0$~\eqref{eq:sumG1}, tako operator $\overline{\cdots}$ možemo dobiti iteriranjem operacije $*$ na početnoj vrijednosti $\langle\rangle$. Dakle, vrijedi
\begin{align}
    \overline{\f F}(\vec x,y+1)&=\overline{\f F}(\vec x,y)*\langle\f F(\vec x,y)\rangle=\overline{\f F}(\vec x,y)*\bigl\langle\f G\bigl(\vec x,\overline{\f F}(\vec x,y)\bigr)\bigr\rangle\text,
\shortintertext{odnosno}
    \f H(\vec x,y,z)&:=z*\f{Code}^1\bigl(\f G(\vec x,z)\bigr)\text.
\end{align}
	Sada je funkcija $\f H$ (primitivno) rekurzivna prema lemi~\ref{lm:starprn} i propoziciji~\ref{prop:Codekprn}, pa je i $\overline{\f F}=\f C_1^{k-1}\pr\f H$ (primitivno) rekurzivna jer je dobivena primitivnom rekurzijom iz (primitivno) rekurzivnih funkcija (za $k=1$ to je degenerirana primitivna rekurzija $\overline{\f F}=1\pr\f H$, pa je $\overline{\f F}$ (primitivno) rekurzivna po propoziciji~\ref{prop:F1prn} odnosno po korolaru~\ref{kor:F1rek}). Prema~\eqref{eq:rekpov} je $\f F$ dobivena kompozicijom iz $\f G$, $\overline{\f F}$ i koordinatnih projekcija, pa je i ona (primitivno) rekurzivna.
\end{proof}

\subsection{Primjeri korištenja rekurzije s poviješću}

\begin{primjer}[{name=[primitivna rekurzivnost Fibonaccijeva niza]}]
Poznata funkcija definirana rekurzijom s poviješću je Fibonaccijev niz:
\begin{align}
%\SwapAboveDisplaySkip
    \f{Fib}(n)&:=n\text{, za  $n<2$;}\\
    \f{Fib}(n)&:=\f{Fib}(n-1)+\f{Fib}(n-2)\text{, inače.}
\end{align}
Dokažimo da je $\f{Fib}^1$ primitivno rekurzivna. Po propoziciji~\ref{prop:rekpov}, dovoljno je naći primitivno rekurzivnu funkciju $\f G$ koja prima povijest $p:=\overline{\f{Fib}}(n)$ (kod prvih $n$ vrijednosti Fibonaccijeva niza) te vraća sljedeću vrijednost $\f{Fib}(n)$. Kao što smo rekli, $n$ uvijek možemo dobiti kao $\f{lh}(p)$. Pomoću njega možemo i napisati pomoćnu funkciju za indeksiranje "s kraja" (moderni programski jezici često dozvoljavaju indeksiranje s kraja pomoću negativnih indeksa, ali mi nemamo negativne brojeve pa ćemo upotrijebiti drugu funkciju):
\begin{align}\label{eq:rpartdef}
    \f{rpart}(c,i)&:=\begin{cases}
    c[\f{lh}(c)\dotminus\f{Sc}(i)],&i<\f{lh}(c)\\
    0,&\text{inače}
    \end{cases}\text.
\intertext{Sada točkovna definicija od $\f G$ glasi:}
    \f G(p)&:=\begin{cases}
    \f{lh}(p),&\f{lh}(p)<2\\
    \f{rpart}(p,0)+\f{rpart}(p,1),&\text{inače}
    \end{cases}\text.
\end{align}
    Prema teoremu o grananju (primitivno rekurzivna verzija), funkcija $\f{rpart}$, pa onda i funkcija $\f G$, je primitivno rekurzivna, a tada je $\f{Fib}$ primitivno rekurzivna po propoziciji~\ref{prop:rekpov}, jer je dobivena rekurzijom s poviješću iz $\f G$.
\end{primjer}

Iako smo rekurziju s poviješću uveli koristeći funkcije, promatranjem karakterističnih funkcija dobivamo analogni rezultat i za relacije. Ugrubo, ako pri utvrđivanju vrijedi li $\f R(\vec x,n)$ koristimo samo istinitosti $\f R(\vec x,m)$ za $m<n$, na neki način koji čuva (primitivnu) rekurzivnost, tada je i $\f R$ (primitivno) rekurzivna. Evo jednog važnog primjera, koji će također poslužiti kao uvod u sljedeću točku, pokazujući da se mogu kodirati razni objekti --- ne samo konačni nizovi prirodnih brojeva.

\begin{primjer}[{name=[primitivna rekurzivnost skupa svih formula logike sudova]}]\label{pr:lskod}
Kodiramo formule logike sudova: propozicijsku varijablu $P_i$ kao $\langle0,i\rangle$, negaciju $\lnot\varphi$ kao $\langle1,u\rangle$ gdje je $u$ kod od $\varphi$, a kondicional $(\varphi\to\psi)$ kao $\langle2,u,v\rangle$ gdje su $u$ i $v$ kodovi od $\varphi$ i $\psi$ redom. Ostali veznici se mogu dobiti pomoću negacije i kondicionala na dobro poznat način: pogledajte~\cite{skr:VukML}. Recimo, kod varijable $P_0$ je $\langle0,0\rangle=2^1\cdot3^1=6$, a kod formule $(P_0\to P_0)$ je \begin{equation}
    \langle2,6,6\rangle=2^3\cdot3^7\cdot5^7=1\,366\,875\,000\text.
\end{equation}

Ovakva vrsta kodiranja, gdje se tip zapisuje na početku kao element nekog početnog komada od $\N$ (tzv\!.\ \texttt{enum}), a nakon njega ostali podaci ili kodovi (koji odgovaraju \emph{pokazivačima} na podatke kod rekurzivno definiranih struktura), česta je u računarstvu. U imperativnim jezicima (Pascal, Ada,~\ldots) obično se koristi pojam \emph{variant record}, a u funkcijskima (Haskell, Scala,~\ldots) pojam \emph{algebraic data type}. Recimo, u Haskellu bi deklaracija tog tipa izgledala ovako:
\begin{equation}
\texttt{data PF = PropVar Integer | Not PF | Implies PF PF}
\end{equation}
i reprezentacija elementa takvog tipa u memoriji računala bila bi vrlo slična kodiranju koje smo mi napravili. Još jedan primjer, koji nije rekurzivno zadan pa ne treba "pokazivače", vidjet ćemo na početku sljedeće točke.

Može se vidjeti da je to kodiranje injekcija, jer je kompozicija dvije injekcije: prva se dobije tako da "zamijenimo šiljate zagrade oblima", pa dobijemo elemente od $\N^*$, a druga je kodiranje $\N^*$. Ova druga je injekcija prema propoziciji~\ref{prop:codeinj}, ali zašto je prva injekcija? Ako su dvije formule različitih tipova (recimo, jedna je propozicijska varijabla, a druga negacija), preslikavaju se u konačne nizove s različitim prvim elementom. No ako su istog tipa, zapravo trebamo provesti neku indukciju po složenosti formule da bismo dokazali injektivnost. (Pokušajte --- to je dobra vježba.) Uostalom, i sama definicija je rekurzivna po izgradnji formula: recimo, u kodiranju $\lnot\varphi$ pretpostavljamo da već imamo kod od $\varphi$.

Pokušajmo sada dokazati da je slika tog kodiranja (nazovimo je $\f{PF}$) primitivno rekurzivna. Karakterističnu funkciju te slike, $\chi_{\f{PF}}$, definirat ćemo rekurzijom s poviješću. Kao i prije, trebamo naći primitivno rekurzivnu funkciju $\f G$ koja prima povijest $\overline{\chi_{\f{PF}}}(n)$ i vraća je li $n$ kod formule logike sudova. Kako vraća $0$ ili $1$ ($bool$), $\f G$ možemo shvatiti kao karakterističnu funkciju: $\f G=\chi_{\f R}$, gdje je
\begin{equation}
    \f R(p)\Longleftrightarrow\text{"$n:=\f{lh}(p)$ je kod neke formule logike sudova".}
\end{equation}
	Dakle, pretpostavimo da imamo $n$ i razmislimo kako bismo odlučili je li kod neke formule --- propozicijske varijable, ili negacije, ili kondicionala. Prvi disjunkt možemo napisati kao $\exists i\,(n\eq\langle0,i\rangle)$, što nije dovoljno dobro jer je kvantifikacija neograničena. Kako je ograničiti? Ključno je da je \textbf{svaki element konačnog niza manji od koda tog niza}:
\begin{equation}\label{eq:elem<kod}
    x_i<x_i+1<2^{x_i+1}\!=p_0^{x_i+1}\!\le p_i^{x_i+1}\!\le(\cdots)\cdot p_i^{x_i+1}\!\cdot(\cdots)=\langle\,\dotsc,x_i,\dotsc\rangle\text.
\end{equation}
Dakle, ako postoji takav $i$, on je sigurno manji od $n$, pa prvi disjunkt možemo napisati u obliku ograničene kvantifikacije $(\exists i<n)(n\eq\langle0,i\rangle)$, što je primitivno rekurzivno.

    Za drugi disjunkt, opet možemo napisati $\exists u\bigl(n\eq\langle1,u\rangle\,\land\,\f{PF}(u)\bigr)$, i kao i prije možemo ograničiti kvantifikaciju na $(\exists u<n)$, ali što ćemo s rekurzivnim pozivom $\f{PF}(u)$? Njegovu istinitost izvući ćemo iz povijesti $p$, u kojoj su zapisane sve vrijednosti karakteristične funkcije $\chi_{\f{PF}}$ na brojevima manjim od $n$. Dakle, drugi disjunkt je
\begin{equation}
    (\exists u<n)\bigl(n\eq\langle1,u\rangle\land p[u]\eq1\bigr)\text,
\end{equation}
što je primitivno rekurzivno. Analogno bismo dobili i treći disjunkt (s dvije ograničene kvantifikacije),  primitivno rekurzivan dvostrukom primjenom propozicije~\ref{prop:okvantrek} (i brojnih drugih rezultata koji pokazuju da je kvantificirana relacija primitivno rekurzivna).

Tada je $\f R$ primitivno rekurzivna kao disjunkcija tri primitivno rekurzivne relacije (propozicija~\ref{prop:skupl}), što znači da je njena karakteristična funkcija $\f G=\chi_{\f R}$ primitivno rekurzivna. I~za kraj, prema propoziciji~\ref{prop:rekpov}, $\chi_{\f{PF}}$ je tada primitivno rekurzivna, dakle $\f{PF}^1$ je primitivno rekurzivna relacija.
\end{primjer}

\section{Kodiranje RAM-modela izračunljivosti}

Napokon imamo dovoljno alata da možemo proći kroz točku~\ref{sec:RAMizr} i sve bitno u njoj kodirati prirodnim brojevima. Tako ćemo dobiti mogućnost simulacije rada RAM-stroja primitivno rekurzivnim funkcijama, a time i parcijalnu rekurzivnost RAM-izračunljivih funkcija. Krenimo redom: prvo su na redu RAM-instrukcije.

%\subsection{Kodiranje instrukcija i programa}

Dok još nije dio RAM-programa, instrukcija ima samo tip (\inc, \dec\ ili \goto) te, ovisno o tipu, adresu registra na koji djeluje, i\slash ili odredište (na koje zasad nema nikakvih uvjeta). Posljednje dvoje već jesu prirodni brojevi, a tip instrukcije možemo kodirati na način standardan za konačne skupove: fiksiramo neki poredak. Konkretno, uzet ćemo kodiranje koje preslikava $\inc\mapsto0$, $\dec\mapsto\mspace{-1mu}1$ i $\goto\mapsto2$, kao da smo deklarirali
\begin{equation}\label{eq:enumIns}
\texttt{enum ins\_type \string{ INC, DEC, GOTO \string};}
\end{equation}
u programskom jeziku C --- time smo dobili injekciju s $\mathscr Ins$ u $\N^*$, čije kodiranje već imamo. Sličnu stvar smo već napravili manje formalno u dokazu leme~\ref{lema:alef0ins}: disjunktifikacija unije skupova $A$ i $B$ u obliku $\{0\}\times A\cup\{1\}\times B$, koju poznajemo iz teorije skupova, upravo odgovara ovakvom kodiranju.

\begin{definicija}[{name=[kodiranje skupa $\mathscr Ins$]}]\label{def:kodIns}
    Za proizvoljnu RAM-instrukciju $I$, definiramo \emph{kod instrukcije} $\N\mathscr Ins(I)=:\kins{I}$, jednadžbama:
\begin{alignat*}{3}
\SwapAboveDisplaySkip
    \kins{\incr j\!}&:=\langle0,j\rangle&\;=\;&&\f{codeINC}(j)&=6\cdot3^j\text,\\
    \kins{\decr jl}&:=\langle1,j,l\rangle&\;=\;&&\f{codeDEC}(j,l)&=60\cdot3^j\cdot5^l\text,\\
    \kins{\goto\;l}&:=\langle2,l\rangle&\;=\;&&\f{codeGOTO}(l)&=24\cdot3^l\text,
\end{alignat*}
za sve $j,l\in\N$.
\end{definicija}
U desnom stupcu napisani su konstruktori kao aritmetički izrazi, iz kojih se vide neka njihova brojevnoteorijska svojstva, i kao primitivno rekurzivne funkcije od $j$ i\slash ili $l$. Injektivnost kodiranja $\kins{\cdots}$ slijedi iz definicije~\ref{def:ins} i propozicije~\ref{prop:codeinj}. Da mu je slika $\f{Ins}:=\im{\,\kins{\cdots}}$ primitivno rekurzivna, možemo vidjeti standardnom tehnikom "pokušaja rekodiranja iz komponenti", kao u dokazu korolara~\ref{kor:Seqprn}, ili u primjeru~\ref{pr:lskod}.
Komponente $j$ odnosno $l$ te tip definiramo kroz dvije funkcije i tri relacije.

\begin{lema}[{name=[primitivna rekurzivnost slike kodiranja RAM-instrukcija]}]\label{lm:InsTYPEprn}
    Skupovi $\f{InsINC}$, $\f{InsDEC}$ i $\f{InsGOTO}$, kodova instrukcija pojedinog tipa,\\
	kao i skup svih kodova instrukcija $\f{Ins}$, primitivno su rekurzivni.
\end{lema}
\begin{proof}
Tvrdimo da je
\begin{align}
\SwapAboveDisplaySkip
    \label{eq:InsINC3}\f{InsINC}(i)&\Longleftrightarrow i\eq\f{codeINC}(i[1])\text,\\
    \label{eq:InsDEC3}\f{InsDEC}(i)&\Longleftrightarrow i\eq\f{codeDEC}(i[1],i[2])\text,\\
    \label{eq:InsGOTO3}\f{InsGOTO}(i)&\Longleftrightarrow i\eq\f{codeGOTO}(i[1])\text.
\end{align}
    Dokazujemo samo~\eqref{eq:InsINC3}; ostale ekvivalencije su sasvim analogne.
	
	Za smjer $(\Rightarrow)$, ako je $i$ kod instrukcije tipa $\inc$, recimo $i=\kins{\incr j\!}$, tada po definiciji~\ref{def:kodIns} vrijedi $i=\f{codeINC}(j)=\langle0,j\rangle$, pa je $j=\langle0,j\rangle[1]=i[1]$ po propoziciji~\ref{prop:lhpartprn}\eqref{stav:part<k}. % Štoviše, svaki element niza je manji od koda tog niza~\eqref{eq:elem<kod}, pa je $j=i[1]<i$ --- odnosno mogli smo ograničiti kvantifikaciju.

    Za smjer $(\Leftarrow)$, očito je $i=\f{codeINC}(i[1])=\kins{\incr{i[1]}\!}$ kod instrukcije tipa $\inc$.

    Primitivna rekurzivnost skupa $\f{Ins}=\f{InsINC}\cup\f{InsDEC}\cup\f{InsGOTO}$ slijedi iz propozicije~\ref{prop:skupl}.
\end{proof}

\begin{lema}[{name=[primitivna rekurzivnost komponenata instrukcije]}]\label{lm:regndestprn}
    Definiramo $\f{regn}(t)$ kao adresu registra na koji djeluje instrukcija koda $t$, ako takva postoji i djeluje na neki registar, a $0$ inače. Analogno definiramo $\f{dest}(t)$ za odredište. Funkcije $\f{regn}^1$ i $\f{dest}^1$ su primitivno rekurzivne.
\end{lema}
\begin{proof}
    Iz dokaza leme~\ref{lm:InsTYPEprn} odmah se vidi da ako je $t$ kod instrukcije tipa $\inc$, adresa njenog registra je $t[1]$. Ako je tipa $\dec$, adresa registra je i dalje $t[1]$, a odredište je $t[2]$. Ako je tipa $\goto$, odredište je $t[1]$.
    Koristeći tu činjenicu i teorem o grananju (primitivno rekurzivnu verziju), odmah pišemo točkovne definicije:
\begin{equation}
    \f{regn}(t)=\begin{cases}
    t[1],&\f{InsINC}(t)\lor\f{InsDEC}(t)\\
    0,&\text{inače}
    \end{cases}\text,\qquad
    \f{dest}(t)=\begin{cases}
    t[2],&\f{InsDEC}(t)\\
    t[1],&\f{InsGOTO}(t)\\
    0,&\text{inače}
    \end{cases}\text.
\end{equation}
Ako bolje pogledamo, napisane jednakosti su "obrnuto" napisana definicija~\ref{def:kodIns}.
\end{proof}

% \subsection{Kodiranje RAM-programa}

%Kao što smo najavili, programe kodiramo kao konačne nizove instrukcija.

\begin{definicija}[{name=[kodiranje skupa $\mathscr Prog$]}]\label{def:kodProg}
Za proizvoljni RAM-program
$P:=\begin{prog}
t.&I_t
\end{prog}_{t<n}$
definiramo \emph{kod programa} $P$ kao
	$\kprog P:=\N\mathscr Pr\mspace{-1mu}o\mspace{-2mu}g(P):=\langle\kins{I_0\!},\kins{I_1\!},\dotsc,\kins{I_{n-1}\!}\rangle$.
\end{definicija}

To je također kodiranje, iako bismo za konstruktore trebali napraviti dinamičke \emph{generatore koda} (jer većina programskih konstrukcija koje smo napravili nemaju fiksnu, statičku duljinu), koji primaju izračunljivu funkciju koja za svaki $i<n$ daje kod instrukcije s rednim brojem~$i$. To se može napraviti sasvim općenito, i vidjeti da su sve konstrukcije programa koje smo dosad sreli (i koje ćemo još sresti u nastavku) primitivno rekurzivne, ali dva su razloga zašto to nećemo raditi.

Prvo, makroi kompliciraju stvar: većinu zanimljivih programa (recimo, one za računanje kompozicije, primitivne rekurzije i minimizacije) nismo napisali kao RAM-programe, nego kao makro-programe. Mogli bismo kodirati makroe kao zaseban tip instrukcija (prirodno se nameće $\kins{P^*}:=\langle3,\kprog{P}\rangle$ kao logičan nastavak definicije~\ref{def:kodIns}) i onda dobiti spljoštenje kao primitivno rekurzivnu funkciju $\f{flat}^1$ na kodovima, ali~\ldots\ postoji i drugi razlog, a taj je da je takvo razmišljanje u potpunoj općenitosti nepotrebno. Kad dokažemo univerzalnost našeg modela, vidjet ćemo da možemo jednu jednostavnu transformaciju programa --- specijalizaciju --- napraviti kao primitivno rekurzivnu funkciju, a sve ostale transformacije pomoću nje.

%Ipak, možemo vidjeti jedan jednostavni primjer.

\begin{primjer}[{name=[primitivna rekurzivnost generatora koda za konstantne funkcije]}]\label{pr:kodkonst}
U dokazu teorema~\ref{tm:alef0izr} napisali smo RAM-pro\-gra\-me $P_n$~\eqref{eq:konstRAM} koji računaju konstantne funkcije. Za svaki $n$ možemo izračunati kod tog programa, tako da je preslikavanje $n\mapsto\kprog{P_n}$ primitivno rekurzivno. Doista, svaka instrukcija u tim programima je $\incr0$, s kodom $\f{codeINC}(0)=6$, pa je
\begin{equation}
    \kprog{P_n}=\langle6,6,\dotsc,6\rangle\text{ [$n$ šestica]}=\langle \f C_6(0),\f C_6(1),\dotsc,\f C_6(n-1)\rangle=\overline{\f C_6}(n)\text.
\end{equation}
$\overline{\f C_6^1}$ je primitivno rekurzivna po propoziciji~\ref{prop:konst} i lemi~\ref{lm:povijestrek}.
    Isto možemo dobiti dinamizacijom ove šestice kao u primjeru~\ref{pr:IdinC}, ili čak potenciranjem primorijela: $\kprog{P_n}=\overline{\f I_1^2}(6,n)=\bigl(\overline{\f Z}(n)\bigr)^7$ --- vidite li zašto?
\end{primjer}

\begin{primjer}[{name=[kod spljoštenja programa $Q$]}]\label{pr:Qflatkod}
%Evo i jednog statičkog primjera:
	U primjeru~\ref{pr:flat} naveden je RAM-program $Q^\flat$~\eqref{eq:Qflat}, čiji je kod%. Njegov kod, koji ćemo koristiti i kasnije u primjerima, je
	\begin{gather*}\renewcommand{\qedsymbol}{}
e_Q:=\kprog{Q^\flat}=\langle\kins{\decr12},\kins{\goto\;0},\kins{\decr22},\kins{\decr16},\kins{\incr0},\dotsc,\kins{\goto\;9}\rangle={}\\
    =\langle\langle1,1,2\rangle,\langle2,0\rangle,\langle1,2,2\rangle,\langle1,1,6\rangle,\langle0,0\rangle,\langle2,3\rangle,\langle1,2,9\rangle,\langle0,0\rangle,\langle2,6\rangle,\langle1,3,12\rangle,\langle0,0\rangle,\langle2,9\rangle\rangle=\\
		=\langle4\,500, 24, 13\,500, 2\,812\,500, 6, 648, 1\,054\,687\,500,
	6, 17\,496, 395\,507\,812\,500, 6, 472\,392\rangle={}\\
       2^{4501}
		\mathord{\cdot\,}  3^{25}
		\mathord{\cdot\,}  5^{13501}
		\mathord{\cdot\,}  7^{2812501}
		\mathord{\cdot\,} 11^{7}
		\mathord{\cdot\,} 13^{649}
		\mathord{\cdot\,} 17^{1054687501}
		\mathord{\cdot\,} 19^{7}
		\mathord{\cdot\,} 23^{17497}
		\mathord{\cdot\,} 29^{395507812501}
		\mathord{\cdot\,} 31^{7}
		\mathord{\cdot\,} 37^{472393}\text.\qedhere
	%\renewcommand{\qedsymbol}{\relax}
\end{gather*}
%Taj kod ćemo koristiti u kasnijim primjerima.
\end{primjer}

Injektivnost preslikavanja $\kprog{\cdots}$ slijedi iz injektivnosti od $\kins{\cdots}$ i $\langle\cdots\rangle$: dva različita programa se razlikuju ili po duljini (pa njihovi kodovi imaju različit $\f{lh}$), ili u nekoj instrukciji, recimo onoj na rednom broju $i$ (pa njihovi kodovi imaju različit $\f{part}$ na mjestu $i$, jer je kodiranje instrukcij\=a injektivno).

\begin{lema}[{name=[primitivna rekurzivnost slike kodiranja RAM-programa]}]
	Slika kodiranja RAM-programa, $\f{Prog}^1:=\,\im{\N\mathscr P\mspace{-1mu}r\mspace{-2mu}o\mspace{-2mu}g}=\{\kprog P\mid P\in\mathscr Pr\mspace{-1mu}o\mspace{-2mu}g\}$,\\ primitivno je rekurzivna.
\end{lema}
\begin{proof}
Za RAM-program treba specificirati da se radi o konačnom nizu instrukcija, čija su odredišta (ako postoje) manja ili jednaka duljini programa:
\begin{equation}\label{eq:Progget}
    \f{Prog}(e)\Longleftrightarrow\f{Seq}(e)\wedge\bigl(\forall i<\f{lh}(e)\bigr)\bigl(\f{Ins}(e[i])\land\f{dest}(e[i])\le \f{lh}(e)\bigr)\text.\\
\end{equation}
Ovdje koristimo činjenicu da je $\f{dest}(t)\eq0$ ako instrukcija koda $t$ nema od\-re\-di\-šte, a uvijek je $0\le\f{lh}(e)$. Marljiva evaluacija od $\land$ (odnosno $\f{mul}^2$) znači da će se $\f{lh}(e)$ uvijek izračunati, čak i kad $e$ nije kod konačnog niza, ali rezultat čitavog izraza će tada sigurno biti $\mathit{false}$ (odnosno $0$), a nećemo zapeti u beskonačnoj petlji jer je $\f{lh}$ totalna. Izračunavanje će biti dulje jer nemamo \emph{shortcircuiting}, ali izračunljivost se neće promijeniti.
\end{proof}

%Za kodiranje programa ne koristimo nikakve posebne komponente osim onih koje već imamo za konačne nizove: $\f{lh}(e)$ za duljinu programa te $e[i]$ za dohvaćanje instrukcije rednog broja $i$. Uostalom, već smo ih koristili u~\eqref{eq:Progget}.

%Samo još napomenimo da kodove RAM-programa obično označavamo slovom $e$. To je neka blaga vrsta "mađarske notacije", ponekad korištene u programiranju, u kojoj iz oblika imena zaključujemo tip vrijednosti koju tim imenom reprezentiramo.

%I to je sve što se programa tiče. Spremni smo za idući korak.

\subsection{Kodiranje stanja registara i RAM-konfiguracija}

Konfiguraciju RAM-stroja smo definirali kao jednu funkciju, ali zapravo je jasno da trebamo pratiti dvije odvojene stvari: stanje registara i vrijednost programskog brojača. Vrijednost programskog brojača već jest prirodan broj pa je ne kodiramo, odnosno kodiramo je identitetom. Sa stanjem registara imamo više posla.

Na prvi pogled, skup svih mogućih stanja registara ne možemo uopće kodirati jer je neprebrojiv: imamo prebrojivo mnogo registara, svaki može sadržavati jednu od prebrojivo mnogo vrijednosti, a $\aleph_0^{\aleph_0}\!=\mathfrak c>\aleph_0$. Ipak, definicija~\ref{def:RAMconf} kaže da promatramo samo konfiguracije s konačnim nosačem --- i to je doista dovoljno. Naime, početna konfiguracija (bilo kojeg RAM-stroja s bilo kojim ulazom) je $0$ na svim registrima osim najviše $k$ ulaznih, a u svakom koraku izračunavanja se nosač može povećati najviše za jedan element --- izvršavanjem instrukcije tipa $\inc$ na registru čiji je sadržaj bio $0$.

Iz teorije skupova znamo da nizova prirodnih brojeva s konačnim nosačem ima prebrojivo mnogo, no kako ih kodirati? Jedna elegantna metoda koristi istu ideju kao za konačne nizove, samo bez sljedbenika eksponenata. Dakle, za proizvoljni niz prirodnih brojeva s konačnim nosačem $(r_0,r_1,r_2,\dotsc,0,0,0,\dotsc)$ definiramo kod kao
\begin{equation}\label{eq:defkreg}
    \knk{r_0,r_1,r_2,\dotsc,0,0,0,\dotsc}:=\prod_{i\in\N}p_i^{r_i}\,\text.
\end{equation}
Zbog konačnosti nosača samo konačno mnogo eksponenata je pozitivno (svi ostali su~$0$) pa samo konačno mnogo prim-brojeva sudjeluje u produktu.

Važno je da takvo kodiranje stanja registara ne ovisi o konkretnom RAM-stroju odnosno programu. Alternativno bismo mogli naći širinu programa $m_P$ pa kodirati stanje kao konačan niz registara do $\reg{m_P}$\! --- ali to bi ovisilo o programu: dodavanje potpuno irelevantnih instrukcija koje se možda uopće ne mogu izvršiti (\emph{unreachable code}\/) moglo bi promijeniti kod stanja registara za isto izračunavanje (isti niz konfiguracija) pa kodiranje ne bi bilo funkcija.

Treba nam jedan važan konstruktor, a to je %\emph{proširenje nulom} zadanog konačnog niza. Kako već imamo kodiranje konačnih nizova, možemo ga definirati na kodovima.
početna konfiguracija RAM-stroja s ulazom $\vec x$ (prenesenim preko koda, jer želimo imati jednu funkciju za sve mjesnosti).

\begin{lema}[{name=[primitivna rekurzivnost generatora početne konfiguracije]}]\label{lm:startprn}
    Postoji primitivno rekurzivna funkcija $\f{start}^1$ %\!, s parcijalnom specifikacijom:
	takva da za svaki neprazni konačni niz $\vec x\in\N^+$ vrijedi $\f{start}(\langle\vec x\rangle)=\knk{0,\vec x,0,0,0,\dotsc}$.
\end{lema}
\begin{proof}
Samo treba napisati rastav na prim-faktore:
\begin{equation}
    \f{start}(x):=\;\prod_{i=0}^{\mathclap{\f{lh}(x)-\!1}}p_{i+1}^{x[i]}=\;\prod_{\mathclap{i\,<\,\f{lh}(x)}}\f{pow}\bigl(\f{prime}\bigl(\f{Sc}(i)\bigr),\f{part}(x,i)\bigr)\text.
\end{equation}
Sada primitivna rekurzivnost slijedi iz propozicija~\ref{pp:primeprn} i~\ref{prop:lhpartprn}, leme~\ref{lm:sumprodrek} i primjera~\ref{pr:addmulpow}.\\
	Prim-brojevi su pomaknuti jer adrese ulaznih registara počinju od $1$.
\end{proof}

Funkcija $\f{start}$ nije injekcija: recimo, $\f{start}(\langle2,1\rangle)=\f{start}(\langle2,1,0,0\rangle)=\knk{0,2,1,0,0,\dotsc}$, odnosno $\f{start}(72)=\f{start}(2520)=45$. Ali preslikavanje $\knk{\cdots}$ jest injekcija (kao što kodiranje i treba biti), po osnovnom teoremu aritmetike. Također po osnovnom teoremu aritmetike, slika mu je $\im{\knk{\cdots}}=\N_+$, primitivno rekurzivna po primjeru~\ref{pr:N+prn}.

Što se komponenata tiče, $\f{lh}$ nema smisla, a za indeksiranje služi funkcija $\f{ex}$ iz leme~\ref{lm:exprn}. Doista, $\f{ex}(\knk{r_0,r_1,\dotsc,0,0,\dotsc},i)=r_i$, jer je to upravo eksponent od $p_i$ u tom kodu. Koristit ćemo je za očitavanje rezultata (sadržaja registra $\reg0$) iz završne konfiguracije.
\begin{equation}\label{eq:resultdef}
    \f{result}(c):=\f{ex}(c,0)
\end{equation}

Za s\=amo izvršavanje instrukcija na registrima, koristit ćemo množenje odnosno dijeljenje s $p_j$ za inkrement odnosno dekrement registra $\reg j$. Jasno je da time povećavamo odnosno smanjujemo eksponent odgovarajućeg prim-broja za $1$. Konkretno
\begin{align}
\label{eq:knkppj}\knk{r_0,r_1,\dotsc,r_{j-1},r_j+1,r_{j+1},r_{j+2},\dotsc,0,0,\dotsc}
&=
\knk{r_0,r_1,\dotsc,0,0,\dotsc}\cdot p_j\text,
    \\\intertext{i odmah iz toga (za $r_j>0$)}
\label{eq:knkkpj}\knk{r_0,r_1,\dotsc,r_{j-1},r_j-1,r_{j+1},r_{j+2},\dotsc,0,0,\dotsc}
&=
\knk{r_0,r_1,\dotsc,0,0,\dotsc}\div p_j\text.
\end{align}
%(jasno, \eqref{eq:knkkpj} vrijedi samo ako je $r_j>0$).

Sada možemo kodirati dokaz leme~\ref{lema:ramdet}: za preslikavanje $nextconf$ koje konfiguraciju RAM-stroja preslikava u "sljedeću" konfiguraciju (u koju ova prelazi), konstruirat ćemo $\N nextconf$ kao izračunljivu funkciju. Ona ima dva izlaza, pa ćemo je reprezentirati kroz dvije primitivno rekurzivne funkcije --- koje će primati trenutnu instrukciju $I_{c(\textsc{pc})}$ kao da ona uvijek postoji, a završnim konfiguracijama ćemo se baviti kasnije.

\begin{lema}[{name=[primitivna rekurzivnost prijelaza između RAM-konfiguracija]}]\label{lm:NextRegCountprn}
	Za proizvoljnu RAM-konfiguraciju $c$, označimo kod stanja njenih registara s $c[\reg{}]:=\knk{c(\reg0),c(\reg1\mspace{-2mu}),\dotsc}$. Tada postoje primitivno rekurzivne funkcije $\f{NextReg}^2$ i $\f{NextCount}^3$ takve da za svaku RAM-instrukciju $I$, i za sve RAM-kon\-fi\-gu\-ra\-ci\-je $c$ i $d$ takve da $c\leadsto d$ po instrukciji $I$, vrijedi
\begin{align}
	\SwapAboveDisplaySkip
	\f{NextReg}\bigl(\kins{I},c[\reg{}]\bigr)&=d[\reg{}]\text{, i}\\
	\f{NextCount}\bigl(\kins{I},c[\reg{}],c(\textsc{pc})\bigr)&=d(\textsc{pc})\text.
\end{align}
\end{lema}
\begin{proof}
	Označimo argumente s $i:=\kins{I}\in\f{Ins}$, $r:=c[\reg{}]\in\N_+$ te $p:=c(\textsc{pc})\in\N$.

$\f{NextReg}$ treba pomnožiti ili podijeliti (ako je djeljiv) $r$ s $p_j$, ako $I$ djeluje na $\reg j$ --- ili ga ostaviti na miru, u suprotnom. $\f{NextCount}$ treba inkrementirati $p$ ako je $I$ promijenila neki registar, ili ga postaviti na njeno odredište ako nije.
\begin{align}
%\SwapAboveDisplaySkip
    \label{eq:NextRegdef}\f{NextReg}(i,r)&:=\begin{cases}
	    r\cdot pj,&\f{InsINC}(i)\Longleftrightarrow:Up\\
	    r\div pj,&\f{InsDEC}(i)\land pj\mid r\Longleftrightarrow:Down\\
    r,&\text{inače}
    \end{cases}%\text,
\\
    \f{NextCount}(i,r,p)&:=\begin{cases}
    \f{Sc}(p),&Up\lor Down\\
    \f{dest}(i),&\text{inače}
    \end{cases}%\text,
\\
\text{uz pokratu }
pj&:=\f{prime}\bigl(\f{regn}(i)\bigr)%\text,
%\\
%Up&:\Longleftrightarrow\f{InsINC}(i)%\text,
%\\
%Down&:\Longleftrightarrow\f{InsDEC}(i)\land pj\mid r%\text.
\end{align}
Uvjeti $Up$ i $Down$ su disjunktni jer su već $\f{InsINC}$ i $\f{InsDEC}$ disjunktni ($i[0]$ ne može istovremeno biti $0$ i $1$). Također, uvjeti su primitivno rekurzivni, kao i pojedine grane funkcij\=a $\f{NextReg}$ i $\f{NextCount}$, pa su one primitivno rekurzivne po teoremu~\ref{tm:grek}.

	Za parcijalnu specifikaciju, neka su $I$ i $c$ (odnosno $i$, $r$ i $p$) kao na početku dokaza. Tvrdimo: $\f{NextReg}(i,r)$ i $\f{NextCount}(i,r,p)$ kodiraju konfiguraciju u koju $c$ prelazi po $I$.

Ako je $I$ tipa $\inc$, recimo $I=(\incr j)$, tada vrijedi $Up$ i $pj=\f{prime}(j)=p_j$, pa je $r'=r\cdot p_j$, što prema~\eqref{eq:knkppj} kodira upravo stanje registara nakon izvršavanja $I$.

Ako je $I$ tipa $\goto$, recimo $I=(\goto\;l)$, tada ne vrijedi ni $Up$ ni $Down$ pa je $r'=r$, a $p'=\f{dest}(i)=\f{dest}(\kins{\goto\;l})=l$, kao što i treba biti.

	Ako je pak $I$ tipa $\dec$, recimo $I=(\decr jl)$, tada je opet $pj=p_j$ te $Up$ ne vrijedi, a $Down\Leftrightarrow p_j\mid r=c[\reg{}]\Leftrightarrow c(\reg j)>0$. Ako to vrijedi, $p'=p+1$ i $r'=r\div p_j$, a inače, $p'=\f{dest}(\kins{\decr jl})=l$ i $r'=r$, što i treba biti po semantici instrukcije tipa $\dec$.
\end{proof}

\subsection{Kodiranje RAM-izračunavanja po koracima}

Sada raspolažemo svime potrebnim da bismo kodirali postupak iz\-ra\-ču\-na\-va\-nja kao niz konfiguracija. Konkretno, neka je $P^k$ RAM-algoritam te $\vec x\in\N^k$ ulaz za njega. Htjeli bismo konstruirati izračunljivu funkciju koja prima $k\in\N_+$, $\vec x\in\N^k$ i $P\in\mathscr Pr\mspace{-1mu}o\mspace{-2mu}g$ te vraća niz $(c_n)_{n\in\N}$ koji predstavlja $P$-izračunavanje s $\vec x$.

Izrazimo taj zadatak preko brojevnih funkcija. Umjesto $\vec x$ i $P$ prenijet ćemo njihove kodove $x:=\langle\vec x\rangle\in\f{Seq}':=\f{Seq}\setminus\{\langle\rangle\}$ i $e:=\kprog{P}\in\f{Prog}$. Tada ne treba prenositi $k$ jer ga uvijek možemo odrediti kao $\f{lh}(x)$. No kako vratiti niz? Nizova konfiguracij\=a ima neprebrojivo mnogo, pa moramo malo modificirati sučelje.
%Skup kodova stanja registara je $\im{\knk{\cdots}}=\N_+$, a skup "kodova" vrijednosti programskog brojača je $\N$ (zapravo $[0\dd\f{lh}(e)]$, ali želimo imati jednu kodomenu za sve $e\in\f{Prog}$), dakle skup kodova konfiguracija je $\N_+\!\times\N$, a skup kojem pripadaju izračunavanja je onda skup nizova $(\N_+\!\times\N)^\N$. Preslikavanje koje konstruiramo tada je element skupa
%\begin{equation}
%    \bigl((\N_+\!\times\N)^\N\bigr)^{\f{Seq}'\times\f{Prog}}\cong
%    (\N_+\!\times\N)^{\f D}\cong\N_+^{\f D}\times\N^{\f D}\text,
%\end{equation}
%gdje smo označili $\f D:=\f{Seq}'\times\f{Prog}\times\N$ --- dakle zapravo želimo dvije tromjesne funkcije s ulaznim podacima $(x,e,n)\in\f D$, gdje je $n$ broj koraka izračunavanja koje smo napravili.
Ukratko, nizove vraćamo "točkovno" tako da zapravo vraćamo njihove članove, dodavši indeks u nizu kao još jedan ulazni podatak --- a algoritam s dva izlazna podatka (k\=od stanja registara i vrijednost programskog brojača) po napomeni~\ref{nap:brip} shvaćamo kao dva algoritma s istim ulaznim podacima. %Sada je još samo potrebno proširiti te funkcije do totalnih tako da budu primitivno rekurzivne.

\begin{lema}[{name=[primitivna rekurzivnost RAM-izračunavanja]}]\label{lm:RegCountprn}
Postoje primitivno rekurzivne funkcije $\f{Reg}^3$ i $\f{Count}^3$, čija parcijalna specifikacija glasi:
za svaki RAM-program $P$, za svaki neprazni konačni niz $\vec x$, za svaki prirodni broj $n$, $\f{Reg}(\langle \vec x\rangle,\kprog{P},n)$ je kod stanja registara, a $\f{Count}(\langle \vec x\rangle,\kprog{P},n)$ je vrijednost programskog brojača, nakon $n$ koraka $P$-izračunavanja s $\vec x$.
\end{lema}
\begin{quote}
Preciznije, ako je $P$-izračunavanje s $\vec x$ niz RAM-konfiguracij\=a $(c_n)_{n\in\N}$,\\ tada je $\f{Reg}(\langle\vec x\rangle, \kprog{P},n)=c_n[\reg{}]$ te $\f{Count}(\langle\vec x\rangle,\kprog{P},n)=c_n(\textsc{pc})$.
\end{quote}
\begin{proof}
    To što smo razdvojili reprezentaciju izračunavanja na dvije funkcije ne znači da ih možemo računati odvojenim algoritmima. Prema lemi~\ref{lema:ramdet} sljedeća konfiguracija ovisi samo o neposredno prethodnoj (izračunavanje je \emph{memoryless} --- kao Markovljev lanac, samo deterministično), ali o oba njena dijela --- i o registrima i o brojaču. To znači da je prirodni način definiranja tih funkcija simultana rekurzija.

Za nju nam prvo trebaju inicijalizacije, odnosno vrijednosti traženih funkcija u $n=0$. Nakon $0$ koraka stanje registara je početna konfiguracija s ulazom $\vec x$, čiji se kod može dobiti iz koda $\langle\vec x\rangle$ funkcijom $\f{start}$ iz leme~\ref{lm:startprn}:
\begin{equation}
    \f{Reg}(\langle\vec x\rangle,e,0)=\knk{0,x_1,x_2,\dotsc,x_k,0,0,\dotsc}=\f{start}(\langle\vec x\rangle)\text,
\end{equation}
pa za točkovnu definiciju inicijalizacijske funkcije za $\f{Reg}$ (gdje je $x\in\N$ proizvoljan) uzmimo
\begin{equation}
    \f{Reg}(x,e,0):=\f G_1(x,e):=\f{start}(x)\text.
\end{equation}
Inicijalizacija $\f{Count}$ je $\f G_2:=\f C_0^2$, jer je početna vrijednost programskog brojača uvijek $0$.

Prelazimo na korak računanja. Za njega nam trebaju funkcije $\f H_1^5$ i $\f H_2^5$, koje primaju $x$ i $e$, broj već napravljenih koraka $n$ te stare vrijednosti koda stanja registara $r$ i programskog brojača $p$ --- a vraćaju nove vrijednosti $r'$ i $p'$ redom. Njih dobijemo pomoću $\f{NextReg}$ i $\f{NextCount}$, s tim da sad moramo voditi računa i o završnim konfiguracijama, ostavljajući ih fiksnima. $\f{NextReg}$ to već čini, jer ako $t$ nije kod instrukcije,~\eqref{eq:NextRegdef} kaže da je $\f{NextReg}(t,r)=r$ --- no za $\f H_2$ ćemo morati granati.
\begin{align}
%\SwapAboveDisplaySkip
    \f H_1(x,e,n,r,p)&:=\f{NextReg}(e[p],r)\text,\\
    \f H_2(x,e,n,r,p)&:=\begin{cases}
        \f{NextCount}(e[p],r,p),&
        p<\f{lh}(e)\\
        p,&\text{inače}
    \end{cases}\text.
\end{align}

Funkcije $\f H_1$ i $\f H_2$ su primitivno rekurzivne po teoremu o grananju~\ref{tm:grek}, propoziciji~\ref{prop:lhpartprn}, lemi~\ref{lm:NextRegCountprn} i primjeru~\ref{pr:m-v}. Sada je jasno da su $\f{Reg}$ i $\f{Count}$, definirane s
\begin{align}
%\SwapAboveDisplaySkip
    \f{Reg}(x,e,0)&:=\f G_1(x,e)=\f{start}(x)\text,\\
    \f{Count}(x,e,0)&:=\f G_2(x,e)=0\text,\\
    \label{eq:stepReg}\f{Reg}(x,e,n+1)&:=\f H_1\bigl(x,e,n,\f{Reg}(x,e,n),\f{Count}(x,e,n)\bigr)\text,\\
    \label{eq:stepCount}\f{Count}(x,e,n+1)&:=\f H_2\bigl(x,e,n,\f{Reg}(x,e,n),\f{Count}(x,e,n)\bigr)\text,
\end{align}
dobivene simultanom primitivnom rekurzijom iz primitivno rekuzivnih funkcija $\f G_1$, $\f G_2$, $\f H_1$ i $\f H_2$ pa su primitivno rekurzivne po propoziciji~\ref{prop:simultrek}.

    Dokažimo da doista ispunjavaju navedenu parcijalnu specifikaciju. U tu svrhu, neka je $\vec x$ neprazni konačni niz, $P$ RAM-program te $x$ i $e$ njihovi kodovi redom. Tvrdnju dokazujemo indukcijom po broju koraka $n$. Za $n=0$, $\f{Count}(x,e,n)=0$, što je po definiciji vrijednost programskog brojača nakon $0$ koraka izračunavanja. Također, iz leme~\ref{lm:startprn} slijedi da je $\f{Reg}(x,e,0)$ kod stanja registara na početku izračunavanja.

	Pretpostavimo da je parcijalna specifikacija zadovoljena nakon $n$ koraka i pogledajmo što se događa u ($n+1$).\ koraku. Ako je konfiguracija $c_n$ (nakon $n$ koraka) završna, tada je po pretpostavci indukcije $\f{Count}(x,e,n)=c_n(\textsc{pc})=\f{lh}(e)$ pa ne vrijedi uvjet grananja u definiciji $\f H_2$ pozvanoj  iz~\eqref{eq:stepCount}. Također je prema propoziciji~\ref{prop:lhpartprn}\eqref{stav:part=0} $e[\f{lh}(e)]=0\notin\f{Ins}$, što znači da funkcija $\f H_1$ vraća nepromijenjen kod stanja registara (ne vrijedi ni $Up$ ni $Down$ u~\eqref{eq:NextRegdef}). Iz toga je $\f{Reg}(x,e,n+1)=\f{Reg}(x,e,n)$ i $\f{Count}(x,e,n+1)=\f{Count}(x,e,n)$, što i treba biti jer je $c_{n+1}=c_n$.

Ako pak $c_n$ nije završna, tada je $p:=c_n(\textsc{pc})<\f{lh}(e)$ te je $i:=e[p]$ kod instrukcije koja se izvršava u ($n+1$).\ koraku. Tada je po pretpostavci indukcije i lemi~\ref{lm:NextRegCountprn},
\begin{multline}
    \f{Reg}(x,e,n+1)=\f H_1\bigl(x,e,n,\f{Reg}(x,e,n),p\bigr)=\\
	=\f{NextReg}\bigl(e[p],\f{Reg}(x,e,n)\bigr)=\f{NextReg}\bigl(i,c_n[\reg{}]\bigr)=c_{n+1}[\reg{}]\text,
\end{multline}
i analogno $\f{Count}(x,e,n+1)=c_{n+1}(\textsc{pc})$, čime je proveden korak indukcije.
\end{proof}

\subsection{Prepoznavanje završne konfiguracije i čitanje rezultata}

Pomoću funkcije $\f{Count}$ možemo detektirati završnu konfiguraciju.
\begin{equation}
    \f{Final}'(x,e,n):\Longleftrightarrow\f{Count}(x,e,n)\eq\f{lh}(e)
\end{equation}
%(Razlog zašto nam definicije imaju crtice je u tome da ovaj pristup, iako intuitivan, ima nekoliko mana i to zapravo neće biti "prave" definicije. Njih ćemo napisati kasnije.)

Zbog $\chi_{\f{Final}'}^3=\chi_\eq\circ(\f{Count},\f{lh}\circ\f I_2^3)$, to je primitivno rekurzivna relacija, a za sve $P\in\mathscr Prog$, $\vec x\in\N^+$ i $n\in\N$, $\f{Final}'(\langle\vec x\rangle,\kprog P,n)$ znači da je konfiguracija nakon $n$ koraka $P$-izračunavanja s $\vec x$ završna.
%
Ipak, za proizvoljne $(x,e,n)\in\N^3$, može se dogoditi da vrijedi $\f{Final}'(x,e,n)$, iako $e$ uopće nije kod RAM-programa, niti je $x$ kod nepraznog konačnog niza.

\begin{primjer}[{name=[neintuitivnost parcijalno specificiranih relacija]}]\label{pr:Final'}
Recimo, za $x=100$ i $e=10^{217}$, prvo bismo odredili
$\f{start}(100)$. Broj $100$ ima dva prim-djelitelja ($2$ i $5$), pa je $\f{lh}(100)=2$. Iz toga $\f{start}(100)=3^{100[0]}\cdot5^{100[1]}=\knk{0,1,0,0,\dotsc}=3=\f{Reg}(100,10^{217},0)$. Dakle, $\reg1$ kreće od $1$, a svi ostali registri od nule.  $\f{Count}(100,10^{217},0)=0$ jer \textsc{pc} uvijek kreće od nule.
% \eq stigao do ovdje % dovde stiglo jednakost

	Sada odredimo "trenutnu instrukciju": $e[0]=216=2^3\cdot3^3=\langle2,2\rangle=\kins{\goto\;2\,}\in\f{InsGOTO}$ pa je $\f{Count}(100,10^{217},1)=\f{dest}(216)=2=\f{lh}(e)$. Dakle, $\f{Final}'(100,10^{217},1)$ vrijedi --- no nema smisla reći da to reprezentira zaustavljanje nekog iz\-ra\-ču\-na\-va\-nja, jer ne postoje $P\in\mathscr Pr\mspace{-1mu}o\mspace{-2mu}g$ i $\vec x\in\N^+$ takvi da bi to bilo $P$-izračunavanje s $\vec x$.
\end{primjer}

Primjer~\ref{pr:Final'} pokazuje da trebamo biti oprezni s parcijalnim specifikacijama. Dok su za primitivno rekurzivne funkcije one ponekad "nužno zlo" ili barem "manje zlo", za primitivno rekurzivne \emph{relacije} je mnogo prirodnije isključiti sve nespecificirane točke (efektivno, promatrati presjek s područjem specifikacije).
\begin{equation}
\f{Final}(x,e,n):\Longleftrightarrow\f{Seq'}(x)\land\f{Prog}(e)\land\f{Final}'(x,e,n)
\end{equation}

\begin{lema}[{name=[primitivna rekurzivnost završnosti konfiguracije]}]\label{lm:Finalspec}
Relacija $\f{Final}^3$ je primitivno rekurzivna te je $(x,e,n)\in\f{Final}$ ako i samo ako je $x$ kod nekog nepraznog konačnog niza $\vec x\in\N^+$\!, $e$ je kod nekog RAM-programa $P$, a $P$-izračunavanje s~$\vec x$ stane nakon najviše $n$ koraka.
\end{lema}
\begin{proof}
    Za primitivnu rekurzivnost: jednočlana relacija $\{\langle\rangle\}=\{1\}$ je primitivno rekurzivna po lemi~\ref{lm:r1prn}. Tada je $\f{Seq'}:=\f{Seq}\setminus\{1\}$ primitivno rekurzivna po propoziciji~\ref{prop:vezn}, a onda i $\f{Final}$ po propoziciji~\ref{prop:skupl}.

Za specifikaciju, smjer slijeva nadesno, raspetljavanjem definicije od $\f{Final}(x,e,n)$ vidimo da mora vrijediti:
\begin{itemize}
    \item $\f{Seq}(x)$, dakle $x=\langle\vec x\rangle$ za neki $\vec x\in\N^*$, jer je $\f{Seq}=\im{\langle\cdots\rangle}$;
    \item $x\ne1=\langle\rangle$, dakle $\vec x$ je neprazan, jer je $\langle\cdots\rangle$ injekcija;
    \item $\f{Prog}(e)$, dakle $e=\kprog{P}$ za neki RAM-program $P$, jer je $\f{Prog}=\im{\kprog{\cdots}}$;
    \item $\f{Count}(x,e,n)\eq\f{lh}(e)$, što prema lemi~\ref{lm:RegCountprn} (koju možemo primijeniti zahvaljujući prethodnim trima stavkama) znači da je $n$-ta konfiguracija u $P$-izračunavanju s $\vec x$ završna --- iz čega slijedi da ono stane; štoviše, da je prvi indeks završne konfiguracije u izračunavanju manji ili jednak $n$.
\end{itemize}
Zaključivanjem u suprotnom smjeru lako dobijemo i drugi smjer tvrdnje.
\end{proof}

To je u redu ako već imamo (kandidat za) $n$ --- ali možemo li \emph{izračunati} $n$? Svakako, minimizacijom: $\f{step}:=\mu\,\f{Final}$ je parcijalno rekurzivna funkcija takva da je $\f{step}(\langle\vec x\rangle,\kprog P)\simeq\mu n\,\f{Final}(\langle\vec x\rangle,\kprog{P},n)$ upravo broj koraka $P$-izračunavanja s $\vec x$ do dolaska u završnu konfiguraciju. To je definirano samo za izračunavanja koja stanu: $HALT:=\dom{\f{step}}=\exists_*\f{Final}$ je dvomjesna relacija takva da $HALT(\langle \vec x\rangle,\kprog P)$ vrijedi ako i samo ako $P$-izračunavanje s $\vec x$ stane.

\begin{napomena}[{name=[totalna specifikacija zaustavljanja izračunavanja]}]\label{nap:HaltProg}
Zahvaljujući oprezu sa specifikacijom prije, sad možemo biti i precizniji: kad god $e$ nije kod nekog programa, ili $x$ nije kod nepraznog konačnog niza, ne vrijedi $\f{Final}(x,e,n)$ ni za koji $n$. Dakle, tada $(x,e)\notin HALT$, odnosno izraz $\f{step}(x,e)$ nema vrijednost.
\end{napomena}

Uočite da $HALT$ nismo napisali u "izračunljivom fontu", jer nemamo algoritam za računanje $\chi_{HALT}$. To što je $HALT$ domena parcijalno rekurzivne funkcije, odnosno projekcija primitivno rekurzivne relacije, nije dovoljno: ako je $(x,e)\in HALT$, to ćemo doznati čim nađemo broj koraka $n$ --- ali ako $(x,e)\notin HALT$, to nećemo nikada doznati tim pristupom. Pokazat ćemo, štoviše, da \textbf{nijedan pristup ne radi za sve parove} $(x,e)$, iako u nekim slučajevima (poput $e\notin\f{Prog}$) možemo utvrditi $\lnot HALT(x,e)$. Precizno, pokazat ćemo da skup $HALT$ nije rekurzivan --- što će biti jedan od prvih primjera nepostojanja algoritma za neki problem. No to će morati još malo pričekati.

Pozabavimo se sada čitanjem rezultata izračunavanja (izlaznog podatka algoritma, odnosno vrijednosti funkcije koja se računa na ulaznim podacima). Za $HALT(x,e)$, izraz $\f{Reg}\bigl(x,e,\f{step}(x,e)\bigr)$ ima vrijednost koja kodira stanje registara u završnoj konfiguraciji izračunavanja. Za $\lnot HALT(x,e)$, što uključuje i $\lnot\f{Prog}(e)$ i $\lnot\f{Seq}'(x)$, taj izraz nema vrijednost. Još treba dokomponirati primitivno rekurzivnu funkciju $\f{result}$ iz~\eqref{eq:resultdef}, dobivši
\begin{equation}
\label{eq:univdef}\f{univ}(x,e):\simeq\f{result}\bigl(\f{Reg}\bigl(x,e,\f{step}(x,e)\bigr)\bigr)\text,
\end{equation}
\emph{univerzalnu} funkciju koja preslikava RAM-program i ulaz za njega u rezultat iz\-ra\-ču\-na\-va\-nja, i to ako i samo ako je taj rezultat definiran.

\begin{lema}[{name=[parcijalna rekurzivnost univerzalne funkcije]}]\label{lm:univspec}
Funkcija $\f{univ}^2$ je parcijalno rekurzivna, i za sve $x,e\in\N$ vrijedi:
\begin{enumerate}
    \item\label{tv:univ} Ako je $x$ kod nekog nepraznog konačnog niza $\vec x$, ako je $e$ kod nekog RAM-programa $P$\\ te ako $P$-izračunavanje s $\vec x$ stane, tada je $\f{univ}(x,e)$ rezultat tog izračunavanja.
    \item\label{tv:nuniv} U svim ostalim slučajevima, $(x,e)\notin\dom{\f{univ}}$ (izraz $\f{univ}(x,e)$ nema vrijednost).
\end{enumerate}
\end{lema}
\begin{proof}
Parcijalna rekurzivnost slijedi iz~\eqref{eq:univdef}, iz primitivne rekurzivnosti korištenih funkcija $\f{result}=\f{ex}\circ(\f I_1^1,\f Z)$ i $\f{Reg}$ te parcijalne rekurzivnosti funkcije $\f{step}$.

Za tvrdnju~\ref{tv:univ}, pretpostavke kažu da postoji završna konfiguracija u $P$-izračunavanju s $\vec x$. Prema lemi~\ref{lm:Finalspec}, to znači $\exists n\,\f{Final}(x,e,n)$, dakle $(x,e)\in\exists_*\f{Final}=\dom{\f{step}}$, pa postoji $\f{step}(x,e)=:n_0$, i $\f{Reg}(x,e,n_0)$ je kod stanja registara u završnoj konfiguraciji $c_{n_0}$ tog izračunavanja.
\begin{equation}
	z:=\f{Reg}(x,e,n_0)=c_{n_0}[\reg{}]=\knk{c_{n_0}(\reg0),c_{n_0}(\reg1\mspace{-2mu}),\dotsc}
\end{equation}
Sada je $\f{univ}(x,e)=\f{result}(z)=\f{ex}(\knk{c_{n_0}(\reg0),\dotsc},0)=c_{n_0}(\reg0)$, sadržaj registra $\reg0$ u završnoj konfiguraciji, što smo i trebali.

	Za tvrdnju~\ref{tv:nuniv}, ako neki od  uvjeta nije zadovoljen, prema lemi~\ref{lm:Finalspec} (drugi smjer) ni za koji $n$ ne vrijedi $\f{Final}(x,e,n)$, iz čega $(x,e)\notin\dom{\f{step}}$. Iz pretpostavke o marljivoj evaluaciji~\eqref{eq:domkomp} slijedi da $(x,e)$ ne može biti ni u domeni od $\f{univ}$.
\end{proof}

\section{Kleenejev teorem o normalnoj formi}

Funkcija $\f{univ}$ je univerzalna, jer može simulirati bilo koji RAM-stroj, odnosno ra\-ču\-na\-ti bilo koju RAM-izračunljivu funkciju, pa time (po teoremu~\ref{tm:pir}) i svaku parcijalno rekurzivnu funkciju. Na neki način, $\f{univ}$ predstavlja funkcijski \emph{interpreter} za RAM-stroj, nasuprot imperativnom \emph{kompajleru} za simboličke definicije izgrađenom u poglavlju~\ref{ch:rek}. %No iz raznih razloga, uglavnom tehničkih i povijesnih, zapravo se univerzalna funkcija uvodi na malo drugačiji način.
No iz tehničkih i povijesnih razloga, univerzalna funkcija obično se uvodi malo drugačije.

Htjeli bismo napisati što jednostavniju "simboličku definiciju" univerzalne funkcije. Definicija~\eqref{eq:univdef} ima nezgodno svojstvo da dvaput koristi $x$ i $e$, odnosno napisana je kao kompozicija dvije funkcije, svaka od kojih ovisi o ulaznim podacima. No vanjska funkcija ne mora primati $x$ i $e$, ako joj unutarnja funkcija pošalje završnu konfiguraciju, ili nešto iz čega se ona može odrediti. Razlog zašto ih trenutno prima je u tome što joj unutarnja funkcija pošalje samo broj koraka, sam po sebi nedovoljan za određivanje završne konfiguracije. No koristeći kodiranje $\N^*\!$, poslana vrijednost može biti proizvoljno komplicirana.

Drugo, od osnovnih operatora ($\circ$, $\pr$ i $\mu$) moramo koristiti minimizaciju jer $\f{univ}$ nije totalna --- ali htjeli bismo je koristiti što "kasnije", tako da što veći dio stabla koje predstavlja njenu simboličku definiciju bude primitivno rekurzivan. Tehnikama svođenja iz poglavlja~\ref{ch:ne} može se pokazati da minimizacija ne može biti u korijenu (ne postoji rekurzivna relacija $\f{R}^3$ takva da je $\f{univ}=\mu\,\f{R}$) --- dakle moramo nakon $\mu$ primijeniti još neki operator. To ne može biti $\pr$ jer bismo time opet dobili totalnu funkciju, dakle mora biti kompozicija. Najjednostavnija "normalna forma" koja zadovoljava te uvjete je $\f{univ}^2=\f U^1\circ\mu\f{\check T}^3$ za primitivno rekurzivne $\f U$ i $\f{\check T}$ ($\f U$ je funkcija, $\f{\check T}$ je relacija).

%Još jedan tehnički detalj je da želimo primiti argumente zasebno, a ne kao kod konačnog niza. To znači da ćemo umjesto $x$ imati $\vec x$ duljine $k$ te ćemo umjesto jedne relacije $\f{\check T}^3$ imati po jednu relaciju $\f T_k^{k+2}$ za svaki $k\in\N_+$, a umjesto $\f{univ}^2$ imat ćemo familiju parcijalnih funkcija $\f{comp}_k^{k+1}$, $k\in\N_+$, koje će zadovoljavati
%\begin{equation}\label{eq:comp=univ}
    %\f{comp}_k(\vec x^k,e)\simeq\f{univ}(\langle\vec x\rangle,e)\text.
%\end{equation}
%Drugim riječima, za svaki $k\in\N_+$, $\f{comp}_k$ je dobivena kompozicijom iz parcijalno rekurzivnih funkcija $\f{univ}$ i $\f{Code}^k$, pa je parcijalno rekurzivna. Još je preostalo naći $\f U$ i $\f T_k$ takve da je $\f{comp}_k=\f U\circ\mu\,\f T_k$.

Funkciji $\f U$ trebamo poslati izračunavanje --- možemo li ga kodirati prirodnim brojem? Ako ne stane, teško: može se ponavljati ciklički, ali se može i ponašati vrlo komplicirano. Ali izračunavanja koja ne stanu ionako nas ne zanimaju, jer ne želimo da $\f U\circ\mu\f{\check T}$ bude definirano u tom slučaju.

Dakle, promotrimo izračunavanje $(c_n)_{n\in\N}$ koje stane. Vidjeli smo da ono mora biti oblika $(c_0,c_1,\dotsc,c_{n_0},c_{n_0},c_{n_0},\dotsc)$, gdje je $c_{n_0}$ završna, a nijedna $c_i$ za $i<n_0$ nije završna. Za potrebe kodiranja, dovoljno je gledati samo konačan niz $(c_0,c_1,\dotsc,c_{n_0})$ duljine $n_0+1$, jer se iz njega beskonačnim ponavljanjem posljednjeg elementa može dobiti i čitavo izračunavanje. Za kodirati pojedinu $c_i$, trebali bismo uračunati i $\f{Reg}(x,e,i)$ i $\f{Count}(x,e,i)$, no s obzirom na to da nam je u završnoj konfiguraciji po definiciji poznata ova druga vrijednost ($c_{n_0}(\textsc{pc})=\f{lh}(e\mspace{1mu})$) i zapravo nam treba sadržaj registra $\reg0$, pamtit ćemo samo vrijednosti funkcije $\f{Reg}$. Drugim riječima, treba nam povijest $\overline{\f{Reg}}(x,e,n_0+1)$, što je izračunljivo jednom kad imamo $n_0:=\f{step}(x,e)$.

\begin{definicija}[{name=[kod izračunavanja]}]\label{def:kodizr}
	Neka je $P^k$ RAM-algoritam te $\vec x\in\N^k$ takav da $P$-izračunavanje s $\vec x$ stane. \emph{K$\mspace{-2mu}$od} tog izračunavanja definiramo kao povijest kodova stanja registara, do uključivo prvog indeksa završne konfiguracije u tom izračunavanju. Za izračunavanja koja ne stanu kod nije definiran.
\end{definicija}

Propozicija~\ref{prop:ramdet}, restringirana samo na izračunavanja koja stanu (jer jedino takva znamo kodirati), može se iskazati kao: tromjesna relacija \begin{equation}\label{eq:Trace}
	T\!race\bigl(\vec x,P,(c_n)_{n\in\N}\bigr):\Longleftrightarrow\text{"$(c_n)_{n\in\N}$ je $P$-izračunavanje s $\vec x$, koje stane"}
\end{equation}
ima funkcijsko svojstvo. Tada će i $\f{\check T}^3:=\N T\!race$ imati funkcijsko svojstvo. Cilj nam je dokazati da je $T\!race$ izračunljiva, odnosno da je $\f{\check T}$ primitivno rekurzivna.

U skladu s napomenom iz primjera~\ref{pr:concat}, $T\!race$ ćemo shvatiti kao ($k+2$)-mjesnu relaciju, tako da svaki $x_i$ shvatimo kao zasebni argument. To vodi na promatranje familije relacija $\f T_k^{k+2},k\in\N_+$ --- a jednom kad dobijemo primitivnu rekurzivnost od $\f{\check T}$, dobit ćemo i primitivnu rekurzivnost svih $\f T_k$, jer je
\begin{equation}\label{eq:TkviadotT}
\f T_k(\vec x,e,y)\Longleftrightarrow\f{\check T}(\langle\vec x\rangle,e,y)\text,
\end{equation}
dakle $\f T_k$ je dobivena iz $\f{\check T}$ kompozicijom s $\f{Code}^k$ i koordinatnim projekcijama.

\begin{primjer}[{name=[{kod $Q^\flat$-izračunavanja s ${(2,4)}$}]}]
U primjeru~\ref{pr:makro} je naveden primjer makro-programa $Q$ i $Q$-izračunavanja s $(2,4)$, koje stane. Kako $Q^\flat$-izračunavanje s $(2,4)$ prolazi kroz ista stanja registara, možemo iz~\eqref{ml:Qstane} izračunati kod tog izračunavanja (iz definicije~\ref{def:makrolead} trebamo zanemariti prijelaze tipa~\ref{stav:carry}, jer oni ne odgovaraju nikakvim prijelazima RAM-stroja, kao i one tipa~\ref{stav:zav}, jer smo tada već stigli do završne konfiguracije):
\begin{multline}
    c_0:=\langle5625,1875,1875,625,625,625,125,125,25,50,50,10,20,20,4,8,8,8,8\rangle=\\
	=2^{5626}\cdot3^{1876}\cdot5^{1876}\cdot7^{626}\cdot11^{626}\cdot13^{626}\cdot17^{126}\mathbin{\dotsm}61^9\cdot\mspace{1mu}67^9\text.
\end{multline}
Recimo, $c_0[6]=\f{part}(c_0,6)=\f{pd}\bigl(\f{ex}(c_0,6)\bigr)=\f{pd}(126)=125=5^3=\knk{0,0,3,0,\dotsc}$, jer nakon $6$ koraka $Q^\flat$-izračunavanja s $(2,4)$ u $\reg2$ bude broj $3$, a u svim ostalim registrima broj $0$.

Drugi način za iskazati to isto je $\f{Reg}(\langle2,4\rangle,\kprog{Q^\flat},6)=\knk{0,0,3,0,\dotsc}$. Ako iz\-ra\-ču\-na\-mo $\langle2,4\rangle=2^3\cdot3^5=1944$ i upotrijebimo $e_Q:=\kprog{Q^\flat}$ iz primjera~\ref{pr:Qflatkod}, možemo napisati i $\f{Reg}(1944,e_Q,6)=5^3$. Vidimo da je $c_0$ povijest funkcije $\f{Reg}$, konkretno $\f{\check T}(1944,e_Q,c_0)$ znači $c_0=\overline{\f{Reg}}(1944,e_Q,19)$, gdje je $\f{pd}(19)=18=\f{step}(1944,e_Q)$.
\end{primjer}

%\subsection{Grafovi totalnih funkcija}

Funkcija $\f{step}$ jest izračunljiva, ali budući da nam treba \emph{relacija} za minimizaciju, koristit ćemo njen graf $\f{Step}^3:=\graf{\f{step}}$ kao relaciju iz koje možemo dobiti njene vrijednosti.

\begin{napomena}[{name=[problemi s parcijalnom jednakošću]}]\label{nap:parc=}
Važno: \textbf{ne možemo} napisati $n=\f{step}(x,e)$ kao točkovnu definiciju relacije $\f{Step}$ --- to bi simbolički glasilo $\chi_{\f{Step}}=\chi_=\circ\bigl(\f I_3^3,\f{step}\circ(\f I_1^3,\f I_2^3)\bigr)$, što nije istina jer te dvije funkcije imaju različite domene: lijeva je totalna, a desna je definirana samo na $HALT\times\N$. To je samo jedan od problema koje imamo s parcijalnim funkcijama, koji su osnovni razlog zašto se držimo primitivno rekurzivnih funkcija dok god možemo: vidjet ćemo kasnije da općenito graf (baš kao ni domena) izračunljive funkcije ne mora biti izračunljiv\!.
\end{napomena}

Ipak, za totalne funkcije takav rezultat vrijedi, i možemo ga već sada dokazati. Prvo strogo definirajmo graf i dokažimo jednu tehničku lemu.

\begin{definicija}[{name=[graf brojevne funkcije]}]
Neka je $k\in\N_+$ i $f^k$ funkcija. \emph{Graf} funkcije $f$ je relacija $\graf f^{k+1}$ zadana s
\begin{equation}
	\label{eq:defgraf}\graf f(\vec x,y):\Longleftrightarrow\vec x\in\dom f\land y\simeq f(\vec x)\text{.\qedhere}
\end{equation}
\end{definicija}
%Uvjet $\vec x\in\dom f$ služi tome da osigura da je u drugom konjunktu desna strana definirana, pane treba pisati jer slijedi iz $y=f(\vec x)$, ali je naveden zbog jasnoće
U definiciji općenito ne smijemo napisati $y=f(\vec x)$ umjesto $y\simeq f(\vec x)$ jer bi to impliciralo totalnost od $f$ (pogledajte napomenu~\ref{nap:parc=}), ali ako je $f$ već totalna, onda možemo.

\begin{napomena}[{name=[funkcijsko svojstvo grafova]}]\label{nap:graf=funsv}
    Iz elementarne matematike znamo da je relacija $R$ graf neke funkcije ako i samo ako ima \emph{funkcijsko svojstvo}: $R(\vec x,y_1)\land R(\vec x,y_2)\Rightarrow y_1=y_2$. Riječima, "svaka vertikala siječe graf u najviše jednoj točki".
\end{napomena}

\begin{lema}[{name=[projekcija i minimizacija grafa]}]\label{lm:projmugraf}
Za svaki $k\in\N_+$, za svaku funkciju $f^k$\!, vrijedi
%\begin{align}
    %\label{eq:projgraf}
	$\exists_*\graf f=\dom f$ i %\text,\\
    %\label{eq:mugraf}
	$\mu\,\graf f=f$.
%\end{align}
\end{lema}
\begin{proof}
Za prvu jednakost, iz $\vec x\in\exists_*\graf f$ slijedi da postoji $y\in\N$ takav da je $\vec x\in\dom f$ i $y=f(\vec x)$. Specijalno to znači $\vec x\in\dom f$. U drugom smjeru, $\vec x\in\dom f$ znači da postoji $f(\vec x)\in\N$, a onda zbog $\graf f\bigl(\vec x,f(\vec x)\bigr)$ vrijedi $\vec x\in\exists_*\graf f$.

Dokažimo sada drugu jednakost. Prva jednakost kaže da te dvije funkcije imaju istu domenu~\eqref{eq:dommu}; trebamo još vidjeti da se podudaraju u svim točkama te domene. U tu svrhu, neka je $\vec x\in\dom f$. Tada postoji $f(\vec x)=:y_0\in\N$ i vrijedi $\graf f(\vec x,y_0)$. Štoviše, zbog funkcijskog svojstva, ni za koji $y\ne y_0$ ne vrijedi $\graf f(\vec x,y)$, dakle skup $\{y\in\N\mid\graf f(\vec x,y)\}$ je jednočlan skup $\{y_0\}$, pa mu je najmanji element $\mu y\,\graf f(\vec x,y)=y_0=f(\vec x)$.
\end{proof}

\begin{teorem}[Teorem o grafu za totalne funkcije]\label{tm:graftot}
Neka je $k\in\N_+$ te $\f{f}^k$ totalna funkcija.\\ Tada je $\graf{\f f}$ rekurzivan ako i samo ako je $\f f$ rekurzivna.
\end{teorem}
\begin{proof}
Za smjer ($\Rightarrow$): po pretpostavci, $\chi_{\graf{\f f}}$ je rekurzivna, dakle parcijalno rekurzivna. Skup parcijalno rekurzivnih funkcija je zatvoren na minimizaciju, pa je $\mu\,\graf f$ također parcijalno rekurzivna --- no ta funkcija je jednaka $\f f$ po lemi~\ref{lm:projmugraf}. Dakle, $\f f$ je parcijalno rekurzivna, a po pretpostavci teorema je totalna, pa je rekurzivna.

	Za smjer ($\Leftarrow$): kako je $\f f$ totalna, uvjet $\vec x^k\in\dom{\f f}=\N^k$ uvijek vrijedi, i $\f f(\vec x)$ uvijek postoji, pa~\eqref{eq:defgraf} postaje $\graf{\f f}(\vec x,y)\Longleftrightarrow y=\f f(\vec x)$, odnosno $\chi_{\graf{\f f}}$ je dobivena kompozicijom iz $\chi_=$, $\f f$ i koordinatnih projekcija. Jednakost i koordinatne projekcije su rekurzivne po korolarima~\ref{kor:jednakost} i~\ref{kor:prnrek}, a $\f f$ je rekurzivna po pretpostavci, pa je $\chi_{\graf{\f f}}$ rekurzivna po lemi~\ref{lm:comprek}.
\end{proof}

Istaknimo da u teoremu~\ref{tm:graftot} ne možemo staviti riječ "primitivno" u zagrade, kao što smo činili u mnogim rezultatima do sada: postoje rekurzivne funkcije čiji grafovi su primitivno rekurzivni, ali one same nisu primitivno rekurzivne. \emph{Ackermannova} funkcija, opisana u~\cite[dodatak]{skr:Vuk}, primjer je takve funkcije.

%\subsection{Relacije \texorpdfstring{$\f{Step}$ i $\f T_k$}{Step i Tk}}
%\subsection{Univerzalne funkcije \texorpdfstring{$\f{comp}_k$}{comp}}
\subsection{Kodiranje RAM-izračunavanja jednim brojem}

Kako $\f{step}$ nije totalna, ne možemo primijeniti teorem~\ref{tm:graftot}, ali možemo neke druge rezultate. Prema lemi~\ref{lm:projmugraf} je $\f{step}=\mu\,\f{Step}$, no $\f{step}$ je već definirana minimizacijom primitivno rekurzivne relacije $\f{Final}$. Relacije $\f{Step}$ i $\f{Final}$ nisu jednake jer jedna ima funkcijsko svojstvo a druga nema (čim vrijedi $\f{Final}(x,e,n_0)$, vrijedi i $\f{Final}(x,e,n)$ za sve $n>n_0$), ali možemo li dobiti jednu pomoću druge? $\f{Final}(x,e,n)\Leftrightarrow(\exists m\le n)\f{Step}(x,e,m)$ znači da je $\f{Final}$ dobivena ograničenom egzistencijalnom kvantifikacijom iz $\f{Step}$, ali nama treba drugi smjer.

Relacija $\f{Step}(x,e,m)\Leftrightarrow m= \mu n\,\f{Final}(x,e,n)$, koju dobijemo doslovnim čitanjem definicije $\f{Step}=\graf{\f{step}}$, čini se kao dobar početak: jedino što joj nedostaje je totalnost ove minimizacije na desnoj strani. Taj problem smo već imali nekoliko puta u točki~\ref{sec:teobroj} i uvijek smo ga uspješno rješavali ograničavanjem minimizacije. Postoji li gornja granica za $n$ do koje je dovoljno provjeravati vrijedi li $\f{Final}(x,e,n)$, da bismo znali je li $m$ najmanji takav $n$? Naravno --- to je upravo $m+1$! Odnosno, dovoljno je provjeravati do uključivo $m$.

\begin{lema}[{name=[primitivna rekurzivnost grafa brojenja koraka do zaustavljanja]}]
Relacija $\f{Step}^3:=\graf{\f{step}^2}$ je primitivno rekurzivna.
\end{lema}
\begin{proof}
Kao što smo upravo rekli, cilj nam je dokazati
\begin{equation}
    \f{Step}(x,e,m)\Longleftrightarrow m=(\mu n\le m)\f{Final}(x,e,n)
\end{equation}
--- iz toga će onda slijediti primitivna rekurzivnost prema (redom) lemi~\ref{lm:Finalspec}, propoziciji~\ref{prop:ominprn}, napomeni~\ref{nap:igpk} i korolaru~\ref{kor:jednakost}.

Pretpostavimo da vrijedi $\f{Step}(x,e,m)$. Tada vrijedi $(x,e)\in\dom{\f{step}}=HALT$ i $m=\f{step}(x,e)$. Dakle vrijedi $\f{Final}(x,e,m)$, i ni za koji $n<m$ ne vrijedi $\f{Final}(x,e,n)$, pa je $\mu n\bigl(n\le m\to\f{Final}(x,e,n)\bigr)=\mu n\,\f{Final}(x,e,n)=\f{step}(x,e)=m$.

	Ako pak ne vrijedi $\f{Step}(x,e,m)$, tada negiranjem~\eqref{eq:defgraf} vidimo da ili ne vrijedi $HALT(x,e)$, ili pak postoji $s:=\f{step}(x,e)$, ali je različit ($\mspace{-1mu}$veći ili manji) od $m$. Tvrdimo da ni u kojem od tih slučajeva broj $t:=(\mu n\le m)\f{Final}(x,e,n)$ nije jednak $m$.

Ako $\lnot HALT(x,e)$, tada ne postoji $n$ takav da vrijedi $\f{Final}(x,e,n)$, pa je
\begin{equation}
    t = \mu n(n\le m\to\bot)=\mu n\lnot(n\le m)=\mu n(n>m)= m+1\ne m\text.
\end{equation}

Ako je $s<m$, tada je $t=s$, pa je opet $t\ne m$.
	
	Ako je $s>m$, tada (po definiciji funkcije $\f{step})$ za svaki $n<s$ --- pa posebno za svaki $n\le m$ --- vrijedi $\lnot\f{Final}(x,e,n)$, iz čega opet $t=m+1\ne m$.
\end{proof}

Sada se napokon možemo pozabaviti relacijama $\f{\check T}$ i $\f T_k,k\in\N_+$. Prisjetimo se, one su dobivene kodiranjem argumenata relacije $T\!race$, prva kodirajući ulazne podatke $\vec x$ kao element od $\N^*\!$, a druga gledajući ih zasebno.
\begin{equation}\label{eq:Tkdef}
    \f T_k(\vec x^k,e,y):\Longleftrightarrow(\exists P\in\mathscr Prog)(e=\kprog{P}\land \text{"$y$ je kod $P$-izračunavanja s $\vec x$"})
\end{equation}

\begin{propozicija}[{name=[primitivna rekurzivnost Kleenejeve relacije]}]\label{prop:Tkprn}
Za svaki $k\in\N_+$, relacija $\f T_k$ je primitivno rekurzivna.
\end{propozicija}
\begin{proof}
Kao što smo već rekli, prvo ćemo dokazati primitivnu rekurzivnost relacije $\f{\check T}$,
\begin{equation}\label{eq:dotTdef}
	\f{\check T}(x,e,y):\Longleftrightarrow(\exists\vec x\in\N^+\mspace{-2mu})\bigl(x=\langle\vec x\rangle\land\f T_{\f{lh}(x)}(\vec x,e,y)\bigr)\text.
\end{equation}

Tvrdimo da je njena točkovna definicija
\begin{equation*}
    \check{\f T}(x,e,y)\Longleftrightarrow\f{Step}(x,e,n)\land y=\overline{\f{Reg}}\bigl(x,e,\f{Sc}(n)\bigr)\text{,\quad uz pokratu }n:=\f{pd}\big(\f{lh}(y)\bigr)\text.
    %\f T_k(\vec x^k,e,y)&:\Longleftrightarrow\check{\f T}(\langle\vec x\rangle,e,y)\text{, za svaki $k\in\N_+$.}
\end{equation*}

	U jednom smjeru, pretpostavimo da vrijedi $\f{\check T}(x,e,y)$. Tada prema~\eqref{eq:dotTdef} i~\eqref{eq:Tkdef} postoje $\vec x\in\N^+$ (njegovu duljinu označimo s $k$) i $P\in\mathscr Prog$ takvi da je $x$ kod od $\vec x$, $e$ je kod od $P$, a $y$ je kod $P$-izračunavanja s $\vec x$. Po definiciji~\ref{def:kodizr}, to znači da $P$-izračunavanje s $\vec x$ stane (inače kod ne bi bio definiran) --- odnosno vrijedi $HALT(x,e)$, pa postoji $n_0:=\f{step}(x,e)$ --- i $y$ je upravo povijest stanja registara prvih $n_0+1$ (od $c_0$ do $c_{n_0}$) konfiguracija u tom izračunavanju.%, od $c_0$ do uključivo $c_{n_0}$.


Iz $n_0=\f{step}(x,e)$ slijedi $\f{Step}(x,e,n_0)$, povijest stanja registara opisana je funkcijom $\overline{\f Reg}$, a upravo smo vidjeli da je $\f{lh}(y)=\f{Sc}(n_0)$. Dakle, $n_0=\f{pd}\bigl(\f{lh}(y)\bigr)$, što se upravo tvrdi u točkovnoj definiciji.

U drugom smjeru, pretpostavimo da vrijedi točkovna definicija. Tada iz $(x,e,n)\in\f{Step}=\graf{\f{step}}$ slijedi $(x,e)\in\dom{\f{step}}=HALT$ i $n:=\f{pd}\bigl(\f{lh}(y)\bigr)=\f{step}(x,e)=(\mu\,\f{Final})(x,e)$. Specijalno vrijedi $\f{Final}(x,e,n)$, pa je po lemi~\ref{lm:Finalspec} $x$ kod nekog nepraznog konačnog niza $\vec x$, $e$ je kod nekog RAM-programa $P$ te $P$-izračunavanje s $\vec x$ stane nakon najviše $n$ koraka --- zapravo u ovom slučaju nakon točno $n$ koraka, jer je $n=\f{step}(x,e)$.

Također vrijedi $y=\overline{\f{Reg}}\bigl(x,e,\f{Sc}(n)\bigr)$, dakle $\f{lh}(y)=\f{Sc}(n)>0$. To znači da je $y$ povijest stanja registara prvih $n+1$ konfiguracija, što je upravo kod tog izračunavanja.

    Nažalost, nismo mogli napisati $y=\overline{\f{Reg}}\bigl(x,e,\f{lh}(y)\bigr)$, jer bi to zadovoljavao i kod praznog niza: $1=\overline G\bigl(\vec x,\f{lh}(1)\bigr)$ bez obzira na specifikaciju funkcije $G$ i vrijednosti argumenata $\vec x$. Na neki način, $0$ je problematična kao $m=\f{lh}(y)$, pa smo umjesto $m$ napisali $\f{Sc}\bigl(\f{pd}(m)\bigr)=m\bump$ u duhu napomene~\ref{nap:crtica}.

Sada za proizvoljni $k$ primitivna rekurzivnost $\f T_k$ slijedi iz~\eqref{eq:TkviadotT}.
\end{proof}

\begin{korolar}[{name=[funkcijsko svojstvo i projekcija Kleenejeve relacije]}]\label{kor:funHaltTk}
    Za svaki $k\in\N_+$, relacija $\f T_k$ ima funkcijsko svojstvo, a projekcija joj je
    \begin{equation}
        \exists_*\f T_k=\{(\vec x,e)\in\N^{k+1}\mid HALT(\langle\vec x\rangle,e)\}=:Halt_k\text.
    \end{equation}
\end{korolar}
\begin{proof}
Za proizvoljne $\vec x$ i $e$, postoji najviše jedan RAM-program $P$ s kodom $e$ ($\kprog{\cdots}$ je injekcija), pa onda postoji jedinstveno $P$-izračunavanje s $\vec x$ (propozicija~\ref{prop:ramdet}), a ako ono stane, postoji jedinstven njegov kod. Ako $P$ ne postoji, ili ako izračunavanje ne stane, ne postoji nijedan $y$ takav da vrijedi $\f T_k(\vec x,e,y)$. Dakle, uvijek postoji \emph{najviše} jedan takav $y$, a postoji \emph{točno} jedan takav $y$ ako i samo ako je $(\vec x,e)\in Halt_k$ --- što je upravo tvrdnja koju smo željeli dokazati.
\end{proof}

Skupovi $Halt_k,k\in\N_+$ čine familiju neizračunljivih relacija, svaka od kojih je fiksne mjesnosti i predstavlja određenu "krišku" univerzalne neizračunljive relacije $HALT$.

%\subsection{Funkcije \texorpdfstring{$\f U$ i $\f{comp}_k$}{U i comp}}

Korolar~\ref{kor:funHaltTk} prema napomeni~\ref{nap:graf=funsv} kaže da je za svaki pozitivni $k$, relacija $\f T_k$ graf neke funkcije. Štoviše, po lemi~\ref{lm:projmugraf}, ta funkcija je upravo $\mu\f T_k$, njena domena je $Halt_k$, i ona preslikava svaki $(\vec x^k,\kprog{P})\in Halt_k$ (svaki element od $Halt_k$ mora biti tog oblika, po napomeni~\ref{nap:HaltProg}) u kod $P$-izračunavanja s $\vec x$. Sada, da bismo dobili \emph{rezultat} tog izračunavanja, samo treba dokomponirati slijeva funkciju zadanu s
\begin{equation}\label{eq:Udef}
    \f U(y):=\f{result}\bigl(\f{rpart}(y,0)\bigr)=\f{ex}(y[\f{pd}(\f{lh}(y))],0)\text,
\end{equation}
doslovno "sadržaj registra $\reg0$ u posljednjoj konfiguraciji kodiranoj s $y$", čime dobijemo
\begin{equation}
    \f{comp}_k(\vec x,e):\simeq \f U\bigl(\mu y\,\f T_k(\vec x,e,y)\bigr)\text.
\end{equation}

\begin{propozicija}[{name=[parcijalna rekurzivnost univerzalnih funkcija dane mjesnosti]}]\label{prop:compspec}
Funkcija $\f U$ je primitivno rekurzivna. Za svaki $k\in\N_+$,\\ funkcija $\f{comp}_k$ je parcijalno rekurzivna s domenom $\dom{\f{comp}_k}=Halt_k$ te vrijedi \begin{equation}\label{eq:comp=univ}
    \f{univ}(\langle\vec x\rangle,e)\simeq\f{comp}_k(\vec x,e)\text.
\end{equation}
\end{propozicija}
\begin{proof}
Prvo, $\f U=\f{result}\circ\f{rpart}\circ(\f I_1^1,\f Z)$ je simbolička definicija od $\f U$: funkcija $\f{result}$ je točkovno definirana u~\eqref{eq:resultdef}, a $\f{rpart}$ u~\eqref{eq:rpartdef}, pomoću primitivno rekurzivnih funkcija ($\f{ex}$, $\f{part}$, $\f{pd}$ i $\f{lh}$), pa su $\f{result}$ i $\f{rpart}$ --- a onda i $\f U$ --- primitivno rekurzivne.

	Sada je $\f{comp}_k=\f U\circ\mu\f T_k$ parcijalno rekurzivna jer je dobivena kompozicijom i minimizacijom iz primitivno rekurzivnih $\f U$ i $\f T_k$. Prema korolaru~\ref{kor:funHaltTk} domena joj je $Halt_k$, baš kao i domena funkcije $(\vec x,e)\mapsto\f{univ}(\langle\vec x\rangle,e)$ (prema~\eqref{eq:domkomp}, jer je $\f{Code}^k$ totalna). Još treba vidjeti da se te dvije funkcije podudaraju na toj domeni. Za svaki $(\vec x,e)\in Halt_k$ (uz oznake $x:=\langle\vec x\rangle$ i $n:=\f{step}(x,e)$, tako da vrijedi $\f{Step}(x,e,n)$) imamo:
\begin{multline}
    \f{univ}(x,e)=
    \f{result}\bigl(\f{Reg}(x,e,n)\bigr)=
    \f{result}\bigl(\overline{\f{Reg}}(x,e,\f{Sc}(n))[n]\bigr)=\\
    =
    \f{result}\bigl(\f{rpart}\bigl(\overline{\f{Reg}}(x,e,\f{Sc}(n)),0\bigr)\bigr)=
    \f U\bigl(\overline{\f{Reg}}(x,e,\f{Sc}(n))\bigr)
    =\\
    =\f U\bigl(\mu y\bigl(y=\overline{\f{Reg}}(x,e,\f{Sc}(n))\bigr)\bigr)=
    \f U\bigl(\mu y\bigl(y=\overline{\f{Reg}}(x,e,\f{Sc}(n))\land\f{Step}(x,e,n)\bigr)\bigr)=\\
    =\f U\bigl(\mu y\f{\check T}(x,e,y)\bigr)=
    \f U\bigl(\mu y\f T_k(\vec x,e,y)\bigr)=
    \f{comp}_k(\vec x,e)\text,
\end{multline}
iz čega slijedi tražena parcijalna jednakost.
\end{proof}

\begin{korolar}[{name=[specifikacija univerzalnih funkcija]}]\label{kor:compspec}
Za svaki $k\in\N_+$, za sve $(\vec x,e)\in\N^{k+1}$ vrijedi:
\begin{enumerate}
    \item\label{tv:comp} Ako je $e$ kod nekog RAM-programa $P$ te ako $P$-izračunavanje s $\vec x$ stane,\\ tada je $\f{comp}_k(\vec x,e)$ rezultat tog izračunavanja.
    \item\label{tv:ncomp} U ostalim slučajevima ($e=\kprog{P}$ tako da $P$-izračunavanje s $\vec x$ ne stane,\\ ili uopće $e\notin\f{Prog}$), izraz $\f{comp}_k(\vec x,e)$ nema vrijednost.
\end{enumerate}
\end{korolar}
\begin{proof}
Ovo je zapravo lema~\ref{lm:univspec}, iskazana koristeći parcijalnu jednakost~\eqref{eq:comp=univ} --- i pojednostavljena jer je uvijek $\langle\vec x^k\rangle\in\f{Seq}'$ za $k\in\N_+$, pa to ne treba pisati u uvjete.
\end{proof}

\subsection{Indeksi izračunljivih funkcija}

Sve bitno što smo dosad napravili u ovoj točki može se iskazati u jednom teoremu.

\begin{teorem}[Kleenejev teorem o normalnoj formi]\label{tm:Kleene}
Postoji primitivno rekurzivna funkcija $\f U$ takva da za svaki $k\in\N_+$ postoji primitivno rekurzivna relacija $\f T_k$, tako da za svaku parcijalno rekurzivnu funkciju $\f f$ mjesnosti $k$ postoji prirodni broj $e$, takav da za sve $\vec x\in\N^k$ vrijede sljedeće dvije tvrdnje:
\begin{gather}
	\SwapAboveDisplaySkip
    \label{eq:kleenedom}\vec x\in\dom{\f f}\Longleftrightarrow\exists y\,\f T_k(\vec x,e,y)\text,\\
    \label{eq:kleeneval}\f f(\vec x)\simeq\f U\bigl(\mu y\,\f T_k(\vec x,e,y)\bigr)\,\text.
\end{gather}
\end{teorem}
\begin{proof}
	Funkcija $\f U$ je definirana s~\eqref{eq:Udef} i dokazano je da je primitivno rekurzivna u propoziciji~\ref{prop:compspec}. Za svaki $k\in\N_+$, relacija $\f T_k$ je definirana s~\eqref{eq:Tkdef} i dokazano je da je primitivno rekurzivna u propoziciji~\ref{prop:Tkprn}. Neka je sada $\f f$ proizvoljna parcijalno rekurzivna funkcija. Prema teoremu~\ref{tm:pir}, postoji RAM-program $P$ koji računa $\f f$. Označimo $e:=\kprog P$, i neka je $\vec x\in\N^k$ proizvoljan.

Prema definiciji~\ref{def:compute}, ako je $\vec x\in\dom{\f f}$, tada $P$-izračunavanje s $\vec x$ stane, pa postoji njegov kod $y_0$. Tada po definiciji~\eqref{eq:Tkdef} vrijedi $\f T_k(\vec x,e,y_0)$, pa postoji $y$ (konkretno, $y_0$) takav da vrijedi $\f T_k(\vec x,e,y)$. Ako pak $\vec x\notin\dom{\f f}$, tada opet po definiciji~\ref{def:compute} $P$-izračunavanje ne stane, pa nema kod, odnosno ne postoji $y$ takav da vrijedi $\f T_k(\vec x,e,y)$. Time je dokazano~\eqref{eq:kleenedom}, odnosno dokazano je da u~\eqref{eq:kleeneval} lijeva i desna strana imaju vrijednost za iste $\vec x$ (jer lijeva ima vrijednost za $\vec x\in\dom{\f f}$, a desna za $(\vec x,e)\in\exists_*\f T_k$).

Za takve $\vec x$, kao što smo vidjeli, postoji kod $P$-izračunavanja s $\vec x$, koji smo označili s $y_0$ i vidjeli da vrijedi $\f T_k(\vec x,e,y_0)$. Ali $\f T_k$ ima funkcijsko svojstvo, dakle $y_0$ je \emph{jedini}, pa onda i najmanji, $y$ takav da vrijedi $\f T_k(\vec x,e,y)$. To znači da na desnoj strani zapravo piše $\f U(y_0)$, odnosno stanje registra $\reg0$ u posljednjoj konfiguraciji kodiranoj s $y_0$ --- što je po definiciji~\ref{def:compute} jednako $\f f(\vec x)$, jer ta konfiguracija mora biti završna.
\end{proof}

\begin{korolar}[{name=[jedna minimizacija je dovoljna]}]
Za svaku parcijalno rekurzivnu funkciju postoji simbolička definicija u kojoj se operator $\mu$ pojavljuje točno jednom.
\end{korolar}
\begin{proof}
Zapišimo~\eqref{eq:kleeneval} simbolički:
\begin{equation}
    \f f=\f U\circ\mu\f T_k\circ(\f I_1^k,\f I_2^k,\dotsc,\f I_k^k,\f C_e^k)\text.
\end{equation}
Vidimo da su $\f U$, $\f T_k$, $\f I_n^k$ i $\f C_e^k$ primitivno rekurzivne, pa se u njihovim simboličkim definicijama ne pojavljuje minimizacija. Dakle, jedina njena pojava služi za dobivanje funkcije $\mu\f T_k$.
\end{proof}

%Štoviše, za fiksni $k$, postoje brojevi $z_k$, $r_k$ i $i_{nk}$, $n\in[1\mspace{-1mu}\dd k]$, takvi da svaka $k$-mjesna parcijalno rekurzivna funkcija ima simboličku definiciju u kojoj se $\f Z$ pojavljuje točno $z_k$ puta, $\f I_n^k$ točno $i_{nk}$ puta te primitivna rekurzija točno $r_k$ puta. Jedino što se mijenja je broj pojava funkcije $\f{Sc}$ i operatora kompozicije, zbog $\f C_e^k=\f{Sc}\circ\f{Sc}\circ\dotsb\circ\f{Sc}\circ\f Z\circ\f I_1^k$.

%\subsection{Indeksi izračunljivih funkcija}

Kad fiksiramo $\f U$ i sve $\f T_k$ te pomoću njih definiramo funkcije $\f{comp}_k$ (kao što smo učinili), Kleenejev teorem o normalnoj formi možemo izreći jednostavnije (i precizirati što je točno broj $e$ o kojem taj teorem govori).

\begin{definicija}[{name=[indeks]}]\label{def:indeks}
Za fiksne $k\in\N_+$ i $e\in\N$, $k$-mjesnu brojevnu funkciju $\vec x\mapsto\f{comp}_k(\vec x,e)$\\ označavamo s $\kf e^k$, ili samo s $\kf e$ ako joj ne trebamo istaknuti mjesnost.

Broj $e$ zovemo \emph{indeksom} funkcije $\kf e^k$ (broj $k$ je mjesnost funkcije $\kf e^k$).

Za funkciju $f^k$ kažemo da \emph{ima indeks} ako postoji $e\in\N$ takav da je $\kf e^k=f^k$.
\end{definicija}

\begin{korolar}[{name=[parcijalna rekurzivnost funkcije zadane indeksom]}]\label{kor:iip}
Za sve $k\in\N_+$, za sve $e\in\N$, funkcija $\kf e^k$ je parcijalno rekurzivna.
\end{korolar}
\begin{proof}
	Simbolički, definicija~\ref{def:indeks} glasi
%Samo treba zapisati upravo navedenu definiciju simbolički pomoću kompozicije:
	$\kf e^k:=\f{comp}_k\circ(\f I_1^k,\f I_2^k,\dotsc\f I_k^k,\f C_e^k)$. Sada tvrdnja slijedi iz propozicije~\ref{prop:compspec}.
\end{proof}

\begin{propozicija}[{name=[specifikacija funkcije zadane indeksom]}]\label{prop:computeind}
Za sve $k\in\N_+$ i $e\in\N$ vrijedi:
\begin{enumerate}
	\item\label{it:progind} Ako je $e\in\f{Prog}$, tada je $\kf e^k$ jedinstvena funkcija koju računa RAM-al\-go\-ri\-tam $P^k$,\\ gdje je $P$ jedinstveni RAM-program takav da je $\kprog P=e$. (Geslo: "$P^k$ računa $\kf{\kprog P}^k$.")
    \item\label{it:nprogind} Ako $e\notin\f{Prog}$, tada je $\kf e^k=\varnothing^k$.
\end{enumerate}
\end{propozicija}
\begin{proof}
Ako je $e\in\f{Prog}$, tada postoji $P\in\mathscr Prog$ takav da je $\kprog P=e$, i jedinstven je jer je $\kprog{\cdots}$ injekcija. Po korolaru~\ref{kor:ram1fun}, postoji jedinstvena funkcija $\f f^k$ koju $P^k$ računa. Po definiciji~\ref{def:compute}, za tu funkciju vrijedi: za sve $\vec x\in\dom{\f f}$, $P$-izračunavanje s $\vec x$ stane, pa je po korolaru~\ref{kor:compspec}\eqref{tv:comp}, $\f f(\vec x)=\f{comp}_k(\vec x,e)=\kf e^k(\vec x)$. Za sve pak $\vec x\notin\dom{\f f}$, $P$-izračunavanje s $\vec x$ ne stane, pa po korolaru~\ref{kor:compspec}\eqref{tv:ncomp} izraz $\f{comp}_k(\vec x,e)\simeq\kf e^k(\vec x)$ nema vrijednost, baš kao ni $\f f(\vec x)$. Dakle uvijek je $\f f(\vec x)\simeq\kf e(\vec x)$, odnosno $\f f=\kf e$.

S druge strane, ako $e\notin\f{Prog}$, tada opet po korolaru~\ref{kor:compspec}\eqref{tv:ncomp} izraz $\f{comp}(\vec x,e)\simeq\kf e(\vec x)$ nema vrijednost, ali ovaj put neovisno o $\vec x\in\N^k$. Drugim riječima, tada je $\dom{\kf e^k}\!=\emptyset^k$, odnosno jedino je moguće $\kf e^k=\varnothing^k$.
\end{proof}

%\begin{korolar}[{name=[kod programa koji računa funkciju je indeks funkcije]}]\label{kor:computeind}
%Svaki RAM-algoritam $P^k$ računa funkciju $\kf{\kprog P}^k$.
%\end{korolar}
%\begin{proof}
%Ovo je samo jezgrovit zapis propozicije~\ref{prop:computeind}\eqref{it:progind}.
%\end{proof}

\begin{korolar}[{name=[svaka izračunljiva funkcija je specijalizacija univerzalne]}]\label{kor:pimi}
Svaka funkcija $\f f\in\mathscr Comp$ je oblika $\kf e^k$ za neke $k\in\N_+$ i $e\in\N$.
\end{korolar}

\begin{proof}
	Za $k$ stavimo mjesnost funkcije $\f f$, a za $e$ kod nekog RAM-programa koji računa $\f f$\\ (koji postoji jer je $\f f$ RAM-izračunljiva).\\ Sada $f=\kf e^k$ slijedi iz propozicije~\ref{prop:computeind}\eqref{it:progind} i korolara~\ref{kor:ram1fun}.
\end{proof}

\begin{korolar}[{name=[svaka parcijalno rekurzivna funkcija ima indeks]}]\label{kor:pii}
Svaka parcijalno rekurzivna funkcija ima indeks.
\end{korolar}

\begin{proof}
Neka je $k\in\N_+$ te $\f f^k$ parcijalno rekurzivna funkcija. Prema teoremu~\ref{tm:pir}, $\f f\in\mathscr Comp$. Sada prema korolaru~\ref{kor:pimi} postoje $k'$ i $e$ takvi da je $\f f^k=\kf e^{k'}$. Jednake funkcije moraju imati iste mjesnosti, pa je zapravo $k'=k$, odnosno $\f f^k=\kf e^k$.
\end{proof}

\begin{napomena}[{name=[nejedinstvenost indeksa]}]\label{nap:>1ind'}
Ponekad se govori: "\,\ldots,~dakle funkcija $f$ ima indeks, označimo ga s $e_1$". Tu frazu nije dobro koristiti, jer sugerira jedinstvenost indeksa, što je očito pogrešno: programerska intuicija nam kaže da svaki RAM-program ima beskonačno mnogo ekvivalentnih RAM-programa (možemo dodavati irelevantne ili nedostupne instrukcije). Kako kasnije najčešće ne koristimo nikakva svojstva broja $e_1$ osim da je indeks od $f$, zapravo taj izričaj treba shvatiti kao pokratu za "\ldots,~dakle funkcija $f$ ima indeks; odaberimo jedan njen indeks, fiksirajmo ga u daljnjem razmatranju, i nazovimo ga $e_1$", kao što ćemo uglavnom pisati ubuduće.

	Alternativno, možemo smatrati da smo uzeli \emph{najmanji} indeks za $f$, koji sigurno postoji ako $f$ ima indeks, i jednoznačno je određen zbog dobre uređenosti od $\N$, ali takav pristup ima jedan bitni nedostatak: često iz specifikacije neke funkcije $f$ možemo \emph{izračunati} neki indeks za $f$, ali \textbf{ne možemo} izračunati najmanji indeks za nju. Ugrubo, možemo provjeravati brojeve $e$ redom, ali uvjet zaustavljanja $\kf e=f$ je jednakost funkcij\=a, koja nije izračunljiva. Čak i da su funkcije totalne (što ne moraju biti), morali bismo provjeriti jednakost za sve $\vec x$ iz $\N^k$, kojih je beskonačno mnogo.
\end{napomena}

Drugim, riječima, tromjesna relacija %$index$ (zadana s $\kf e^k=\f f$)
\begin{equation}
index(e,k,\f f):\Longleftrightarrow \kf e^k=\f f
\end{equation}
između $\N$, $\N_+$ i $\mathscr Comp$ nema funkcijsko svojstvo po prvoj varijabli --- ali ima po trećoj: za svaki broj $e$ i mjesnost $k$, propozicija~\ref{prop:computeind} precizno opisuje funkciju $\kf e^k$.

Tako $index$ može poslužiti kao neka vrsta kodiranja: kad želimo algoritmu dati izračunljivu funkciju kao ulazni podatak, ili je vratiti kao izlazni podatak, možemo prenijeti neki njen indeks $e$ ($k$ se obično vidi iz konteksta). To nije doista kodiranje, jer nije jednoznačna funkcija ako kažemo "bilo koji indeks", a nije izračunljiva funkcija ako kažemo "najmanji indeks" --- kao što je opisano u napomeni~\ref{nap:>1ind'}. Ipak, ako takav rad s indeksima shvatimo kao parcijalnu specifikaciju, to može funkcionirati.

\begin{primjer}[{name=[zadavanje funkcije višeg reda na indeksima]}]\label{pr:parcspecind}
Zamislimo da imamo funkciju $F:\mathscr Comp_2\rightharpoonup\mathscr Comp_3$, koja %. Drugim ri\-je\-či\-ma, $F$
	preslikava dvomjesne RAM-izračunljive funkcije u tromjesne RAM-izračunljive funkcije. Kao i prije, htjeli bismo izračunljivost funkcije $F$ opisati pomoću izračunljivosti prateće funkcije $\N F$, koja prima indeks funkcije $\f f$ i vraća indeks funkcije $F(\f f)$. Zbog napomene~\ref{nap:>1ind'} to nije potpuni opis funkcije $\N F$, ali važno svojstvo koje želimo sačuvati % ne možemo time potpuno opisati, ali možemo reći što od nje tražimo: to 
	je da \emph{za svaki} $e\in\N$ bude
\begin{equation}\label{eq:parcspecind}
    \kf{\N F(e)}^3=F(\kf e^2)\text.
\end{equation}
Riječima, ako $F$ preslikava $\f f^2$ u $\f g^3$, tada $\N F$ mora preslikavati \emph{svaki} indeks za $\f f^2$ u \emph{neki} (ne nužno isti) indeks za $\f g^3$ --- a ako $\f f\notin\dom F$, tada \emph{nijedan} indeks za $\f f$ ne smije biti u $\dom{\N F}$. Takvih funkcija općenito ima neprebrojivo mnogo --- jer indeksa za svaku $\f g\in\im F$ ima beskonačno mnogo --- pa ih ima i neizračunljivih. Ali ako \emph{postoji} takva funkcija $\N F$ koja je izračunljiva u nekom smislu i zadovoljava~\eqref{eq:parcspecind}, kažemo da je $F$ izračunljiva u istom tom smislu.

Takve funkcije možemo i komponirati: ako imamo $G:\mathscr Comp_3\rightharpoonup\mathscr Comp_1$ sa sličnom specifikacijom, koja preslikava $\f g^3$ u $\f h^1$, tada iako ne znamo koji će nam indeks od $\f g$ funkcija $\N F$ dati, funkcija $\N G$ mora ispravno raditi za \emph{sve} indekse od $\f g$, pa će na kraju $\N G\circ\N F$ dati neki indeks za $\f h$, ako joj damo (bilo koji) indeks za $\f f$.
\end{primjer}

\subsection{Restrikcije i grananja parcijalnih funkcija}

Sheme poput one iz primjera~\ref{pr:parcspecind} možemo kombinirati s "pravim" kodiranjima: recimo, za svaki $k\in\N_+$, funkcija $apply_k:\N^k\times\mathscr Comp_k\rightharpoonup\N$, koja prima $\vec x^k$ i $\f f^k$, i vraća $\f f(\vec x)$ ako je $\vec x\in\dom{\f f}$, ima svoju prateću funkciju koja prima $\langle\vec x\rangle$ i bilo koji indeks za $\f f$, i vraća $\f f(\vec x)$ ako postoji.
\begin{equation}\label{eq:Napply}
    \N apply_k(x,e):\simeq\f{univ}(x,e)\text{,\quad za }\f{lh}(x)\eq k
\end{equation}

\begin{napomena}[{name=[restrikcija na izračunljiv skup čuva izračunljivost]}]\label{nap:restrprek}
	Nažalost, iz~\eqref{eq:Napply} još uvijek ne slijedi da je $\N apply$ izračunljiva, iako su $\f{univ}$, $\f{lh}$ i $=$ izračunljive --- jer trebamo neki rezultat koji kaže da je restrikcija parcijalno rekurzivne funkcije na (primitivno) rekurzivan skup ponovo parcijalno rekurzivna. To sigurno možemo "na prste" --- recimo, probajte pokazati da je
    \begin{equation}\label{eq:restrprek}
        (\f G|_{\f R})(\vec x)\simeq\f G(\vec x)+\mu y\bigl(\f{Sc}(y)\eq\chi_{\f R}(\vec x)\bigr)
\end{equation}
--- ali zapravo će to trivijalno slijediti iz rezultata koji ćemo uskoro dokazati. %u idućoj točki. %Ipak, ideja prikaza restrikcije kao zbroja s funkcijom koja je na nekom lijepom skupu nula, a izvan njega nedefinirana --- bit će nam od koristi kasnije, u poglavlju~\ref{ch:re}.
\end{napomena}

%\subsection{Parcijalno rekurzivna verzija teorema o grananju}

Na početku točke~\ref{sec:tech} bilo je riječi o teškoćama koje marljiva evaluacija donosi ako želimo u našem funkcijskom jeziku implementirati grananje s funkcijama koje nisu nužno totalne. Zapravo, jedino što možemo koristiti je kompozicija, jer primitivna rekurzija je definirana samo na totalnim funkcijama, a minimizacija na relacijama čije karakteristične funkcije su također totalne --- ali marljiva evaluacija znači da se u kompoziciji sve "unutarnje" funkcije evaluiraju uvijek, pa parcijalnost bilo koje od njih znači parcijalnost čitave kompozicije.

Dakle, način da se izvučemo je da našoj funkciji $If$ ne damo već izračunane \emph{vrijednosti} $\f g(\vec x)$ i $\f h(\vec x)$, već neevaluirane \emph{funkcije} $\f g$ i $\f h$. Tada s obzirom na uvjet odaberemo jednu od njih, i onda je tek izračunamo na $\vec x$: umjesto $y\t?\f g(\vec x)\t:\f h(\vec x)$ imamo $(y\t?\f g\t:\f h)(\vec x)$. Indeksi (kao "pokazivači na funkcije") nam omogućuju da tu tehniku doista provedemo.

\begin{teorem}[Teorem o grananju, parcijalno rekurzivna verzija]\label{tm:gprek}
Neka su $k,l\in\N_+$, neka su $\f G_0^k$, $\f G_1^k$, $\f G_2^k$,~\ldots, $\f G_l^k$ parcijalno rekurzivne funkcije, a $\f R_1^k$, $\f R_2^k$,~\ldots, $\f R_l^k$ u parovima disjunktne rekurzivne relacije, sve iste mjesnosti.
	
	Tada je funkcija $\f F:=\IF{\f R_1:\f G_1,\f R_2:\f G_2,\dots,\f R_l:\f G_l,\f G_0}$ također parcijalno rekurzivna.
\end{teorem}
\begin{proof}
Za svaki $i\in[0\dd l]$, funkcija $\f G_i^k$ je parcijalno rekurzivna, pa prema korolaru~\ref{kor:pii} ima indeks; fiksirajmo jedan i označimo ga s $e_i$ (pogledajte napomenu~\ref{nap:>1ind'} za značenje ove fraze). Prema teoremu~\ref{tm:grek} (rekurzivna verzija), funkcija
%\begin{equation}
$\f H^k:=\IF{\f R_1\!:\f C_{e_1}^k,\f R_2:\f C_{e_2}^k,\dots,\f R_l:\f C_{e_l}^k,\f C_{e_0}^k}$
%\end{equation}
je rekurzivna (konstante su primitivno rekurzivne pa su rekurzivne, a uvjeti su u parovima disjunktni i rekurzivni po pretpostavci). Tvrdimo da je
\begin{equation}\label{eq:gprekdef}
    \f F(\vec x)\simeq\f{comp}_k\bigl(\vec x,\f H(\vec x)\bigr)\text.
\end{equation}
	Doista, neka je $\vec x\in\N^k$ proizvoljan. Ako vrijedi $\f R_i(\vec x)$ za neki (zbog disjunktnosti jedinstveni) $i\in[1\mspace{-1mu}\dd l]$, tada je po teoremu~\ref{tm:grek}, $\f H(\vec x)=\f C_{e_i}(\vec x)=e_i$, pa je
\begin{equation}
    \f{comp}_k\bigl(\vec x,\f H(\vec x)\bigr)\simeq\f{comp}_k(\vec x,e_i)\simeq\kf{e_i}(\vec x)\simeq\f G_i(\vec x)\simeq\f F(\vec x)\text.
\end{equation}
Ako pak ne vrijedi $\f R_i(\vec x)$ ni za koji $i$, tada je opet po teoremu~\ref{tm:grek}, $\f H(\vec x)=\f C_{e_0}(\vec x)=e_0$, pa je kao i prije $\f{comp}_k\bigl(\vec x,\f H(\vec x)\bigr)\simeq\f G_0(\vec x)\simeq\f F(\vec x)$.

Sada parcijalna rekurzivnost slijedi iz~\eqref{eq:gprekdef}, jer je $\f F$ dobivena kompozicijom iz parcijalno rekurzivnih funkcija $\f{comp}_k$, $\f H$ i koordinatnih projekcija.
\end{proof}

U teoremu~\ref{tm:grek} nismo mogli ispustiti $\f G_0$, jer njena podrazumijevana vrijednost $\varnothing^k$ nije rekurzivna (nije uopće totalna). Ali $\varnothing^k$ jest parcijalno rekurzivna, tako da ovdje možemo ispustiti granu "inače" --- samo nam treba neki indeks za $\varnothing^k$, da bi $\f H$ bila totalna funkcija.

Za to možemo iskoristiti propoziciju~\ref{prop:computeind}\eqref{it:nprogind} --- svi brojevi iz $\f{Prog}\kompl$ indeksi su prazne funkcije. Posebno lijep takav broj je $0$, koji nije u $\f{Prog}$ jer uopće nije u $\f{Seq}$: naime, $\overline{\f{part}}\bigl(0,\f{lh}(0)\bigr)=\overline{\f{part}}(0,0)=\langle\rangle=1\ne0$.

\begin{korolar}[{name=[{teorem o grananju, parcijalno rekurzivna verzija, bez "inače"}]}]\label{kor:gprek}
Neka su $k,l\in\N_+$, neka su $\f G_1^k$, $\f G_2^k$,~\ldots, $\f G_l^k$ parcijalno rekurzivne funkcije, a $\f R_1^k$, $\f R_2^k$,~\ldots, $\f R_l^k$ u parovima disjunktne rekurzivne relacije, sve iste mjesnosti.

	Tada je i funkcija $\f F:=\IF{\f R_1\mspace{-1mu}:\f G_1,\f R_2:\f G_2,\dots,\f R_l:\f G_l}$ parcijalno rekurzivna.
\end{korolar}
\begin{proof}
	Tvrdnja slijedi iz teorema~\ref{tm:gprek}, uvrštavajući za $\f G_0$ parcijalno rekurzivnu (primjer~\ref{pr:varnothingprek}) funkciju $\varnothing^k$, odnosno njen indeks $e_0=0$ u dokaz.
\end{proof}

\begin{korolar}[{name=[restrikcija na rekurzivan skup čuva parcijalnu rekurzivnost]}]\label{kor:restrprek}
Neka je $k\in\N_+$, neka je $\f G^k$ parcijalno rekurzivna funkcija i $\f R^k$ rekurzivna relacija iste mjesnosti. Tada je i restrikcija $\f G|_{\f R}$ parcijalno rekurzivna.
\end{korolar}
\begin{proof}
Tvrdnja slijedi iz korolara~\ref{kor:gprek}, uvrštavajući $l:=1$, $\f G_1:=\f G$ te $\f R_1:=\f R$. Funkcija $\IF{\f R:\f G}$ je upravo jednaka $\f G|_{\f R}$: domena joj je $\dom{\f G}\cap\f R$, a vrijednosti su joj jednake vrijednostima funkcije $\f G$ na tom skupu.
\end{proof}

%\begin{napomena}\label{nap:restrprekcomp}
%    Korolar~\ref{kor:restrprek} smo zapravo već dokazali s~\eqref{eq:restrprek}. Još jedan duhovit dokaz na isti trik:
%\begin{equation}
%    (\f G|_{\f R})(\vec x)\simeq\f G(\vec x)+\f{comp}\bigl(\vec x,\chi_{\f R}(\vec x)\bigr)\text,
%\end{equation}
%    što proizlazi iz $\chi_{\f R}(\vec x)\in\{0,1\}$, s tim da je $0$ indeks prazne funkcije, a $1=\kprog{[\,]}$ indeks nulfunkcije, koja zbrojena s $\f G$ opet daje $\f G$.
%\end{napomena}