Andrej Bauer
   selected papers and notes
 "Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability ",
  with Alex Simpson

December 19, 2003

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 Z extends to a sequentially continuous function from X to R. 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 R 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.

[postscript letter] [postscript A4] [PDF letter] [PDF A4]

 "Propositions as [Types]",
  with Steven Awodey, technical report

June 11, 2001

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.

Technical report at Institut Mittag-Leffler

[postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF] [PDF A4] [DVI]

  "A Relationship between Equilogical Spaces and Type Two Effectivity"

April 10, 2001

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, wEqu, 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 T0-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 wEqu, consisting of the so-called 0-equilogical spaces. This establishes a pair of adjoint functors between Rep(B) and wEqu. The inclusion Rep(BB) --> wEqu 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 wEqu are essentially different. However, in a second comparison we show that Rep(B) and wEqu do share a common cartesian closed subcategory that contains all countably based T0-spaces. Therefore, the domain-theoretic approach and TTE yield equivalent topological semantics of computation for all higher-order types over countably based T0-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.

To appear at MFPS XVII.

[postscript] [gzip postscript] [PDF]

 "Sheaf Toposes for Realizability",
  with Steven Awodey, preprint

April 10, 2001

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.

Preprint at Philosophy Department, CMU

[postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF]

 "Continuous Functionals of Dependent Types and Equilogical Spaces",
 with Lars Birkedal

May 18, 2000

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(N)).

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

[postscript] [gzip postscript] [postscript A4] [gzip postscript A4] [PDF]

 "Mixed multibasic and hypergeometric Gosper-type algorithms",
 with Marko Petkovsek

August, 1997

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 polunomial as well as hypergeometric solutions to recurrences in the mixed case. We do not require the based to be transcedental, butonly that q1k1 . . . qmkm != 1 unless k1 = ... = km = 0. Finally, we generalize the concept of greatest factorial factorization to the mixed hypergeometric case.

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

[postscript] [gzip postscript]

 "Analytica --- An Experiment in Combining Theorem Proving and Symbolic Computation",
 with Edmund Clarke and Xudong Zhao

August, 1997

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.

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

[postscript] [gzip postscript]