In various mathematical forums, mostly those of a logical flavor, I regularly see people asking basic questions about constructive mathematics. I also see misconceptions about constructive mathematics. I shall make a series of posts, Constructive Gems and Stones, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics.
A constructive gem is something nice about constructive mathematics that makes you want to know more about it. In contrast, a constructive stone is a complication in constructive mathematics which does not exist in the classical counterpart.
Here we go! The first one is about finite sets.
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
Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarskiâ€™s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.
Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of Programming Semantics (MFPS XXV)
I show how monads in Haskell can be used to structure infinite search algorithms, and indeed get them for free. This is a follow-up to my blog post Seemingly impossible functional programs. In the two papers Infinite sets that admit fast exhaustive search (LICS07) and Exhaustible sets in higher-type computation (LMCS08), I discussed what kinds of infinite sets admit exhaustive search in finite time, and how to systematically build such sets. Here I build them using monads, which makes the algorithms more transparent (and economic). Continue reading A Haskell monad for infinite search in finite time
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
At MSFP 2008 in Iceland I chatted with Dan Piponi about physics and intuitionistic mathematics, and he encouraged me to write down some of the ideas. I have little, if anything, original to say, so this seems like an excellent opportunity for a blog post. So let me explain why I think intuitionistic mathematics is good for physics.
Continue reading Intuitionistic mathematics for physics
With Iztok Kavkler.
Abstract: We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous Ï‰-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real numbers.
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
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