# Mathematics and Computation

## A blog about mathematics for computers

Postsby categoryby yearall

# Posts in the category Publications

For a more comprehensive list of publications by Andrej Bauer, please visit:

### On fixed-point theorems in synthetic computability

I forgot to record the fact that already two years ago I wrote a paper on Lawvere's fixed-point theorem in synthetic computability:

Andrej Bauer: On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, Volume 10: Issue 3, pp. 167–181.

It was a special issue in honor of Professors Peter J. Freyd and F. William Lawvere on the occasion of their 80th birthdays.

Lawvere's paper "Diagonal arguments and cartesian closed categories proves a beautifully simple fixed point theorem.

Theorem: (Lawvere) If $e : A \to B^A$ is a surjection then every $f : B \to B$ has a fixed point.

Proof. Because $e$ is a surjection, there is $a \in A$ such that $e(a) = \lambda x : A \,.\, f(e(x)(x))$, but then $e(a)(a) = f(e(a)(a)$. $\Box$

Lawvere's original version is a bit more general, but the one given here makes is very clear that Lawvere's fixed point theorem is the diagonal argument in crystallized form. Indeed, the contrapositive form of the theorem, namely

Corollary: If $f : B \to B$ has no fixed point then there is no surjection $e : A \to B^A$.

immediately implies a number of famous theorems that rely on the diagonal argument. For example, there can be no surjection $A \to \lbrace 0, 1\rbrace^A$ because the map $x \mapsto 1 - x$ has no fixed point in $\lbrace 0, 1\rbrace$ -- and that is Cantors' theorem.

It not easy to find non-trivial instances to which Lawvere's theorem applies. Indeed, if excluded middle holds, then having a surjection $e : A \to B^A$ implies that $B$ is the singleton. We should look for interesting instances in categories other than classical sets. In my paper I do so: I show that countably based $\omega$-cpos in the effective topos are countable and closed under countable products, which gives us a rich supply of objects $B$ such that there is a surjection $\mathbb{N} \to B^\mathbb{N}$.

Enjoy the paper!

### Runners in action

It has been almost a decade since Matija Pretnar and I posted the first blog posts about programming with algebraic effects and handlers and the programming language Eff. Since then handlers have become a well-known control mechanism in programming languages.

Handlers and monads excel at simulating effects, either in terms of other effects or as pure computations. For example, the familiar state monad implements mutable state with (pure) state-passing functions, and there are many more examples. But I have always felt that handlers and monads are not very good at explaining how a program interacts with its external environment and how it gets to perform real-world effects.

Danel Ahman and I have worked for a while on attacking the question on how to better model external resources and what programming constructs are appropriate for working with them. The time is right for us to show what we have done so far. The theoretical side of things is explained in our paper Runners in action, Danel implemented a Haskell library Haskell-Coop to go with the paper, and I implemented a programming language Coop.

### What is algebraic about algebraic effects?

Published as arXiv:1807.05923.

Abstract: This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra. We draw an uninterrupted line of thought between algebra and computational effects. We begin on the mathematical side of things, by reviewing the classic notions of universal algebra: signatures, algebraic theories, and their models. We then generalize and adapt the theory so that it applies to computational effects. In the last step we replace traditional mathematical notation with one that is closer to programming languages.

### Five stages of accepting constructive mathematics

In 2013 I gave a talk about constructive mathematics “Five stages of accepting constructive mathematics” (video) at the Institute for Advanced Study. I turned the talk into a paper, polished it up a bit, added things here and there, and finally it has now been published in the Bulletin of the American Mathematical Society. It is not quite a survey paper, but it is not very technical either. I hope you will enjoy reading it.

Free access to the paper:  Five stages of accepting constructive mathematics (PDF)

### A Brown-Palsberg self-interpreter for Gödel’s System T

In a paper accepted at POPL 2016 Matt Brown and Jens Palsberg constructed a self-interpreter for System $F_\omega$, a strongly normalizing typed $\lambda$-calculus. This came as a bit of a surprise as it is “common knowledge” that total programming languages do not have self-interpreters.

Thinking about what they did I realized that their conditions allow a self-interpreter for practically any total language expressive enough to encode numbers and pairs. In the PDF note accompanying this post I give such a self-interpreter for Gödel’s System T, the weakest such calculus. It is clear from the construction that I abused the definition given by Brown and Palsberg. Their self-interpreter has good structural properties which mine obviously lacks. So what we really need is a better definition of self-interpreters, one that captures the desired structural properties. Frank Pfenning and Peter Lee called such properties reflexivity, but only at an informal level. Can someone suggest a good definition?

### The troublesome reflection rule (TYPES 2015 slides)

Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is  taking place in Tallinn, Estonia – a very cool country in many senses (it’s not quite spring yet even though we’re in the second half of May, and it’s the country that gave us Skype).

### 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.

### The HoTT book

The HoTT book is finished!

Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.

### Programming with Algebraic Effects and Handlers

With Matija Pretnar.

Abstract: Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.

ArXiv version: arXiv:1203.1539v1 [cs.PL]

### On the Bourbaki-Witt Principle in Toposes

Abstract: The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.

ArXiv version: arXiv:1201.0340v1 [math.CT]

This paper is an extension of my previous paper on the Bourbaki-Witt and Knaster-Tarski fixed-point theorems in the effective topos (arXiv:0911.0068v1).

### Constructive gem: an injection from Baire space to natural numbers

I am not sure whether to call this one a constructive gem or stone. I suppose it is a matter of personal taste. I think it is a gem, albeit a very unusual one: there is a topos in which $\mathbb{N}^\mathbb{N}$ can be embedded into $\mathbb{N}$.

### Stone Duality for Skew Boolean Algebras with Intersections

With Karin Cvetko Vah.

For the last two months or so I got “distracted” by a topic which is not properly my core interest, namely non-commutative algebra. It was very strange at first, but now that I got used to non-commutative lattices (yes, there is such a thing) it’s kind of fun. Anyhow, Karin Cvetko Vah and I worked out Stone duality for skew Boolean algebras with intersections. Classical Stone duality tells us that Boolean algebras are dual to Stone spaces (zero-dimensional compact Hausdorff spaces), and that the generalized Boolean algebras (which are like Boolean algebras without a top element) are dual to Boolean spaces (zero-dimensional locally-compact Hausdorff spaces). Our skew version of duality says that right-handed skew Boolean algebras with intersections are dual to surjective etale maps between Boolean spaces. It is quite a mouthful to say “right-handed skew Boolean algebra with intersections”, let alone get used to it, but in a certain sense this is a very natural non-commutative structure. And we can get rid of the “right-handed” condition to obtain duality for “skew Boolean algebras with intersections”, as well as several other versions. We use the duality to construct a right-handed skew Boolean algebra with intersections which does not have a lattice section. It has been an open question whether such skew lattices exist.

arXiv: 1106.0425

Abstract: We extend Stone duality between generalized Boolean algebras and Boolean spaces, which are the zero-dimensional locally-compact Hausdorff spaces, to a non-commutative setting. We first show that the category of right-handed skew Boolean algebras with intersections is dual to the category of surjective étale maps between Boolean spaces. We then extend the duality to skew Boolean algebras with intersections, and consider several variations in which the morphisms are restricted. Finally, we use the duality to construct a right-handed skew Boolean algebra without a lattice section.

And now I can get back to homotopy type theory and Coq hacking.

### Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

Jens Blanck and I presented a paper at Computability and Complexity in Analysis 2009 with a complicated title (I like complicated titles):

Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions

which has been published in Volume 16, Issue 18 of the Journal of Universal Computer Science. I usually just post the abstract, but this time I would like to explain the general idea informally, the way one can do it on a blog. But first, here is the abstract:

Abstract: We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others.

### Metric Spaces in Synthetic Topology

With Davorin Lešnik.

Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces coincide if they do so for Baire space. In Russian Constructivism the match between synthetic and metric topology breaks down, as even a very simple complete totally bounded space fails to be compact, and its topology is strictly finer than the metric topology. In contrast, in Brouwer’s intuitionism synthetic and metric notions of topology and compactness agree.

### On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos

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.

### A constructive theory of domains suitable for implementation

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.

### Implementing real numbers with RZ

With Iztok Kavkler.

Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program speciï¬cations 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 speciï¬cation 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.

### RZ: a tool for bringing constructive and computable mathematics closer to programming practice

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.

### König’s Lemma and the Kleene Tree

For the benefit of the topology seminar audience at the math department of University of Ljubljana, I have written a self-contained explanation of the Kleene tree, which is an interesting object in computability theory. For the benefit of the rest of the planet, I am publishing it here.

### Realizability as the Connection between Computable and Constructive Mathematics

Lecture notes for my tutorial at Computability and Complexity in Analysis 2005, Kyoto. → continue reading (13 comments)

### The Dedekind Reals in Abstract Stone Duality

With Paul Taylor.

Abstract: Abstract Stone Duality (ASD) is an approach to topology that provides an abstract and conceptually satisfying account of topological spaces. The calculus of ASD reveals the computational content of various topological notions and suggests how to compute with them. The distinguishing feature of ASD is a direct axiomatisation in terms of spaces and maps, which does not rely on an underlying set-theoretic or topos-theoretic foundation.

This paper makes the first step in real analysis within ASD, namely the construction of the real line using two-sided Dedekind cuts. Compactness and overtness of the closed interval are proved, and the arithmetic operations are defined. The ASD calculus gives programs for computing the arithmetic operations and the quantifiers that express compactness and overtness.

As the paper aims to be a self-contained introduction to ASD for those interested in constructive and computable topology and analysis, it includes a rapid survey of the ASD calculus. The foundational background to the calculus was covered in detail in earlier work.

Further topics in real analysis within ASD, such as the Intermediate Value Theorem, are presented in a separate paper by Paul Taylor which builds on this one.

To be presented at Computability and Complexity in Analysis 2005, Kyoto, Japan.

### Blog as a repository for research papers

So I decided to put all my research papers on the blog. → continue reading

### First Steps in Synthetic Computability Theory (MFPS XXI)

Abstract: Computability theory, which investigates computable functions and computable sets, lies at the foundation of computer science. Its classical presentations usually involve a fair amount of Gödel encodings which sometime obscure ingenious arguments. 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 Gödel encodings, but rather use familiar concepts from set theory and topology.

Presented at: Mathematical Foundations of Programming Semantics XXI, Birmingham, 2004 (invited talk).

### Specifications via Realizability (CLASE 2005)

How to build specifications for abstract data types using realizability → continue reading

### Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability

With Alex Simpson.

Abstract: We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ZZ extends to a sequentially continuous function from X to RR. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact CSM. Both results rely on having careful constructive formulations of the concepts involved.

As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from X to RR are continuous”, when X is an inhabited CSM without isolated points, and when X is an inhabited locally non-compact CSM. One situation in which the latter case applies is in models based on “domain realizability”, in which the failure of the continuity principle for any inhabited locally non-compact CSM, X, generalizes a result previously obtained by Escardo and Streicher in the special case X = C[0,1].

As a second application, we show that, when the notion of inhabited complete separable metric space without isolated points is interpreted in a recursion-theoretic setting, then, for any such space X, there exists a Banach-Mazur computable function from X to the computable real numbers that is not Markov computable. This generalizes a result obtained by Hertling in the special case that X is the space of computable real numbers.

Published in: Mathematical Logic Quarterly, 50(4,5):351-369, 2004.

### Propositions as [Types]

With Steve Awodey.

Abstract: Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content, and formalizing a notion of proof irrelevance. Indeed, semantically, the notion of a support is sometimes used as surrogate proposition asserting inhabitation of an indexed family.

We give rules for bracket types in dependent type theory and provide complete semantics using regular categories. We show that dependent type theory with the unit type, strong extensional equality types, strong dependent sums, and bracket types is the internal type theory of regular categories, in the same way that the usual dependent type theory with dependent sums and products is the internal type theory of locally cartesian closed categories.

We also show how to interpret first-order logic in type theory with brackets, and we make use of the translation to compare type theory with logic. Specifically, we show that the propositions-as-types interpretation is complete with respect to a certain fragment of intuitionistic first-order logic. As a consequence, a modified double-negation translation into type theory (without bracket types) is complete for all of classical first-order logic.

Published in: Journal of Logic and Computation. Volume 14, Issue 4, August 2004, pp. 447-471.

### A Relationship between Equilogical Spaces and Type Two Effectivity

Abstract: In this paper I compare two well studied approaches to topological semantics—the domain-theoretic approach, exemplified by the category of countably based equilogical spaces, omegaEqu, and Type Two Effectivity, exemplified by the category of Baire space representations, Rep(B). These two categories are both locally cartesian closed extensions of countably based T_0-spaces. A natural question to ask is how they are related.

First, we show that Rep(B) is equivalent to a full coreflective subcategory of omegaEqu, consisting of the so-called 0-equilogical spaces. This establishes a pair of adjoint functors between Rep(B) and omegaEqu. The inclusion of Rep(B) in omegaEqu and its coreflection have many desirable properties, but they do not preserve exponentials in general. This means that the cartesian closed structures of Rep(B) and omegaEqu are essentially different. However, in a second comparison we show that Rep(B) and omegaEqu do share a common cartesian closed subcategory that contains all countably based T_0-spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based T_0-spaces. We consider several examples involving the natural numbers and the real numbers to demonstrate how these comparisons make it possible to transfer results from one setting to another.

Published in: Mathematical logic quarterly, 2002, vol. 48, suppl. 1, 1-15.

### Equilogical Spaces

With Lars Birkedal and Dana Scott.

Abstract: It is well known that one can build models of full higher-order dependent type theory (also called the calculus of constructions) using partial equivalence relations (PERs) and assemblies over a partial combinatory algebra (PCA). But the idea of categories of PERs and ERs (total equivalence relations) can be applied to other structures as well. In particular, we can easily define the category of ERs and equivalence-preserving continuous mappings over the standard category Top of topological T_0-spaces; we call these spaces (a topological space together with an ER) equilogical spaces and the resulting category Equ. We show that this category—in contradistinction to Top—is a cartesian closed category. The direct proof outlined here uses the equivalence of the category Equ to the category PEqu of PERs over algebraic lattices (a full subcategory of Top that is well known to be cartesian closed from domain theory). In another paper with Carboni and Rosolini (cited herein) a more abstract categorical generalization shows why many such categories are cartesian closed. The category Equ obviously contains Top as a full subcategory, and it naturally contains many other well known subcategories. In particular, we show why, as a consequence of work of Ershov, Berger, and others, the Kleene-Kreisel hierarchy of countable functionals of finite types can be naturally constructed in Equ from the natural numbers object N by repeated use in Equ of exponentiation and binary products. We also develop for Equ notions of modest sets (a category equivalent to Equ) and assemblies to explain why a model of dependent type theory is obtained. We make some comparisons of this model to other, known models.

Published in: Theoretical Computer Science, 315(1):35-59, 2004.

### Comparing Functional Paradigms for Exact Real-number Computation

With Alex Simpson and MartÃ­n EscardÃ³.

Abstract: We compare the definability of total functionals over the reals in two functional-programming approaches to exact real-number computation: the extensional approach, in which one has an abstract datatype of real numbers; and the intensional approach, in which one encodes real numbers using ordinary datatypes. We show that the type hierarchies coincide for second-order types, and we relate this fact to an analogous comparison of type hierarchies over the external and internal real numbers in Dana Scott’s category of equilogical spaces. We do not know whether similar coincidences hold at third-order types. However, we relate this question to a purely topological conjecture about the Kleene-Kreisel continuous functionals over the natural numbers. Finally, we demonstrate that, in the intensional approach to exact real-number computation, parallel primitives are not required for programming second-order total functionals over the reals.

Published in: In Proceedings ICALP 2002, Springer LNCS 2380, pp. 488-500, 2002.

### Sheaf Toposes for Realizability

with Steve Awodey.

Abstract: We compare realizability models over partial combinatory algebras by embedding them into sheaf toposes. We then use the machinery of Grothendieck toposes and geometric morphisms to study the relationship between realizability models over different partial combinatory algebras. This research is part of the Logic of Types and Computation project at Carnegie Mellon University under the direction of Dana Scott.

Sumitted for publication.

### The Realizability Approach to Computable Analysis and Topology

This is my Ph.D. dissertation, which I forgot to post on this blog. So I am doing it now. → continue reading

### Continuous Functionals of Dependent Types and Equilogical Spaces

with Lars Birkedal.

Abstract: We show that dependent sums and dependent products of continuous parametrizations on domains with dense, codense, and natural totalities agree with dependent sums and dependent products in equilogical spaces, and thus also in the realizability topos RT(P(NN)).

Published in: In Proceedings of Computer Science Logic 2000, Lecture Notes in Computer Science, Vol. 1862, Editors: P.G. Clote, H. Schwichtenberg, Springer, August 2000, pp. 202-216.

### Mixed multibasic and hypergeometric Gosper-type algorithms

with Marko Petkovšek.

Abstract: Gosper’s summation algorithm finds a hypergeometric closed form of an indefinite sum of hypergeometric terms, if such a closed form exists. We extend the algorithm to the case when the terms are simultaneously hypergeometric and multibasic hypergeometric. We also provide algorithms for finding polynomial as well as hypergeometric solutions to recurrences in the mixed case. We do not require the based to be transcedental, but only that q_1^(k_1) . . . q_m^(k_m) != 1 unless k_1 = … = k_m = 0. Finally, we generalize the concept of greatest factorial factorization to the mixed hypergeometric case.

Published in: Journal of Symbolic Computation, Vol. 28 (1999) 711-736.

### Analytica — An Experiment in Combining Theorem Proving and Symbolic Computation

with Edmund Clarke and Xudong Zhao.

Abstract: Analytica is an automatic theorem prover for theorems in elementary analysis. The prover is written in Mathematica language and runs in the Mathematica environment. The goal of the project is to use a powerful symbolic computation system to prove theorems that are beyond the scope of previous automatic theorem provers. The theorem prover is also able to deduce correctness of certain simplification steps that would otherwise not be performed. We describe the structure of Analytica and explain the main techniques that it uses to construct proofs. Analytica has been able to prove several non-trivial theorems. In this paper, we show how it can prove a series of lemmas that lead to Bernstein approximation theorem.

Published in: Journal of Automated Reasoning, Vol. 21, no.3 (1998) 295-325