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.
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.)
なお、１４、１５は、会場貸借規約の関係上、終了時間は厳守です。
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.
