プログラム (ALGI2002)
***12月16日（CC-Seminar）***
10:00-10:30 講演者 赤間陽二（東北大学） 題目 Systems of Typed Limiting Computations 概要 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. 10:35-11:05 講演者 石原哉（北陸先端大学院大学） 題目 Pointwise and Sequential Continuity in Constructive Analysis 概要 We will discuss the relationship between pointwise and sequential continuity in Bishop's constructive mathematics. 11:10-11:40 講演者 竹内泉（東邦大学） 題目 Computable Structure and Effective Categoricity 概要 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. 13:30-14:00 講演者 立木秀樹（京都大学） 題目 Dimension of limits of algebraic domains 概要 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. 14:10-14:40 講演者 三好博之（京都産業大学） 題目 Mereotopology and Computation 概要 14:50-15:35 講演者 Rene Vestergaard (JAIST) 題目 Structural Induction and the lambda-Calculus 概要 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. 15:45-16:30 講演者 Jamie Gabbay (ケンブリッジ大学) 題目 Fraenkel-Mostowski Semantics for Names and Binding 概要 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. *** 12月17日 *** 9:45-10:45 講演者 大崎人士（産総研） 題目 Equational Tree Automata: Towards Automated Verification of Network Protocols (I) 概要 Equational tree automata provide a powerful tree language framework that manipulates the congruence closures of tree languages. In the first part of this talk I will summarize the closure properties and decidability results on the extended tree automata. In particular, I will show the (intersection-)emptiness problem for AC-tree automata, which was open in my previous work, is decidable, by the straightforward reduction to the reachability problem for ground AC-term rewriting. The newly obtained results generalize decidability of so-called reachable property problem [Mayr & Rusinowitch, 1999]. In the second part, we discuss the usefulness of this tree automata theory. To be precise, I will explain how equational tree automata can be applied to equational unification problems. We then demonstrate how the network security problem, such as for Diffie-Hellman key exchange algorithm, can be dealt with the equational tree automata theory. This tutorial talk is basically the same talk of ones at RTA 2002 and UNIF2002 in Copenhagen. 11:00-12:00 講演者 大崎人士（産総研） 題目 Equational Tree Automata: Towards Automated Verification of Network Protocols (II) 概要 (I)の続き 13:30-14:30 講演者 Alex Simpson（エディンバラ大学） 題目 What is a category of domains? 概要 Domain theory is usually taken to be the study of complete partial orders, possibly satisfying additional properties (continuity, algebraicity, etc.). However, there are other types of mathematical structure equally suited to modelling computation. Such structures form categories sharing many properties in common with the more familiar categories of domains. In this talk, I shall describe several examples of such structures, and I shall give a survey of work done in the 1990s on "axiomatic domain theory", which studied the characteristic properties of categories of domains in general. 14:45-16:15 講演者 下嶋篤（北陸先端大学院大学） 題目 Channel theory as a philosophical experiment 概要 In this short tutorial, I will introduce basic concepts of channel theory (Barwise and Seligman 1997), with an emphasis on philosophical motivations behind them. Specifically, we will see how the theory has been designed to give a general, naturalistic theory of information and thereby that of "representations", where the term broadly refers to symbols, pictures, and physical models in everyday life, as well as such abstract objects as mathematical models. ******************************************************* * 懇親会 * * １７日（火曜日）１８：００～ * * 「天' (みそら)」（京大農学部前、会場から徒歩３分） * * 電話 (075)771-1239 * ******************************************************* *** 12月18日 *** 9:45-10:45 講演者 永山操（東京女子大学） 題目 Ludics and proof-nets (Part I) 概要 11:00-12:00 講演者 永山操（東京女子大学） 題目 Ludics and proof-nets (Part II) 概要 13:30-14:00 講演者 本多和正（九州大学） 題目 関係データベースにおける従属性検証と反例の自動生成 概要 W.MacCaullによる従属性証明系は健全かつ完全な証明系ではあるが、 自動証明を行わせると非常に時間がかかる。 そこで、自動証明に向くように各規則を変更すると 短時間で問題を解くことができるようになったが、 系の完全性が崩れ、正しい解答が得られなくなった。 しかし、この系は反例の候補を抽出していると見ることもできる。 そこで、本研究ではそれらの候補が本当に反例となるかを 検証することで失われた完全性を補なうことを考える。 14:00-14:30 講演者 大隈ひとみ （九州大学） 題目 Demonic orders and quasi-totality in Dedekind categories （joint work with Yasuo Kawahara) 概要 Relation algebras are suitable for describing semantics of relational programming. In particular demonic composition and demonic orderings will be useful for designing nondeterministic programs. We give definitions of two refinement orderings using quasi-total relations, and provide existence conditions of the supremum and values of supremum and infimum of a set of relations with respect to both refinement orderings. Finally we prove that the demonic composition is monotonic on these orderings, respectively. 14:45-15:15 講演者 澤田康秀（京都大学） 題目 型付きλ計算体系λεへの部分型の導入 概要 佐藤、桜井、Burstallによって提案された型付きλ計算の体系“λε”は、 明示的環境を扱う計算体系であり、レコード計算と類似した構造をもつ。 よって、レコード計算と同じく部分型による拡張が可能であると考えられた。 しかし部分型をもつ環境計算では、環境が束縛する変数の名前の衝突が 問題となる。本研究では、coercionをうまく利用することで この問題の解決を図っている。 15:30-16:30 講演者 板谷聡子（ATR) 題目 A study on an immune network dynamical system model 概要 First, we summarize the immune system of humans, the theory of immune networks and various existing models. Moreover, we introduce examples of application of immune networks theorys to other fields, and describe the aims of our study. Next, we investigate the possible steady states in an idiotype network model introduced by Varela et. al. and in two modified models. In all these three models, both chaotic and periodic states exist. Next, we investigate the response of the model immune systems to invasion by antigens. It is found that compared to periodic states, the response time in a chaotic state shows less dependence on antigen type. Moreover, we show that the introduction of thresholds in the immune system model enhances the stability of the network and results in localization of the immune response. Finally, we study connectivity of networks. We found that in the case that a network has fixed strength of connectivity, local coupling results in oscillatory behavior which could be advantageous for dynamic coupling in the network. Further, we find that a system with mutation results in formation of sub-networks, which could be advantageous for stability. *** 12月19日 *** 9:45-10:15 講演者 長谷川真人（京都大学） 題目 Coherence of the Double Involution on *-Autonomous Categories (joint work with R. Cockett and R.A.G. Seely) 概要 10:30-12:00 講演者 菊池誠（神戸大学） 題目 An Introduction to Abstract Design Theory 概要 Design is one of the most important activities of human reasoning, which is not easy to deal with mathematically. Abstract Design Theory is a mathematical framework for the analysis of design proposed by Kakuda in 1999. The basic idea of the theory is that design in an activity of producing information flow between the realm of our consciousness and the real world. In part, the theory is an application of Channel Theory, a mathematical theory of information flow invented by Barwise and Seligman. The philosophy of Yoshikawa's General Design Theory, in which design is discussed in terms of two topologies defined by functions and attributes of artifacts, plays an important role for the developments of the theory, and some of the arguments in General Design Theory have been justified mathematically by Abstract Design Theory. This talk is an introduction to Abstract Design Theory in which the motivations and the basic part of the mathematical machinery will be presented. It includes also a brief review of Channel Theory and General Design Theory and no background is assumed. 13:30-14:30 講演者 Alex Simpson（エディンバラ大学） 題目 A convenient category of topological domains 概要 In this talk, I'll begin by setting out a list of desirable properties that an ideal category of domains, convenient for applications in the semantics of computation, should possess. No existing category of domains satisfies all the conditions identified. To remedy this, I shall propose a new category of domains, consisting of certain simple topological spaces, that does promise to fulfill all of the requirements. This is work in progress. 14:45-15:15 講演者 松岡聡（産総研） 題目 Exponential-Free Typed Boehm Theorem (part II) 概要 In this talk I discuss typed Boehm theorem on the intuitionistic implicational multiplicative additive fragment of Linear Logic. In the previous ALGI workshop, I only discussed the fragment without additives although type instantiations and contexts include additives. 15:15-15:45 講演者 長谷川立（東京大学） 題目 T.B.A. 16:00-16:30 講演者 白旗優（慶応義塾大学） 題目 Review of "Geometry of Interaction and linear combinatory algebras" 概要 I would like to review S. Abramsky, E. Haghverd and P. Scott, "Geometry of Interaction and linear combinatory algebras", (MSCS, October 2002) which utilizes traced monoidal categories to give an axiomatic framework for Geometry of Interaction. I hope to have a vigorous discussion on this issue with the audience. *** 12月20日 *** 講演申し込みがあれば何かします。 それから、ALGIの一部と言う訳ではないですが、 Alex Simpson さんと長谷川真人さんが日頃行って おります連続セミナー 「Interpreting Set Theory in Toposes」 第５回が11時から12時まで４０２号室で行われる 予定になっております。興味があるかたはどうぞ。
メールでの申し込み〆切 １２月１４日午後１時
ALGI開催中に何か話したくなった人は長谷川真人か古澤仁まで申し出て下さい。