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