rek.tex

\chapter{Rekurzivne funkcije}\label{ch:rek}

Iz uglavnom povijesnih razloga, prvi doticaj s programiranjem za većinu ljudi bude kroz \emph{imperativno} programiranje: algoritmi kao \emph{programi}, nizovi \emph{naredaba} koje mijenjaju stanje neke zajedničke \emph{memorije} nad kojom se izvršavaju. Mnogo \emph{mainstream} programskih jezika spada u tu paradigmu: gotovo svi jezici niske razine, C, C\texttt{++}, Python, Rust,~\ldots\ (Java preko tog imperativnog sloja prostire "objektno-orijentirani veo", ali fundamentalno, provođenje algoritma je i dalje izvršavanje naredaba i mijenjanje memorije). Kontrola toka (izvršavanje određenih naredbi nula ili više puta, što može ovisiti o stanju memorije) se u takvim jezicima obično ostvaruje \emph{skokovima} (uvjetnim ili bezuvjetnim, kao što su \dec\ ili \goto\ u RAM-stroju), ili na višoj razini, \emph{petljama} koje mijenjaju \emph{kontrolnu varijablu} i testiraju je da bi ustanovile trebaju li se nastaviti izvršavati, ili zaustaviti.

Ipak, postoji i drugi pristup: matematičke formule kojima se definiraju funkcije često se mogu shvatiti kao algoritmi za njihovo računanje. Važno je primijetiti da se u tom slučaju nikakve vrijednosti ne mijenjaju: $\f f(x,y):=x^2+3y+2$ nije naredba koja mijenja $x$ niti $y$, već matematička definicija, koja kazuje kako izračunati vrijednosti funkcije $\f f$, primjerice na prirodnim brojevima, ako ih znamo potencirati, množiti i zbrajati.

U toj paradigmi, umjesto praznog programa, imamo aksiom da je nulfunkcija izračunljiva. Umjesto instrukcije \inc\ koja mijenja sadržaj registra na kojem djeluje, imamo funkciju \emph{sljedbenika}, koja proizvodi novi prirodni broj: sljedbenik ulaznog podatka. Umjesto ulaznih registara, imamo \emph{koordinatne projekcije} koje vraćaju pojedini ulazni podatak. Umjesto pomoćnih registara imamo pomoćne funkcije, kojima korak po korak gradimo ono što nam treba. Umjesto slijednog izvršavanja naredaba ovdje imamo \emph{kompoziciju}, kojom npr.\ iz funkcija $\f{add}^3$, $\f{mul}^2$ i $\f{pow}^2$, konstanti $\f C_2^2$ i $\f C_3^2$ te koordinatnih projekcija $\f I_1^2$ i $\f I_2^2$ dobivamo funkciju $\f f$ iz prethodnog odlomka. Umjesto grananja ovdje imamo definiciju funkcije \emph{po slučajevima}, gdje su uvjeti disjunktne relacije (vrijedi najviše jedan od njih; ako ne vrijedi nijedan, funkcija nije definirana). Umjesto petlji (ne možemo mijenjati kontrolnu varijablu!) funkcijsko programiranje koristi \emph{rekurziju}, kao način da se elegantno opiše izračunavanje funkcija više puta s različitim vrijednostima argumenata, a da nikakve varijable pritom ne mijenjaju svoje vrijednosti. 

Specijalni slučaj --- \emph{primitivna} rekurzija --- odgovara petljama koje se izvršavaju unaprijed određeni broj puta, i kao takve ne mogu biti beskonačne. To znači da algoritmi dobiveni primitivnom rekurzijom uvijek stanu, pa su \emph{primitivno rekurzivne} funkcije koje oni računaju uvijek totalne. To je dobro za programiranje konkretnih funkcija, ali vidjeli smo već u uvodu da totalni algoritmi nisu dovoljni da bi opisali \emph{sve} izračunljive funkcije. Zato nam treba \emph{opća rekurzija}, odnosno sasvim općenit način da unutar definicije neke funkcije koristimo (najčešće pozivamo) istu tu funkciju. Tehniku za to razvit ćemo tek u točki~\ref{sec:rec}, a zasad ćemo samo uvesti jedan posebni oblik koji odgovara \emph{minimizaciji} relacije --- traženju najmanjeg prirodnog broja s nekim svojstvom. To neće nužno dati totalnu funkciju (na primjer, u slučaju prazne relacije), ali ponekad hoće. Funkcije nastale tim postupkom iz izračunljivih relacija (eventualno još komponirane s nekim izračunljivim funkcijama) zovemo \emph{parcijalno rekurzivnim} funkcijama, a one među njima koje su totalne zovemo \emph{rekurzivnim} funkcijama. Naša intuicija o nužnosti razmatranja parcijalnih funkcija da bismo dobili sve totalne izračunljive funkcije, sada se može formalizirati kao: postoje rekurzivne funkcije koje nisu primitivno rekurzivne. Dokaz te tvrdnje može se pronaći u~\cite[dodatak]{skr:Vuk}. Važniji rezultat, koji ćemo dokazati, je da se skup parcijalno rekurzivnih funkcija podudara sa skupom $\mathscr Comp$ RAM-izračunljivih funkcija.

%\section{Inicijalne funkcije}

Ako želimo dobivati izračunljive funkcije slaganjem (kompozicijom, primitivnom rekurzijom,~\ldots) drugih funkcija, odnekud moramo početi: neke \emph{najjednostavnije} brojevne funkcije moramo aksiomatski prihvatiti kao izračunljive. Te će funkcije biti toliko jednostavne da neće biti sumnje u njihovu izračunljivost, a moći ćemo navesti i formalniji razlog zašto ih smatramo izračunljivima: dokazat ćemo da su makro-izračunljive, pa time i RAM-izračunljive.

\begin{definicija}[{name=[inicijalne funkcije]}]\label{def:init}
\emph{Inicijalne funkcije} su sljedeće:
\begin{itemize}
    \item \emph{nulfunkcija} $\f Z^1$, zadana sa $\f Z(x):=0$;
    \item \emph{sljedbenik} $\f{Sc}^1$, zadana sa $\f{Sc}(x):=x+1$;
    \item za svaki $k\in\N_+$, za svaki $n\in[1\mspace{-1mu}\dd k]$, \emph{$n$-ta $k$-mjesna koordinatna projekcija} $\f I_n^k$,\\ zadana s $\f I_n(\vec x^k):=\f I_n(x_1,x_2,\dotsc,x_k):=x_n$.\qedhere
\end{itemize}
\end{definicija}

Prvu stavku možemo interpretirati kao izračunljivost (karakteristične funkcije) prazne relacije~$\emptyset^1$. Treća stavka zapravo govori da je identiteta $id_{\N^*}$ izračunljiva, ako je razdvojimo po mjesnostima u familiju $id^k,k\in\N$ pa u skladu s napomenom~\ref{nap:brip} svaku $id^k=id_{\N^k}$ prikažemo pomoću $k$ koordinatnih funkcija $\f I_n^k,n\in[1\mspace{-1mu}\dd k]$.

\begin{napomena}[{name=[totalnost inicijalnih funkcija]}]\label{nap:inittot}
Sve inicijalne funkcije su totalne: $\dom{\f Z}=\dom{\f{Sc}}=\N$, a $\dom{\f I_n^k}=\N^k$.
\end{napomena}

Vidimo da inicijalnih funkcija zapravo ima beskonačno (prebrojivo) mnogo, ali su samo triju mogućih tipova. Nulfunkcija i sljedbenik omogućavaju reprezentaciju brojeva kao konstantnih jednomjesnih funkcija, a koordinatne projekcije omogućavaju individualni rad sa svakim pojedinim argumentom funkcije prema njegovu rednom broju $n$ (od $k$ njih ukupno).

\begin{propozicija}[{name=[makro-izračunljivost inicijalnih funkcija]}]\label{prop:initmacro}
Svaka inicijalna funkcija je makro-izračunljiva.
\end{propozicija}
\begin{proof}
    Već smo vidjeli da prazan (makro- ili RAM-\!) program (algoritam $[\,]^1$) računa funkciju $\f Z$. Iz semantike instrukcije \textsc{remove} vidimo da za sve $k\ge n\ge 1$ makro-algoritam $\begin{prog}0.&\remove{n}{0}\end{prog}^k$ računa $\f I_n^k$. Također, makro-algoritam $\begin{prog}
0.&\remove10\\
1.&\incr0
\end{prog}^1$ računa $\f{Sc}$:
\vspace{-0.3em}
\begin{equation}
    \begin{array}{r@{\;}l|cc}
\SwapAboveDisplaySkip
        & & \reg0 & \reg1 \\
        & & 0 & x\\\hline 
        0.&\remove10&x & 0\\
        1.&\incr0 & x+1 & 0
    \end{array}\text{\;.\qedhere}
\end{equation}
\end{proof}

\begin{korolar}[{name=[RAM-izračunljivost inicijalnih funkcija]}]\label{kor:initram}
Svaka inicijalna funkcija je RAM-izračunljiva.
\end{korolar}
\begin{proof}
Spljoštenja makro-programa iz dokaza propozicije~\ref{prop:initmacro}\\ daju nam RAM-algoritme za inicijalne funkcije.
\end{proof}

\section{Kompozicija}

Kompozicija je intuitivno jednostavna operacija (kao i slijedno izvršavanje naredaba u imperativnim programima): izračunamo vrijednost jedne funkcije, i uvrstimo je u definiciju druge funkcije. No definicija je prilično tehnička.%, uglavnom zbog nekih odluka koje smo donijeli na početku, o tome kako shvaćamo algoritme.

Htjeli bismo reći: "kompozicija $\f H\circ\f G$ dviju izračunljivih funkcija, $\f G^k$ i $\f H^l$, je izračunljiva funkcija". Da bi ta kompozicija bila dobro definirana, kodomena od $\f G^k$ bi morala biti $\N^l$. U skladu s napomenom~\ref{nap:brip}, to znači da imamo $l$ izračunljivih koordinatnih funkcija, $\f G_1^k,\dotsc,\f G_l^k$, svaka od kojih daje po jedan ulazni podatak za $\f H^l$. Zato komponiranje više nije nužno binarna operacija: pišemo $\f H\circ(\f G_1,\dotsc,\f G_l)$.

Drugi tehnički detalj tiče se domene kompozicije. Promotrimo kompoziciju $\f F^1:=\f I_1^2\circ(\f Z^1,\varnothing^1)$. Ta funkcija je svakako izračunljiva, ali \emph{što} je ona? Konkretno, koliko je $\f F(5)$? Na prvi pogled, $\f F(5)=\f I_1\bigl(\f Z(5),\varnothing(5)\bigr)=\f Z(5)=0$ --- i tako za svaki ulaz, dakle $\f F =\f Z$. Na drugi pogled, da bismo izračunali $\f F(5)$, moramo izračunati $\f Z(5)=:y_1$, zatim "izračunati" $\varnothing(5)=:y_2$, i na kraju izračunati $\f I_1(y_1,y_2)=y_1$. Tako algoritam za računanje $\f F$ ne stane s ulazom $5$ (niti s ikojim drugim ulazom), jer njegov drugi korak ne stane --- dakle $\f F=\varnothing$. Što je od toga?

%\subsection{Lijena i marljiva evaluacija}

Ta dilema je dobro poznata u modernom računarstvu, i oba pristupa nalazimo u današnjim programskim jezicima. Prvi pristup zove se \emph{lijena} evaluacija (\emph{lazy evaluation}) i koriste ga neki čisto funkcijski jezici poput Haskella. Prednost je bogatija semantika (više izraza ima vrijednost), a i beskonačne strukture nisu nužno problem ako nam treba samo njihov konačni početak. Pogledajmo kako to izgleda u Haskellu:
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
    Prelude> let i12(x, y) = x
    Prelude|     z(x) = 0
    Prelude|     prazna(x) = undefined
    Prelude|     f(x) = i12(z(x), prazna(x))
    Prelude| in f(5)
    0
\end{verbatim}
\end{minipage}\end{equation}

Drugi pristup zove se \emph{marljiva} evaluacija (\emph{eager evaluation}) i podrazumijeva se u gotovo svim imperativnim jezicima, pa i mnogim funkcijskima (kao što je ML\@). Prednost je lakša implementacija, i lakše razmišljanje o kodu (a time i lakši \emph{debugging}). %Primjer u Pythonu:
\begin{equation}\begin{minipage}{0.8\textwidth}
\begin{verbatim}
    >>> def i12(x, y): return x
    >>> def z(x): return 0
    >>> def prazna(x):
    ...     while True: pass
    >>> def f(x): return i12(z(x), prazna(x))
    >>> f(5)
    ^C KeyboardInterrupt
\end{verbatim}
\end{minipage}\end{equation}

Važno je napomenuti da, kao i inače kad je riječ o implementaciji algoritama (princip opće izračunljivosti), bilo koji od tih pristupa može \emph{simulirati} onaj drugi. S obzirom na to da nas performanse ne zanimaju, odabrat ćemo \textbf{marljivu} evaluaciju jer je jednostavnija za implementaciju (u našem slučaju, za dokaz ekvivalentnosti s RAM-izračunljivošću odnosno za konstrukciju kompajlera u RAM-programe), a poslije ćemo opisati kako simulirati lijenu evaluaciju kad nam bude potrebna. Jedno od mjesta gdje će nam sigurno trebati je implementacija grananja gdje nisu sve grane totalne, poput onog što radi operator \texttt{?:}\ u programskom jeziku C; recimo, \texttt{1?z(5):prazna(5)} ima vrijednost $0$. U našoj terminologiji, to će biti funkcija definirana po slučajevima iz parcijalno rekurzivnih funkcija. U početku ćemo se baviti samo totalnim (primitivno rekurzivnim i rekurzivnim) funkcijama, pa nam to neće trebati --- no dobro je odmah pravilno formalizirati domenu kompozicije, da ne bismo morali poslije mijenjati definiciju.

Dakle, želimo da je $\f H\circ(\f G_1,\dotsc,\f G_l)$ definirana u $\vec x$ ako je \emph{svaka} $\f G_i$ definirana u $\vec x$, a ako označimo $g_i:=\f G_i(\vec x)$, još je $\f H$ definirana u $\vec g^{l}$. Matematički rečeno, u domeni kompozicije su sve one $k$-torke iz presjeka domena pojedinih $\f G_i$, takve da je $l$-torka njihovih vrijednosti element domene od $\f H$.
\begin{definicija}[{name=[kompozicija]}]
Neka su $k,l\in\N_+$ te neka su $G_1^k$, $G_2^k$,~\ldots, $G_l^k$ i $H^l$ funkcije. Za funkciju $F^k$ definiranu s
\begin{align}
\SwapAboveDisplaySkip
\label{eq:domkomp}
    \dom{F}&:=\left\{\vec x\in\bigcap\nolimits_{i=1}^l\dom{G_i}\;\middle|\;\bigl(G_1(\vec x),G_2(\vec x),\dotsc,G_l(\vec x)\bigr)\in\dom{H}\right\}\text,\\
\label{eq:defkomp}
    F(\vec x)&:=H\bigl(G_1(\vec x),G_2(\vec x),\dotsc,G_l(\vec x)\bigr)\text{, za sve $\vec x\in\dom F$,}
\end{align}
kažemo da je dobivena \emph{kompozicijom} iz funkcija $G_1$, $G_2$,~\ldots, $G_l$ i $H$.

	Skraćeno pišemo $F:=H\circ(G_1,G_2,\dotsc,G_l)$. %Operator $\circ$ smatramo lijevo asociranim.

Za skup funkcija $\mathcal F$ kažemo da je \emph{zatvoren na kompoziciju} ako za sve $k,l\in\N_+$, za sve $k$-mjesne $G_1,G_2,\dotsc,G_l\in\mathcal F$ te za sve $l$-mjesne $H\in\mathcal F$, vrijedi $H\circ(G_1,G_2,\dotsc,G_l)\in\mathcal F$.
\end{definicija}
U skladu s napomenom~\ref{nap:parcdef}, izraze~\eqref{eq:domkomp} i~\eqref{eq:defkomp} zajedno skraćeno pišemo kao
\begin{equation}
    F(\vec x):\simeq H\bigl(G_1(\vec x),G_2(\vec x),\dotsc,G_l(\vec x)\bigr)\text,
\end{equation}
gdje podrazumijevamo da izraz s ugniježđenim funkcijskim pozivima $f(\vec v^{k})$ ima vrijednost ako (rekurzivno) svaki $v_i$ ima vrijednost, a $k$-torka njihovih vrijednosti je element $\dom{f}$.

Dakle, kod komponiranja parcijalnih funkcija moramo voditi računa o domeni --- ali dobro je znati da s\=amo komponiranje ne može narušiti totalnost.

\begin{lema}[{name=[domena kompozicije slijeva s totalnom funkcijom]}]\label{lm:comptot}
    Neka su $k,l\in\N_+$ te neka su $G_1^k$, $G_2^k$, \ldots, $G_l^k$ i $H^l$ funkcije.
    
    Ako je $H$ totalna, tada je $\dom{H\circ(G_1,\dotsc,G_l)}=\bigcap_{i=1}^l\dom{G_i}$.
\end{lema}
\begin{proof}
    Tvrdnja slijedi iz~\eqref{eq:domkomp}, jer je uvjet $\bigl(G_1(\vec x),\dotsc,G_l(\vec x)\bigr)\in\dom H=\N^l$ uvijek ispunjen za $\vec x\in\bigcap_{i=1}^l\dom{G_i}$.
\end{proof}

\begin{korolar}[{name=[kompozicija s totalnom funkcijom slijeva ne mijenja domenu]}]\label{kor:comptot}
    Ako je $H^1$ totalna funkcija, i $G$ brojevna funkcija, tada je $\dom{H\circ G}=\dom G$.
\end{korolar}
\begin{proof}
    Ovo je tvrdnja leme~\ref{lm:comptot} za $l=1$.
\end{proof}

\begin{propozicija}[{name=[totalnost kompozicije totalnih funkcija]}]\label{prop:comptot}
Svaka kompozicija totalnih funkcija je totalna.
\end{propozicija}
\begin{proof}
    Ako je svaka $G_i^k$ totalna, tada je $\dom{G_i}\!=\N^k$ za sve $i$, pa je po lemi~\ref{lm:comptot} također i $\dom{H\circ(G_1,\dotsc,G_l)}=\bigcap_{i=1}^l\N^k=\N^k$.
\end{proof}

\begin{primjer}[{name=[prikaz konstante kao kompozicije inicijalnih funkcija]}]\label{pr:C23}
	$\f C_2^3=\f{Sc}\circ\f{Sc}\circ\f Z\circ\f I_1^3$. Doista, za sve $(x,y,z)\in\N^3$ je
\begin{multline}
(\f{Sc}\circ\f{Sc}\circ\f Z\circ\f I_1^3)(x,y,z)=(\f{Sc}\circ\f{Sc}\circ\f Z)\bigl(\f I_1^3(x,y,z)\bigr)=(\f{Sc}\circ\f{Sc}\circ\f Z)(x)=\\
=(\f{Sc}\circ\f{Sc})\bigl(\f Z(x)\bigr)=(\f{Sc}\circ\f{Sc})(0)=\f{Sc}\bigl(\f{Sc}(0)\bigr)=\f{Sc}(1)=2=\f C_2^3(x,y,z).\text\qedhere
\end{multline}
    %Sve konstante $\f C_n^k$ se mogu slično tako prikazati (propozicija~\ref{prop:konst}).
\end{primjer}

%\subsection{RAM-izračunljivost kompozicije}

\begin{lema}[{name=[zatvorenost skupa $\mathscr Comp$ na kompoziciju]}]\label{lm:compram}
Skup RAM-izračunljivih funkcija, $\mathscr Comp$, zatvoren je na kompoziciju.
\end{lema}
\begin{proof}
Pomoću funkcijskog makroa i uz marljivu evaluaciju, algoritam je očit: prvo izračunamo sve $\f G_i$ u istim argumentima $\vec x$, spremimo njihove povratne vrijednosti u $l$ pomoćnih registara nakon ulaznih, a zatim izračunamo $\f H$ s tako dobivenim brojevima.

Precizno, neka su $k,l\in\N_+$ proizvoljni te neka su $\f G_1^k$, $\f G_2^k$,~\ldots,~$\f G_l^k$ i $\f H^l$ proizvoljne RAM-izračunljive funkcije. To znači da postoje RAM-algoritmi $P_{\f G_1}^k$, $P_{\f G_2}^k$,~\ldots, $P_{\f G_l}^k$ i $P_{\f H}^l$, koji ih redom računaju. Tvrdimo da makro-program
\begin{equation}
\label{eq:compmacro}
    Q_{\f F}:=\begin{prog}\!
    0.&P_{\f G_1}(\reg1,\reg2,\dotsc,\reg k)\to\reg{k+1}\textsc{ using }\reg{k+l+1}..\\
    1.&P_{\f G_2}(\reg1,\reg2,\dotsc,\reg k)\to\reg{k+2}\textsc{ using }\reg{k+l+1}..\\
    &\vdots\\
    (l-1).&P_{\f G_l}(\reg1,\reg2,\dotsc,\reg k)\to\reg{k+l}\textsc{ using }\reg{k+l+1}..\\
    l.&P_{\f H}(\reg{k+1},\reg{k+2},\dotsc,\reg{k+l})\to\reg0\textsc{ using }\reg{k+l+1}..
    \end{prog}
\end{equation}
	računa $\f F:=\f H\circ(\f G_1,\f G_2,\dotsc,\f G_l)$. Prema definiciji~\ref{def:compute}, neka je $\vec x\in\N^k$ proizvoljan. Ako je $\vec x\in\dom F$, prema definiciji~\eqref{eq:domkomp} je za sve $i\in[1\mspace{-1mu}\dd l]$, $\vec x\in\dom{\f G_i}$, pa izvršavanje svake od prvih $l$ instrukcija programa $Q_{\f F}$ stane, i u $\reg{k+i}$ zapiše vrijednost $\f G_i(\vec x)=:y_i$. Pritom je važno da će, prema propoziciji~\ref{prop:semfmacro}, svi ostali registri do $\reg{k+l}$ ostati sačuvani, odnosno računanje $y_i$ neće uništiti one ranije izračunane, niti ikoji $x_j$ potreban za računanje kasnijih. Uvjet $\vec y^{l}\in\dom{\f H}$, također iz~\eqref{eq:domkomp}, znači da će i izvršavanje zadnje instrukcije u $Q_{\f F}$ stati, i u $\reg0$ zapisati $\f H(\vec y)=F(\vec x)$. Tablično,
\begin{equation}
    \begin{array}{r@{\;}l|ccccccc}
\SwapAboveDisplaySkip
      &               &\reg0       &\reg1&\reg{k}&\reg{k+1}     &\reg{k+2}     &\reg{k+l}     &\reg{k+l+1}..\\
      &               & 0          &x_1  &x_k    &0             &0             &0             &0            \\\hline
0.    &P_{\f G_1}\dots& 0          &x_1  &x_k    &\f G_1(\vec x)&0             &0             &0            \\
1.    &P_{\f G_2}\dots& 0          &x_1  &x_k    &\f G_1(\vec x)&\f G_2(\vec x)&0             &0            \\
      &\vdots                                                                                               \\
(l-1).&P_{\f G_l}\dots& 0          &x_1  &x_k    &\f G_1(\vec x)&\f G_2(\vec x)&\f G_l(\vec x)&0            \\
l.    &P_{\f H}\dots  &\f F(\vec x)&x_1  &x_k    &\f G_1(\vec x)&\f G_2(\vec x)&\f G_l(\vec x)&0
    \end{array}\text.
\end{equation}
\smallskip

Ako $\vec x\notin\dom{\f F}$, prema~\eqref{eq:domkomp} to se može dogoditi na dva načina. Ako $\vec x\notin\bigcap_{i=1}^l\dom{\f G_i}$, postoji neki $i$ takav da $\vec x\notin\dom{\f G_i}$, pa označimo s $i_0$ najmanji takav\!. Tada će izvršavanje programa $Q_{\f F}$ doći do instrukcije s rednim brojem $i_0-1$, ali izvršavanje te instrukcije neće nikada stati prema propoziciji~\ref{prop:semfmacro}, pa ni $Q_{\f F}$-izračunavanje s $\vec x$ neće stati. Ako pak $l$-torka dobivenih povratnih vrijednosti nije u $\dom{\f H}$, izvršavanje $Q_{\f F}$ će zapeti u beskonačnoj petlji na zadnjoj instrukciji, pa opet $Q_{\f F}$-izračunavanje s $\vec x$ neće stati.
Sada prema teoremu~\ref{tm:rem} RAM-algoritam $Q_{\f F}^{\flat k}$ također računa $\f F$, pa je $\f F\in\mathscr Comp$.
\end{proof}

\section{Primitivna rekurzija}

Iz dokaza leme~\ref{lm:compram} je jasno kako točno kompozicija odgovara slijednom iz\-vrša\-va\-nju naredbi. Ipak, već za funkcije poput zbrajanja nam trebaju \emph{petlje}: način da određene naredbe izvršimo neki broj puta koji ovisi o ulaznim podacima. Rekli smo da u funkcijskom programiranju tome odgovaraju rekurzije, no opće rekurzije su vrlo komplicirane za implementaciju, a osim toga teško je ustanoviti kada točno daju totalne funkcije. Zato ćemo aksiomatski propisati samo jedan jednostavni oblik rekurzije, koji odgovara petljama čiji je broj ponavljanja zadan prije početka njihova izvršavanja. Tek kasnije ćemo vidjeti kako se u ovom modelu mogu rješavati opće rekurzije.%definirati izračunljive funkcije kao rješenja općih rekurzija.

%"Broj ponavljanja je poznat" ne djeluje dovoljno precizno --- zapravo, broj ponavljanja bi trebao biti \emph{izračunljiv} nekom funkcijom $\f B$ istog tipa. Da bismo to omogućili, dat ćemo broj ponavljanja kao dodatni argument $y$ našoj funkciji, pa ćemo kompozicijom s $\f B$ na mjestu tog argumenta dobiti željeni broj ponavljanja. Primjer te tehnike vidjet ćete u napomeni~\ref{nap:sumprodH}.
%Način da to preciziramo koristit ćemo još mnogo puta u razvoju teorije, pa je dobro zapamtiti ga: broj ponavljanja dat ćemo kao dodatni argument našoj funkciji, a onda ćemo kompozicijom (na mjestu zadnjeg argumenta) s nekom funkcijom za koju već znamo da je izračunljiva, dobiti željeni broj ponavljanja. Usporedite to s napomenom~\ref{nap:blokovi}.

Za funkcionalni opis petlje moramo prvo opisati \emph{inicijalizaciju} $\f G$, koja odgovara stanju prije početka izvršavanja petlje, a zatim \emph{tijelo} (ponekad zvano \emph{korak}) petlje kao funkciju $\f H$ koja preslikava stanje na početku jednog prolaza kroz petlju, u stanje na kraju tog prolaza. %Vrlo grubo rečeno, želimo modelirati funkciju $\f G\pr\f H:=\f H\circ\f H\circ\dotsb\circ\f H\circ\f G$, gdje je broj $\f H$-ova zadan kao posebni argument $y$.

Programski, primjerice u Pythonu, ograničene petlje kakve promatramo imaju oblik:
\begin{equation}
	\begin{minipage}{0.8\textwidth}
\begin{verbatim}
z = ...  # inicijalizacija varijable z, u nekom kontekstu
for i in range(y): z = ...z...  # tijelo, ažurira z
\end{verbatim}
	\end{minipage}
\end{equation}

Tijelo, pored konteksta $\vec x$ i prethodno izračunane vrijednosti $z$, obično može koristiti i kontrolnu varijablu (u kodu nazvanu \texttt i), koja broji koliko smo puta prošli kroz petlju.

%Ipak, dozvolit ćemo još jednu stvar uobičajenu u petljama: tijelu petlje $\f H$ kao još jedan argument prenijet ćemo "kontrolnu varijablu", koja broji koliko puta smo već prošli kroz petlju. Imperativni jezici niže razine obično implementiraju "primitivne" petlje kontrolnom varijablom koja ide od $0$ do isključivo $y$, recimo C:
%\begin{equation}\label{prog:Cprloop}
%\texttt{for(i=0; i<y; ++i) /* ovdje možemo koristiti i */;}
%\end{equation}
%Ako nam u nekoj petlji ne treba kontrolna varijabla, samo ćemo kompozicijom s prikladnom koordinatnom projekcijom izvući ono što nam treba (npr.\ stanje prije prolaza kroz petlju).

%Formalizirajmo sada to sve u obliku matematičke definicije.

\begin{definicija}[{name=[primitivna rekurzija]}]\label{def:pr}
Neka je $k\in\N_+$ te neka su $G^k$ i $H^{k+2}$ totalne funkcije. Za funkciju $F^{k+1}$\\ definiranu s
\begin{align}
\SwapAboveDisplaySkip
\label{eq:defprb}
F(\vec x,0)&:=G(\vec x)\text,\\
\label{eq:defprk}
F(\vec x,y+1)&:=H\bigl(\vec x,y,F(\vec x,y)\bigr)\text{, za sve $y\in\N$,}
\end{align}
kažemo da je dobivena \emph{primitivnom rekurzijom} iz funkcija $G$ i $H$.

	Skraćeno pišemo $F:=G\pr H$. Smatramo da operator $\pr$ ima niži prioritet od $\circ$.

Za skup funkcija $\mathcal F$ kažemo da je \emph{zatvoren na primitivnu rekurziju} ako za svaki $k\in\N_+$, za svaku totalnu $k$-mjesnu funkciju $G\in\mathcal F$ te za svaku totalnu $(k+2)$-mjesnu funkciju $H\in\mathcal F$ vrijedi $G\pr H\in\mathcal F$.
\end{definicija}

\begin{napomena}[{name=[ulazi i izlaz primitivne rekurzije su totalne funkcije]}]\label{nap:prtot}
	Iz Dedekindova teorema rekurzije~\cite{skr:VukTS} slijedi da je jednadžbama~\eqref{eq:defprb} i~\eqref{eq:defprk} zadana jedinstvena totalna funkcija. Također, primitivna rekurzija je \emph{definirana} samo za totalne funkcije, pa se ne moramo baviti domenama od $G$, $H$ i $G\pr H$ (uvijek su jednake redom $\N^k$, $\N^{k+2}$ i $\N^{k+1}$ za neki $k\in\N_+\mspace{-1mu}$).
\end{napomena}

Budući da ne promatramo brojevne funkcije s nula ulaznih podataka, funkcija $G$ koja zadaje početni uvjet mora biti barem jednomjesna, a onda funkcija $F$ dobivena primitivnom rekurzijom mora biti barem dvomjesna. Svakako bismo htjeli definirati i jednomjesne funkcije primitivnom rekurzijom: kanonski primjer je vjerojatno faktorijel,
\begin{align}
%\SwapAboveDisplaySkip
\label{eq:faktb}
	0!&:=1\text,&&\texttt{f = 1}\\
\label{eq:faktk}
	(n+1)!&:=(n+1)\cdot n!\text,&&\texttt{for i in range(n):~f = (i+1)*f}
\end{align}
samo zasad ne možemo reći da je funkcija $\f{factorial}^1$ ($n\mapsto n!$) dobivena primitivnom rekurzijom, jer ne postoji odgovarajuća funkcija $G$. Recimo, za $\f G:=\f C_1^1$, i odgovarajuću funkciju $\f H^3$, definicija~\ref{def:pr} bi nam dala $\f{factorial}^2$, što nije funkcija koju tražimo. (Ali nije ni daleko od nje, kao što ćemo vidjeti kasnije.)

Definicija višemjesnih funkcija primitivnom rekurzijom sasvim lijepo funkcionira.

\begin{primjer}[{name=[{zbrajanje, množenje i potenciranje primitivnom rekurzijom}]}]\label{pr:addmulpow}
$\f{add}^2=\f I_1^1\pr\f{Sc}\circ\f I_3^3$. Doista, zbrajanje dva broja možemo prikazati kao
\begin{align}
\label{eq:addb}
    x+0&=x & \f{add}(x,0)&=\f I_1^1(x),\\
\label{eq:addk}
    x+(y+1)&=(x+y)+1 &\f{add}(x,y+1)&=(\f{Sc}\circ\f I_3^3)\bigl(x,y,\f{add}(x,y)\bigr).
\end{align}
Slično, $\f{mul}^2=\f Z\pr\f{add}^2\circ(\f I_1^3,\f I_3^3)$. (Sami napišite $\f{pow}$!)
\end{primjer}

Vidimo da se mnoge funkcije mogu napisati koristeći samo inicijalne funkcije, kompoziciju i primitivnu rekurziju --- drugim riječima, primitivno su rekurzivne. No prije formalizacije tog pojma, dokažimo da se primitivna rekurzija može izvršavati na RAM-stroju.

\begin{lema}[{name=[zatvorenost skupa $\mathscr Comp$ na primitivnu rekurziju]}]\label{lm:prram}
Skup $\mathscr Comp$ je zatvoren na primitivnu rekurziju.
\end{lema}
\begin{proof}
Neka je $k\in\N_+$ te neka su $\f G^k,\f H^{k+2}\in\mathscr Comp$ totalne funkcije. One su RAM-izračunljive, pa postoje RAM-algoritmi $P_{\f G}^k$ i $P_{\f H}^{k+2}$ koji ih redom računaju. Želimo naći program koji računa funkciju $\f F^{k+1}:=\f G\pr\f H$. Dakle, u registrima $\reg1$ do $\reg{k}$ se nalazi $\vec x$, dok se u $\reg{k+1}$ nalazi $y$, broj ponavljanja petlje odnosno broj izračunavanja funkcije $\f H$. Prvo, prije petlje moramo izračunati funkciju $\f G$ na prvih $k$ ulaznih registara. Rezultat između prolazaka kroz petlju držat ćemo u $\reg0$, tako da završetkom petlje već bude spreman kao izlazni podatak. Petlju pišemo na standardni način koji smo već vidjeli u makroima $\textsc{zero}$, $\textsc{remove}$, $\textsc{move}$, i programu $P_{\f{add}^3}$. Kontrolnu varijablu držimo u pomoćnom registru $\reg{k+2}$ --- ne možemo koristiti $\reg{k+1}$ jer ide u suprotnom smjeru: svakim izvršavanjem tijela petlje $\reg{k+1}$ se dekrementira, dok se kontrolna varijabla mora inkrementirati (brojeći prolaze kroz petlju).

	Kontrolnu varijablu ne treba inicijalizirati: kako $\reg{k+2}$ nije ulazni registar, na početku izračunavanja njegov sadržaj već jest $0$. Također, inkrementirati kontrolnu varijablu moramo \emph{nakon} izvođenja tijela petlje (funkcijski makro s $P_{\f H}$) jer želimo brojiti samo "završene" prolaze. %inkrementiranjem prije računanja $\f H$ postigli bismo brojenje od $1$ do uključivo $y$. Programski jezici koji broje od nule obično zahtijevaju inkrement poslije: recimo, standard jezika C propisuje da se u~\eqref{prog:Cprloop} inkrement \texttt{++i} obavi nakon tijela petlje (iako se piše prije).

Sve u svemu, tvrdimo da makro-program
\begin{equation}
\label{eq:prmacro}
    Q_{\f F}:=\begin{prog}
    0.&P_{\f G}(\reg1,\reg2,\dotsc,\reg{k})\to\reg0\textsc{ using }\reg{k+3}..\\
    1.&\decr{k+1}5\\
    2.&P_{\f H}(\reg1,\reg2,\dotsc,\reg{k},\reg{k+2},\reg0)\to\reg0\textsc{ using }\reg{k+3}..\\
    3.&\incr{k+2}\\
    4.&\goto\;1
    \end{prog}
\end{equation}
računa $\f F$. U tu svrhu, po definiciji~\ref{def:compute}, neka je $(\vec x,y)\in\N^{k+1}$ proizvoljan. Na početku $Q_{\f F}$-izračunavanja s $(\vec x,y)$ imamo makro-konfiguraciju
$(0,\vec x,y,0,0,\dotsc,0,0)$, koja iz\-vr\-ša\-va\-njem funkcijskog makroa rednog broja $0$ prelazi u $\bigl(\f G(\vec x),\vec x,y,0,0,\dotsc,1,0\bigr)$ (jer je $\f G$ totalna). % --- ne znamo sadržaj registara od $\reg{k+3}$ nadalje, ali nam nije ni bitan.
	Broj u $\reg0$ je prema~\eqref{eq:defprb} jednak $\f F(\vec x,0)$. Sada ako za sve $i\in[0\dd y]$ označimo $d_i:=\bigl(\f F(\vec x,i),\vec x,y-i,i,0,\dotsc,1,0\bigr)$, upravo smo došli do konfiguracije $d_0$.

	Tvrdimo da za svaki $i<y$, $d_i\leadsto^*d_{i+1}$. %svaka konfiguracija $d_i$ za $i<y$, prelazi u konačno mnogo koraka u neku konfiguraciju oblika $d_{i+1}$.
	Doista, iz $i<y$ slijedi $y-i>0$, pa imamo
\begin{multline}\label{eq:prkonf}
    d_i=\bigl(\f F(\vec x,i),\vec x,y-i,i,0,\dotsc,1,0\bigr)\leadsto
    \bigl(\f F(\vec x,i),\vec x,y-i-1,i,0,\dotsc,2,0\bigr)\leadsto^*\\
	\leadsto^*\bigl(\f H\bigl(\vec x,i,\f F(\vec x,i)\bigr),\vec x,y-i-1,i,0,\dotsc,3,0\bigr)%\leadsto{}\\
    \leadsto\bigl(\f F(\vec x,i+1),\vec x,y-i-1,i+1,0,\dotsc,4,0\bigr)\leadsto\\
    \leadsto\bigl(\f F(\vec x,i+1),\vec x,y-(i+1),i+1,0,\dotsc,1,0\bigr)= d_{i+1}\text.
\end{multline}
Ovdje je bilo važno da je i $\f H$ totalna, pa računanje vrijednosti $\f H\bigl(\vec x,i,\f F(\vec x,i)\bigr)$ (prema~\eqref{eq:defprk} jednake $\f F(\vec x,i+1)$) doista stane nakon konačno mnogo koraka, predstavljenih strelicom $\leadsto^*$ u~\eqref{eq:prkonf}. Sada odmah indukcijom po $i$ slijedi da za svaki $i\le y$, $Q_{\f F}$-izračunavanje s $(\vec x,y)$ sadrži konfiguraciju $d_i$. Specijalno, u njemu postoji konfiguracija $d_y$, koja prelazi u završnu konfiguraciju
\begin{equation}
    d_y=\bigl(\f F(\vec x,y),\vec x,y-y,y,0,\dotsc,1,0\bigr)\leadsto\bigl(\f F(\vec x,y),\vec x,0,y,0,\dotsc,5,0\bigr)\lcirclearrowleft
\end{equation}
	oblika $\bigl(\f F(\vec x,y),\dotsc\mspace{-1mu}\bigr)$, što smo i trebali. Sada prema teoremu~\ref{tm:rem}, RAM-algoritam $(Q_{\f F}^\flat)^{k+1}$ također računa $\f F$, pa je $\f F\in\mathscr Comp$.
\end{proof}

Primijetimo da smo na ovaj način posredno dobili i RAM-program za $\f{add}^2$, pa time i za $\f{mul}^2$, a onda i $\f{pow}$ (pogledajte primjer~\ref{pr:addmulpow}). Takav RAM-program je ogroman i nikad ga tako ne bismo "ručno" napisali, ali to upravo pokazuje snagu funkcijske paradigme: funkcijski programi se bolje slažu u veće cjeline nego RAM-programi (to svojstvo se u programskim jezicima obično zove \emph{composability}). 
\subsection{Primitivno rekurzivne funkcije}

Već smo nekoliko puta spomenuli primitivno rekurzivne funkcije. Vrijeme je da taj pojam formalno definiramo.

\begin{definicija}[{name=[primitivno rekurzivne funkcije]}]\label{def:prn}
Skup \emph{primitivno rekurzivnih} funkcija je najmanji skup funkcija koji sadrži sve inicijalne funkcije te je zatvoren na kompoziciju i na primitivnu rekurziju.
\end{definicija}

Tehnički, da bi definicija bila dobra, trebalo bi vidjeti da postoji \emph{ikoji} takav skup (tada postoji i najmanji kao presjek svih takvih), no skup svih brojevnih funkcija $\mathscr Func:=\bigcup_{k\in\N_+}\!\mathscr Func_k$ svakako zadovoljava uvjete.

Definicija~\ref{def:prn} je elegantna i matematički pogodna za dokazivanje, ali nije baš operativna. Za konkretne funkcije, lakše je dokazati da su primitivno rekurzivne korištenjem sljedeće karakterizacije.

\begin{propozicija}[{name=[simboličke definicije primitivno rekurzivnih funkcija]}]\label{prop:symbdef}
Neka je $F$ brojevna funkcija. Tada je $F$ primitivno rekurzivna ako i samo ako se $F$ može dobiti iz inicijalnih funkcija pomoću konačno mnogo primjena kompozicije i primitivne rekurzije.
\end{propozicija}
\begin{proof}
Označimo sa $\mathcal S$ skup funkcija koje se mogu dobiti iz inicijalnih pomoću ko\-nač\-no mnogo primjena kompozicije i primitivne rekurzije. 

	Ako je $F$ inicijalna funkcija, tada ona svakako pripada skupu $\mathcal S$ jer ju je moguće dobiti iz inicijalnih pomoću $0$ primjena kompozicije i primitivne rekurzije.

Ako su $k,l\in\N_+$ te $G_1^k,\dotsc,G_l^k,H^l\in\mathcal S$, tada se svaka $G_i$ može dobiti iz inicijalnih pomoću, recimo, $c_i$ primjena kompozicije i $r_i$ primjena primitivne rekurzije. Također se $H$ može dobiti iz inicijalnih, recimo, pomoću $c$ primjena kompozicije i $r$ primjena primitivne rekurzije. Tada se $H\circ(G_1,\dotsc,G_l)$ može dobiti iz inicijalnih funkcija pomoću najviše $1+c+\sum_{i=1}^lc_i$ primjena kompozicije, i najviše $r+\sum_{i=1}^lr_i$ primjena primitivne rekurzije --- što je konačno mnogo, pa je $H\circ(G_1,\dotsc,G_l)\in\mathcal S$.

Ako je $k\in\N_+$ te $G^k,H^{k+2}\in\mathcal S$ totalne funkcije, tada se one mogu dobiti iz inicijalnih pomoću recimo $c_G$ odnosno $c_H$ primjena kompozicije, uz $r_G$ odnosno $r_H$ primjena primitivne rekurzije. Tada se $G\pr H$ može dobiti iz inicijalnih funkcija pomoću najviše $c_G+c_H$ primjena kompozicije, i najviše $r_G+r_H+1$ primjena primitivne rekurzije --- što je konačno mnogo, pa je $G\pr H\in\mathcal S$.

Prethodna tri odlomka pokazuju da skup $\mathcal S$ sadrži sve inicijalne funkcije te da je zatvoren na kompoziciju i na primitivnu rekurziju. Kako je skup primitivno rekurzivnih funkcija najmanji takav skup, slijedi da je podskup od $\mathcal S$, odnosno svaka primitivno rekurzivna funkcija je u $\mathcal S$.

Za drugi smjer, neka je $F\in\mathcal S$ proizvoljna funkcija. To znači da se može dobiti iz inicijalnih, recimo, pomoću $c$ primjena kompozicije i $r$ primjena primitivne rekurzije. Dokažimo da je $F$ primitivno rekurzivna, jakom indukcijom po $c+r$.

Ako je $c+r=0$, tada mora biti $c=r=0$, odnosno $F$ mora biti inicijalna. Skup primitivno rekurzivnih funkcija sadrži sve inicijalne funkcije, pa tako i $F$.

Pretpostavimo da za sve $t<c+r$, za svaku funkciju $g\in\mathcal S$ dobivenu s $c'$ primjena kompozicije i $r'$ primjena primitivne rekurzije tako da je $c'+r'=t$, vrijedi da je $g$ primitivno rekurzivna.

    Neka je sad $F\in\mathcal S$ dobivena s $c$ primjena kompozicije i $r$ primjena primitivne rekurzije ($c+r>0$), iz inicijalnih funkcija. Tada $F\in\mathcal S$ znači da je ili $F=H\circ(G_1,\dotsc,G_l)$ za neke $G_1,\dotsc,G_l,H\in\mathcal S$, ili pak $F=G\pr H$, za neke totalne $G,H\in\mathcal S$ (odgovarajućih mjesnosti).

	U svakom od tih slučajeva pojedine funkcije, pomoću kojih je dobivena $F$, dobivene su iz inicijalnih funkcija sa strogo manje ukupno primjena kompozicije i primitivne rekurzije: recimo, ako je $F=G\pr H$, tada je $r>0$ te su $G$ i $H$ dobivene iz inicijalnih pomoću najviše $c$ primjena kompozicije i najviše $r-1$ primjena primitivne rekurzije. Po pretpostavci indukcije, $G$ i $H$ su primitivno rekurzivne. Kako je skup primitivno rekurzivnih funkcija zatvoren na primitivnu rekurziju, zaključujemo da je $F=G\pr H$ primitivno rekurzivna. Analogno bi se dokazalo da je $F$ oblika $H\circ(G_1,\dotsc,G_l)$ primitivno rekurzivna.
\end{proof}

\begin{napomena}[{name=[ulančavanje simboličkih definicija]}]\label{nap:symbdef}
Umjesto "\emph{ab ovo}" od inicijalnih funkcija, možemo krenuti od nekih funkcija za koje smo već utvrdili da su primitivno rekurzivne. Zapis koji pokazuje kako se neka funkcija $F$ može dobiti kompozicijom i primitivnom rekurzijom iz već utvrđeno primitivno rekurzivnih funkcija zovemo \emph{simboličkom definicijom} funkcije $F$. Recimo, u primjeru~\ref{pr:C23} navedena je simbolička definicija od $\f C_2^3$, a u primjeru~\ref{pr:addmulpow}, simboličke definicije od $\f{add}^2$ i $\f{mul}^2$.
\end{napomena}

Simboličke definicije su koncizne i izražajne, ali nisu baš čitljive. Umjesto njih, često se pišu \emph{točkovne} definicije, gdje funkciju definiramo "po točkama" tako da kažemo što je $F(\vec x)$, umjesto da kažemo što je $F$. Većina modernih programskih jezika upravo tako definira funkcije. Lijevi stupac~\eqref{eq:addb}--\eqref{eq:addk} sadrži točkovnu definiciju zbrajanja dvaju brojeva, iz koje se vidi da je ono primitivno rekurzivno. U desnom stupcu je također točkovna definicija, ali manje čitljiva jer je namještena na oblik~\eqref{eq:defprb}--\eqref{eq:defprk}, iz kojeg se odmah može pročitati simbolička definicija. Programski, imali bismo:
\begin{equation}
	\begin{minipage}{0.8\textwidth}
		\begin{verbatim}
z = x                         # G(x)=x
for i in range(y): z = z + 1  # H(x,i,z)=Sc(z)
		\end{verbatim}
	\end{minipage}
\end{equation}

Točkovne definicije su katkad neprecizne, i na nekim mjestima morat ćemo pribjeći simboličkoj definiciji da bi se znalo što zapravo pokušavamo definirati. No u ogromnom broju slučajeva, posebno za kompliciranije funkcije (i relacije), pisat ćemo točkovne definicije. Važno je imati na umu da se svaka takva točkovna definicija može \emph{pretvoriti} u simboličku --- evo primjera.

\begin{primjer}[{name=[pretvorba točkovne definicije u simboličku]}]
Točkovna definicija
\begin{align}
    \f f(x,y,z,0)&:=\f g\bigl(x,\f h(x,y,z)\bigr)\\
    \f f(x,y,z,t+1)&:=\f h\bigl(z,\f f(x,y,z,t),\f g(t,z)\bigr)
\intertext{ekvivalentna je simboličkoj definiciji}
\f f^4&:=\f g^2\circ(\f I_1^3,\f h^3)\pr \f h^3\circ\bigl(\f I_3^5,\f I_5^5,\f g^2\circ(\f I_4^5,\f I_3^5)\bigr)\text.
\end{align}
Kompozicijom s odgovarajućim koordinatnim projekcijama možemo postići i da primitivna rekurzija ne ide po zadnjem argumentu.
\end{primjer}

Stroga formalizacija točkovnih definicija, i njihova pretvaranja u simboličke, zahtijevala bi alate logike prvog reda: funkcije kompozicijski definiramo kao terme, a relacije kao formule prvog reda s ograničenim kvantifikatorima. Koristimo prirodne brojeve kao konstantske simbole te već dokazano primitivno rekurzivne funkcije i relacije kao funkcijske odnosno relacijske simbole. To ne trebamo raditi u potpunoj općenitosti, iz vrlo sličnog razloga iz kojeg nismo napravili ni strogi dokaz teorema~\ref{tm:rem} --- jer nam sveukupno do univerzalnosti treba samo konačno mnogo oblika takvih definicija, pa možemo svaki od njih zasebno pretvoriti u simbolički oblik ako treba.

Definiciju~\ref{def:prn} možemo iskoristiti za  dokazivanje da sve primitivno rekurzivne funkcije imaju neko svojstvo $\wp$, baš kao što smo to učinili u dokazu propozicije~\ref{prop:symbdef}. Definiramo $\mathcal S$ kao skup svih brojevnih funkcija sa svojstvom $\wp$, dokažemo da sve inicijalne funkcije imaju svojstvo $\wp$ te da je skup $\mathcal S$ zatvoren na kompoziciju i na primitivnu rekurziju. Skup primitivno rekurzivnih funkcija je podskup bilo kojeg skupa koji ima ta svojstva, pa tako i od $\mathcal S$. (Zaključivanje matematičkom indukcijom također je takvog oblika: $\N$ je najmanji skup koji sadrži $0$ i zatvoren je na $\f{Sc}$.) Evo dva primjera.

\begin{propozicija}[{name=[totalnost primitivno rekurzivnih funkcija]}]\label{prop:prntot}
Sve primitivno rekurzivne funkcije su totalne.
\end{propozicija}
\begin{proof}
    Iz napomene~\ref{nap:inittot} slijedi da je skup svih totalnih brojevnih funkcija nadskup skupa svih inicijalnih funkcija. Iz propozicije~\ref{prop:comptot} slijedi da je taj skup zatvoren na kompoziciju, a iz napomene~\ref{nap:prtot} da je zatvoren i na primitivnu rekurziju. Dakle tvrdnja slijedi po definiciji~\ref{def:prn}.
\end{proof}

\begin{propozicija}[{name=[RAM-izračunljivost primitivno rekurzivnih funkcija]}]\label{prop:prnram}
Sve primitivno rekurzivne funkcije su RAM-izračunljive.
\end{propozicija}
\begin{proof}
Po definiciji~\ref{def:prn}, koristeći korolar~\ref{kor:initram} te leme~\ref{lm:compram} i~\ref{lm:prram}.
\end{proof}

\subsection{Primjeri primitivno rekurzivnih funkcija i relacija}

Već smo vidjeli simboličke definicije od $\f{add}^2$ i $\f{mul}^2$, što prema propoziciji~\ref{prop:symbdef} znači da su one primitivno rekurzivne. Sada ćemo vidjeti još brojne druge primjere. Prvo poopćimo primjer~\ref{pr:C23}.

\begin{propozicija}[{name=[primitivna rekurzivnost konstantnih funkcija]}]\label{prop:konst}
Za sve $n\in\N$ i za sve $k\in\N_+$, konstantna funkcija $\f C_n^k$, \\ zadana s $\f C_n^k(\vec x):=n$, primitivno je rekurzivna.
\end{propozicija}
\begin{proof}
Fiksirajmo $k\in\N_+$, i dokažimo tvrdnju "sve $\f C_n^k$ su primitivno rekurzivne", \\ indukcijom po $n$. Baza: $\f C_0^k=\f Z\circ\f I_1^k$ je simbolička definicija od $\f C_0^k$. Doista,
\begin{equation}
    (\f Z\circ\f I_1^k)(\vec x)=\f Z\bigl(\f I_1^k(\vec x)\bigr)=\f Z(x_1\!)=0=\f C_0^k(\vec x)\text.
\end{equation}
To znači da je $\f C_0^k$ dobivena iz dvije inicijalne funkcije kompozicijom, pa je primitivno rekurzivna (po propoziciji~\ref{prop:symbdef}, na koju se više nećemo eksplicitno pozivati).

Pretpostavka: pretpostavimo da je $\f C_m^k$ primitivno rekurzivna, za neki $m\in\N$. 
Korak: tvrdimo da je $\f C_{m+1}^k\!=\f{Sc}\circ\f C_m^k$ simbolička definicija od $\f C_{m+1}^k$. Doista,
\begin{equation}
    (\f{Sc}\circ\f C_m^k)(\vec x)=\f{Sc}\bigl(\f C_m^k(\vec x)\bigr)=\f{Sc}(m)=m+1=\f C_{m+1}^k(\vec x)\text.
\end{equation}
To znači da je $\f C_{m+1}^k$ dobivena iz inicijalne i (po pretpostavci indukcije) primitivno rekurzivne funkcije kompozicijom, pa je primitivno rekurzivna. Po principu matematičke indukcije, tvrdnja vrijedi za svaki $n\in\N$.
\end{proof}

Sada napokon možemo riješiti i problem jednomjesnih funkcija definiranih "degeneriranim" rekurzijama poput one u~\eqref{eq:faktb}--\eqref{eq:faktk}. Takve funkcije neće biti "u korijenu" dobivene primitivnom rekurzijom (već kompozicijom), ali će biti primitivno rekurzivne.

\begin{propozicija}[{name=[jednomjesna funkcija primitivnom rekurzijom]}]\label{prop:F1prn}
Neka je $a\in\N$ i $\f H^2$ primitivno rekurzivna funkcija.
    Tada je primitivno rekurzivna i funkcija $\f F^1$, zadana s
\begin{align}
\SwapAboveDisplaySkip
%\label{eq:F1b}
    \f F(0)&:=a\text,\\
%\label{eq:F1k}
    \f F(x+1)&:=\f H\bigl(x,\f F(x)\bigr)\text.
\end{align}
%također primitivno rekurzivna.
\end{propozicija}
\begin{proof}
	Dodat ćemo još jedan argument funkciji $\f F$, koji neće raditi ništa osim što će povećavati sve mjesnosti za $1$. Precizno, definiramo funkciju $\f F^2$ (različitu od $\f F^1$\!, jer je mjesnost dio identiteta funkcije) s $\f F(x,y):=\f F(y)$ (za sve $x$ i $y$). Tada jednakosti
\begin{align}
%\SwapAboveDisplaySkip
%\label{eq:F2b}
	\f F(x,0)=\f F(0)&=a=\f C_a^1(x)\text,\\
%\label{eq:F2k}
	\f F(x,y+1)=\f F(y+1)&=\f H\bigl(y,\f F(y)\bigr)=\f H\bigl(y,\f F(x,y)\bigr)=:\f H\bigl(x,y,\f F(x,y)\bigr)\text,
\end{align}
	kažu da je $\f F^2$ dobivena (pravom) primitivnom rekurzijom iz primitivno rekurzivnih funkcija $\f G^1:=\f C_a^1$ i $\f H^3:=\f H^2\circ(\f I_2^3,\f I_3^3)$, pa je primitivno rekurzivna. %Te funkcije su primitivno rekurzivne pa su po propoziciji~\ref{prop:prntot} totalne, što znači da je primitivna rekurzija dobro definirana i $\f F^2=\f G^1\pr\f H^3$ je primitivno rekurzivna. (Općenito ćemo u frazi poput "funkcija dobivena primitivnom rekurzijom iz primitivno rekurzivnih funkcija je ponovo primitivno rekurzivna" prešutno koristiti propoziciju~\ref{prop:prntot}, koja nam kaže da je primitivna rekurzija takvih funkcija uopće dobro definirana.)
%
%Sada dokažimo da za sve $n\in\N$ vrijedi $\f F^2(0,n)=\f F^1(n)$, matematičkom indukcijom po $n$. Baza: $\f F^2(0,0)=a$ po~\eqref{eq:F2b}, a to je jednako $\f F^1(0)$ po~\eqref{eq:F1b}. Pretpostavka: pretpostavimo da je $\f F^2(0,m)=\f F^1(m)$ za neki $m\in\N$. Korak: tada je redom prema~\eqref{eq:F2k}, pretpostavci indukcije i~\eqref{eq:F1k},
%\begin{equation}
%    \f F^2(0,m+1)=\f H\bigl(m,\f F^2(0,m)\bigr)=\f H\bigl(m,\f F^1(m)\bigr)=\f F^1(m+1)\text,
%\end{equation}
%pa tvrdnja vrijedi po principu matematičke indukcije. To znači da
	Sada je (primjerice) $\f F(x)=\f F(0,x)$, odnosno $\f F^1=\f F^2\circ(\f Z,\f I_1^1\mspace{-1mu})$, iz čega slijedi da je i $\f F^1$ primitivno rekurzivna.
\end{proof}

\begin{definicija}[{name=[degenerirana primitivna rekurzija]}]\label{def:F1prn}
	Za takve funkcije ubuduće pišemo "simboličku definiciju" $\f F^1:=a\pr\f H^2:=\f C_a^0\pr\f H^2$,\\ imajući na umu da je to samo pokrata za $\f F^1:=\bigl(\f C_a^1\pr\f H^2\circ(\f I_2^3,\f I_3^3)\bigr)\circ(\f Z,\f I_1^1\mspace{-1mu})$.

Takvo zadavanje funkcije zvat ćemo \emph{degeneriranom primitivnom rekurzijom}.
\end{definicija}

Pomoću propozicije~\ref{prop:F1prn} možemo dokazati primitivnu rekurzivnost raznih funkcija.% Evo nekoliko primjera.

\begin{primjer}[{name=[primitivna rekurzivnost funkcije faktorijel]}]\label{pr:factorialprn}
Jednadžbe~\eqref{eq:faktb} i~\eqref{eq:faktk} kažu da je $\f{factorial}^1\!=1\pr\f{mul}^2\circ(\f{Sc}\circ\f I_1^2,\f I_2^2)$\\ simbolička definicija funkcije faktorijel, pa je ona primitivno rekurzivna.
\end{primjer}

\begin{primjer}[{name=[primitivna rekurzivnost funkcije prethodnik]}]
	Funkcija \emph{prethodnik} zadana je s $\f{pd}(x):=\max\,\{x-1,0\}$. Iz toga slijedi $\f{pd}\bigl(\f{Sc}(x)\bigr)=x$ za sve $x\in\N$, dakle $\f{pd}$ je lijevi inverz funkcije $\f{Sc}$. Naravno, $\f{Sc}$ nema desni inverz jer nije surjekcija: ne poprima vrijednost $0$, pa $\f{pd}(0)=0$ moramo posebno definirati. Te dvije jednakosti (napisane desno u obliku koda u Pythonu):
\begin{align}
%\SwapAboveDisplaySkip
	\f{pd}(0)&=0\text,&&\texttt{p = 0}\\
	\f{pd}(y+1)&=y\text,&&\texttt{for i in range(y):~p = i}
\end{align}
kažu da je $\f{pd}$ dobivena degeneriranom primitivnom rekurzijom $\f{pd}=0\pr\f I_1^2$, pa je primitivno rekurzivna po propoziciji~\ref{prop:F1prn}.
\end{primjer}

\begin{napomena}[{name=[zamjena nule jedinicom u nekim brojevnim funkcijama]}]\label{nap:crtica}
	Još jedan način definiranja funkcije $\f{pd}$, koji ćemo često koristiti kasnije, je sljedeći: htjeli bismo definirati $\f{pd}(x)$ kao $x-1$, no problem je $x=0$ (ako hoćemo da funkcija bude primitivno rekurzivna, dakle totalna). Često se u takvim funkcijama onda problematična vrijednost $0$ zamijeni prvom sljedećom vrijednosti $1$, koja nije problematična. Ako točkicom $\bump$ označimo tu transformaciju (formalno, $n\bump$ je $n$ ako je pozitivan, a $1$ ako je $n=0$), tada možemo precizno definirati $\f{pd}(x):=x\bump-1$($=x\dotminus1$, pogledajte primjer~\ref{pr:sub}).
\end{napomena}

Kad imamo prethodnik kao primitivno rekurzivnu funkciju, njenom iteracijom mo\-že\-mo definirati neku vrst oduzimanja. Ipak, zbog $\f{pd}(0)=0$, vrijednosti tog oduzimanja bit će "odsječene odozdo" na nuli.

\begin{primjer}[{name=[primitivna rekurzivnost ograničenog oduzimanja]}]\label{pr:sub}
Za $x,y\in\N$, označimo $x\dotminus y:=\max\,\{x-y,0\}$. Iz jednakosti\slash koda
\begin{align}
	x\dotminus0&=x\text,&&\texttt{s = x}\\
	x\dotminus(y+1)&=\f{pd}(x\dotminus y)\text,&&\texttt{for i in range(y):~s = pd(s)}
\end{align}
vidimo da je \emph{ograničeno oduzimanje} dobiveno primitivnom rekurzijom iz funkcija $\f I_1^1$ i $\f{pd}\circ\f I_3^3$, pa je ono primitivno rekurzivna operacija. "Operacija" nam znači dvomjesnu totalnu brojevnu funkciju koja se piše infiksno između operanada. Kao funkciju, ograničeno oduzimanje zovemo $\f{sub}$. Dakle, $\f{sub}^2=\f I_1^1\pr\f{pd}\circ\f I_3^3$. Još jedan način dolaska do te simboličke definicije je da uzmemo simboličku definiciju za $\f{add}^2$ (primjer~\ref{pr:addmulpow}) i zamijenimo u njoj $\f{Sc}$ s $\f{pd}$.
\end{primjer}

Osim računskih operacija (dijeljenje s ostatkom definirat ćemo kasnije, kad uvedemo još neke tehnike), brojeve možemo i \emph{uspoređivati}, raznim dvomjesnim relacijama poput $<$, $\ge$ ili~$\eq$. Rekosmo, izračunljivost relacija zapravo je izračunljivost njihovih karakterističnih funkcija.

\begin{primjer}[{name=[primitivna rekurzivnost pozitivnosti]}]\label{pr:N+prn}
Za početak pogledajmo pozitivnost --- formalno, jednomjesnu relaciju $\N_+$. Njena karakteristična funkcija je $0$ u nuli, a $1$ u svim ostalim prirodnim brojevima, pa se u literaturi još zove funkcija predznaka ili \emph{signum}. Definicija te funkcije vodi na degeneriranu primitivnu rekurziju $\chi_{\N_+}\!=0\pr\f C_1^2$, iz čega zaključujemo da je $\N_+$ primitivno rekurzivan.
	%Drugim riječima, pozitivnost je primitivno rekurzivno svojstvo, odnosno skup $\N_+$ je primitivno rekurzivan.
\end{primjer}

Kada imamo pozitivnost i ograničeno oduzimanje, možemo odmah vidjeti primitivnu rekurzivnost strogog uređaja. %Ostale uređajne relacije dokazat ćemo primitivno rekurzivnima kasnije, kad ustanovimo kako se radi s logičkim veznicima.

\begin{primjer}[{name=[primitivna rekurzivnost relacija strogog uređaja]}]\label{pr:m-v}
Rastavom na slučajeve vidimo da je $x>y$ ako i samo ako je $x\dotminus y$ pozitivan, iz čega je $\chi_>=\chi_{\N_+}\!\circ\f{sub}$, pri\-mi\-tiv\-no rekurzivna funkcija. Očito je $x<y$ ako i samo ako je $y>x$, dakle $\chi_<=\chi_>\circ(\f I_2^2,\f I_1^2)$ je također primitivno rekurzivna.
\end{primjer}

\section{Minimizacija}

Primitivno rekurzivne funkcije su korisne i pogodne za rad, ali njihova totalnost je na neki način i nedostatak. Recimo, u funkcijskoj paradigmi još uvijek nismo dobili izračunljivost prazne funkcije $\varnothing^1$, što je bilo gotovo trivijalno u RAM-paradigmi. Da bismo dobili i parcijalne (netotalne) funkcije, moramo uvesti novi operator, pored $\circ$ i $\pr$. Taj operator --- \emph{minimizacija} --- djelovat će na \emph{relacijama} (zadanim karakterističnim funkcijama) i tražit će najmanji prirodni broj koji ima neko svojstvo. Intuitivno, odgovarat će \emph{neograničenim} petljama (poput petlje \texttt{while} u Pythonu, samo s negiranim uvjetom) koje se ne izvršavaju određeni broj puta, nego dok se ne ispuni neki uvjet.

Općenite neograničene petlje su raznolike i između provjeravanja uvjeta mogu na razne načine mijenjati stanje memorije, ali aksiomatski ćemo pretpostaviti samo izračunljivost petlji oblika \texttt{for(unsigned y=0; !R(y); ++y);}. Kasnije ćemo vidjeti da u tom modelu možemo pisati i općenite petlje.

\begin{definicija}[{name=[minimizacija]}]
Neka je $k\in\N_+$ i $R^{k+1}$ relacija. Za funkciju $F^k$ definiranu s
\begin{align}
    \label{eq:dommu}\dom F&:=\{\vec x\in\N^k\mid\exists yR(\vec x,y)\}=:\exists_*R\text,\\
    F(\vec x)&:=\min\,\{y\in\N\mid R(\vec x,y)\}\text{, za sve $\vec x\in\exists_* R$,}
\end{align}
kažemo da je dobivena \emph{minimizacijom} relacije $R$.
	Pišemo $F^k:=\mu R^{k+1}$, ili točkovno $F(\vec x):\simeq\mu yR(\vec x,y)$.
    Za skup funkcija $\mathcal F$ kažemo da je \emph{zatvoren na minimizaciju} ako za svaki $k\in\N_+$, za svaku $(k+1)$-mjesnu relaciju $R$, $\chi_R\in\mathcal F$ povlači $\mu R\in\mathcal F$. 
\end{definicija}

Domena funkcije $\mu R^{k+1}$ je $k$-mjesna relacija koju označavamo s $\exists_*R$ i zovemo je \emph{projekcija} relacije $R$. Motivaciju za taj naziv možemo vidjeti ako zamislimo tromjesnu relaciju $R^3$ grafički prikazanu kao skup točaka u 3D-prostoru. Tada je grafički prikaz od $\exists_*R^3$ upravo 2D-projekcija (niz os $z$) toga skupa na ravninu $x$-$y$. Točka $(x,y)$ će biti u $\exists_*R$ ako i samo ako iznad nje postoji neka točka $(x,y,z)\in R$ (može ih biti i više).

U tom prikazu možemo vizualizirati i funkciju $\mu R$: za svaku točku $(x,y)$ iz projekcije, $\mu\mspace{2mu}z\mspace{2mu}R(x,y,z)$ je visina do koje vidimo prazan prostor, odnosno visina na kojoj vidimo prvu točku u relaciji $R$ iznad $(x,y)$. 

Da bi izraz $\mu yR(\vec x,y)$ imao vrijednost, očito je nužno da bude $\vec x\in\exists_*R$. Za obrat --- da za \emph{svaki} $\vec x\in\exists_*R$, izraz $\mu yR(\vec x,y)$ ima vrijednost --- zaslužna je dobra uređenost od $\N$: ako postoji neki $y\in\N$ za koji vrijedi $R(\vec x,y)$, tada postoji i najmanji takav\!.

\begin{primjer}[{name=[prazna funkcija minimizacijom]}]\label{pr:varnothingprek}
Praznu funkciju možemo dobiti minimizacijom prazne relacije: konkretno, za svaki $k\in\N_+$, $\varnothing^k=\mu\,\emptyset^{k+1}$. Naime, projekcija prazne relacije je opet prazna, a jedina funkcija s praznom domenom je prazna funkcija.
\end{primjer}

Dodavanjem minimizacije proširili smo skup izračunljivih funkcija u ovom modelu.

\begin{definicija}[{name=[(parcijalno) rekurzivne funkcije i relacije]}]\label{def:parcrek}
Skup \emph{parcijalno rekurzivnih} funkcija je najmanji skup funkcija koji sadrži sve inicijalne funkcije te je zatvoren na kompoziciju, na primitivnu rekurziju i na minimizaciju. Skup \emph{rekurzivnih} funkcija je presjek skupa parcijalno rekurzivnih i skupa totalnih funkcija. Za relaciju $R$ kažemo da je \emph{rekurzivna} ako je njena karakteristična funkcija $\chi_R$ rekurzivna.
\end{definicija}

Izraz "parcijalno rekurzivna relacija" je beskoristan: svaka karakteristična funkcija je po definiciji totalna, pa ako je parcijalno rekurzivna, tada je zapravo rekurzivna.

\begin{lema}[{name=[zatvorenost skupa rekurzivnih funkcija na kompoziciju]}]\label{lm:comprek}
Skup rekurzivnih funkcija zatvoren je na kompoziciju.
\end{lema}
\begin{proof}
Neka su $k,l\in\N_+$ te $\f G_1^k$,~\ldots, $\f G_l^k$ i $\f H^l$ rekurzivne funkcije. Tada su one po definiciji totalne i parcijalno rekurzivne. Skup parcijalno rekurzivnih funkcija je zatvoren na kompoziciju, pa je $\f H\circ(\f G_1,\dotsc,\f G_l)$ parcijalno rekurzivna, no prema propoziciji~\ref{prop:comptot}, ona je i totalna --- dakle rekurzivna funkcija.
\end{proof}

\begin{lema}[{name=[zatvorenost skupa rekurzivnih funkcija na primitivnu rekurziju]}]\label{lm:prrek}
Skup rekurzivnih funkcija zatvoren je na primitivnu rekurziju.
\end{lema}
\begin{proof}
    Neka je $k\in\N_+$ te $\f G^k$ i $\f H^{k+2}$ rekurzivne funkcije. Jer su $\f G$ i $\f H$ totalne, postoji $\f F^{k+1}:=\f G\pr\f H$, i ona je totalna po napomeni~\ref{nap:prtot}. Također, kako su $\f G$ i $\f H$ parcijalno rekurzivne, a skup parcijalno rekurzivnih funkcija je po definiciji zatvoren na primitivnu rekurziju, $\f F$ je parcijalno rekurzivna. Iz toga dvojeg slijedi: $\f F$ je rekurzivna funkcija.
\end{proof}

\begin{korolar}[{name=[rekurzivnost primitivno rekurzivnih funkcija]}]\label{kor:prnrek}
Svaka primitivno rekurzivna funkcija je rekurzivna.
\end{korolar}
\begin{proof}
    Po definiciji~\ref{def:prn}: sve inicijalne funkcije su totalne po napomeni~\ref{nap:inittot}, a parcijalno su rekurzivne po definiciji, dakle rekurzivne su.
	Sada samo treba primijeniti leme~\ref{lm:comprek} i~\ref{lm:prrek}.
\end{proof}

\begin{korolar}[{name=[degenerirana primitivna rekurzija iz rekurzivne funkcije]}]\label{kor:F1rek}
Neka je $a\in\N$ i $\f H^2$ rekurzivna funkcija. Tada je i funkcija $a\pr\f H$ rekurzivna.
\end{korolar}
\begin{proof}
%Iz dokaza propozicije~\ref{prop:F1prn} vidimo
	Po definiciji~\ref{def:F1prn} je $a\pr\f H^2=\bigl(\f C_a^1\pr\f H^2\circ(\f I_2^3,\f I_3^3)\bigr)\circ(\f Z,\f I_1^1)$ pa tvrdnja slijedi iz propozicije~\ref{prop:konst}, korolara~\ref{kor:prnrek} te lema~\ref{lm:comprek} i~\ref{lm:prrek}.
\end{proof}

Slično kao propoziciju~\ref{prop:symbdef}, mogli bismo dokazati da je funkcija parcijalno rekurzivna ako i samo ako je dobivena iz inicijalnih pomoću konačno mnogo primjena kompozicije, primitivne rekurzije (samo na totalne dobivene funkcije) i minimizacije (na relacije čije su karakteristične funkcije već dobivene). To bi bilo poopćenje simboličke definicije za parcijalno rekurzivne funkcije. No takvim funkcijama najčešće ćemo pisati točkovne definicije --- a i Kleenejev teorem o normalnoj formi, koji ćemo dokazati kasnije, reći će da tolika općenitost nije potrebna: dovoljno je promatrati funkcije oblika $\f U\circ\mu\f T$, za primitivno rekurzivne $\f U$ i $\f T$.

%Zapravo, imamo još mnogo toga za reći o primitivno rekurzivnim funkcijama; razlog zašto već sad uvodimo minimizaciju je što će se nekoliko rezultata vezanih uz definiciju po slučajevima moći jednako dokazati za primitivno rekurzivne i za rekurzivne funkcije --- a za rekurzivne funkcije će nam ti rezultati trebati kasnije, tako da ih nećemo morati ponovo dokazivati. Naime, dokazi će transformirati neke \emph{ulazne} funkcije u \emph{izlazne}, komponirajući ih s primitivno rekurzivnim funkcijama. Tada je jasno, s obzirom na to da je skup rekurzivnih funkcija zatvoren na kompoziciju (i primitivnu rekurziju) --- kao presjek dva takva skupa --- da ako ulazne funkcije budu primitivno rekurzivne, i izlazne će biti primitivno rekurzivne, a ako ulazne budu rekurzivne, i izlazne će biti rekurzivne.

%\subsection{Kompajler za funkcijski jezik}\label{sec:pir}

Pogledajmo sada kako možemo proširiti rezultat iz propozicije~\ref{prop:prnram} na parcijalno rekurzivne funkcije. Nedostaje nam jedino opis izvršavanja neograničenih petlji na RAM-stroju.

Ideja nije ništa revolucionarno: kao "kontrolnu varijablu" koristimo upravo $\reg0$, iz istog razloga kao u dokazu leme~\ref{lm:prram} --- da eventualnim završetkom petlje bude već spremna kao izlazni podatak. U tom smislu, već je inicijalizirana na nulu na početku izračunavanja --- samo je treba inkrementirati poslije svake provjere uvjeta $R$.

Ili prije? Ovdje imamo mali tehnički problem: htjeli bismo da provjera bude na samom dnu programa, jer tako najbolje odgovara semantici negiranog uvjeta. Terminologijom jezika Pascal, implementiramo \texttt{until}, ne \texttt{while}. Iz sličnog razloga kao naši strojevi, Pascal \texttt{while}-uvjet provjerava na vrhu, a \texttt{until}-uvjet na dnu petlje. Semantika skoka je ista: ako je uvjet istinit nastavljamo (ulazimo u \texttt{while}-petlju, ili izlazimo iz \texttt{until}-petlje), a ako je lažan skačemo na drugi kraj (izlazimo iz \texttt{while}-petlje, ili ponovo izvršavamo \texttt{until}-petlju) --- što je baš semantika instrukcije tipa $\dec$.

Ali \texttt{until}-petlje imaju jedan nedostatak: njihovo tijelo uvijek se izvrši barem jednom (kao kod petlje \texttt{do...while} u jeziku C). Kako se u petlji mora nalaziti instrukcija $\incr0$, čini se da teško možemo postići da $\reg0$ na kraju bude $0$, što može biti problem: recimo, za univerzalnu relaciju, $\mu y\,\N^{k+1}(\vec x,y)=0$.

Rješenje problema se nalazi na drugom kraju, odnosno početku programa: program možemo početi izvršavati iz sredine! Na početak programa možemo staviti instrukciju tipa $\goto$, kako bismo preskočili instrukciju $\incr0$ kod prvog prolaza.

\begin{lema}[{name=[zatvorenost skupa $\mathscr Comp$ na minimizaciju]}]\label{lm:muram}
Skup $\mathscr Comp$ je zatvoren na minimizaciju.
\end{lema}
\begin{proof}
Neka je $k\in\N_+$ te $\f R^{k+1}$ RAM-izračunljiva. To znači da postoji RAM-program $P_{\f R}$ koji računa karakterističnu funkciju $\chi_{\f R}^{k+1}$. Tvrdimo da makro-program
\begin{equation}
\label{eq:mumacro}
    Q_{\f F}:=\begin{prog}
    0.&\goto\;2\\
    1.&\incr0\\
    2.&P_{\f R}(\reg1,\reg2,\dotsc,\reg{k},\reg0)\to\reg{k+1}\textsc{ using }\reg{k+2}..\\
    3.&\decr{k+1}{1}
    \end{prog}
\end{equation}
računa funkciju $\f F^k:=\mu\f R$.\\ U tu svrhu, po definiciji~\ref{def:compute}, neka je $\vec x\in\N^k$ proizvoljan. Moramo dokazati dvije tvrdnje:
	\begin{enumerate}
		\item Ako $Q_{\f F}$-izračunavanje s $\vec x$ stane, tada $\vec x\in\exists_*\f R=\dom{\mu\f R}$.
		\item Ako je $\mu y\f R(\vec x,y)=n\in\N$, tada $Q_{\f F}$-izračunavanje s $\vec x$ stane s rezultatom $n$.
	\end{enumerate}
	Primijetimo da se za vrijeme $Q_{\f F}$-izračunavanja s $\vec x$ sadržaj registara $\reg 1$, \ldots, $\reg k$ ne mijenja (RAM-instrukcije u $Q_{\f F}$ nemaju odredišta između $1$ i $k$, a funkcijski makro čuva prvih $k+1$ registara), pa je čitavo vrijeme njihov sadržaj jednak $\vec x$.

	Za prvu tvrdnju, jedini način da promatrano izračunavanje stane je da makro-stroj dođe u završnu konfiguraciju oblika $(y,\vec x,t,\dots,4,0)$, a jedini pak način da se to dogodi je dolazak iz konfiguracije $(y,\vec x,t+1,\dots,3,0)$, jer nema odredišta $4$. Makro-instrukcija izvršena prije toga morala je biti funkcijski makro, što zbog činjenice da $P_{\f R}$ računa $\chi_{\f R}$ znači da je $\chi_{\f R}(\vec x,y)=t+1>0$, odnosno vrijedi $\f R(\vec x,y)$, pa je $\vec x\in\exists_*\f R$.

	Za drugu tvrdnju, dokažimo prvo (indukcijom po $n$) pomoćnu tvrdnju: ako ni za koji $y<n$ ne vrijedi $\f R(\vec x,y)$, tada makro-stroj u nekom trenutku dođe u konfiguraciju $(n,\vec x,0,\dots,2,0)=:q_n$. Za $n=0$ antecedens trivijalno vrijedi, ali vrijedi i konzekvens: početak izračunavanja je
	\begin{equation}
		(0,\vec x,0,\dots,0,0)\leadsto(0,\vec x,0,\dots,2,0)=q_0\text.
	\end{equation}

	Pretpostavimo sada da za sve $y<n+1$ vrijedi $\lnot\f R(\vec x,y)$. Tada posebno to vrijedi i za sve $y<n$, pa po pretpostavci indukcije makro-stroj nekada dođe u konfiguraciju $q_n$. Dalje se izračunavanje odvija ovako (zbog $n<n+1$ je $\lnot\f R(\vec x,n)$, što znači da funkcijski makro stavi $\chi_{\f R}(\vec x,n)=0$ u $\reg{k+1}$): 
	\begin{equation*}
		q_n=(n,\vec x,0,\dots,2,0)\leadsto^*(n,\vec x,0,\dots,3,0)\leadsto(n,\vec x,0,\dots,1,0)\leadsto(n+1,\vec x,0,\dots,2,0)=q_{n+1}\text.
	\end{equation*}

	Sada, ako je $n=\mu y\f R(\vec x,y)$, tada očito ni za koji $y<n$ ne vrijedi $\f R(\vec x,y)$, pa prema pomoćnoj tvrdnji makro-stroj dođe u konfiguraciju $q_n$. Dalje se izračunavanje odvija ovako (zbog $\f R(\vec x,n)$ funkcijski makro stavi $\chi_{\f R}(\vec x,n)=1$ u $\reg{k+1}$):
	\begin{equation*}
		q_n=(n,\vec x,0,\dots,2,0)\leadsto^*(n,\vec x,1,\dots,3,0)\leadsto(n,\vec x,0,\dots,4,0)\lcirclearrowleft\text.
	\end{equation*}

	%Ako $\vec x\notin\exists_*\f R$, dakle ne postoji $y\in\N$ takav da vrijedi $\f R(\vec x,y)$, to zapravo znači da za svaki $y\in\N$ vrijedi 
%$\chi_{\f R}(\vec x,y)=0$. Ta će vrijednost biti izračunana kad god makro-stroj izvrši instrukciju rednog broja $2$ (s $\textsc{using }\reg{k+2}..$ čuvamo originalne ulazne registre), redom za sve prirodne brojeve $y$, i završit će u $\reg{k+1}$. Nakon toga, instrukcija s rednim brojem $3$ će pokušati dekrementirati $\reg{k+1}$, ustanoviti da je njegov sadržaj $0$, i postaviti $\textsc{pc}$ na $1$. Tada će se inkrementirati $\reg0$, i ponovo testirati uvjet~\ldots\ i tako dalje. Preciznije, imat ćemo sljedeće $Q_{\f F}$-izračunavanje s $\vec x$:
%\begin{multline}
    %(0,\vec x,0,0,\dotsc,0,0)
    %\leadsto(0,\vec x,0,0,\dotsc,2,0)\leadsto^*
    %(0,\vec x,0,0,\dotsc,3,0)\leadsto
	%(0,\vec x,0,0,\dotsc,1,0)\leadsto{}\\
	%{}\leadsto(1,\vec x,0,0,\dotsc,2,0)\leadsto^*
    %(1,\vec x,0,0,\dotsc,3,0)\leadsto
    %(1,\vec x,0,0,\dotsc,1,0)\leadsto\\
    %\leadsto(2,\vec x,0,0,\dotsc,2,0)\leadsto^*
    %(2,\vec x,0,0,\dotsc,3,0)\leadsto
    %(2,\vec x,0,0,\dotsc,1,0)\leadsto\dotsb
%\end{multline}
%koje nikada ne stane jer nijedna konfiguracija u njemu nije završna.
%
%Ako je pak $\vec x\in\exists_*\f R$, tada je $\f F(\vec x)\in\N$ --- označimo tu vrijednost s $y_0$. Tada za svaki $y<y_0$ i dalje vrijedi $\chi_{\f R}(\vec x,y)=0$, pa će $Q_{\f F}$-izračunavanje s $\vec x$ izgledati isto sve do trenutka kad se sadržaj registra $\reg0$ približi odozdo $y_0$, kada će izgledati ovako:
%\begin{multline}
    %\dotsb\leadsto(y_0-1,\vec x,0,0,\dotsc,1,0)\leadsto
    %(y_0,\vec x,0,0,\dotsc,2,0)\leadsto^*
    %(y_0,\vec x,1,0,\dotsc,3,0)\leadsto{}\\
    %{}\leadsto(y_0,\vec x,0,0,\dotsc,4,0)\lcirclearrowleft\text,
%\end{multline}
	%odnosno doći će do završne konfiguracije oblika $(y_0,\dotsc\mspace{-1mu})$ pa će izlazni podatak biti $y_0=\f F(\vec x)$ kao što i treba. Ako je $\f F(\vec x)=0$, tada nema nikakvog približavanja odozdo, već izračunavanje izgleda ovako:
%\begin{equation*}
    %(0,\vec x,0,0,\dotsc,0,0)\leadsto
    %(0,\vec x,0,0,\dotsc,2,0)\leadsto^*
    %(0,\vec x,1,0,\dotsc,3,0)\leadsto(0,\vec x,0,0,\dotsc,4,0)\lcirclearrowleft\text,
%\end{equation*}
	%što znači da u konačno mnogo koraka dođe do završne konfiguracije oblika $(0,\dotsc\mspace{-1mu})$, pa je izlazni podatak $0$, kao što i treba biti.

    Sada prema teoremu~\ref{tm:rem} RAM-algoritam $Q_{\f F}^{\flat k}$ računa $\f F$, pa je $\f F\in\mathscr Comp$.
\end{proof}

Napokon možemo dokazati da se svi funkcijski programi mogu simulirati odgovarajućim imperativnim programima u našoj formalizaciji.

\begin{teorem}[{name=[RAM-izračunljivost parcijalno rekurzivnih funkcija]}]\label{tm:pir}
Svaka parcijalno rekurzivna funkcija je RAM-izračunljiva.
\end{teorem}
\begin{proof}
Skup $\mathscr Comp$ sadrži sve inicijalne funkcije prema korolaru~\ref{kor:initram}, a zatvoren je na kompoziciju, primitivnu rekurziju i minimizaciju prema lemama~\ref{lm:compram},~\ref{lm:prram} i~\ref{lm:muram} --- dakle nadskup je najmanjeg takvog skupa, skupa svih parcijalno rekurzivnih funkcija.
\end{proof}

Upravo napisani dokaz je zapravo sasvim konstruktivan: ako imamo zadanu parcijalno rekurzivnu funkciju ili relaciju, tada možemo napisati njenu simboličku definiciju u obliku stabla. Listovi tog stabla su inicijalne funkcije, a čvorovi mu predstavljaju funkcije dobivene (kompozicijom, primitivnom rekurzijom ili minimizacijom) iz čvorova ispod, ili pak relacije čije su karakteristične funkcije dobivene na isti način. U korijenu stabla je funkcija ili relacija koju tražimo.

Sada \emph{postorder}-obilaskom tog stabla možemo konstruirati preslikavanje (apstraktni tip podataka \texttt{Mapping}) $compile$ koje svaku od tih funkcija odnosno relacija preslikava u RAM-program koji je računa. Kad obilazimo list $L$, koristimo dokaz propozicije~\ref{prop:initmacro} da bismo pogledali koji makro-program $Q_L$ računa $L$ te definiramo $compile[L]:=Q_L^{\,\flat}$. Ako se nalazimo na unutarnjem čvoru $N$, ovisno o tome kako je dobiven iz svoje djece koristimo dokaz leme~\ref{lm:compram},~\ref{lm:prram} ili~\ref{lm:muram} da utvrdimo koji oblik makro-programa ---~\eqref{eq:compmacro},~\eqref{eq:prmacro} ili~\eqref{eq:mumacro} --- računa $N$, u taj predložak (\emph{template}) uvrštavajući funkcijske makroe koji na odgovarajućem mjestu pozivaju $compile[D_i]$, gdje su $D_i$ djeca čvora $N$. (Zbog \emph{postorder}-obilaska, $D_i$ su već kompilirani.) Dobivši tako makro-program $Q_N$, definiramo $compile[N]:=Q_N^{\,\flat}$. Na kraju \emph{postorder}-obilaska nalazi se korijen $K$, i $compile[K]$ će biti RAM-program koji računa parcijalno rekurzivnu funkciju (ili relaciju) zadanu simboličkom definicijom.

Za obrat teorema~\ref{tm:pir} morat ćemo se više potruditi. To je tema poglavlja~\ref{ch:univ}.

\section{Tehnike za rad s (primitivno) rekurzivnim funkcijama}\label{sec:tech}

Korištenje marljive evaluacije olakšalo nam je dokaz RAM-izračunljivosti simbolički definiranih funkcija --- jer marljiva kompozicija upravo odgovara slijednom izvršavanju instrukcija u programu --- ali će otežati dokaz suprotnog smjera, jer neke, u RAM-modelu jednostavne, programske tehnike zasad ne znamo ostvariti u funkcijskom modelu s marljivom evaluacijom.

Jedan primjer je \emph{grananje}: imamo dva RAM-programa $P_{\mathit{true}}$ i $P_{\mathit{false}}$. Želimo izvršiti jedan od ta dva programa ovisno o tome je li $r_j$ pozitivan ili nije, ali tako da ako je npr.\ $P_{\mathit{true}}$ prazan program, $P_{\mathit{false}}$ beskonačna petlja, a $r_j=1$, čitavo izračunavanje stane. Možemo napisati makro
\vspace{-2mm}
\begin{equation}
    (\textsc{if $\reg{j}$ then $P_{\mathit{true}}^*$ else $P_{\mathit{false}}^*$}):=\begin{prog}
    0.&\decr{j}{4}\\
    1.&\incr{j}\\
    2.&P_{\mathit{true}}^*\\
    3.&\goto\;5\\
    4.&P_{\mathit{false}}^*
    \end{prog}^{\flat*}\text,
\end{equation}
ali ne možemo napisati odgovarajuću funkciju $If^3$ takvu da $f(\vec x,y):\simeq If\bigl(y,\f g(\vec x),\f h(\vec x)\bigr)$ ima analognu semantiku: ako je $\f g$ totalna a $\f h$ prazna, bez obzira na $y$ marljiva evaluacija ima za posljedicu da je $f$ također prazna. Za to ćemo trebati razviti druge tehnike, no za početak pokažimo kako je nezaustavljanje \emph{jedini} problem --- jer nas zanima samo postojanje algoritma a ne i performanse, s totalnim izračunljivim funkcijama nešto poput $If$ možemo napraviti relativno lako. 
%\subsection{Izračunljivost skupovnih\slash logičkih operacija}
 Za početak, za implementaciju $\textsc{else}$ trebamo dokazati da negiranje uvjeta ne kvari izračunljivost.% moći negirati uvjete i ostati u istoj "klasi" izračunljivosti.

\begin{propozicija}[{name=[komplement čuva (primitivnu) rekurzivnost]}]\label{prop:kompl}
Neka je $k\in\N_+$ te $\f R^k$ (primitivno) rekurzivna relacija.\newline Tada je i relacija $(\f R\kompl)^k$, zadana s $\f R\kompl(\vec x):\Longleftrightarrow\lnot \f R(\vec x)$, također (primitivno) rekurzivna.
\end{propozicija}

Uočimo nekoliko važnih detalja u upravo iskazanoj propoziciji. Prvo, kako smo već rekli u uvodu, na $k$-mjesne relacije gledamo simultano kao na formule s $k$ slobodnih varijabli, i kao na skupove $k$-torki. Zato koristimo oznaku za skupovni komplement, dok u definiciji formulom koristimo logičku negaciju. U sljedećoj propoziciji to ćemo koristiti za dvomjesne logičke veznike odnosno skupovne operacije.

Drugo, mjesnost  $\f R\kompl$ smatramo istom kao mjesnost od $\f R$. Čak i u slučaju prazne relacije, $(\emptyset^k)\kompl=\N^k$ ("univerzalni skup"), u skladu s našom odlukom da prazne relacije različitih mjesnosti gledamo kao različite relacije (komplementi su im različiti).

I treće, u iskazu propozicije pojavljuje se riječ "primitivno" u zagradama. Taj način izražavanja koristit ćemo još mnogo puta u sljedećim propozicijama. To znači da zapravo \textbf{iskazujemo dvije propozicije}: jedna kaže da je komplement primitivno rekurzivne relacije ponovo primitivno rekurzivna relacija, a druga kaže da je komplement rekurzivne relacije ponovo rekurzivna relacija. Dakle, u jednoj verziji čitamo riječ "primitivno" na svim mjestima gdje se pojavljuje u zagradama, a u drugoj je ne čitamo ni na jednom takvom mjestu.

\begin{proof}
Želimo prikazati karakterističnu funkciju $\chi_{\f R\kompl}$ pomoću $\chi_{\f R}$. Dakle, potrebna nam je funkcija koja $0$ preslikava u $1$, a $1$ u $0$. Jedna takva je $x\mapsto1-x$, ali nama treba \emph{brojevna} funkcija s $\N$ u $\N$. Zato ćemo uzeti $\f f_0(x):=1\dotminus x$, koja jednako djeluje na skupu $\{0,1\}$, a sve vrijednosti su joj prirodni brojevi. Ta funkcija je primitivno rekurzivna po propoziciji~\ref{prop:symbdef}: $\f f_0:=\f{sub}\circ(\f C_1^1,\f I_1^1)$ njena je simbolička definicija, $\f{sub}$ je primitivno rekurzivna po primjeru~\ref{pr:sub}, $\f C_1^1$ po propoziciji~\ref{prop:konst}, a $\f I_1^1$ je inicijalna.

Sada točkovna jednakost $\chi_{\f R\kompl}(\vec x)=1\dotminus\chi_{\f R}(\vec x)$ simbolički glasi $\chi_{\f R\kompl}=\f f_0\circ\chi_{\f R}$. Ako je $\chi_{\f R}$ primitivno rekurzivna, tada je i $\chi_{\f R\kompl}$ primitivno rekurzivna, jer je skup primitivno rekurzivnih funkcija zatvoren na kompoziciju.
Ako pak samo znamo da je $\chi_{\f R}$ rekurzivna, tada zaključujemo ovako: $\f f_0$ je rekurzivna prema korolaru~\ref{kor:prnrek}. Prema lemi~\ref{lm:comprek}, tada je i $\chi_{\f R\kompl}$ rekurzivna kao kompozicija dvije rekurzivne funkcije.
\end{proof}

Ubuduće ćemo samo napisati točkovnu definiciju tražene funkcije iz zadanih funkcija, koristeći neke pomoćne primitivno rekurzivne funkcije te kompoziciju i eventualno primitivnu rekurziju. Podrazumijevat ćemo da na kraju dokaza uvijek imamo argumentaciju poput ove u prethodnom odlomku, tako da ako su zadane funkcije primitivno rekurzivne, tada je i tražena funkcija primitivno rekurzivna, a ako su zadane funkcije rekurzivne, tada je i tražena funkcija rekurzivna. Efektivno, imamo poopćenje napomene~\ref{nap:symbdef}, gdje polazimo od rekurzivnih funkcija umjesto od primitivno rekurzivnih.

\begin{korolar}[{name=[primitivna rekurzivnost relacija nestrogog uređaja]}]\label{kor:mj-vj}
Brojevne relacije nestrogog uređaja $\le$ i $\ge$ su primitivno rekurzivne.
\end{korolar}
\begin{proof}
Tvrdnje slijede iz primjera~\ref{pr:m-v}, propozicije~\ref{prop:kompl} te očitih ekvivalencija
\begin{align}
    x\le y&\Longleftrightarrow\lnot(x>y) & (\le) &= (>)\kompl\text,\\
    x\ge y&\Longleftrightarrow\lnot(x<y) & (\ge) &= (<)\kompl
\end{align}
(točkovno u lijevom stupcu, simbolički u desnom).
\end{proof}

\begin{propozicija}[{name=[logički veznici čuvaju (primitivnu) rekurzivnost]}]\label{prop:vezn}
Neka je $k\in\N_+$ te $\f R^k$ i $\f P^k$ (primitivno) rekurzivne relacije iste mjesnosti.\\ Tada su (primitivno) rekurzivne i relacije zadane logički\slash skupovno s
\begin{align}
%\SwapAboveDisplaySkip
    \f Q_1(\vec x)&:\Longleftrightarrow\f R(\vec x)\land\f P(\vec x)
    &
    \f Q_1 &:=\f R \cap\f P\text,
    \\
    \f Q_2(\vec x)&:\Longleftrightarrow\f R(\vec x)\lor\f P(\vec x)
    &
    \f Q_2 &:=\f R \cup\f P\text,
    \\
    \f Q_3(\vec x)&:\Longleftrightarrow\f R(\vec x)\to\f P(\vec x)
    &
    \f Q_3 &:=(\f R\setminus\f P)\kompl\text,
    \\
    \f Q_4(\vec x)&:\Longleftrightarrow\f R(\vec x)\leftrightarrow\f P(\vec x)
    &
    \f Q_4 &:=(\f R\mathbin\triangle\f P)\kompl\text.
\end{align}
\end{propozicija}
\begin{proof}
	Prvo pokažimo da su skupovne i logičke definicije ekvivalentne za upravo definirane relacije. Za $\f Q_1$ i $\f Q_2$ to je upravo definicija presjeka i unije. Za $\f Q_3(\vec x)$ imamo
    \begin{equation}
    \vec x\in(\f R\setminus\f P)\kompl\Leftrightarrow\lnot(\vec x\in\f R\land\vec x\notin\f P)\Leftrightarrow\vec x\notin\f R\lor\vec x\in\f P\Leftrightarrow\vec x\in \f R\to\vec x\in\f P\text.
\end{equation}
	Za $\f Q_4(\vec x)$, logička definicija kaže da je $\chi_{\f R}(\vec x)=\chi_{\f P}(\vec x)$. Njena negacija kaže da su ta dva broja različiti, a kako su oba iz skupa $\{0,1\}$, mora jedan od njih biti $0$ a drugi $1$. To upravo znači da se $\vec x$ nalazi u točno jednom od skupova $\f R$ i $\f P$, dakle $\vec x\in\f R\mathbin\triangle\f P$.

Za primitivnu rekurzivnost tih relacija, kao u dokazu propozicije~\ref{prop:kompl}, trebamo naći dvomjesne primitivno rekurzivne funkcije $\f f_i$ koje će preslikavati $\chi_{\f R}(\vec x)$ i $\chi_{\f P}(\vec x)$ u $\chi_{\f Q_i}(\vec x)$, odnosno one koje će na skupu $\{0,1\}$ djelovati onako kako propisuju tablice istinitosti za pojedine logičke veznike.

Za konjunkciju odnosno presjek, to je upravo $\f f_1=\f{mul}^2$ --- u starijoj literaturi za konjunkciju se još rabi izraz "logičko množenje", a u programskom jeziku Pascal isti simbol \texttt{*} služio je za množenje brojeva i za presjek skupova.

Svi se ostali logički veznici mogu ekvivalentno zapisati pomoću negacije i konjunkcije:
\begin{align}
    \varphi\lor\psi&\Longleftrightarrow\lnot(\lnot\varphi\land\lnot\psi)
    &
    \f f_2(x,y)&:=
    \f f_0\bigl(
      \f f_0(x)\cdot\f f_0(y)
    \bigr)\text,
    \\
    \varphi\to\psi&\Longleftrightarrow\lnot\varphi\lor\psi
    &
    \f f_3(x,y)&:=\f f_2\bigl(\f f_0(x),y\bigr)\text,
    \\
    \varphi\leftrightarrow\psi&\Longleftrightarrow(\varphi\to\psi)\land(\psi\to\varphi)
    &
    \f f_4(x,y)&:=\f f_3(x,y)\cdot\f f_3(y,x)\text,
\end{align}
iz čega odmah čitamo točkovne definicije funkcija $\f f_2$, $\f f_3$ i $\f f_4$ (desni stupac).
\end{proof}

Sada primjenom propozicije~\ref{prop:kompl} na $\f Q_3$ i $\f Q_4$ dobijemo da je skupovna razlika, kao i simetrična skupovna razlika, (primitivno) rekurzivnih relacija iste mjesnosti ponovo (primitivno) rekurzivna.

\begin{korolar}[{name=[primitivna rekurzivnost jednakosti]}]\label{kor:jednakost}
Jednakost (dvomjesna brojevna relacija) je primitivno rekurzivna.
\end{korolar}
\begin{proof}
To slijedi iz korolara~\ref{kor:mj-vj}, propozicije~\ref{prop:vezn} i očite ekvivalencije ("Cantor--Bernstein za konačne skupove")
%\begin{equation}
    $x \eq y \Longleftrightarrow x\le y\land x\ge y$,
%\end{equation}
simbolički $(\eq)=(\le)\cap(\ge)$.%, odnosno $\chi_\eq=\chi_\le\cdot\chi_\ge=\f{mul}^2\circ(\chi_\le^2,\chi_\ge^2)$.
\end{proof}

%\subsection{Višestruke operacije}
\subsection{Teorem o grananju za totalne funkcije}

Sada ćemo nešto reći o višestrukim zbrojevima, umnošcima, unijama i presjecima. U većini programskih jezika npr.\ zbrajanje je sintaksno realizirano kao infiksni operator, najčešće lijevo asociran, a jedina operacija doista implementirana u procesoru je dvomjesno zbrajanje --- tako da se npr.\ $a+b+c+d$ shvaća kao $\bigl((a+b)+c\bigr)+d$, odnosno kompilira se kao slijed tri instrukcije zbrajanja. Mi ćemo učiniti isto, samo ćemo u skladu s funkcijskom paradigmom slijed implementirati kao kompoziciju.

\begin{lema}[{name=[primitivna rekurzivnost višestrukog zbrajanja i množenja]}]\label{lm:addmulk}
Za svaki $k\in\N_+$, funkcije $\f{add}^k$ i $\f{mul}^k$, zadane s
\begin{align}
    \f{add}(x_1,x_2,\dotsc,x_k)&:=x_1+x_2+\dotsb+x_k\text,\\
    \f{mul}(x_1,x_2,\dotsc,x_k)&:=x_1\!\cdot x_2\mathbin{\dotsb}x_k\text,
\end{align}
primitivno su rekurzivne.
\end{lema}
\begin{proof}
Matematičkom indukcijom po $k$. Za $k=1$, vidimo da je $\f{add}^1=\f{mul}^1=\f I_1^1$, inicijalna funkcija. Za $k=2$, tvrdnja slijedi iz primjera~\ref{pr:addmulpow}. Pretpostavimo sad da su za neki $l\in\N\setminus\{0,1\}$, funkcije $\f{add}^l$ i $\f{mul}^l$ primitivno rekurzivne. Tada definiciju
\begin{align}
%\SwapAboveDisplaySkip
    x_1+x_2+\dotsb+x_l+x_{l+1}&:=(x_1+x_2+\dotsb+x_l)+x_{l+1}
\intertext{možemo zapisati kao}
    \f{add}(x_1,x_2,\dotsc,x_l,x_{l+1})&=\f{add}\bigl(\f{add}(x_1,x_2,\dotsc,x_l),x_{l+1}\bigr)
\intertext{ili simbolički}
\SwapAboveDisplaySkip
    \f{add}^{l+1}&=\f{add}^2\circ\bigl(\f{add}^l\circ(\f I_1^{l+1},\f I_2^{l+1},\dotsc,\f I_l^{l+1}),\f I_{l+1}^{l+1}\bigr)\text,
\end{align}
pa tvrdnja slijedi iz pretpostavke indukcije i primjera~\ref{pr:addmulpow}. Potpuno analogno, zamjenom $\f{add}$ s $\f{mul}$, slijedi i druga tvrdnja za $l+1$, odnosno po principu matematičke indukcije za svaki $k\in\N_+$.
\end{proof}

\begin{propozicija}[{name=[višestruke unije i presjeci čuvaju (primitivnu) rekurzivnost]}]\label{prop:skupl}
Neka su $k,l\in\N_+$ te $\f R_1^k$, $\f R_2^k$,~\ldots, $\f R_l^k$ (primitivno) rekurzivne relacije iste mjesnosti. Tada su $\bigcap_{i=1}^l\!\f R_i$ i $\bigcup_{i=1}^l\!\f R_i$ također (primitivno) rekurzivne.
\end{propozicija}
\begin{proof}
Za presjek, koristimo istu tehniku kao u dokazu propozicije~\ref{prop:vezn} za $\f Q_1$, samo umjesto funkcije $\f f_1=\f{mul}^2$ koristimo $\f{mul}^l$. Konkretno, tvrdimo da je \begin{equation}
    \chi_{\bigcap_{i=1}^l\!\f R_i}=\chi_{\f R_1}\!\cdot\chi_{\f R_2}\dotsb\,\chi_{\f R_l}=\f{mul}^l\circ(\chi_{\f R_1},\chi_{\f R_2},\dotsc,\chi_{\f R_l})
\end{equation}
    --- doista, ako je $\vec x$ u presjeku, imamo jednakost $1=1\cdot1\mathbin{\dotsb}1$, a ako nije, tada po De Morganovu pravilu nije u nekoj $\f{R}_i$, pa na lijevoj strani stoji $0$, a na desnoj je umnožak u kojem je barem jedan faktor jednak $0$, i jednakost opet vrijedi.

Za uniju, možemo opet iskoristiti De Morganovo pravilo i propoziciju~\ref{prop:kompl}, ali možemo i upotrijebiti drugačiju tehniku, koja će nam biti korisna kasnije. U našem skupu nema negativnih brojeva, pa je zbroj $0$ jedino ako su svi pribrojnici $0$ --- odnosno, zbroj je pozitivan ako i samo ako je neki pribrojnik pozitivan. To znači da %ako u širem smislu shvatimo sve pozitivne prirodne brojeve (a ne samo broj $1$) kao istinite, 
    $l$-struka unija odgovara funkciji $\chi_{\N_+}\!\circ\f{add}^l$:
\begin{equation}
\label{eq:unk}
	\chi_{\bigcup_{i=1}^{\;l}\!\f R_i}=\chi_{\N_+}\!\circ\f{add}^l\circ(\chi_{\f R_1},\chi_{\f R_2},\dotsc,\chi_{\f R_l})\text,
\end{equation}
što je (primitivno) rekurzivno ako su sve $\chi_{\f R_i}$ (primitivno) rekurzivne.
\end{proof}

%\subsection{Teorem o grananju za totalne funkcije}

Napokon možemo dokazati teorem o grananju za totalne funkcije, samo prethodno moramo precizno definirati pojmove.

\begin{definicija}[{name=[grananje]}]\label{def:gr}
Neka su $k,l\in\N_+$, neka su $G_0^k$, $G_1^k$,~\ldots, $G_l^k$ funkcije, a $R_1^k$, $R_2^k$,~\ldots, $R_l^k$ u~parovima disjunktne relacije iste mjesnosti. Za funkciju $F^k$ definiranu s
\begin{align}
%\SwapAboveDisplaySkip
	\label{eq:domgran}
    \dom{F}&:=\bigcup_{i=0}^l\,(\dom{G_i}\cap R_i)\text{, \quad gdje je }
    R_0:=\Bigl(\bigcup\nolimits_{i=1}^{\,l}R_i\Bigr)\kompl\text,\\
    F(\vec x)&:=\begin{cases}
    G_1(\vec x),&R_1(\vec x)\\
    G_2(\vec x),&R_2(\vec x)\\
    &\vdots\\
    G_l(\vec x),&R_l(\vec x)\\
    G_0(\vec x),&\text{inače}
    \end{cases}\text{ za sve $\vec x\in\dom F$,}
\end{align}
kažemo da je dobivena \emph{grananjem} iz \emph{grana} $G_0,G_1,G_2,\dotsc,G_l$ i \emph{uvjeta} $R_1,R_2,\dotsc,R_l$. Simbolički pišemo $F:=\IF{R_1\!:\!G_1,R_2\!:\!G_2,\dots,R_l\!:\!G_l,G_0}$. Ako ne navedemo $G_0$, smatramo da je $G_0:=\varnothing^k$ (odnosno $F$ nije definirana izvan unije svih uvjeta).
\end{definicija}

Zahtjev da su svi uvjeti u~parovima disjunktni znači da je za svaki $\vec x\in\N^k$ najviše jedan od njih ispunjen. Tako ne moramo brinuti o redoslijedu provjeravanja uvjeta --- no ako već imamo fiksiran redoslijed ne nužno disjunktnih uvjeta $R_1$, $R_2$,~\ldots, $R_l$, uvijek možemo napraviti nove disjunktne uvjete s istom unijom:
\begin{align}
    P_1&:=R_1\text,\\
    P_i&:=R_i\mathbin{\big\backslash}\,\bigcup\nolimits_{j=1}^{i-1}R_j\text{, za sve $i\in[2\dd l]$,}
\end{align}
koji će biti (primitivno) rekurzivni ako su $R_i$ takvi, po propozicijama~\ref{prop:vezn} i~\ref{prop:skupl}. U tom smislu, podrazumijevajući da u samom provjeravanju uvjeta nema beskonačnih petlji (karakteristične funkcije su totalne), grananje odgovara uobičajenom grananju poput \texttt{if}/\texttt{elif}/\texttt{else}, ili \texttt{switch}/\texttt{case}/\texttt{default} (u jeziku Python odnosno C).

Kao što smo već napomenuli, još ne znamo dokazati da je to izračunljivo ako grane $G_i$ nisu totalne, ali ako jesu, to možemo dokazati već sada.

\begin{teorem}[Teorem o grananju, (primitivno) rekurzivna verzija]\label{tm:grek}
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$ (primitivno) rekurzivne funkcije, a $\f R_1^k$, $\f R_2^k$,~\ldots, $\f R_l^k$ u~parovima disjunktne (primitivno) rekurzivne relacije, sve iste mjesnosti.

	Tada je i 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 (primitivno) rekurzivna.
\end{teorem}

Ovdje ne smijemo ispustiti $\f G_0$, jer $\varnothing^k$ nije (primitivno) rekurzivna!

\begin{proof}
$\f R_0:=\bigl(\bigcup\nolimits_{i=1}^{\,l}\f R_i\bigr)\kompl$ je (primitivno) rekurzivna po propozicijama~\ref{prop:skupl} i~\ref{prop:kompl}.\newline Tvrdimo da je
\begin{equation}\label{eq:grek}
    \f F=\chi_{\f R_0}\!\cdot \f G_0+\chi_{\f R_1}\!\cdot \f G_1+\chi_{\f R_2}\!\cdot \f G_2+\dotsb+\chi_{\f R_l}\!\cdot\f G_l\text,
\end{equation}
dakle dobivena je kompozicijom iz (primitivno) rekurzivnih $\chi_{\f R_i}$, $\f G_i$ te $\f{mul}^2$ i $\f{add}^{l+1}$.

	Doista, neka je $\vec x\in\N^k$ proizvoljan, i promotrimo funkcijsku jednakost~\eqref{eq:grek} u $\vec x$. Ako je $\vec x$ u nekoj $\f R_i$, tada je $\chi_{\f R_i}(\vec x)=1$, pa je $i$-ti (brojeći od nule) pribrojnik u~\eqref{eq:grek} jednak $\f G_i(\vec x)$. Štoviše, jer su uvjeti u~parovima disjunktni, $\vec x\notin\f R_j$ za sve $j\in[1\mspace{-1mu}\dd l]\setminus\{i\}$, dok iz definicije $\f R_0$ slijedi također $\vec x\notin\f R_0$ --- što znači da svi ostali pribrojnici imaju faktor $0$, pa iznose $0$ i ne utječu na zbroj. Dakle ako je $\vec x\in\f R_i$, tada je $\f F(\vec x)=\f G_i(\vec x)$.

S druge strane, ako $\vec x$ nije ni u jednoj $\f R_i$, tada po De Morganovu pravilu nije ni u njihovoj uniji, dakle $\vec x\in\f R_0$, pa je početni pribrojnik u~\eqref{eq:grek} jednak $\f G_0(\vec x)$, a svi ostali pribrojnici, kao i u prethodnom odlomku, jednaki su $0$. Dakle tada je $\f F(\vec x)=\f G_0(\vec x)$, kao što i treba biti.
\end{proof}

Domena funkcije dobivene grananjem~\eqref{eq:domgran} je još kompliciranija od domene funkcije dobivene kompozicijom~\eqref{eq:domkomp}. I ovdje zato pišemo definiciju u stilu napomene~\ref{nap:parcdef},
\begin{equation}
    F(\vec x):\simeq\begin{cases}
    G_1(\vec x),&R_1(\vec x)\\
    %G_2(\vec x),&R_2(\vec x)\\
    &\vdots\\
    %G_l(\vec x),&R_l(\vec x)\\
    G_0(\vec x),&\text{inače}\text,
    \end{cases}
\end{equation}
uz dogovor da izraz na desnoj strani ima vrijednost samo za one $\vec x$ za koje izraz u $i$-tom retku ima vrijednost, ako uvjet u tom retku vrijedi, a za one $\vec x$ za koje izraz u zadnjem retku ima vrijednost, ako nijedan od prethodnih uvjeta ne vrijedi. Dakle, ne zahtijevamo (kao prije) da \emph{svaki} podizraz izraza na desnoj strani ima vrijednost, već samo oni koji se nalaze u "relevantnom retku" definicije.

No kao što smo već rekli, komplikacije s domenom bit će nam bitne kasnije. Zasad radimo s (primitivno) rekurzivnim funkcijama i relacijama, koje su totalne --- a pod tim uvjetima i funkcija dobivena grananjem je totalna, štoviše također (primitivno) rekurzivna, dok god navedemo i funkciju $G_0$ za "podrazumijevani slučaj" ($\mspace{-2mu}$\emph{default}).

% \subsection{Editiranje totalnih funkcija}

Kao primjenu teorema~\ref{tm:grek}, dokazat ćemo da \emph{konačnom promjenom} ("editiranjem") vrijednosti ne možemo pokvariti izračunljivost funkcije.

\begin{lema}[{name=[primitivna rekurzivnost jednočlanih relacija]}]\label{lm:r1prn}
Svaka jednočlana brojevna relacija je primitivno rekurzivna.
\end{lema}
\begin{proof}
Neka je $\f R$ jednočlana; označimo s $k$ njenu mjesnost, a s $\vec c=(c_1,\dotsc,c_k)$ jedini njen element. Tada po definiciji jednakosti $k$-torki vrijedi
\begin{equation}
    \f R(\vec x)\Longleftrightarrow\vec x\in\{\vec c\}\Longleftrightarrow\vec x=\vec c\Longleftrightarrow x_1\eq c_1\land\dotsb\land x_k\eq c_k\text,
\end{equation}
a svaki pojedini konjunkt ($x_i\eq c_i$) predstavlja primitivno rekurzivnu relaciju, karakteristične funkcije $\chi_\eq\circ(\f I_i^k,\f C_{c_i}^k)$, primitivno rekurzivne po korolaru~\ref{kor:jednakost}, propoziciji~\ref{prop:konst} i definiciji~\ref{def:prn}. Dakle $\f R$ je primitivno rekurzivna po propoziciji~\ref{prop:skupl}.
\end{proof}

\begin{korolar}[{name=[primitivna rekurzivnost konačnih relacija]}]\label{kor:konprn}
Svaka konačna brojevna relacija je primitivno rekurzivna.
\end{korolar}
\begin{proof}
Odmah po propoziciji~\ref{prop:skupl} i lemi~\ref{lm:r1prn}, jer je $\{\vec c_1,\vec c_2,\dotsc,\vec c_l\}=\bigcup_{i=1}^{\,l}\{\vec c_i\}$.
\end{proof}

\begin{propozicija}[{name=[{teorem o editiranju za totalne funkcije}]}]\label{prop:konprom}
Neka je $k\in\N_+$, neka je $\f G^k$ (primitivno) rekurzivna funkcija te $\f F^k$ totalna funkcija koja se podudara s $\f G$ u svima osim konačno mnogo točaka. Tada je i $\f F$ (primitivno) rekurzivna.
\end{propozicija}
Naglasimo, totalnost funkcije $\f F$ je esencijalna. Izbacivanjem već jedne točke iz $\dom{\f G}$ dobit ćemo funkciju koja nije primitivno rekurzivna, po kontrapoziciji propozicije~\ref{prop:prntot}.
\begin{proof}
    Po pretpostavci, skup $\{\vec x\in\N^k\mid\f F(\vec x)\ne\f G(\vec x)\}$ je konačan: označimo mu sve elemente (recimo, poredane leksikografski) s $\vec c_1,\vec c_2,\dotsc,\vec c_l$. Ako je taj skup prazan, tada je $\f F=\f G$ pa je (primitivno) rekurzivna po pretpostavci. Inače je
\begin{equation}
    \f F(\vec x)=\begin{cases}
    \f F(\vec c_1),&\vec x=\vec c_1\\
    %\f F(\vec c_2),&\vec x=\vec c_2\\
    &\vdots\\
    \f F(\vec c_l),&\vec x=\vec c_l\\
    \f G(\vec x),&\text{inače}
    \end{cases}=\begin{cases}
    \f C^k_{\f F(\vec c_1)}(\vec x),&\vec x\in\{\vec c_1\}\\
    %\f C^k_{\f F(\vec c_2)}(\vec x),&\vec x\in\{\vec c_2\}\\
    &\vdots\\
    \f C^k_{\f F(\vec c_l)}(\vec x),&\vec x\in\{\vec c_l\}\\
    \f G(\vec x),&\text{inače}
    \end{cases}\text,
\end{equation}
dakle $\f F$ je dobivena grananjem iz funkcija $\f C^k_{\f F(\vec c_i)}$ (primitivno rekurzivnih po propoziciji~\ref{prop:konst}, jer je $\f F(\vec c_i)\in\N$ zbog totalnosti od $\f F$), funkcije $\f G$ (primitivno) rekurzivne po pretpostavci propozicije, i iz uvjeta $\{\vec c_i\}$ primitivno rekurzivnih po propoziciji~\ref{lm:r1prn}. Po teoremu~\ref{tm:grek}, $\f F$ je također (primitivno) rekurzivna.
\end{proof}

Sada napokon možemo formalizirati intuiciju \emph{lookup}-tablice, koja kaže da su funkcije zadane na konačnom skupu izračunljive. %Za totalnu brojevnu funkciju kažemo da je \emph{s konačnim nosačem} ako poprima vrijednost $0$ svuda osim u konačno mnogo točaka.

\begin{korolar}[{name=[konačne funkcije su proširive do primitivno rekurzivnih]}]\label{kor:kon0}
Neka je $k\in\N_+$ te $\f g^k$ konačna funkcija ($\dom{\f g}$ je konačan skup).
   
    Tada postoji primitivno rekurzivna funkcija $\f F$ takva da je $\f F|_{\dom{\f g}}=\f g$.
\end{korolar}
\begin{proof}
    Za $\f F$ uzmemo $\tilde{\f g}$, proširenje funkcije $\f g$ nulom. Tada se $\f F^k$ i $\f C_0^k$ razlikuju samo na konačnom skupu $\dom{\f g}$, pa tvrdnja slijedi iz propozicija~\ref{prop:konprom} i~\ref{prop:konst}. 
\end{proof}

%\subsection{Ograničene sume, produkti i brojenje}\label{sec:sumprodcount}
\subsection{Programiranje s ograničenim petljama}\label{sec:ogrprog}

Vidjeli smo da, kao što kompozicija odgovara slijednom izvršavanju naredaba u imperativnom modelu, primitivna rekurzija odgovara ograničenim petljama. Kad malo bolje pogledamo, postoji neka vrsta analogije između ta dva pojma.

Kompoziciju koristimo u slučaju \emph{statičke} granice, najčešće vezane uz mjesnost $l$, gdje nam je svih $l$ argumenata zadano eksplicitnim, često različitim, funkcijama. Dakle, prvo specificiramo $l\in\N_+$ i $l$-mjesnu funkciju $\f H$, zatim specificiramo $l$ funkcija $\f G_1$,~\ldots,~$\f G_l$, i tek onda uvrštavamo ulazne podatke. U tom smislu, $l$ nije ulazni podatak, već parametar konstrukcije: za različite $l$ (i time različite $H$), dobit ćemo različite kompozicije, koje se onda mogu računati s (čak istim, ako je $k$ konstantan) ulaznim podacima $\vec x$.

S druge strane, primitivnu rekurziju koristimo u slučaju \emph{dinamičke} granice, naj\-češ\-će vezane uz broj koraka izračunavanja, gdje su nam $y$ različitih "argumenata" (npr.\ konfiguracija) dobiveni iteracijom jedne te iste funkcije $\f H$ počevši od početne konfiguracije dobivene funkcijom $\f G$. Dakle, prvo specificiramo $k$ i $k$-mjesnu funkciju $\f G$, zatim specificiramo \emph{jednu} $(k+2)$-mjesnu funkciju, u koju pored početnih ulaznih podataka $\vec x$ uvrštavamo još i $y$, redni broj koraka (prolaza kroz petlju) koji računamo.

Na taj način, $y$ je kao "dinamički $l$": izgubili smo mogućnost rada s parcijalnim funkcijama, ali smo dobili mogućnost da broj koraka izračunavanja prenesemo kao ulazni podatak. Slikovito, pretvorili smo $\f G_i(\vec x)$ u $\f G(\vec x,i)$, pa možemo reći da smo "dignuli supskript" (ili "spustili superskript", ako se radi o mjesnosti) na razinu ulaznog podatka. U ovoj točki napravit ćemo nekoliko takvih "dinamizacija", za funkcije odnosno familije funkcija koje smo već upoznali, kao i za neke koje još nismo ali se svejedno prirodno i često pojavljuju.

\begin{primjer}[{name=[koordinantna projekcija kao dinamizacija konstantnih funkcija]}]\label{pr:IdinC}
Jedan primjer smo već vidjeli: sa statičke strane, za svaki $n$ imamo primitivno rekurzivnu funkciju $\f C_n^k$ takvu da je $\f C_n^k(\vec x)=n$, ali za različite $n$ to su različite funkcije. S dinamičke strane imamo primitivno rekurzivnu funkciju $\f I_{k+1}^{k+1}$ takvu da je za sve $n\in\N$, $\f I_{k+1}^{k+1}(\vec x,n)=n$. Iako je $\f I_{k+1}^{k+1}$ inicijalna funkcija, najčešće će takve dinamičke funkcije biti definirane primitivnom rekurzijom (dok je $\f C_n^k$ definirana kompozicijom). I ovdje možemo "definirati"
\begin{align}
\SwapAboveDisplaySkip
    \f I_{k+1}^{k+1}(\vec x,0)&=\f C_0^k(\vec x)\text,&
    \f I_{k+1}^{k+1}(\vec x,y+1)&=\f{Sc}\bigl(\f I_{k+1}^{k+1}(\vec x,y)\bigr)\text,
\end{align}
    odnosno $\f I_{k+1}^{k+1}=\f C_0^k\pr\f{Sc}\circ\f I_{k+2}^{k+2}$, ali $\f I_{k+2}^{k+2}$ nije ni po čemu osnovnija od $\f I_{k+1}^{k+1}$ (jer su obje inicijalne), pa nam ta tehnika ovdje ne pomaže.
\end{primjer}

%\subsection{Ograničene sume i produkti}

Evo malo kompliciranijeg primjera: lema~\ref{lm:addmulk} kaže da je za svaki $k$ funkcija $\f{add}^k$ primitivno rekurzivna; ako joj damo $k$ brojeva, ili je komponiramo s $k$ izračunljivih funkcija, ona će ih zbrojiti (funkcije će zbrojiti na presjeku njihovih domena). Sada ćemo promotriti dinamičku varijantu: operator $\sum$ koji za unaprijed zadanu \emph{totalnu} funkciju $\f G$ prima broj koji kaže koliko prvih njenih vrijednosti (u nekom kontekstu) treba zbrojiti. %, i eventualno ostale argumente od $\f G$ ako je ona mjesnosti veće od $1$. Isto ćemo napraviti za množenje.

\begin{napomena}[{name=[izračunljive granice i prazni konteksti]}]\label{nap:igpk}
	U ostatku ove točke dokazat ćemo šest rezultata o ograničenom programiranju: neke neposredno primitivnom rekurzijom, a neke kompozicijom, s već dobivenim funkcijama. Svi će oni imati isto sučelje: (primitivno) rekurzivnu $k$-mjesnu funkciju $\f G$ ili relaciju $\f R$, kontekst $\vec x$ i granicu $y$; te će biti definirani iteracijom po svim $i<y$.
	
	U primjenama, najčešće će granica ovisiti o kontekstu: $i<\f B(\vec x)$ za neku izračunljivu funkciju $\f B$. To samo znači da ćemo primijeniti kompoziciju s $\f B$ na mjestu zadnjeg argumenta $y$, što ostaje (primitivno) rekurzivno ako je $\f B$ takva.

	Drugo, granica može biti uključena: $i\le\f B(\vec x)$ je ekvivalentno s $i<\f{Sc}\bigl(\f B(\vec x)\bigr)$, što samo znači da je granica $\f{Sc}\circ\f B$, koja je (primitivno) rekurzivna ako je $\f B$ takva.

	I treće, kontekst može biti prazan: u slučaju $k=1$, ulaz za $\f G$ odnosno $\f R$ je samo $i$. Tada je primitivna rekurzija degenerirana, što također ne smeta jer ona čuva primitivnu rekurzivnost po propoziciji~\ref{prop:F1prn}, a rekurzivnost po korolaru~\ref{kor:F1rek}.
\end{napomena}

\begin{lema}[{name=[ograničene sume i produkti čuvaju (primitivnu) rekurzivnost]}]\label{lm:sumprodrek}
    Neka je $k\in\N_+$ te $\f G^k$ (primitivno) rekurzivna funkcija. Tada su (primitivno) rekurzivne i funkcije $\f F_1^k$ i $\f F_2^k$, zadane s
\begin{equation}
    \f F_1(\vec x,y):=\sum_{i<y}\f G(\vec x,i)\text,\qquad
    \f F_2(\vec x,y):=\prod_{i<y}\f G(\vec x,i)\text.
\end{equation}
\end{lema}
\begin{proof}
    Kao što smo rekli, prirodno ih je zadati primitivnom rekurzijom.
    \begin{align}
        \label{eq:sumG1}\f F_1(\vec x,0)&:=0&\f F_2(\vec x,0)&:=1
        %& \f G^{k-1}(\vec x)&:=0
        \\
        \label{eq:sumH1}
        \f F_1(\vec x,y+1)&:=\f F_1(\vec x,y)+\f G(\vec x,y)&
        \f F_2(\vec x,y+1)&:=\f F_2(\vec x,y)\cdot\f G(\vec x,y)
        %& \f H^{k+1}(\vec x,y,z)&:=z+\f G(\vec x,y)
    \end{align}
%Treba primijetiti da su svi ti pozivi funkcija mjesnosti $k$, dakle $\vec x$ je duljine $k-1$, odnosno $x$-eva uopće nema ako je $k=1$. To ne smeta u napisanim jednadžbama jer nijednu funkciju ne pozivamo samo na $\vec x$, ali treba uzeti u obzir da je tim jednadžbama napisana obična primitivna rekurzija (definicija~\ref{def:pr}) za $k>1$, a degenerirana primitivna rekurzija (propozicija~\ref{prop:F1prn} ili korolar~\ref{kor:F1rek}) za $k=1$.
	Tada je $\f F_2=\f C_1^{k-1}\pr\f H$ (ili $1\pr\f H$ za $k=1$), gdje je $\f H(\vec x,y,z)=z\cdot\f G(\vec x,y)$ (primitivno) rekurzivna pa je i $\f F_2$ takva. Sasvim analogno za $\f F_1$.
\end{proof}
%Sasvim analogno, možemo računati i ograničene produkte. 

%\begin{napomena}[{name=[(primitivno) rekurzivne granice]}]\label{nap:sumprodH}
    %Lema~\ref{lm:sumprodrek} nam omogućuje da zadamo broj pribrojnika ili faktora kao argument funkcije. To znači da možemo i \emph{izračunati} broj pribrojnika odnosno faktora kao izračunljivu funkciju ostalih argumenata. Precizno, za $k>1$ možemo računati i
%\begin{equation}
%\SwapAboveDisplaySkip
    %\f F_3^{k-1}(\vec x):=\sum_{\mathclap{i<\f H(\vec x)}}\f G(\vec x,i)
    %\text{\quad i\quad}\f F_4^{k-1}(\vec x):=\prod_{\mathclap{i<\f H(\vec x)}}\f G(\vec x,i)\text,
%\end{equation}
%gdje je $\f H^{k-1}$ neka izračunljiva funkcija, komponiranjem funkcije $\f F_1$ odnosno $\f F_2$ s koordinatnim projekcijama i s funkcijom $\f H$.

%Recimo, za $k=3$ vrijedi $\f F_4^2(x,y)=\prod_{i<\f H(x,y)}\f G(x,y,i)=\f F_2^3\bigl(x,y,\f H(x,y)\bigr)$.
%\end{napomena}

%\begin{napomena}\label{nap:sumprodSc}
%Oznaku $\sum_{i<y}$, i analogno za produkt, shvaćamo kao pokratu za $\sum_{i=0}^{y-1}$, uz dodatnu konvenciju (uobičajenu u konkretnoj matematici) da za $y=0$ vrijednost izraza $\sum_{i=0}^{-1}\dotsb$ bude $0$. Mogli bismo tu sumu zapisati i kao $\sum_{i\in[0\dd y\rangle}\dotsb$.

%Ponekad nam je zgodnije imati uključenu gornju granicu: $\sum_{i\in[0\dd y]}$, odnosno $\sum_{i=0}^y$. To možemo prikazati kao
%\begin{equation}
    %\f F_5(\vec x,y):=
    %\sum_{i\le y}\f G(\vec x,i)=\sum_{\mathclap{i<\f{Sc}(y)}}\f G(\vec x,i)=\f F_1\bigl(\vec x,\f{Sc}(y)\bigr)\text.
%\end{equation}
%Dakle, samo smo na prikladnom mjestu dokomponirali inicijalnu funkciju sljedbenik, čime sigurno nismo pokvarili (primitivnu) rekurzivnost.
%\end{napomena}

%Sve rečeno vrijedi potpuno jednako za produkt kao i za sumu.

%\subsection{Ograničeno brojenje i kvantifikacija}

U uvodnom učenju programiranja, obično se prije sumiranja nauči \emph{brojiti} elemente koji zadovoljavaju neko svojstvo: inicijaliziramo brojač na $0$, prolazimo kroz sve elemente koji dolaze u obzir, i za svaki koji zadovoljava svojstvo, inkrementiramo brojač. Ali kako smatramo $bool$ podskupom od $\N$, uz $\mathit{false}=0$ i $\mathit{true}=1$, brojenje je upravo \emph{sumiranje istinitosnih vrijednosti}. Naredbu \texttt{if uvjet:\ brojač += 1} možemo zapisati kao \texttt{brojač += uvjet}, čime algoritam za brojenje postaje obični algoritam za sumiranje. Formalizirajmo to.

\begin{lema}[{name=[ograničeno brojenje čuva (primitivnu) rekurzivnost]}]\label{lm:brojrek}
\!Neka je $k\in\N_+$ te $\f R^k$ (primitivno) rekurzivna relacija. Tada je funkcija $\f F^k$ zadana s
\begin{equation}
    \f F(\vec x,y):=\card\,\{i\in\N\mid i<y\land\f R(\vec x,i)\}\text,
\end{equation}
također (primitivno) rekurzivna. Skraćeno pišemo $\f F(\vec x,y):=(\num i<y)\,\f R(\vec x,i)$.
\end{lema}
\begin{proof}
    Prema pretpostavci, karakteristična funkcija $\chi_{\f R}^k$ je (primitivno) rekurzivna. Sada tvrdnja slijedi iz leme~\ref{lm:sumprodrek}, jer tvrdimo da vrijedi
	\begin{equation}\label{eq:countsum}
        (\num i<y)\,\f R(\vec x,i)=\sum_{i<y}\chi_{\f R}(\vec x,i)\text.
    \end{equation}
    Doista, za svaki $\vec x\in\N^k$, ako skup $S:=[0\dd y\rangle$ rastavimo na dva dijela,
    \begin{equation}
	    S_1:=\{i\in S\mid\f R(\vec x,i)\}\quad\text i\quad
        S_2:=\{i\in S\mid\lnot\f R(\vec x,i)\}\text,
    \end{equation}
    tada je
        $\sum_{i\in S}\chi_{\f R}(\vec x,i)=\sum_{i\in S_1}\!1+\sum_{i\in S_2}0=\card S_1$.
\end{proof}

%\subsection{Ograničena kvantifikacija}

Još jedan čest obrazac (\emph{pattern}) u uvodnim algoritmima je provjera zadovoljava li neki element zadanog konačnog skupa neko zadano svojstvo --- ili dualno, zadovoljavaju li ga svi elementi tog skupa. U nekim modernim programskim jezicima to se ostvaruje kroz funkcije \texttt{any} i \texttt{all}. Na primjer, ustanoviti je li broj $n$ složen možemo ispitujući postoji li $d\in[2\dd n\rangle$ (ili $d\in\bigl[2\dd \lfloor\!\sqrt{n}\rfloor\bigr]$) takav da $d\mathrel|n$. Vidimo da je prirodna matematička formalizacija tog obrasca \emph{ograničena kvantifikacija}, gdje univerzalno ili egzistencijalno kvantificiramo varijable u nekom uvjetu do neke granice.

Razlog zašto se takav obrazac promatra posebno je mogućnost prijevremenog izlaska iz petlje (\emph{shortcircuit evaluation}, u ovom slučaju najčešće realizirana kroz naredbu \texttt{break}), jer ako provjeravamo postoji li element s nekim svojstvom, znamo da postoji onog trena kada ga nađemo --- ne moramo provjeravati ostale elemente. Tako možemo brže pretraživati konačne skupove, a i dobiti odgovor za prebrojive skupove \emph{ako} je taj odgovor pozitivan. O ovom drugom fenomenu reći ćemo više kasnije, kad budemo govorili o \emph{rekurzivno prebrojivim} relacijama --- a prvi fenomen nas ne zanima, jer se ne bavimo performansama algoritama.

Drugim riječima, za nas se ograničena kvantifikacija svodi na brojenje. Prebrojivši elemente do $y$ koji imaju traženo svojstvo, takvi postoje ako ih ima pozitivan broj, a svi su takvi ako ih ima upravo $y$.

\begin{propozicija}[{name=[ograničena kvantifikacija čuva (primitivnu) rekurzivnost]}]\label{prop:okvantrek}
Neka je $k\in\N_+$ te $\f R^k$ (primitivno) rekurzivna relacija.
	
	Tada su takve i relacije $\f P^k$ i $\f Q^k$, zadane s
\begin{align}
	\f P(\vec x,y)&:\Longleftrightarrow(\exists i<y)\,\f R(\vec x,i)\text,&
        \f Q(\vec x,y)&:\Longleftrightarrow(\forall i<y)\,\f R(\vec x,i)\text.
\end{align}
\end{propozicija}
\begin{proof}
    Kao u dokazu leme~\ref{lm:brojrek}, fiksirajmo $\vec x$ i uvedimo oznake $S:=[0\dd y\rangle$\newline te $S_{\f R}:=\{i\in S\mid\f R(\vec x,i)\}\subseteq S$. Sada vrijedi
\begin{gather}
\label{eq:oeqrek}\quad\f P(\vec x,y)\Longleftrightarrow S_{\f R}\ne\emptyset\Longleftrightarrow\card S_{\f R}>0\Longleftrightarrow(\num i<y)\,\f R(\vec x,i)\in\N_+\text{ te\quad}\\
\f Q(\vec x,y)\Longleftrightarrow S_{\f R}=S\Longleftrightarrow\card S_{\f R}=\card S\Longleftrightarrow(\num i<y)\,\f R(\vec x,i)\eq y
\end{gather}
	(za smjer $\card S_{\f R}=\card S\Rightarrow S_{\f R}=S$ koristimo rezultat iz teorije skupova da konačan skup ne može biti ekvipotentan svom pravom podskupu), pa tvrdnja propozicije slijedi iz leme~\ref{lm:brojrek}, primjera~\ref{pr:N+prn} (za $\f P$) i korolara~\ref{kor:jednakost} (za $\f Q$). Uočimo da je~\eqref{eq:oeqrek} dinamizirani~\eqref{eq:unk}, zbog veze~\eqref{eq:countsum} između brojenja i sumiranja.
\end{proof}

%\begin{napomena}[{name=[granice mogu biti i uključene]}]\label{nap:kvantSc}
    %U dosadašnjim rezultatima ove točke imali smo isključenu gornju granicu: $y<\f H(\vec x)$ kao pokrata za $y\in[0\dd \f H(\vec x)\rangle$. Često je uobičajenije koristiti uključene granice: recimo, $\sum_{y=0}^{\f H(\vec x)}\f G(\vec x,y)=\sum_{y\le\f H(\vec x)}\f G(\vec x,y)$. Sve takve funkcije su jednako izračunljive kao i s isključenom granicom, jer je $y\le\f H(\vec x)\Leftrightarrow y<1+\f H(\vec x)=\f{Sc}\bigl(\f H(\vec x)\bigr)$ --- dakle, umjesto funkcije $\f H$ koristimo $\f{Sc}\circ\f H$, koja je (primitivno) rekurzivna ako je $\f H$ takva.
%
%Analogno napomeni~\ref{nap:sumprodSc}, kompozicijom $\f{Sc}$ s $\f H$ dokazali bismo (primitivnu) rekurzivnost i egzistencijalnih kvantifikacija oblika $\bigl(\exists i\le\f H(\vec x)\bigr)\f R(\vec x,i)$, i dakako univerzalnih kvantifikacija s uključenom granicom.
%\end{napomena}

Još ne znamo ništa o izračunljivosti \emph{neograničene} kvantifikacije (\emph{projekcije}) relacije. Kasnije ćemo pokazati da postoje izračunljive relacije $\f R$ čije projekcije $\exists_*\f R$ nisu izračunljive. Kako je po definiciji $\exists_*\f R=\dom{\mu\f R}$, zaključujemo da \textbf{domena izračunljive funkcije ne mora biti izračunljiva}! Što se tu točno zbiva, objasnit ćemo u poglavlju~\ref{ch:re}. %Zasad promotrimo \emph{ograničenu} minimizaciju. %pokažimo da \emph{ograničenom} minimizacijom čuvamo izračunljivost.

\subsection{Ograničena minimizacija}

\begin{definicija}[{name=[ograničena minimizacija]}]
Neka je $k\in\N_+$ te $R^k$ relacija. Za funkciju $F^k$ definiranu s
\begin{equation}\label{eq:defomin}
	F(\vec x,y):=\mu i\bigl(i<y\to R(\vec x,i)\bigr)=:(\mu i<y)\,R(\vec x,i)\text,
\end{equation}
kažemo da je dobivena \emph{ograničenom minimizacijom} relacije $R$.
\end{definicija}

\begin{napomena}[{name=[ograničena minimizacija čuva rekurzivnost]}]\label{nap:mintot}
U~\eqref{eq:defomin} smo napisali $:=$ umjesto $:\simeq$, jer izraz u sredini uvijek ima vrijednost: kondicional će sigurno nekada postati istinit, najkasnije za $i=y$, jer će tada antecedens $i<y$ postati lažan. Zato će $F(\vec x,y)$ biti najmanji broj $i<y$ koji zadovoljava $R(\vec x,i)$ ako takav postoji, a inače će biti $F(\vec x,y)=y$.

	Dakle, $F$ je uvijek totalna funkcija. Štoviše, ako je $\f R$ rekurzivna, $\f F$ će biti parcijalno rekurzivna --- jer je dobivena (neograničenom) minimizacijom relacije $\f P$ zadane s $\f P(\vec x,y,i):\Leftrightarrow i<y\to\f R(\vec x,i)$, rekurzivne zbog primjera~\ref{pr:m-v} i propozicije~\ref{prop:vezn}. Ukratko, ograničenom minimizacijom rekurzivne relacije dobivamo rekurzivnu funkciju.
\end{napomena}

Dokazali smo da ograničena minimizacija čuva rekurzivnost. Važno je da čuva i \emph{primitivnu} rekurzivnost, što ćemo sada dokazati. U tom dokazu, naravno, ne možemo koristiti minimizaciju, već ćemo traženu funkciju definirati primitivnom rekurzijom.

%OVO JE KRIVO; NAVESTI PAMETNIJI PRIMJER Ograničenu minimizaciju možemo koristiti svaki put kad znamo da je postojanje elementa koji zadovoljava zadani uvjet ekvivalentno s postojanjem takvog elementa ispod neke granice koju možemo izračunati. Recimo, broj $x$ je složen ako je djeljiv s nekim brojem $d$ različitim od $1$ i $x$, ali znamo da ako postoji takav $d$, tada postoji i takav $d\le x$; štoviše, postoji i takav $d\le\sqrt x$, ali (jer nas ne zanimaju performanse) bitno nam je samo postojanje granice, ne i njezina veličina.

%Pokušajmo otkriti kako bismo pomoću dosadašnjih konstrukcija --- ograničenog brojenja i kvantifikacije --- karakterizirali ograničenu minimizaciju. Dakle, imamo $k\in\N_+$, $(k+1\mspace{-1mu})$-mjesnu relaciju $\f R$, $k$-mjesnu totalnu funkciju $\f H$, i $\vec x\in\N^k$. Gornju granicu $\f H(\vec x)$ označimo s $a$, i uvedimo jednomjesnu relaciju $\f P(y):\Longleftrightarrow\f R(\vec x,y)$ ($\vec x$ je ionako fiksiran). Za početak pretpostavimo da doista postoji $y<a$ za koji vrijedi $\f P(y)$. Dakle $a>0$, i imamo niz istinitosnih vrijednosti $\f P(0)$, $\f P(1)$,~\ldots, $\f P(a-1)$ u kojem trebamo naći prvu vrijednost $\mathit{true}$.
%
%Kad bismo imali naredbu \texttt{break}, mogli bismo brojiti vrijednosti $\mathit{false}$ i napustiti petlju čim naiđemo na $\mathit{true}$. Kako možemo emulirati \texttt{break}? Jedan način je da imamo još jednu $bool$ varijablu (\emph{flag}) $q$, inicijaliziramo je na $\mathit{false}$, kad naiđemo na $\mathit{true}$ postavimo $q:=\mathit{true}$, a uopće ne izvršavamo tijelo petlje ako je $q=\mathit{true}$. Gledajući kako se $q$ mijenja, vidimo da je u $y$-tom prolasku to upravo istinitosna vrijednost $\f Q(y):\Longleftrightarrow(\exists i\le y)\f P(i)$. Sada je brojenje prvog bloka nula (do prve jedinice) za $\f P$ ekvivalentno brojenju \emph{svih} nula za $\f Q$, jer je $\chi_{\f Q}$ rastuća: kad postane $1$, ostaje $1$. Dakle, još je potrebno negirati $\f Q$ i primijeniti operator brojenja.
%
%To razmišljanje možemo prikazati tablicom: recimo da je $\f P$ svojstvo "biti prim-broj", i da tražimo $(\mu y<7)(y\in\mathbb P)$, najmanji prim-broj manji od $7$. Imali bismo
%\begin{equation}
    %\begin{array}{r|cc|ccccc|c}
%i & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 \\\hline
%i\in\mathbb P\Leftrightarrow:\f P(i) & \bot & \bot & \top & \top & \bot & \top & \bot  \\
%(\exists j\le i)\f P(j)\Leftrightarrow:\f Q(i) & \bot & \bot & \top & \top & \top & \top & \top \\
%\lnot\f Q(i) & \top & \top & \bot & \bot & \bot & \bot & \bot\\
%(\num j<i)\,\lnot\f Q(j) & 0 & 1 & 2 & 2 & 2 & 2 & 2 & 2
%\end{array}\text.
%\end{equation}

\begin{propozicija}[{name=[ograničena minimizacija čuva primitivnu rekurzivnost]}]\label{prop:ominprn}
Neka je $k\in\N_+$ te $\f R^k$ primitivno rekurzivna relacija. Tada je i funkcija $\f F^k$\!, dobivena ograničenom minimizacijom relacije $\f R$, također primitivno rekurzivna.
\end{propozicija}
\begin{proof}
	Za $y=0$, vrijednost funkcije $\f F$ je očito $0$, jer je antecedens kondicionala odmah na početku lažan ($0\not<0$) pa je kondicional istinit. Sada pretpostavimo da imamo već izračunanu vrijednost $z:=\f F(\vec x,y)$ (zbog napomene~\ref{nap:mintot} je $z\le y$), i pitamo se koliko je $\f F(\vec x,y+1)$. Imamo tri slučaja.

	Ako je $z<y$, to znači da postoji "dobar" $i<y<y+1$ takav da vrijedi $\f R(\vec x,i)$, i $z$ je najmanji takav $i$, pa je očito $\f F(\vec x,y+1)$ također jednako $z$. Primijetimo da ovdje sigurno vrijedi $\f R(\vec x,z)$.

	Ako je $z=y$, to znači da ne postoji dobar $i<y$, pa se pitamo vrijedi li $\f R(\vec x,y)$. Ako vrijedi, $y$ je najmanji dobar $i<y+1$, pa je $\f F(\vec x,y+1)=y$, što je opet jednako $z$.
	Inače, nismo našli dobar $i<y+1$, pa je $\f F(\vec x,y+1)=y+1$ u skladu s napomenom~\ref{nap:mintot}.

	Sve u svemu, vidimo da je $\f F=\f C_0^{k-1}\pr\f H$ (ili $0\pr\f H$ za $k=1$), gdje je $\f H$, zadana s
\begin{equation}
	\f H(\vec x,y,z)=\begin{cases}
		z\,,&\f R(\vec x,z)\\
		\f{Sc}(y),&\text{inače}
	\end{cases}\text,
\end{equation}
	primitivno rekurzivna po teoremu~\ref{tm:grek} %, primjeru~\ref{pr:m-v} i propoziciji~\ref{prop:vezn}
	--- pa je i $\f F$ takva.
	%Tvrdimo da je za svaki $\vec x\in\N^k$, vrijednost $\f F(\vec x)$ jednaka
	%\begin{equation}\label{eq:muHprn}
	%\bigl(\mu y<\f H(\vec x)\bigr)\f R(\vec x,y) =
	%\bigl(\num y<\f H(\vec x)\bigr)(\nexists\,i\le y)\f R(\vec x,i)\text,
	%\end{equation}
	%pa je $\f F$ primitivno rekurzivna po napomeni~\ref{nap:kvantSc}, propoziciji~\ref{prop:kompl} i lemi~\ref{lm:brojrek}.
	%
	%Prvo, ako ne postoji $y<\f H(\vec x)$ takav da vrijedi $\f R(\vec x,y)$, tada na lijevoj strani stoji $\f H(\vec x)$ po napomeni~\ref{nap:min=H}. S druge strane, za sve $y<\f H(\vec x)$, svaki $i\le y$ je također manji od $\f H(\vec x)$, pa ni za koji od njih ne vrijedi $\f R(\vec x,i)$. Dakle $(\nexists i\le y)\f R(\vec x,i)$ je uvijek istina, pa je desna strana jednaka $\bigl(\num y<\f H(\vec x)\bigr)\top$, što je također jednako $\f H(\vec x)$.
	%
	%Ako pak postoji neki $y<\f H(\vec x)$ takav da vrijedi $\f R(\vec x,y)$, najmanji takav (vrijednost lijeve strane) označimo s $y_0$. Tada $(\nexists i\le y)\f R(\vec x,i)$ vrijedi za sve $y<y_0$. Također, za sve $y\ge y_0$ to \emph{ne} vrijedi: uvijek možemo uzeti $i:=y_0$ kao kontraprimjer. Dakle svi $y$ za koje vrijedi $(\nexists i\le y)\f R(\vec x,i)$ su upravo svi oni manji od $y_0$, a na desnoj strani piše njihov broj, koji također iznosi $y_0$.
\end{proof}
%U iskazu ove propozicije nismo trebali stavljati riječ "primitivno" u zagrade, jer tvrdnja čitana bez riječi "primitivno" slijedi iz napomene~\ref{nap:min=H}.

%\begin{napomena}[{name=[uključena gornja granica ograničene minimizacije]}]\label{nap:muSc}
%Ista napomena o uključenoj gornjoj granici, poput~\ref{nap:kvantSc}, vrijedi i ovdje:
%$\mu y\le\f H(\vec x)$ shvaćamo kao $\mu y<\f{Sc}\bigl(\f H(\vec x)\bigr)$, a kompozicijom s inicijalnom funkcijom $\f{Sc}$ sigurno nismo pokvarili izračunljivost granice $\f H$.
%\end{napomena}