Mathematics and Computation

With Iztok Kavkler.

Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program specifications using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code from formal proofs, if they so desire. We used this methodology to axiomatize real numbers and implemented the specification computed by RZ. The axiomatization is the standard domain-theoretic construction of reals as the maximal elements of the interval domain, while the implementation closely follows current state-of-the-art implementations of exact real arithmetic. Our results shows not only that the theory and practice of computable mathematics can coexist, but also that they work together harmoniously.

Presented at Computability and Complexity in Analysis 2007.

Download paper: rzreals.pdf

Download slides: cca2007-slides.pdf

The famous theorem by Cantor states that the cardinality of a powerset `P(A)` is larger than the cardinality of `A`. There are several equivalent formulations, and the one I want to consider is

Theorem (Cantor): There is no onto map `A -> P(A)`.

In this post I would like to analyze the usual proof of Cantor’s theorem and present an insightful reformulation of it which has applications outside set theory. (more…)