著者

加藤 紀夫 上田 和紀

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌プログラミング(PRO) (ISSN:18827802)

巻号頁・発行日

vol.46, no.1, pp.155-155, 2005-01-15

---

階層的グラフ構造の書換えに基づく並行言語において,プロセスが形作る構造に関する静的な性質を表現し,解析する新しい枠組みを提案する.本発表では,階層グラフ書換え言語としてLMNtal を例に取り,この言語に型体系を導入する具体的な方法を示す.LMNtal はグラフのノードとしてアトムを持ち,アトム間を結ぶ1 対1 のリンクを持つ.さらにアトムは膜と呼ばれる構文で階層化され,各膜がその膜内に対して局所的に適用される書換えルールを持つ.グラフ書き換え言語をプログラミング言語として見たときには,プログラムの書き方や処理系の最適化に関する指針に関する研究が求められる.しかし,従来の並行グラフ書換え言語は,LMNtal と違って一般のグラフ書き換えを実用に供するプログラミング言語にするというアプローチの研究が不足しているため,一般のプログラムに対して上述の指針を与えるために役に立つ解析技術はあまり存在しない.本発表で提案する型体系は,はじめにアトムをアクティブなものと,非アクティブなものに分類し,アクティブアトムにつながる可能性のあるプロセスやデータを解析することに基づいた強い型をプログラムに導入する.この型体系は,並行論理型言語のうえでの強モード体系をLMNtal に応用したものであるが,膜に関する性質を扱う点で新しい.本発表では,型体系の型安全性を証明する.We propose a new framework for formalizing and analyzing static properties on the shapes of processes in concurrent languages based on hierarchical graph rewriting. We take LMNtal as an example language and show a concrete method to introduce a type system to this language. LMNtal has atoms as graph nodes and one-to-one links that connect together atoms. Moreover, atoms are hierarchized with membranes and each membrane has rewriting rules local to itself. Viewed as programming languages, graph rewriting languages ask for research on how to write programs and how to optimize the runtime system. However, since the graph rewriting languages so far have lacked in research towards making themselves practical programming languages, few analysis techniques exist that can be used for solving the above issues. Our type system firstly classifies atoms into active ones and passive ones, and then introduces to the program strong types based on which processes as well as data can be connected to active atoms. The type system has been obtained by applying the strong mode system of concurrent logic languages to LMNtal, but is new in that it can deal with properties on membranes. The proof of the type safety will be shown.