|
|
 |
|
Vendredi 20 Février
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Coherence spaces for computable analysis |
| Description: |
Kazushige Terui Abstract:
There have been two mainstream approaches in
computable analysis: the type-two theory of effectivity (TTE)
and the theory of domain representations. This paper proposes
an intermediary approach based on coherence spaces, which is
as concrete as TTE and as structured as domain theory.
We import various concepts from TTE such as admissibility,
and provide admissible representations for the real line, Euclidean
spaces and function spaces over them. This allows us
to represent, for instance, a real continuous function by a stable
map. A natural question is then what linear maps correspond
to in terms of analysis. Our answer is that they correspond
to uniformly continuous functions. This leads to an internal
expression of Heine's theorem (every continuous function on a
compact interval of the real line is uniformly continuous) as the
existence of a certain map from a stable function space to a linear
function space.
We finally illustrate an application of coherence spaces as a
type system for lambda calculus, which allows us to verify local
properties of real functions.
This is a joint work with Kei Matsumoto. |
|
|
