Révision 168 CSL17/preliminaries.tex

preliminaries.tex (revision 168)
46 46 
	\begin{enumerate}
47 47 
		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.
48 48 
		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.
49 
		\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.
49 
		\item The successor functions $\succ i ( ; x) := xi$ for $i = 0,1$.
50 50 
		\item The predecessor function $\pred (; x) := \begin{cases}
51 51 
		\epsilon &  \mbox{ if }  x = \epsilon \\
52 52 
		x' &  \mbox{ if }  x = x'i
......
77 77 
		\[
78 78 
		\begin{array}{rcl}
79 79 
		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) \\
80 
		f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
80 
		f (\succ i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
81 81 
		\end{array}
82 82 
		\]
83 83 
		for $i = 0,1$,  so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).
......
101 101 
\[
102 102 
\begin{array}{rcl}
103 103 
f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\
104 
f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
104 
f^j(\succ i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
105 105 
\end{array}
106 106 
\]
107 107 
for $i = 0,1$,  so long as the expressions are well-formed.

Formats disponibles : Unified diff