Mathematics and Computation

These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.

Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational effects such as non-termination, store and exceptions. Therefore, we can use realizability as a framework for program development and extraction which allows any style of programming, not just the purely functional one that is supported by the Curry-Howard correspondence. In joint work with Christopher A. Stone we developed RZ, a tool which uses realizability to translate specifications written in constructive logic into interface code annotated with logical assertions. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. In our experience, RZ is useful for specification of non-trivial theories. While the use of computational effects does improve efficiency it also makes it difficult to reason about programs and prove their correctness. We demonstrate this fact by considering non-purely functional realizers for a Brouwerian continuity principle.

Download: msfp2008-slides.pdf, msfp2008-abstract.pdf

Two versions of this talk were given at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008.

Joint work with Paul Taylor.

Abstract: Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has inspired fewer useful computational ideas. Nevertheless, we can see the computational content of Dedekind reals by constructing them within Abstract Stone Duality (ASD), a computationally meaningful calculus for topology. This provides the theoretical background for a novel way of computing with real numbers in the style of logic programming. Real numbers are defined in terms of (lower and upper) Dedekind cuts, while programs are expressed as statements about real numbers in the language of ASD. By adapting Newton’s method to interval arithmetic we can make the computations as efficient as those based on Cauchy reals.

Slides: slides-map2008.pdf (obsolete version: slides-cca2008.pdf)
Extended abstract: abstract-cca2098.pdf

With Iztok Kavkler.

Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller’s iRRAM and Lambov’s RealLib, do not seem to be based on the interval domain. In fact, their authors have observed that domain-theoretic concepts such as monotonicity of functions hinder efficiency of computation.

I will review the data structures and algorithms that are used in modern implementations of exact real arithmetic. They provide important insights, but some questions remain about what theoretical models support them, and how we can show them to be correct. It turns out that the correctness is not always clear, and that the good old interval domain still has a few tricks to offer.

Download slides: domains8-slides.pdf

A tutorial presented at the Mathematical Foundations of Programming Semantics XXIII Tutorial Day.
(more…)

With Davorin Lešnik.

Abstract: We investigate the relationship between constructive theory of metric spaces and synthetic topology. Connections between these are established by requiring a relationship to exist between the intrinsic and the metric topology of a space. We propose a non-classical axiom which has several desirable consequences, e.g., that all maps between separable metric spaces are continuous in the sense of metrics, and that, up to topological equivalence, a set can be equipped with at most one metric which makes it complete and separable.

Presented at: 3rd Workshop on Formal Topology

Download slides: 3wft.pdf

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

With Chris Stone.

Abstract:
Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

Presented at Computablity in Europe 2007.

Download paper:

• Long version: cie-long.pdf (January 29, 2007)
• Short version: cie-short.pdf (January 29, 2007)

Download slides: cie2007-slides.pdf

Download source code from RZ web page.

With Alex Simpson.

Abstract: We present a constructive meta-theorem about sequential continuity which allows us to conclude from a constructive proof of existence of a function between complete metric spaces satisfying a given system of (functional) equations that there also exists a sequentially continuous function satisfying the system.

Presented at: Trends in Constructive mathematics, Frauenwörth am Chimsee, Germany, June 2006.

Download slides: continuity_begets_continuity_bavaria_slides.pdf

With Chris Stone.

Presented at: Reliable Implementation of Real Number Algorithms: Theory and Practice, Dagstuhl Seminar 06021.

Abstract: see “Specifications via Realizability (CLASE)”.

Talk notes: rz-dagstuhl.pdf (handwritten notes of the talk with examples of how RZ works)

At the EST training workshop in Fischbachau, Germany, I gave two lectures on syntehtic computability theory. This version of the talk contains material on recursive analysis which is not found in the MFPS XXI version of a similar talk.

Abstract:
Computability theory, which investigates computable functions and computable sets, lies at the foundation of logic and computer science. Its classical presentations usually involve a fair amount of Goedel encodings. Consequently, there have been a number of presentations of computability theory that aimed to present the subject in an abstract and conceptually pleasing way. We build on two such approaches, Hyland’s effective topos and Richman’s formulation in Bishop-style constructive mathematics, and develop basic computability theory, starting from a few simple axioms. Because we want a theory that resembles ordinary mathematics as much as possible, we never speak of Turing machines and Goedel encodings, but rather use familiar concepts from set theory and
topology.

Download slides: est.pdf