5^th Colloquium of Research Area KL

Date: June 19, 2015

Venue:  Seminar room 1st floor, Arithmeum, Lennéstr. 2, Bonn

Homepage: Research Institute for Discrete Mathematics

Program:

Abstracts:

Mathematical work is based on basic objects like natural numbers, real numbers, sets and functions, and their elementary properties. Mathematical practice is not overly concerned with exact axiomatic specifications, since these notions are intuitive and sufficiently robust if applied by mathematical experts.

Foundational aspects become however crucial in formal mathematics, which proposes to carry out all of (pure) mathematics completely formal, using computer support. Here one cannot afford vaguenesses or even inconsistencies in the foundations, since they would, without expert intervention, spread automatically throughout the entire formal system.

In my talk I shall mention some major systems for formal mathematics like Isabelle and Coq and their underlying axioms. These systems are being used to prove and proof-check deep theorems, but they lack a number of desirable mathematical features. I shall then present some research on providing natural mechanisms for the introduction of functions (Naproche) and on type systems close to the common flexible typing of mathematical objects (SAD). The (relative) consistency of these approaches is established by relating them to classical logic and axiomatic set theory.

We consider the problem of constructing fast and small binary adder circuits. Among widely-used adders, the Kogge-Stone adder is often considered the fastest, because it computes the carry bits for two n-bit numbers (where n is a power of two) with a depth of 2log n logic gates, size 4 n log n, and all fan-outs bounded by two. Fan-outs of more than two are avoided, because they lead to the insertion of repeaters for repowering the signal and additional depth in the physical implementation.

However, the depth bound of the Kogge-Stone adder is off by almost a factor of two from the lower bound of log n + log log log n.  This bound is achieved asymptotically in two separate constructions by Brent and Krapchenko. Brent's construction gives neither a bound on the fan-out nor the size, while Krapchenko's adder has linear size, but can have up to linear fan-out.

We introduce the first family of adders with an asymptotically optimum depth of log n + o(log n), linear size O(n), and a fan-out bound of two, thereby, combining and improving the best characteristics of all previous adders.

This is joint work with Sophie T. Spirkl.