How to define summation recursively?

29 Views Asked by At

I have attempted to define $s_n=\sum_{i=1}^n a_i=a_1+\cdots+a_n$ in a valid manner, but I'm not sure if my extraction of $(s_i\mid 1\leq i\leq n)$ from $(p_i\mid i\in\mathbb N)$ contains any error. Please help me check that part!

Suppose that $(a_1,\cdots,a_n)$ is a finite sequence in $\mathbb N$. Then there exists a sequence $(s_1,\cdots,s_n)$ such that $s_1=a_1$ and $s_{i+1}=s_i+a_{i+1}$ for all $1\leq i<n$.

My attempt:

We define mapping $f$ as follows: $f: \mathbb N\times\mathbb N\to\mathbb N\times\mathbb N: (i,a)\mapsto\begin{cases} (i+1,a+a_{i+1})&\text{if }i<n\\ (i+1,a)&\text{if }i\geq n \end{cases}$

By recursion theorem, there is a unique sequence $(p_i\mid i\in\mathbb N)$ such that $p_0=(1,a_1)$ and $p_{i+1}=f(p_i)$. Let $\pi:\mathbb N\times\mathbb N\to\mathbb N$ be the projection to the second co-ordinate i.e. $\pi(i,a)=a$. Let $s_i=\pi(p_i)$ for all $1\leq i\leq n$, then $(s_i\mid 1\leq i\leq n)$ is the required sequence. It's clear from the definition of $s_i$ that $s_{i+1}=s_i+a_{i+1}$ for all $1\leq i<n$.