2
$\begingroup$

Recall the fold function for lists:

$fold(f,z,[x,xs]) = fold(f,f(z,x),xs)$

$fold(f,z,[]) = z$

I want to formally proof that if $f$ is associative, commutative and idempotent (meaning $f(x,y) = f(x,f(x,y))$ and we have to lists $l_1$ and $l_2$ such that their contents are equal then $fold(f,z,l_1) = fold(f,z,l_2)$.

What I've tried

  1. I've tried double induction on the sizes of the list but this doesn't clarify much the problem.

  2. I've figured out a procedure that would leave me with a list of non-repeating elements. I take each element of the $f(f(f(\cdots)))$ list and take it to the outside thanks to associative and commutative property. En each step I make sure that if I find two equal elements I remove them using idempotence. The basic rules are as follows:

$f(f(z,x),y) \text{ push x out, push y in} = f(y,f(z,x)) = f((y,z),x) = f(f(z,y),x)$

$f(f(z,x),x) = f(z,x)$

The actual transformation to the list would look like this:

     def transform[A](l: List[A]) := l match {
        case Nil() => Nil()
        case x :: Nil() => x :: Nil()
        case x :: x :: xs => transform(x :: xs)
        case x :: y :: xs  => y :: transform(x :: xs)  
     }

My first problem is how to write the predicate to say that this algorithm gives a list with non-repeating elements. I do it like this:

$\forall x,y. x \in l \land y \in l \land x = y \implies index(x) = index(y)$

But I don't how to proof that my algorithm guarantees that this property holds.

  1. The idea is that if I can proof that this transformation does not leave repeating elements then it would be easy to show that the lists end up with equal lengths and for each first element of one list I could transform the second list to get the very first element and I could apply induction to show that the statement holds.

So in short, if you think my approach is efficient and correct do you know how to solve the problems I got? And if you think you have better ideas can you give me any hints?

Edit

Just realized that my function only eliminates one repeating sequence. So adapt the argument...

$\endgroup$
2
$\begingroup$

"contents are equal" implies that their lengths are equal, so you don't need double induction. Instead, try single induction. A straightforward induction argument on the length of the list should suffice.

I wouldn't suggest trying to remove repeated elements. That is not necessary, and it is an unnecessary complication that turns a simple induction into something really complicated and messy (as you have discovered).

$\endgroup$
  • $\begingroup$ @Rodrigo, I suggest you read my answer again. The 2nd and 3rd sentences of my answer give a suggestion on what to use! $\endgroup$ – D.W. Mar 22 '17 at 23:28

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.