# Thread: Using primitive recursion scheme

1. ## Using primitive recursion scheme

Hi!
I have to define the scheme of primitive recursion of this function:

$remove_from_left: \Sigma^{*}\mbox{x}\mathbb{N} \rightarrow \Sigma^{*}$

Some examples:
$removefromleft(abcdc,7)=\epsilon$

$removefromleft(abcdc,3)=dc$

First I gave a inductive definition for $\Sigma^{*}\mbox{x}\mathbb{N}$ then $\Sigma^{*}\mbox{x}\mathbb{N}$ is defined inductively by the next rules:

$
(i) (\epsilon,0)\in\Sigma^{*}\mbox{x}\mathbb(N)$

$(ii) \mbox{ If } (w,0)\in\Sigma^{*}\mbox{x}\mathbb{N} and \mbox{x}\in\Sigma \Rightarrow (xw,0)\Sigma^{*}\mbox{x}\mathbb{N}$

$(iii)\mbox{ If } (w,n) \in \Sigma^{*}\mbox{x}\mathbb{N} \Rightarrow (w, n+1)\in\Sigma^{*}\mbox{x}\mathbb{N}$

After that I defined the scheme of primitive recursion for $\Sigma^{*}\mbox{x}N:$:

$\displaystyle \mathbb{H}$ Be $\Sigma^{*}$ a set and be :

- $f_0 \in \Sigma^{*}$

- $f_1:\Sigma^{*}\mbox{x} \mathbb{N} \mbox{x}\Sigma \mbox{x}\Sigma^{*}\rightarrow \Sigma^{*}$

- $f_2:\Sigma^{*}\mbox{x} \mathbb{N}\mbox{x}\Sigma^{*}\rightarrow \Sigma^{*}$

$\mathbb{T}$ Then exist only one function $removefromleft:\Sigma^{*}\mbox{x}\mathbb{N}\righta rrow\Sigma^{*}$ that:

$(i) removefromleft((\epsilon,0))=f_0=\epsilon$

$(ii) removefromleft((xw,0))=f_1((w,0),x,removefromleft( w,0))= xw$

$(iii) removefromleft((w,n+1))=f_2((w,n)$
$,removefromleft(w,n))=removefromleft(w,n)$

Is this ok? Perhaps I have to change something...

Thank's!

Sorry for my bad english because I speak spanish

2. When you write ... = removefromleft(w), where is the second argument? Also, it is not clear how w changes from one recursive call to the next in (iii).

Maybe it is easier to give inductive definitions for $\Sigma^*$ and $\mathbb{N}$ separately. Then you can define a helper function by primitive recursion that removes the left character from a word. Then you define the main function by recursion on the second (i.e., numerical) argument; it repeatedly removes the left character.

3. Thank's for the answer, I fixed the point you told me but I don't understand how to do what you say

4. Maybe it is easier to give inductive definitions for and separately.
For $\mathbb{N}$:

$0\in\mathbb{N}$
$n\in\mathbb{N}\Rightarrow S(n)\in\mathbb{N}$

Here $S$ is the successor function. Thus, $\mathbb{N}$ consists of terms $S(S(\dots S(0)\dots))$.

For $\Sigma^*$:

$\epsilon\in\Sigma^*$
for all $x\in\Sigma$, $w\in\Sigma^*\Rightarrow x\cdot w\in\Sigma^*$.

Here $\cdot$ is an infix notation for a binary function $\mbox{add}:\Sigma\times\Sigma^*\to\Sigma^*$ that adds a symbol $x$ to $w$ on the left, i.e., $x\cdot w=\mbox{add}(x,w)$. Thus, $\Sigma^*$ consists of terms $\mbox{add}(x_1,\mbox{add}(x_2,\dots,\mbox{add}(x_n ,\epsilon)\dots))$ where $x_1,\dots,x_n\in\Sigma$.

Let's define $f:\Sigma^*\to\Sigma^*$ by primitive recursion.

$f(\epsilon)=\epsilon$
$f(x\cdot w)=w$

Next, define $\mbox{rfl}:\Sigma^*\times\mathbb{N}\to\Sigma^*$.

$\mbox{rfl}(w,0)=w$
$\mbox{rfl}(w,S(n))=\dots$ (fill in the blank)

Disclaimer. The solution to this problem may depend a lot on the context of the course. First, strictly speaking, $\mbox{rfl}(w,0)=w$ is not a part of legal recursive schema. One should write $\mbox{rfl}(w,0)=P_1^2(w,0)$ where $P_i^n(x_1,\dots,x_n)=x_i$ is the projection function -- one of the base functions considered as given in primitive recursion. Usually such precision is not required.

Second, primitive recursive functions are traditionally defined for natural numbers. However, now, when programming languages like Haskell and ML allow defining new datatypes, it is clear that natural numbers is just the simplest nontrivial (i.e., infinite) example of an inductive type, where one constructor -- 0 -- is a constant and the other constructor -- S -- is a unary function. There is nothing special about this type. One may consider types with more than two constructors that are binary, ternary, etc. E.g., strings form an inductive type with one constant constructor -- $\epsilon$ -- and a binary constructor $\mbox{add}$. Correspondingly, the definition of primitive recursive functions is straightforwardly extended to these types.

Since you started by giving an inductive definition of $\Sigma^*\times\mathbb{N}$, I assumed that your instructor has this more liberal approach. Otherwise, you may consider recursion only on natural numbers and define functions on [tex]\Sigma^*[/MATH, say, using an English description. Then you can define f above using other means and consider only the equations for $\mbox{rfl}$.

If I did not address your question, feel free to give more details.