CC-Seminar

Information on Lecture Notes of Satellite Seminar, CCA2005
(Jointly with CC-Seminar 2005-2)
Program and abstracts are available here
The lecture notes of the following speakers are available by the authors' courtesy
Yoshikawa
Bauer
Kohno
Escardo
Hertling
Mueller

Seminars and other events by JSPS Science Grant 2004-2006
Jointly by Kayamori Information Foundations Grant 2004-2005

Please contact: yasugi@cc.kyoto-su.ac.jp

CC-Seminar 2005-1 July

CC-Seminar　2004-1
Speakers: Professor Klaus Weihrauch, Professor Ulrich Kohlenbach
Date and Time: 21 November 2004; 12:30-15:30
Place: Meeting Room, 3F, Daisan Kenkyuushitutou, Kyoto Sangyo University, Kyoto

日時　１月２０日（金）　１０：３０→１６：００（予定）
場所　京都産業大学・第三研究室棟・会議室

午前　１０：３０→１２：００
講演：　吉川敦氏（九州大学）
Riesz-Frechet および Lax-Milgram の定理の計算可能性解析学版と その応用
　 アブストラクトは下にあります。

午後　１３：３０→１５：３０
アナログ計算可能性とディジタル計算可能性についての討論
吉川・河村両氏を中心に、既存の結果を整理する。

講演アブストラクト：
　Hilbert 空間の線形有界汎関数に関する Riesz-Frechet の表現定理及びその 非対称な
有界正値線形二次形式への拡張である Lax-Milgram の定理を計算可能なHilbert 空間の
枠内で述べ、応用として、簡単な楕円型微分方程式の解の計算可能性を論ずる。 このため、
入れ子になった Hilbert 空間対における計算可能性の遺伝を論じ、埋め込みが コンパクトな
場合は可ながら一般には不成立であることも示す（実用上はコンパクトな場合に 相当）。なお、
もともとの吉川のアプローチは古典的証明の実効化であったが Brattka との共 同でTTEで
記述してあり、それによって明晰になった部分も多い。

1 Colloquium talks, 2 CC-seminar, 3 Informal discussion

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, 15: Kyoto International Community House
December 16: Research Institute of Mathematical Sciences,
Kyoto University
Please note the change of the seminar site.

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:35-14:05 Oda
14:20-15:10 Hayashi
15:30-16:30 Aihara

Please contact directly if you plan to discuss individually in
Free discussion session.

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.