Folding the Heighway dragon curve
This work provides a formal proof of equivalence for a well-known fractal curve, but it is incremental as it applies known functional programming concepts to a specific mathematical construction.
The authors prove the equivalence of two standard constructions of the Heighway dragon curve by generalizing the construction to allow rotations on both sides, showing that the two approaches correspond to foldr and foldl, and using the second duality theorem with distributivity of an interleave operator.
The Heighway dragon curve is one of the most known fractal curves. There are two ways to construct the curve: repeatedly make a copy of the current curve, rotate it by 90 degrees, and connect them; or repeatedly replace each straight segment in the curve by two segments with a right angle. A natural question is how do we prove the equivalence of the two approaches? We generalise the construction of the curve to allow rotations to both sides. It then turns out that the two approaches are respectively a foldr and a foldl, and the key property for proving their equivalence, using the second duality theorem, is the distributivity of an "interleave" operator.