Reductions in computability theory from a constructive point of view

Here are the slides from my Logic Coloquium 2014 talk in Vienna. This is joint work with Kazuto Yoshimura from Japan Advanced Institute for Science and Technology.

Abstract: In constructive mathematics we often consider implications between non-constructive reasoning principles. For instance, it is well known that the Limited principle of omniscience implies that equality of real numbers is decidable. Most such reductions proceed by reducing an instance of the consequent to an instance of the antecedent. We may therefore define a notion of instance reducibility, which turns out to have a very rich structure. Even better, under Kleene’s function realizability interpretation instance reducibility corresponds to Weihrauch reducibility, while Kleene’s number realizability relates it to truth-table reducibility. We may also ask about a constructive treatment of other reducibilities in computability theory. I shall discuss how one can tackle Turing reducibility constructively via Kleene’s number realizability.

Slides with talk notes:  lc2014-slides-notes.pdf

Seemingly impossible constructive proofs

In the post Seemingly impossible functional programs, I wrote increasingly efficient Haskell programs to realize the mathematical statement

$\forall p : X \to 2. (\exists x:X.p(x)=0) \vee (\forall x:X.p(x)=1)$

for $X=2^\mathbb{N}$, the Cantor set of infinite binary sequences, where $2$ is the set of binary digits. Then in the post A Haskell monad for infinite search in finite time I looked at ways of systematically constructing such sets $X$ with corresponding Haskell realizers of the above omniscience principle.

In this post I give examples of infinite sets $X$ and corresponding constructive proofs of their omniscience that are intended to be valid in Bishop mathematics, and which I have formalized in Martin-Löf type theory in Agda notation. This rules out the example $X=2^\mathbb{N}$, as discussed below, but includes many interesting infinite examples. I also look at ways of constructing new omniscient sets from given ones. Such sets include, in particular, ordinals, for which we can find minimal witnesses if any witness exists.

Agda is a dependently typed functional programming language based on Martin-Löf type theory. By the Curry-Howard correspondence, Agda is also a language for formulating mathematical theorems (types) and writing down their proofs (programs). Agda acts as a thorough referee, only accepting correct theorems and proofs. Moreover, Agda can run your proofs. Here is a graph of the main Agda modules for this post, and here is a full graph with all modules.

Continue reading

Brazilian type checking

I just gave a talk at “Semantics of proofs and certified mathematics”. I spoke about a new proof checker Chris Stone and I are working on. The interesting feature is that it has both kinds of equality, the “paths” and the “strict” ones. It is based on a homotopy type system proposed by Vladimir Voevodsky. The slides contain talk notes and explain why it is “Brazilian”.

Download slides: brazilian-type-checking.pdf

GitHub repository: https://github.com/andrejbauer/tt

Abstract: Proof assistants verify that inputs are correct up to judgmental equality. Proofs are easier and smaller if equalities without computational content are verified by an oracle, because proof terms for these equations can be omitted. In order to keep judgmental equality decidable, though, typical proof assistants use a limited definition implemented by a fixed equivalence algorithm. While other equalities can be expressed using propositional identity types and explicit equality proofs and coercions, in some situations these create prohibitive levels of overhead in the proof.
Voevodsky has proposed a type theory with two identity types, one propositional and one judgmental. This lets us hypothesize new judgmental equalities for use during type checking, but generally renders the equational theory undecidable without help from the user.

Rather than reimpose the full overhead of term-level coercions for judgmental equality, we propose algebraic effect handlers as a general mechanism to provide local extensions to the proof assistant’s algorithms. As a special case, we retain a simple form of handlers even in the final proof terms, small proof-specific hints that extend the trusted verifier in sound ways.

Intuitionistic Mathematics and Realizability in the Physical World

This is a draft version of my contribution to “A Computable Universe: Understanding and Exploring Nature as Computation”, edited by Hector Zenil. Consider it a teaser for the rest of the book, which contains papers by an impressive list of authors.

Abstract: Intuitionistic mathematics perceives subtle variations in meaning where classical mathematics asserts equivalence, and permits geometrically and computationally motivated axioms that classical mathematics prohibits. It is therefore well-suited as a logical foundation on which questions about computability in the real world are studied. The realizability interpretation explains the computational content of intuitionistic mathematics, and relates it to classical models of computation, as well as to more speculative ones that push the laws of physics to their limits. Through the realizability interpretation Brouwerian continuity principles and Markovian computability axioms become statements about the computational nature of the physical world.

Download: real-world-realizability.pdf

Univalent foundations subsume classical mathematics

A discussion on the homotopytypetheory mailing list prompted me to write this short note. Apparently a mistaken belief has gone viral among certain mathematicians that Univalent foundations is somehow limited to constructive mathematics. This is false. Let me be perfectly clear:

Univalent foundations subsume classical mathematics!

The next time you hear someone having doubts about this point, please refer them to this post. A more detailed explanation follows.

Continue reading