ALGI 06

第6回 ＡＬＧＩ (代数、論理、幾何と情報科学研究集会) のお知らせ。 第6回のALGIは、第5回のときに相談したとおり、JAMS (日本数理科学協会) 年 会の分科会として開催します。JAMS については http://www.jams.or.jp/ を御覧ください。 講演を募集します。研究発表およびサーベイの講演を歓迎します。 題、講演者、概要、必要な時間などを yoshiki@etl.go.jp までお送りくださ い。設備として、ＯＨＰ、黒板か白板、計算機画面を投影するプロジェクタな どを用意しますが、その他に必要なものあれば合わせてお知らせくだっさい。 日時： 8月5日13:00-17:00 8月6日9:00- JAMS の年会は 8/4〜8/6 の日程ですが、その内上記時間帯 がALGIにわりあてられています。他に 形式体系と計算(Formal systems and computation) 代表者氏名　八杉満利子 ４日午後13:-17:, ５日午前9:30-12:30　 という分科会もあります。 会場： 大阪大学コンベンションセンター (大阪大学吹田キャンパス) 会場への交通： 地下鉄・北大阪急行線 千里中央駅(終点)から阪急バスで「阪大本部前」または 「茨城美穂ヶ丘」行 約10〜20分＊ 阪急電車京都線 茨木市駅から近鉄バスで「阪大本部前」行 約30分＊ JR東海道線 茨木駅から近鉄バスで「阪大本部前」行 約20分＊ いずれも「阪大本部前」下車 会場まで徒歩3分 なお阪大案内図および阪大吹田キャンパス案内図を御覧ください． http://www.med.osaka-u.ac.jp/~derma/jsid/OUCC/OUCC.html http://teils.eng.shizuoka.ac.jp/jspf/picture/nen018.jpg なども役に立つかもしれません． 懇親会について: 8月5日18:00から河久 (大阪駅前第三ビル，電話 06(346)0770) を予 約してあります．鱧定食 7,800 円くらいでいこうかと思っています．

懇親会に参加される方は yoshiki@etl.go.jp 宛 メイルください．

予約の都合上，人数を把握したいのです． 宿の情報: コンベンションセンターのある阪大吹田キャンパスは千里にあります ので，千里中央あるいは北千里，南千里あたりの宿が一番近いと思い ます．江坂や大阪の中心地になると少し遠くなります．大阪をはなれ てン十年になる幹事が，勘をもとに書いているので，地元の方の情報 があればそちらのほうを信用してください． 千里の宿: 千里阪急ホテル (インターネット割引 (約10%) があります) 〒565 大阪府豊中市新千里東町2丁目1番D-1号 TEL06-872-2211 FAX06-832-2161 (地下鉄御堂筋線千里中央駅付近) ホテルマーレ南千里 〒565大阪府吹田市津雲台1-2-D9(阪急千里線南千里駅前) TEL:06-872-1911　FAX:06-872-0062 JR大阪駅、阪急梅田駅より阪急千里線にて約25分。 JR新大阪駅よりタクシーで15分。 江坂の宿一覧 大阪市近辺の宿一覧 プログラム 講演申込は8/4日まで受け付けますので，以下は暫定プログラムです． 8月5日 13:00-13:40 Fer-Jan de Vries (ETL) From metric spaces to actions of semigroups 13:45-14:25 赤間陽二 (東京大学 情報科学) 14:25-14:35 休憩 14:35-15:15 坂井公 (筑波大学 数学系) 体 On_2 上の代数方程式の求解について 15:20-16:00 齋藤孝道 (東京理科大学) 順序ソート項書換え系の停止性判定とそのシステムの実装 16:00-17:00 (JAMS 学術賞・清水賞受賞記念講演) 18:00 ALGI懇親会 於「河久」(電話 06(346)0770 大阪駅前第三ビル最上階) 8月6日 9:00-9:40 長谷川真人 (京都大学 数研) Logical predicates for intuitionistic linear logic 9:45-10:25 森雅生 (九州大学 システム情報科学) 題未定 10:30-11:10 桜井貴文 (千葉大学 数学・情報数理) Explicit Environments 11:10-11:25 休憩 11:25-12:05 大崎人士 (ETL) Self-labelling: An algebraic approach for termination property 12:10-12:50 浜名誠 (京都大学 情報学研究科) 対話的関数論理型言語の意味論 アブストラクト 題: 体 On_2 上の代数方程式の求解について 講演者: 坂井公 筑波大学数学系 概要: 自然数あるいはその拡張としての順序数を 2 進表記し，その上の演 算として排他的論理和(ニム和)を考えれば，順序数の全体が加法群を 作る。Conway は順序数間にニム積と呼ぶ新しい演算を定義し，ニム 和とニム積により順序数の全体が標数 2 の代数的閉体になることを 示した。この体の要素を係数として持つ代数方程式の求解アルゴリズ ムとその計算機上への実装について報告する。 題 順序ソート項書換え系の停止性判定とそのシステムの実装 講演者 齋藤孝道 （東京理科大） 概要 順序ソート項書換え系は、より簡潔かつ強力な記述力を提供する書換 え系である。また、項書換え系の停止性は、その書換え系の応用にお いても非常に重要な性質である。しかし、多ソート項書換え系におい ては、いくつかの停止性判定法が確立しているが、それらは順序ソー ト項書換え系には適用できない。よって、本研究では、任意の順序ソー ト項書換え系を多ソート項書換え系に変換法を与え、その変換を含め た順序ソート項書換え系の停止性判定システムを実装した。 題 Logical predicates for intuitionistic linear logic 講演者 長谷川真人（京都大学数理解析研究所） 概要 We develop the notion of parameterized logical predicates for two fragments of intuitionistic linear logic (MILL and DILL) in terms of their category-theoretic models. Such predicates are derived from the categorical glueing (Freyd covering, sconing) combined with the free symmetric monoidal cocompletion. As applications, we obtain full completeness results of several translations between linearly typed calculi. 題 Self-labelling: An algebraic approach for termination property 講演者 大崎人士 (ETL) 概要 The technique named self-labelling is an algebraic method for verifying the correctness of transformations that attempt to prove termination by transforming term rewrite systems. The simple proof by self-labelling clarifies the relationship among the transformations, such as distribution elimination and dummy elimination. Furthermore, it yields a positive solution to an open problem concerning distribution elimination. In this talk, I address these many applications of self-labelling including a new result about innermost termination. 題 The Representable Functions in Lambda Calculi 講演者 赤間陽二 (東大 情報科学) 概要 Bellantoni and Cook characterized the polynomial-time computable numeric functions by a 2-sorted recursion schemata. We will show that the one sort is for the impredicative natural numbers, and the other is for the predicative natural numbers. According to Leivant, this observation is effective in characterizing the functionals definable by typed lambda terms of 2-order type. We will compare it to other characterizations of the functionals definable by typed lambda terms of arbitrary types (solutions of Plotkin's conjecture). 題 対話的関数論理型言語の意味論 講演者 浜名誠 (京都大学 情報学研究科) 概要 関数論理型プログラミング言語は，関数型言語と論理型言語双方の機 能を合わせ持つ言語である．この言語に参照透明性を保存しつつ，副 作用の機能を付加したものを対話的関数論理型言語と呼ぶ．この言語 の意味論について，等式論理としてMoggiのcomputational metalanguage，圏論的意味論として副作用モナドを使うものを与える． そして操作的意味論をcomputational metalanguageから条件付き項書 換え系への変換として与え，これが二つの論理体型，computational metalanguageと通常の等式論理との間での定理の変換となっているこ とを示す． 幹事： 木下佳樹 (電総研) yoshiki@etl.go.jp 暑い季節の関西ですが、ハモの湯びきはじめ、この季節でないと食べられない ものも沢山ありますので、お楽しみください。沢山の講演申込をお待ちしてお ります。 木下佳樹