# Deriving recursive definition from function specification

Given this function specification, where name xs is bound to a list, # denotes its cardinality and . is the list index operator...

$$\left( \sum i: 0 \leq i < \#xs: xs.i * (i + 1) \right)$$

I need to derive a recursive function using induction.

Base case: []

\begin{align} \left( \sum i: 0 \leq i < \#[]: xs.i * (i + 1) \right) && \text{(Textual substitution - xs is free)} \\ \left( \sum i: 0 \leq i < 0: xs.i * (i + 1) \right) && \text{(Def. of #)} \\ \left( \sum i: False: xs.i * (i + 1) \right) && \text{(Algebra)} \\ \left( \sum i: 0 \leq i < \#xs: xs.i * (i + 1) \right) && \text{(Empty range)} \end{align}

Inductive case: (x:xs)

\begin{align} \left( \sum i: 0 \leq i < \#(x:xs): (x:xs).i * (i + 1) \right) && \text{(Textual substitution - xs is free)} \\ \left( \sum i: 0 \leq i < 1 + \#xs: (x:xs).i * (i + 1) \right) && \text{(Def. of #)} \end{align}

How can I proceed from here ?

Your notation and understanding are pretty good.

It is easier to consider (xs:x) as the inductive case instead of (x:xs)

\begin{align} \sum_{i:\ 0 \leq i < \#(xs:x)} &(xs:x).i * (i + 1)\\ &=\sum _{i:\ 0 \leq i < \#xs+1} (x:xs).i * (i + 1) \\ &=\sum_{i:\ 0 \leq i < \#xs} (xs:x).i * (i + 1)+\sum_{i:\ i=\#xs}(xs:x).i * (i + 1)\\ &=\sum_{i:\ 0 \leq i < \#xs} xs.i * (i + 1)+x*(\#xs+1),\\ \end{align} where we assume that list index starts with 0.

If we denote the function by $$f$$, the above equality becomes $$f(xs:x) = f(xs) + x*(\#xs+1),$$ which is the recursive step of a recursive definition.

The base case, as you have indicated, is $$f([]) = \sum_{ i:\ 0 \leq i < 0} [].i * (i + 1) = \sum_{i: \text{ empty set}}[].i * (i + 1) =0.$$

Exercise. Derive the following recursive formula of the same function $$f$$. $$f(x:xs) = f(xs) + t(xs)+ x,$$ where $$t(xs)=\sum_{i:\ 0 \leq i < \#(xs)} xs.i,$$ the sum of items in $$xs$$.

• Thank you very much! I only have cons (x:xs) operator in my list of definitions (it takes as first parameter a single item). I appreciate the exercise. Will try to do it. – F. Zer Dec 14 '19 at 13:48
• Could you give me a hint on your exercise? Do I need to find f? – F. Zer Dec 15 '19 at 0:46
• Thank you. I checked and I think it is an exact replica of this answer. Perhaps I am missing something ? – F. Zer Dec 17 '19 at 1:25
• Thank you, @Apass.Jack. I liked your solution, but as I said, I am only allowed to prove using (x:xs) pattern. I cannot switch the order of list and single item as in (xs:x). But it was of great help. One question, how does one use those posts with "overlaps". Is there a button to "reveal", or it is only a demonstration? – F. Zer Dec 19 '19 at 12:06
• I now managed to see full LaTeX code and accepted the answer because it solves the problem. – F. Zer Dec 20 '19 at 15:32