(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

Jointly by Kayamori Information Foundations Grant 2004-2005

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

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

CC-Seminar 05-4

日時 １月２０日（金） １０：３０→１６：００（予定）

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

午前 １０：３０→１２：００

講演： 吉川敦氏（九州大学）

Riesz-Frechet および Lax-Milgram の定理の計算可能性解析学版と
その応用

アブストラクトは下にあります。

午後 １３：３０→１５：３０

アナログ計算可能性とディジタル計算可能性についての討論

吉川・河村両氏を中心に、既存の結果を整理する。

講演アブストラクト：

Hilbert 空間の線形有界汎関数に関する Riesz-Frechet の表現定理及びその
非対称な

有界正値線形二次形式への拡張である Lax-Milgram の定理を計算可能なHilbert
空間の

枠内で述べ、応用として、簡単な楕円型微分方程式の解の計算可能性を論ずる。
このため、

入れ子になった Hilbert 空間対における計算可能性の遺伝を論じ、埋め込みが
コンパクトな

場合は可ながら一般には不成立であることも示す（実用上はコンパクトな場合に
相当）。なお、

もともとの吉川のアプローチは古典的証明の実効化であったが Brattka との共
同でTTEで

記述してあり、それによって明晰になった部分も多い。

Seminars and other events by Science Grant 2002

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

1 Colloquium Talks

December 13 (Friday) 2pm-4pm

Kyoto Sangyo University, DaisanKenkyushitutou 3F Meeting Room

Subject: Apartness spaces as a foundation for constructive topology

Speakers: 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, 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.

3 Informal discussion with Kohlenbach

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

10:30-15:00(?)

(Sakamoto, Yamazaki)

Last modified: Sat Jan 14 21:19:43 JST 2006