1 Colloquium Talks, 2 CC-Seminar, 3 Informal discussion

皆様のご参加をお待ちします。

連絡先：yasugi@cc.kyoto-su.ac.jp２月の行事

CC-Seminar in February

場所： 京都産業大学第三研究室棟３F会議室

２月１９日（水） 10:00-12:00

Informal Seminr by Vasco Brattka, FernUniversitaet-Hagen

on Computable Versions of the Uniform Boundedness Theorem

available at http://www.elsevier.nl/locate/entcs/volume66.html

The Uniform Boundedness Theorem states that any pointwise

bounded sequence of linear bounded operators on Banach spaces

is uniformly bounded. We discuss different computational

versions of this theorem.

２月２１日（金） 13:30-15:00

Seminar by Vasco Brattka, FernUniversitaet-Hagen

on The Computable Graph Theorem

The classical Graph Theorem in recursion theory states

that a total function on natural numbers is computable,

if and only if its graph is recursive. We discuss

generalizations of this result to different types of

computable metric spaces.

1. 談話会

日時： １２月１３日（金）2pm-4pm

場所：京都産業大学 第三研究室棟 ３F 会議室

テーマ：Apartness spaces as a foundation for constructive topology

講演者：Douglas Bridges (Introduction) and Luminita Simona Vita (Current topics)

Title: Separatedness in apartness spaces

Abstract:

Bridges: The theory of apartness, analogous to the classical theory of nearness

and proximity, appears to provide a good framework for topology in the

constructive (Bishop-style) setting. I will sketch thge foundations of

that theory in preparation for the talk by L.S. Vita that follows. My

opening remarks will deal with some general aspects of constructive

mathematics, for those not familiar with Bishop's approach.

Vita: We discuss three natural, classically equivalent,

Hausdorff separation
properties for apartness spaces

in constructive mathematics. Using
Brouwerian examples,

we show that our results are the best possible

in our constructive framework.

(If time permits I'll also talk about a new proof technique in constructive mathematics.)

2. CC-Seminar

１２月１４日、１５日： 京都市国際交流会館・第四会議室

１２月１６日：京都大学数理解析研究所 １１５号室

なお、１４、１５は、会場貸借規約の関係上、終了時間は厳守です。

December 14(Saturday) Kyoto International Community House

10:00-10:30 Mori

10:35-11:35 Kohlenbach

11:40-12:10 Tsujii and Yasugi

Lunch

13:30-14:00 Free discussion

14:00-15:00 Yamada

15:20-16:20 Simpson

16:20-16:30 Free discussion

December 15(Sunday)Kyoto International Community House

10:00-12:00 Free discussion

13:00-13:30 Yoshikawa

13:40-14:10 Oda

14:20-15:10 Hayashi

15:30-16:30 Aihara

December 16(Monday) RIMS, Kyoto University

(jointly with ALGI)

10:00-10:30 Akama

10:35-11:05 Ishihara

11:10-11:40 Takeuti

13:30-14:00 Tsuiki

14:10-14:40 Miyoshi

14:50-15:35 Vestergaard

15:45-16:30 Gabbay

Titles

*Aihara: Analog computation by chaotic neural networks

*Akama: Systems of Typed Limiting Computations.

*Gabbay: Fraenkel-Mostowski Semantics for Names and Binding

*Ishihara: Pointwise and Sequential Continuity in Constructive Analysis

*Kohlenbach: A logic-based approach to functional analysis
on convex metric spaces.

*Miyoshi: Mereotopology and Computation

*Mori: Toward an Effective Theory of Walsh-Fourier Series

*Oda: Search and Choice under uncertainty

*Simpson: Higher-type continuity

*Takeuti: Computable Structure and Effective Categoricity

*Tsuiki: Dimension of limits of algebraic domains

*Tsujii and Yasugi: Two notions of sequentially computable functions

*Vestergaard: Structural Induction and the lambda-Calculus

*Yamada: Topological Invariant of Knotted Graphs,and Other Topics

*Yoshikawa: On an ad hoc computability structure of a Hilbert space

Descriptions

*Akama:
The typed limiting computation will be analyzed with the help of

category theories to obtain a typed semi-formal system. Then we will

discuss the concerning problems. We will be led to Howard's typed

lambda-calculus of limiting recursor, and will discuss the upper bound

of ordinal numbers Coquand inductively defined. This talk is based on

on-going work with Susumu Hayashi and Ken-etsu Fujita.

*Gabbay:We often want to reason about systems with names and binding, for

example about syntax such as that of the lambda- or pi-calculus. Yet we

encounter apparently technical difficulties doing so because of problems with

names and binding such as accidental variable capture, or clash of bound

variable names.

The usual solution is to prove lemmas allowing us to rename up to

alpha-equivalence. However, this is no help when we come to the next piece of

work, nor if we need meta-theories such as logics and programming languages

for syntax with names and binding.

Fraenkel-Mostowski techniques observe that these lemmas are all consequences

of a general (first-order) semantic theory of names and binding. Once we

understand this theory, we can appeal to it in order to obtain the required

lemmas "for free", and we can use the semantics to design general programming

and logical tools.

*Ishihara: We will discuss the relationship between pointwise and sequential

continuity in Bishop's constructive mathematics.

*Kohlenbach: The first part of the talk gives a survey on how a monotone version

of Goedel's functional interpretation combined with negative

translation (MFI) can be used to extract quantitative information from

ineffective proofs in numerical functional analysis. We will argue

that MFI provides in many cases the right form of "numerical implication".

In the second part we present recent results (together with

Laurentiu Leustean) obtained by applying

MFI in the area of metric fixed point theory. We will work in

W. Takahashi's setting of convex metric spaces (with additional

properties). Our results not only provide new effective bounds but

even yield systematically new qualitative results concerning the

independence from parameters in metrically bounded spaces (without

any compactness assumption) which in only in special cases had been

obtained by functional analytic methods before.

We finish the talk by presenting a new general meta-theorem which

allows to infer such independence results "a-priori" if certain easy

to check logical conditions are met. Various well-known theorems in

fixed point theory are immediate corollaries of that meta-theorem.

*Simpson: Continuity provides an elegant mathematical abstraction of computability,

modelling the finitary aspects of computation without reference to any

notion of algorithm. In this talk, I shall compare several different

definitions of higher-type continuity and argue for the thesis that,

for spaces of computational interest, there is one canonical notion

of higher-type continuity beneath them all.

*Takeuti: Hertling defined the notion of effective categoricity and

showed that the structure of real number with effective

convergence is effectively categorical (MLQ 45-2, '99). He

defined the notion with the words of representation.

This talk will show another equivalent definition of

effective categoricity with the words of computable

structure. The aim of this work is to compare the two

methods of computable analysis; one is that by

representation and the other is by computable structure.

*Tsuiki: We show that when D is a Coherent algebraic domain,

the dimension of L(D), the set of limits of D, and

the height of L(D) are equal. As a consequence,

a condition on D for the domain representability

of a space X in L(D) is given.

*Tsujii and Yasugi: Two approaches to the computability

problem of "somewhere discontinuous" functions,

that of the uniform space and that of the limiting computation,

are discussed, and their equivalence is proved.

*Vestergaard: We consider formal provability with
structural induction and related

proof principles in the lambda-calculus presented with first-order

abstract syntax over one-sorted variable names. Surprisingly, informal

practice is shown to be a subset of the formal requirements by way of

a general proof methodology that we introduce. The results we establish

range from the relative renaming-freeness of residual theory over

decidability of alpha-equivalence to beta-standardisation.

*Yoshikawa: The main subject of this talk is to construct

a orthonormal system (in a Hilbert space) based on an ad hoc

computability structure.

3. Informal discussion with Kohlenbach

December 17(Tuesday) Kyoto Sangyo University (Yasugi's office)

10:30-15:00(?)

(Sakamoto, Yamazaki)

Last modified: Tue Feb 18 23:06:28 JST 2003