Uppsala, Torsdag den 11 oktober

All talks will be given in room Å2002, Ångströmlaboratoriet.

9.00 - 10.00 Dag Normann, University of Oslo
External and internal density theorems for limitspace-interpretations of some types

10.00 - 10.30 Coffee

10.30 - 11.30 Ulrich Berger, Swansea University
A domain-theoretic characterisation of strong normalisation

11.40 - 12.40 Peter Hertling, Universität der Bundeswehr München
Computability and Non-Computability Results for the Topological Entropy of Shift Spaces

12.40 - 14.15 Lunch

14.15 - 15.15 Warwick Tucker, University of Bergen
Auto-validating numerical methods

15.25 - 16.25 Jens Blanck, Swansea University
Computably stable algebras

16.25 - 16.45 Coffee

16.45 - 17.45 John V Tucker, Swansea University
Computability: algorithmic procedures versus experimental procedures


Dag Normann: Traditional density theorems often have the format that the total objects in some domain form a dense subset of the domain in question, while classical applications of density theorems, like Kreisel's Representation Theorem, can be carried out without reference to the underlying domains or other external structures. In this talk, we will first discuss limitations to possible traditional density theorems for domains representing spaces of continuous functions from one separable metric space to another. Then we will see how we may construct dense countable subsets of some types interpreted in the category of Kuratowski Limit Spaces. The talk will be a report on ongoing research.

Ulrich Berger: We present a domain-theoretic model for the untyped lambda-calculus with pattern matching and term rewriting with the property that a term is strongly normalising if and only if its value is not bottom.

Peter Hertling: The topological entropy, a numerical quantity assigned to a continuous function from a compact space to itself, is invariant under topological conjugacy and serves as a tool for classifying dynamical systems. Therefore, computing the topological entropy is an important problem in dynamical systems theory. We discuss several recent positive and negative results concerning the computability of the topological entropy of shift dynamical systems.

Warwick Tucker: We will present a modern class of numerical methods, based on set-valued computations. Such methods allow for a sought quantity to be enclosed rather than approximated in the traditional sense. Done correctly, this approach provides rigorous error bounds for all intermediate calculations, which can be used adaptively within the numerical method. The end product is a mathematically correct statement, often in terms of verified inequalities.

Despite the underlying theory being known since the sixties, it is only now that these methods are gaining a wider use - both within academia and industry. Set-valued computations appear to have most impact for non-linear global problems of reasonable size. We will present concrete examples where these methods work well, and end by discussing computational environments that support the underlying mathematics.

John V Tucker: In this lecture I will survey some old and new results that try to answer these questions:
1. What are the functions computable by experimental procedures applied to different physical systems?
2. How do they compare with the functions computable by algorithms?
3. Do there exist physical systems that exhibit behaviour not algorithmically computable?
4. What are the physical limits to computation?