Fractal Art 2

As discussed before (see here), Iterated Function System (IFS) can generate Fractals. This method is introduced by Michael Barnsley in 1986. Indeed, he showed the Collage Theorem: if a collection (or collage) of mappings in the IFS satisfy a contracting criterion, any initial image for the iteration will converge eventually to the same fractal image. This means a fractal image can be encoded by some suitable IFS, which can be decoded simply upon iteration of IFS. This is the basis of fractal compression algorithms.

The Collage Theorem belongs to a class of fixed-point theorems in metric space: a system in which a distance is suitably defined. A mapping in metric space maps each point an image point in the same space. The mapping is a contraction if the distance between image points is less than their original distance. That contraction mappings in metric space has a fixed point is a result called the Banach Fix-Point Theorem.

For my project on this topic, I plan to do the following:

1. Formalize metric space up to contraction maps, hence proving Banach Fix-Point Theorem
2. Extend metric space formalization to include IFS, hence proving Collage Theorem

With such formalization I should be able to verify fractal generating algorithms based on IFS. I still have to look up a bit more about fractal compression algorithms to find out if these tools are sufficient to verify such algorithms.

Fractal Art

In terms of visual impact, none has a greater effect than Fractals. They are the most recognizable math images. As static images, they are a form of algorithmic art: the pixels are colored according to a mechanical computation. However, they are also dynamic, as the math behind reveals this remarkable property of fractals: self-similarity: if you zoom in at a spot, you can see finer and finer details — you’ll discover copies of the original, identical or distorted, somewhere in those finer details. This is marvelously printed in The Beauty of Fractals by Heinz-Otto Peitgen and Peter Richter (1986).

Instead of zooming in, you can imagine zooming out, getting less and less details of the fractal. For the computer screen, this means getting bigger and bigger “pixels” — to be simulated by software. This suggests building fractals in stages: the first stage being a very coarse-grain pattern, then repeat the pattern in its sub-parts in the next stage for a less coarse-grain pattern. Keep repeating this process to get the ultimate fine-grain fractal.

This method of generating fractals is called IFS: Iterated Function Systems. You can get some hands-on experience with IFS by folding paper:

• Fold a sheet of paper once, then unfold it, the crease pattern (from side) is: |_.
• Fold the sheet twice, then unfold twice, now the crease pattern is: |_|▔.
• Fold the sheet three times, …. and so on.

If you’re smart enough, you can predict the successive crease patterns. Anyway, you’ll be fascinated by these fold-crease patterns as they develop. These fractals are called Dragon Curves, by iterating (i.e. repeating) a function (e.g. the method of folding).

In 1992 Scott Draves took a variation on this theme, using different functions in iteration and applying novel coloring schemes, leading to Fractal Flames.

Modern cellphones don’t have outside antenna. Instead they have fractal antenna inside, etched on the circuit board, to get better reception and pick up more frequencies such as bluetooth, cellular, and Wi-Fi all from one antenna at the same time!

The IFS technique had been applied to image compression algorithms, since natural objects like trees, mountains, clouds, etc. have an approximate fractal structure. Will verifying such fractal algorithms by a theorem prover be a worthwhile research project?