November 1, 2003

There are several generalizations of topological spaces which are "imaginary" in the sense of Martin Escardo. It is known for general reasons (see G. Rosolini "Equilogical spaces and filter spaces", Rend. Circ. Mat. Palermo, 64, 2000) that equilogical spaces are such an example. In this talk we give a direct and elementary proof of the fact that equilogical spaces satisfy Escardo's requirements for "generalized spaces".

[Slides]

November 2, 2003

In Rosolini's synthetic approach to computation via dominances, Escardo's synthetic topology and Taylor's abstract Stone duality many interesting theorems in topology are proved by clever use of lambda calculus and certain lattice-theoretic properties of the Sierpinski space Sigma. As long as we carefully only argue constructively, all the results can then be interpreted in a recursion-theoretic universe, such as the effective topos. In this way we obtain results of computable topology. But, we can also turn things around and obtain what one might call "topological computability": namely, from one additional axiom for Sigma, namely that the set Sigma^N is countable, we derive basic recursion theoretic results, e.g. Church's thesis, in a purely abstract fashion -- without explicit mention of Turing machines or other recursion-theoretic equipment.

Slides: [Postscript]

October 31, 2003

Much work has been done on extraction of programs from proofs. A less ambitious, but possibly equally rewarding, endeavor is extraction of abstract data types from axiomatizations of first-order theories. We use a realizability interpretation of an (intuitionistic) first-order theory to translate an axiomatization of a mathematical structure to a definition of an abstract data type which implements it. In addition, the interpretation gives us a set of negative formulas which express criteria that a concrete implementation of the abstract data type must satisfy, if it is to be a correct implementation of the original first-order theory. The fact that the correctness criteria are expressed as negative formulas is desirable, because their classical reading is the same as their intuitionistic reading. One practical benefit of this is that also programmers who are not familiar with intuitionistic logic will correctly understand correctness.

Slides: [Postscript]

August 28, 2003

We give a constructive proof of two embedding and extension theorems. The first one states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function f from Cantor space to Z extends to a sequentially continuous function F from X to R. In addition, if f is pointwise continuous then so is F. The second result shows an analogous property of Baire space relative to any inhabited locally non-compact complete separable metric space.

We give two applications of this result. First, we show that, in the presence of certain choice and continuity principles, the statement "all functions from X to R is continuous" is false. This generalizes a result previously obtained by Escardo and Streicher, in the context of "domain realizability", for the special case X = C[0,1]. Second, 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 of Hertling for the special case that X is the space of computable real numbers.

Slides: [Postscript] [PDF] [printer-friendly Postscript]

March 25, 2002

A reflexive domain is one that contains its own continuous function space as a retract. Reflexive domains are models of the untyped lambda calculus, and from them we build categories of partial equivalence relations, also known as PER models. The results presented in this talk were motivated by the question how many PER models on reflexive Scott domains there are, up to equivalence of categories.

We first discuss the notion of "n-coherent" domains, a straightforward generalization of Plotkin's definition of coherently complete domains, and the related notion of a "coherence number" of a domain.

Using results about the existence of universal n-coherent domains, we prove several domain theoretic results about reflexive domains. One such result is that a domain D is reflexive if, and only if, the product D x D is a retract of D. We also show that there are only countably many PER models on reflexive Scott domains, one for each coherence number between 1 and aleph null.

Slides: [Postscript] [PDF] [printer-friendly Postscript]

February 21, 2002

Classical branches of mathematics, such as geometry, real analysis and differential calculus, were developed well before the rise of modern computer science. They have little to say about questions that computer scientists might ask; for example, what are good data structures for representing real numbers, differentiable maps, probability distributions, and other classical mathematical objects.

One way to deal with these questions is offered by realizability theory, where we build an entire mathematical universe on top of a computational model, for example RAM machines or a programming language. In such a custom-made mathematical world every mathematical construction is automatically equipped with an implementation in the underlying computational model. The development of a computation-sensitive mathematics can then proceed at an abstract and conceptual level, with a clear idea of what it means to correctly implement a given mathematical objects.

In the new world, not everything is the same as in classical mathematics. Not all classical axioms are valid anymore, and some classically invalid axioms are validated. These changes influence the properties of well known mathematical objects, such as the real numbers. A computationally minded person will admit, however, that the new world is better than the old one.

Talk: [Windows Media] [low bandwidth]
Slides: [Postscript] [PDF] [printer-friendly Postscript]

5. marec, 2002

Klasične veje matematike, kot so geometrija, analiza in diferencialni račun, so mnogo starejše od računalniške znanosti. Zato ni presenteljivo, da ne ponujajo odgovorov na vprašanja, ki zanimajo računalničarje; na primer, kakšne podatkovne strukture so primerne za predstavitev realnih števil, diferenciabilnih preslikav, verjetnostnih porazredlitev in ostalih klasičnih matematičnih struktur.

Teorija realizabilnosti ponuja en možen odgovor na ta vprašanja: celoten matematični svet zgradimo še enkrat in ga zasnujemo na računskem modelu kot je na primer programski jezik ali na stroj z RAM pomnilnikom. V tako prikrojenem matematičnem svetu je vsaka matematična konstrukcija avtomatično opremljena z ustrezno računalniško implementacijo. Računalniško zavestno matematiko lahko tako razvijemo povsem abstraktno, hkrati pa imamo na voljo matematična orodja, s katerimi zagotovimo pravilnost implementacije matematičnih struktur.

V novem matematičnem svetu ni vse tako kot v klasičnem. Nekateri klasični aksiomi so neveljavni, drugi neklasični aksiomi pa so veljavni. Te spremembe vplivajo na lastnosti osnovnih matematičnih objektov, kot so na primer realna števila. Vendar pa se bodo vsi, ki razmišljajo računsko, strinjali, da je novi svet boljši od starega.

Talk: [RealPlay]
Slides: [Postscript] [PDF] [printer-friendly Postscript]