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]