program

************************************************** * 第九回 ALGI（代数，論理，幾何と情報科学研究集会） * ************************************************** 第九回は JAMS 年会の分科会として，大阪府立大学にて開催します．(交通案内) 日程は以下の通りになっています. ８/２９ １４時から１７時まで ８/３０ ９時３０分から１２時まで それから、今回のJAMSの例会では八杉先生の部会でSelahの講演が８月３０日の 午後１時から予定されております。興味がある方はどうぞ． PROGRAM Aug. 29 14:00 -- 14:35 連続体の、拡張された文字列集合への埋め込みについて 立木 秀樹 京都大学総合人間学部 14:35 -- 15:10 パラメータ付きモジュールの意味について 木下 佳樹　 電総研意味論グループ 15:25 -- 16:00 Relevance Principle for Substructural Logics with Mingle and Strong Negation. 上出　哲広　 和歌山工業高等専門学校、電気工学科 16:00 -- 16:35 Crispness and Representation of Dedekind Categories 河原 康雄 九州大学大学院システム情報科学研究院 講演終了後 懇親会 (詳しい事はまだ決まっていません。 何かリクエストがありましたら、古澤まで。) Aug. 30 9:30 -- 10:05 新たなcountable functionalの構成法 (A new construction of countable functionals) 坂本 伸幸 東北大学大学院理学研究科数学専攻 10:05 -- 10:40 型理論による圏論ぽい話 竹内 泉 京都大学情報工学 10:50 -- 11:25 実効的縮小写像定理 鴨 浩靖 奈良女子大学理学部 11:25 -- 12:00 Nobuko Yoshida (joint work with Matthew Hennessy) Assigning Types to Processes University of Leicester ABSTRACTS 題： 連続体の、拡張された文字列集合への埋め込みについて 講演者： 立木秀樹 概要： 通常の無限文字列集合ではなく、ボトム（不定元）を１つ含む文字列集合を 考えれば、そこに実数の集合を位相的に埋め込むことができること、ボトム を１つ含む文字列集合を入出力するチューリングマシンを考えれば、それが 通常の計算概念を実数の上に導くことを以前示した。この発表では、同じ様に して、実数集合以外の連続な位相空間に計算概念を導入できるかどうか考察す る。次元を考察することにより、n 次元ユークリッド空間はボトム（不定元） を n 個含む文字列集合に埋め込めるが、n-1 個では不可能なことなどを示す。 題：　パラメータ付きモジュールの意味について 講演者：　木下佳樹 概要： We give a semantics of parameterised modules in the framework of functorial semantics. Two mathematical tools are introduced first. One is the Cartesian closed sketch, which enables a functorial semantics of simply typed lambda calculi. Another is Power and Robinson's recent formulation of observational equivalence. We then apply these tools to give a semantics of parameterised modules. In particular, we formulate the correctness of program modules up to observational equivalence. 題：　Relevance Principle for Substructural Logics with Mingle and Strong Negation. 講演者：　上出　哲広 概要：　 We introduce intuitionistic and classical (propositional) substructural logics with structural rules mingle and connective strong negation, and investigate the cut-elimination property and the relevance principle (the variable sharing property) for the logics. The relevance principle does not hold for substructural logics with mingle and usual negation, but holds for that with mingle and strong negation. For example, the principle does not hold for the linear logic MALL+MIX (without the propositional constants), but holds for modified MALL+MIX with strong negation instead of usual one (without the propositional constants).　Moreover we mention Maksimova's principle and paraconsistency for some logics. 題：Crispness and Representation of Dedekind Categories 講演者： 河原 康雄 概要： Dedekind 圏は Goguen の L-関係の圏を抽象化したものである。 しかし、すべての Dedekind 圏はL-関係の圏に埋め込めない。 そこで、どのような条件を追加したら埋め込めるのかという表現 可能性の問題がでてくる。古澤・河原はファジイ関係に関連して、 ある条件を満たすDedekind 圏において、異なる2点を分離する ための scalar crisp 性という概念を導入して表現定理を示した。 しかし、Winter により一般のDedekind 圏では crispness を表現 する formula がないことが証明された。さらに、Winter はcrisp 性 を表現する新しい演算 cut operator を考察し、その基本的な性質 を議論した。 本講演では、Winter の crisp 性のための cut operator をやや 改良して、(cut operatorに依存する)点公理を満たす一様な Dedekind圏の表現定理を示す。 題： 新たなcountable functionalの構成法 (A new construction of countable functionals) 講演者： 坂本 伸幸 概要： 従来の Kleene の関数適用 f|g より直感的に理解しやすい関数適用 f`g を定義し,この関数適用を用いても countable functional を定義できることを 示す.また,この関数適用を用いて type-free theory APP のモデルを構成できる ことも示される. 題： 型理論による圏論ぽい話 講演者： 竹内 泉 概要： 　パラメトリシティーの性質は、多相型の計算体系の意味論的な性 質である。多相型の計算体系には、例えばジラールの体系Ｆがある。 パラメトリシティーの性質の許では、体系Ｆの中で直積や直和、初 代数や終夜代数などの圏論的な性質が表現できることが、長谷川立 らによって示されている。また、体系Ｆに対しるパラメトリシティ ーは、アバディ、キュリアン、プロトキンらによって形式論理の上 での公理化がなされている。 　本研究では、体系Ｆに対して定義されていたパラメトリシティー をバレンドレヒトのλ方体に拡張する。λ方体上のパラメトリシテ ィーを定義する際には、共形性の関係が本質的に働いている。 　λ方体の最高頂点であるλＰωでは、パラメトリシティーの公理 系から、随伴函手の性質など、一部圏論的な性質を証明することが 出来る。 題：実効的縮小写像定理 講演者： 鴨浩靖 概要： 縮小写像の不動点定理の計算可能性版が成り立つことを示し、その応用例をあげる。 題： Assigning Types to Processes 講演者： Nobuko Yoshida 概要： In wide area distributed systems it is now common for higher-order code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. In this talk we propose a fine-grained typing system for a higher-order pi-calculus which can be used to control the effect of such migrating code on local environments. Processes may be assigned different types depending on their intended use. This is in contrast to most of the previous work on typing processes where all processes are typed by a unique constant type, indicating essentially that they are well-typed relative to a particular environment. Our process type takes a form of an interface limiting the resources to which it has access, and the types at which they may be used. Allowing resource names to appear both in process types and process terms, as interaction ports, complicates the typing system considerably. For the development of a coherent typing system, we use a kinding technique, similar to that used by the subtyping of the system F, and the order-theoretic property (finite bounded completeness) of our subtyping relation. Various examples of this paper illustrate the usage of our fine-grained typing system for distributed systems. As a specific application we define a new typed behavioural equivalence for the higher-order pi-calculus. The expressiveness of our types enables us to state and prove interesting identities between typed processes. 大阪府立大学周辺の宿泊施設のリストを作ってみました． ALGIのホームページへ