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$

1 Answer 1

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$
7
  • $\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, 2019 at 13:48
  • $\begingroup$ Could you give me a hint on your exercise? Do I need to find f? $\endgroup$
    – F. Zer
    Dec 15, 2019 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, 2019 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, 2019 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, 2019 at 15:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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