代数, 論理, 幾何と情報科学研究集会 プログラム

************** １０月１３日（金曜日）**************

(1) 13:30-14:15

「Bar Resolution as Parallelization in Process Algebra」高山 幸秀 (立 命館大学理工学部情報学科) [Yukihide TAKAYAMA (Ritsumei-kan University)]

概要： 並列結合 (P|Q), 非決定的選択 P+Q (Σ_i P_i),逐次結合 P;Q, 制限 P＼L を持った単位動作集合Ａ上の簡単なプロセス代数を考える。ラベル付き遷移シ ステムとして操作的意味論を与えることにより、(strong) bisimulation によ る並列プロセスの同値関係 〜を考えることができる。このとき、展開則

(P_1|…| P_n) 〜 Σ{α;(P_1|…|Q_i|…|P_n) ｜P_i ―α→ Q_i, α∈Ａ}

が成り立つことはよく知られている。展開則はプロセス式で書かれた形式的仕 様を並列プログラムに変換するときに重要な役割を果たすが、与えられたプロ セス式の中から展開則の右辺に相当するパターンを見付けてこの規則を適用す るのは一般に容易ではない。以下では、この操作のことを「(並列プロセスの) 並列化」と呼ぶ。

ここでの目的は、並列化アルゴリズムを幾何学的に明解な形で与えることで ある。基本的なアイディアは次の通りである。まずプロセス式を V. Pratt, E. Goubault, T. Jensen らによる 高次元オートマトンとして解釈する。これ は、通常のグラフ理論的な並列計算モデルと似ているが、直観的に言えば並列 結合(P|Q) を PとQを解釈する「グラフ」の直積集合として解釈する点が特徴 である。従って、並列計算は計算の逐次的順序表現する「方向」の概念を持っ たある種のCW複体としてとらえられる。このとき非決定的選択は幾何学的な分 岐として特徴付けらる。並列化操作は分岐部分の端点をある条件に従って貼り 合わせる(これを「マージ操作」と呼ぶ)事により作られるサイクルを、適当な セルによって埋め合わせる操作(これを「サイクル消去」と呼ぶ)に相当する。 このような変換操作によって作られた新しい高次元オートマトンを解析するこ と(これを「逆解釈」と呼ぶ)により、並列化された並列プロセス式が得られる。

サイクル消去操作は、群のコホモロジー論で使われる棒構成(Bar resolution) によって行なうことができる。具体的にはマージ操作によって生成されたサイ クルをホモロジー群の極小生成元として求め、その生成元にある種の鎖ホモト ピー写像を適用してサイクルを埋めるためのセルを構成する。このように棒構 成の機構を直接的に使うためには、高次元オートマトンモデルを棒式(Bar expression)によって構成しなければならない。棒式の幾何学的実現は単体複 体であるが、高次元オートマトンモデルは立方複体である。従って、我々は対 称群の棒式に対する作用によって作られる規道を貼り合わせたものを立方単体 の代用とする。また、同期通信 (P|Q)＼L をモデル化するために、立方単体は 同期通信に相当する silent action を表現する部分複体を含まなければなら ない場合がある。これも貼り合わせ面に対するある種の関係式を導入すること により実現される。

逆解釈では、高次元オートマトンを高次元計算経路と呼ばれる部分空間に分 解し、それらの交叉の様子を調べる。一般に高次元計算経路は非決定的分岐を 表わすが、複数のものが集まってインターリーブ (P_1;…;P_m)|(Q_1;…;Q_n) を表現している事もある。後者を区別するために、高次元計算経路にホモトピー 関係を定義し、十分な数の要素を持ったホモトピー類を見付ける操作も必要に なる。

(2) 14:20-15:05

「空間プロセス代数による近似解析」 磯部 祥尚, 佐藤 豊, 大蒔 和仁 (電子技術総合研究所) [Yoshinao Isobe, Yutaka Sato and Kazuhito Ohmaki (ETL)]

概要： 並行プロセスを解析する数学的道具としてプロセス代数が知られており、既 に目的に応じた多種のプロセス代数が提案されている。しかし、観測可能なア クションが増加するにつれて状態数も急激に増加するため、大規模システムの 解析は困難となる問題がある。

我々は各アクションにその重要度を示す値(グレイド(Grade)と呼ぶ)を付加 することによって、並行プロセスを近似的に解析可能なプロセス代数 CCSG (a Calculus of Communicating Systems with Graded Actions)を提案する。CCSG にはグレイドを減少させるためのルータが用意されており、遠方で生じたアク ションのグレイドを距離とともに減少させることができる。つまり、遠方で生 じた重要度の低いアクションは観測できないという仮定に基づいた近似解析が 可能である。我々はこのような近似的な等価性を双模倣関係に基づいて定義し、 その特性を示すいくつかの命題を与える。

参考文献:

「ソフトウェア工学の基礎II」 日本ソフトウェア科学会FOSE'95 近代科学社レクチャーノート PP.71-80

(3) 15:30-16:15

「Shortcut Deforestation in Calculational Form」 高野 明彦 (日立基礎研) [Akihiko TAKANO (HARL)]

概要： In functional programming, intermediate data structures are often used to "glue" together the smaller programs. Deforestation is the program transformation to remove these intermediate data structures automatically.

In this talk, we present a simple algorithm for Deforestation based on two fusion rules of hylomorphism. We introduce a generic notation for hylomorphism, where natural transformations are explicitly factored out, and use it to represent the structures of programs. For this representation of hylomorphism, the left/right fusion rules can be stated as the simple rules without side conditions, which is essential when we apply them to automatic program transformation.

(4) 16:20-17:05

「Simple gap termination for term graph rewriting systems

(or Kruskal-type theorems and termination)」 小川 瑞史 (NTT基礎研) [Mizuhito Ogawa (NTT Basic Research Lab.)]

概要： これはこの前のＰＲＯで話したのと同じ題ですが、まだまだ研究は始めたばかり です。いろいろな Kruskal の定理の拡張（私自身の結果を含め）の話だけでも 話しても面白いと思いますし、さらにその応用として rewriting system の停止性 の十分条件とかある特定のクラスのプログラムの自動合成（の可能性）などまで話 しても面白いかとも思います。

************** １０月１４日（土曜日）**************

(5) 9:00-9:45

「線型論理とclosed monoidal categoryの話」 白旗 優 (北陸先端科学技術大学院大学情報科学研究科) [Masaru SHIRAHATA (JAIST)]

概要：

(6) 9:50-10:25

「スケッチの一般化について」 三好 博之 (慶應義塾大学湘南藤沢メディアセンター) [Hiroyuki MIYOSHI (Keio, Shonan-Fujisawa Media centre)]

概要：

(7) 11:00-11:45 「Primitive Recursion in Categories」Fer-Jan de Vries (日立基礎研[HARL]) (joint work with Hidetaka Kondoh and Akihirko Takano)

(8) 11:50-12:35

「Datatype as lax-pullback」 立木 秀樹 (京都産業大学理学部計算機科学科) [Hideki TSUIKI (Kyoto Sangyo University)]

概要： Merge に対応する Datatype を カテゴリでいう lax-pullback としてとらえ、 総称的な関数を lax-transformation としてとらえる考え方を提唱する。そし て、λm という言語の意味を、そのカテゴリの手法で与える。

(9) 14:00-14:45

「Category of Partial Equivalence Relations and Strong Normalization Argument」 赤間 陽二 (東京大学大学院理学系研究科情報科学専攻) [Yoji Akama (Tokyo)]

概要： We explain that how categorical models of higher typed lambda-calculi yields the strong normalization in the light of the notion of realizability. In this process, we employ the translation from lambda-terms to CL-terms which reflects the strong normalizability.

(10) 14:50-15:35

「An algebraic account of data refinement」木下 佳樹 (電子技術総合研究 所) [KINOSHITA Yoshiki (ETL)], joint work with A.J. Power (LFCS, Edinburgh)

概要： We give a mathematical background of Hoare's algebraic account for data refinement. In particular, we use lax/oplax transformations to explain Hoare's upward/downward transformation, and the enriched adjunction to explain why one only has to prove laxness/oplaxness for the primitive commands of data types, in order to prove it for the entire collection of commands. Since many of the audience attended my talk at SLACS in Hiroshima, we will focus about how the enriched categorical construction will be used in our explanation of data refinement.