My research and investigations

Archive for November, 2010

Theorem-Proving in Finite Fields

This is my PhD project proposal.

Introduction

Finite fields are also known as Galois fields, in honor of the French mathematical genius Évariste Galois (1811 – 1832). The theory is developed from a small list of axioms, with subject matter intimately related to the arithmetic of remainders under division. Division by prime numbers give base fields, while division by primitive polynomials give nice extensions of base fields. Such is the power of a simple theory, unifying ideas from diverse topics.

There are many theorems, big and small, in the theory of Finite Fields. Since axioms are very low-level, but theorems can be high-level, the chain of reasoning from axioms to theorems is often very long. It is not uncommon to find in textbooks proof sketches of high-level theorems, leaving tedious details as exercises. Such tasks are better suited to a theorem-prover, working tirelessly and attending to logical details.

Applications

Although a topic in abstract algebra, Finite Fields have found applications in digital computers and digital communication. Two areas of interest to this project are:

  • Linear Feedback Shift Register (LFSR) – this is a simple logical circuit to deliver a sequence of binary bits. The bits look random: but since the number of circuit states is finite, the bits will repeat after a period. For cryptography, where long pseudo-random sequences can provide security for encryption, the problem is how to design LFSRs with long periods. Such work is pioneered by Solomon Golomb in 1955, showing the best LFSR designs are related to primitive polynomials in finite fields. Nowadays, LFSR have extensive military, industrial and consumer applications. For example, A5/1, a stream cipher used to encrypt mobile phone conversations in GSM standard, is LFSR-based (see here). Global Positioning System (GPS) uses an LFSR to rapidly transmit a sequence that indicates high-precision relative time offsets.
  • Error-Correcting Codes (ECC) – these are coding schemes for reliable communication through a noisy channel. Examples are Bose-Chaudhuri-Hocquenghem (BCH) codes, which are based on primitive polynomials over a finite field. Because BCH codes can detect and correct multiple error bits, they are crucial for digital data storage and retrieval, and make NASA space missions possible. Reed-Solomon codes, a special type of BCH code, was used in Voyager 2 probe to send back color pictures of inner and outer planets. Today (see here) Reed-Solomon codes can be found in devices using CDs, DVDs, Blu-ray Discs; in hard-drives and flash-drives; as well as in communication protocols over networks, both cable and wireless.

The BCH codes and Reed-Solomon codes were conceived around 1960. Initially there is one drawback: while the codes can encode messages fast, the decoding process is complex and slow. In 1967, Elwyn Berlekamp invented an efficient algorithm for decoding BCH codes. Later in 1969, James Massey developed an algorithm for a different problem: how to find the shortest LFSR for given a binary sequence. Massey soon realized that his algorithm was essentially an improved version of Berlekamp’s algorithm. This Berlekamp-Massey algorithm, based on the theory of finite fields, turns using Reed-Solomon codes in error-detection and error-recovery a practical reality.

Proposal

I intend to work on the formalization of Finite Fields, with the goal of proving Berlekamp-Massey algorithm. Major milestones are:

  1. Formalize elementary field theory from its axioms, based upon a finite set.
  2. Extend this formalization to include primitive polynomials of finite fields.
  3. Prove properties of LFSR within this finite fields formalization.
  4. Prove properties of BCH codes within this finite fields formalization.
  5. Show that the problems of BCH decoding and shortest LFSR are equivalent.
  6. Show that Berlekamp-Massey algorithm is correct.

Notes

  • The theorem-prover to be used is HOL4, a system with some packages for group theory and number theory.
  • This formalization only covers the fundamental parts of the theory of Finite Fields.

Finite Fields 2

The applications of the theory of finite fields (see here) depend on finding primitive polynomial of the field. This is due to the fact that a root of the primitive polynomial can act as a generator of the whole finite field.

My own presentation of this topic can be found here (click Primes for Random, then Simple Machines), showing how primitive polynomials underlie the construction of LFSRs for pseudo-random number generation.

In 1967, Elwyn Berlekamp invented an algorithm for decoding BCH codes, which is a type of polynomial code based on primitive polynomials of finite fields. Later James Massey simplified the algorithm, and recognized its application to LFSR which is also based on primitive polynomials of finite fields. Their algorithm is now known as Berlekamp-Massey algorithm.

My plan for the project work on this topic is to do the following:

  1. Formalize elementary field theory from its axioms, based upon a finite set.
  2. Extend this formalization to include the primitive polynomials of finite fields.

With these tools, I can try to prove the Berlekamp-Massey algorithm. I am now studying a Java applet that demonstrates this algorithm.

Elliptic Curve 2

The theory of elliptic curves (EC) can go very deep, but its applications (see here) need only an understanding of the group law which is unique to elliptic curves. Many algorithms of these applications work for any group, although the special structure of the elliptic curve group has implications in reliability (e.g. cryptography) or efficiency (e.g. factoring) of the algorithm.

Originally, my plan for the project work on this topic is to do the following:

  1. Formalize elementary group theory from its axioms
  2. Extend this formalization to include the group structure of elliptic curves

Then use this formalization to verify EC algorithms. However:

Since Romain Cosse haven’t published formal proofs of his new EC factorization algorithms, I may be able to fill in this gap by building upon the works of Joe and Laurent.

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.

Turtle Geometry 2

In their book (see here), Harold and Andrea begin with a program POLY: steps for a turtle tracing polygons on the plane. A polygon is a closed path: we can see that clearly from outside, but how does a turtle know its path is closed from inside, without measuring its coordinates ? They discuss this in detail, leading to:

  • Closed Path Theorem: the total turning along any closed path in the plane is an integer multiple of 360°. That integer is called the winding number of the closed path.
  • Simple Closed Path Theorem: a simple closed path, which is non-crossing, in the plane has winding number ±1.
  • Whitney-Graustein Theorem: two closed paths in the plane can be deformed into one another if and only if they have the same winding number.

They proved the first, gave a detail sketch of the second, and showed only half of the third — all using elementary topology. As an application of these ideas, they put a stop condition for POLY (so turtle really knows its path is closed), worked out the symmetry of the polygon from the input parameters of POLY, and taught the turtle to escape a fair maze via Pledge algorithm.

Then they let the turtle wander on the sphere, a curved surface that can still be visualized. The turtle will find that Closed Path Theorem breaks down. They showed skillfully how the theorem can be restored, by introducing an intrinsic turning that serves to measeure curvature. The whole discussion makes use of elementary topology of surfaces.

Of course, they let the turtle wander on the torus, the Möbius strip, even Klein’s bottle — leading to this result:

  • Gauss-Bonnet Theorem – for any closed surface, the total curvature K and Euler characteristic χ are related by K = 2πχ.

Eventually they let the turtle wander in Einstein’s curved spacetime – a curved 3D (simplify to 2D space + time) that can only be viewed from inside. It’s amazing that they can talked about differential geometry and Lorentz transform using only diagrams!

For my project, I plan to follow the book’s approach, with the following:

  1. Formalize topology of closed path, hence proving Whitney-Graustein Theorem
  2. Formalize topology of closed surfaces, hence proving Gauss-Bonnet Theorem

Pledge algorithm of solving maze can be formally verified as a result. I am not sure if its recreational use is of any benefit in serious research.

Finite Fields

In abstract algebra, a field is a system within which add, subtract, multiply and divide are possible. An example of such a system is all the fractions (called rationals Q in math), but the number of fractions is infinite. Finite systems with suitably-defined +-*/ do exist, and they are known as finite fields. It was a remarkable discovery by Évariste Galois, a math genius, that finite fields are characterized only by its number of elements, which must be either a prime or power of a prime. Due to this, finite fields are also known as Galois fields.

Finite fields have many practical applications, including cryptography, error-correcting codes and LFSRs (Linear feedback shift register) for pseudo-random number generation. There is a large collection of algorithms based on theory of finite fields.

Search on Net shows the Google project: coq-galois-theory. Its timeline suggests that some progress have been made, but still a lot of work to be done. Maybe I can do a project on proving/verifying finite field algorithms in error codes and LFSRs.

Formalize X, Apply Y

My proposed research topics are of the theme: formalize a theory X, apply to verification of algorithm Y. I still haven’t picked a topic to go ahead. Here are some of my thoughts:

  1. Turtle Geometry – Differential geometry and topology are the theories behind advanced turtle geometry. This is a wide range of topics – perhaps too many. The algorithms are just graphic procedures, although their validity are based on theorems. Such graphic algorithms probably have no practical applications, so are they worth verifying?
  2. Fractal Art – Like turtles, graphic algorithms to display fractals probably don’t have research value. Generating fractals is based on the theory of IFS. There is one practical application of IFS: (natural) image compression. I’m not sure if compression algorithms are worth verifying.
  3. Elliptic Curves – The theory of elliptic curves (EC) overlaps with number theory, group theory and modular forms. There are many elliptic curve algorithms in actual use, including factoring and cryptography. Certainly there are incentives to verify these algorithms, and Joe Hurd had been working on EC cryptography. Will doing only EC factoring be enough for research work?

I was thinking, formalizing EC is just putting textbook math into the theorem prover. That sounds easy. Joe’s paper showed that this is no easy task at all, and it’s only the beginning.