Notes - Functional Programming MT22, Duality theorems
Flashcards
What is the “first duality theorem” in functional programming?
\[\text{foldr } (\oplus) \text{ a xs} = \text{foldl } (\oplus) \text{ a xs}\]
whenever $\oplus$ and $a$ form a monoid and $\text{xs}$ is a finite list.
What is the “second duality theorem” in functional programming?
Suppose that, for all $x, y, z$
\[\begin{aligned} x \oplus (y \otimes z) &= (x \oplus y) \otimes z \\\\ x \oplus a &= a \otimes x \end{aligned}\](i.e. they associate with eachother and satisfy this condition about the identity), then
\[\text{foldr } (\oplus) \text{ a xs} = \text{foldl } (\otimes) \text{ a xs}\]When proving the second duality theorem, that if for all $x, y, z$
\[\begin{aligned}
x \oplus (y \otimes z) &= (x \oplus y) \otimes z \\\\
x \oplus a &= a \otimes x
\end{aligned}\]
(i.e. they associate with eachother and satisfy this condition about the identity), then
\[\text{foldr } (\oplus) \text{ a xs} = \text{foldl } (\oplus) \text{ a xs}\]
what auxilary result is needed that makes the proof by induction easy?
\[x \oplus (\text{foldl } (\otimes) \text{ a xs} ) = \text{foldl } (\otimes) \text{ a (x:xs)}\]
What is the “third duality theorem” in fucntional programming?
\[\text{foldl } (\oplus) \text{ a xs } = \text{foldr } (\text{flip } \oplus) \text{ a (reverse xs) }\]