2
$\begingroup$

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 ?

$\endgroup$
3
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – F. Zer Dec 14 '19 at 13:48
  • $\begingroup$ Could you give me a hint on your exercise? Do I need to find f? $\endgroup$ – F. Zer Dec 15 '19 at 0:46
  • $\begingroup$ Thank you. I checked and I think it is an exact replica of this answer. Perhaps I am missing something ? $\endgroup$ – F. Zer Dec 17 '19 at 1:25
  • $\begingroup$ 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? $\endgroup$ – F. Zer Dec 19 '19 at 12:06
  • 1
    $\begingroup$ I now managed to see full LaTeX code and accepted the answer because it solves the problem. $\endgroup$ – F. Zer Dec 20 '19 at 15:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.