With Chris Stone.
We present a system, called RZ, for automatic generation of program specifications from mathematical theories. We translate mathematical theories to specifications by computing their realizability interpretations in the ML language augmented with assertions (as comments). While the system is best suited for descriptions of those data structures that can be easily described in mathematical language (e.g., finitely presented groups, real arithmetic, graphs, etc.), it also elucidates the relationship between data structures and constructive mathematics.
Constructive Logic for Automated Software Engineering (CLASE), Satellite event of ETAPS 2005, Edinburgh, 9th April 2005
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.
Download: continuity.pdf, continuity.ps.gz
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.
Download: bracket_types.pdf, bracket_types.ps.gz
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, `omega`Equ, 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 `omega`Equ, consisting of the so-called `0`-equilogical spaces. This establishes a pair of adjoint functors between Rep(B) and `omega`Equ. The inclusion of Rep(B) in `omega`Equ 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 `omega`Equ are essentially different. However, in a second comparison we show that Rep(B) and `omega`Equ 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.
Download: equtte.pdf, equtte.ps.gz
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.
Download: equ.pdf, equ.ps.gz.
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.
Download: paradigms.pdf, paradigms.ps.gz, paradigms_proofs.ps.gz (long version, with proofs)
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.
Download: sheaves_realizability.pdf, sheaves_realizability.ps.gz
Ph.D. dissertation. Available as CMU technical report CMU-CS-00-164.
Advisor: Dana S. Scott
School of Computer Science
Carnegie Mellon University
In this dissertation, I explore aspects of computable analysis and topology in the framework of relative realizability. The computational models are partial combinatory algebras with subalgebras of computable elements, out of which categories of modest sets are constructed. The internal logic of these categories is suitable for developing a theory of computable analysis and topology, because it is equipped with a computability predicate and it supports many constructions needed in topology and analysis. In addition, a number of previously studied approaches to computable topology and analysis are special cases of the general theory of modest sets.
In the first part of the dissertation, I present categories of modest sets and axiomatize their internal logic, including the computability predicate. The logic is a predicative intuitionistic first-order logic with dependent types, subsets, quotients, inductive and coinductive types.
The second part of the dissertation investigates examples of categories of modest sets. I focus on equilogical spaces, and their relationship with domain theory and Type Two Effectivity (TTE). I show that domains with totality embed in equilogical spaces, and that the embedding preserves both simple and dependent types. I relate equilogical spaces and TTE in three ways: there is an applicative retraction between them, they share a common cartesian closed subcategory that contains all countably based T0-spaces, and they are related by a logical transfer principle. These connections explain why domain theory and TTE agree so well.
In the last part of the dissertation, I demonstrate how to develop computable analysis and topology in the logic of modest sets. The theorems and constructions performed in this logic apply to all categories of modest sets. Furthermore, by working in the internal logic, rather than directly with specific examples of modest sets, we argue abstractly and conceptually about computability in analysis and topology, avoiding the unpleasant details of the underlying computational models, such as GÃ¶del encodings and representations by sequences.
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.
Download: dependent_functionals.pdf, dependent_functionals.ps.gz
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.
Download: gengosper.pdf, gengosper.ps.gz