並行計算の最前線 : タイプシステム
スポンサーリンク
概要
- 論文の詳細を見る
The π-calculus has achieved a remarkable simplification by focusing on naming and allowing the communicated data along channels (names) to be names themselves. The calculus is sufficiently expressive to describe mobile systems and the ability of natural embeddings of both lazy and call-by-value λ-calculi into the π-calculus suggests that it may form an appropriate foundation for the design of new programming languages. It has been shown that higher-order processes can be faithfully encoded in the π-calculus. The polyadic π-calculus by Milner is a straightforward generalization of the monadic π-calculus, in which finite tuples of names, instead of single names, are the atomic unit of communication. Furthermore, the fact that a tuple of names is exchanged at each communication step suggests a natural discipline of sorting. In the literature, there have been intensive studies on typing (sorting) systems for the polyadic π-calculus, originated by Milner's sorting discipline based on name matching. The proposed systems, so far, are categorized into the two groups-systems by name matching and ones by structure matching (possibly with subtyping)-and obtain similar results. A natural question arises "Is there any relationship between the two paradigms?". With this motivation, the present paper gives deeper investigations between the two approaches. For this purpose, a sorting system by name matching, a quite similar to the system in, and a typing system by structure matching with subtyping, a slight extension of the system in, are presented, along with several basic properties. Then, correspondence between the sorting system and the typing system is investigated via transformations both form sortings to typing and from typings to sortings. Let N be a set of names. The basic syntax of processes we consider in this paper is defined by the following grammar: P::=0|a(x^^~).P|a^^-<b^^~>.P|P|Q|(vx)P|!P where 0 is the nil process; a(x^^~).P and a^^-<b^^~>.P are input-prefixes and output-prefixes, respectively; P|Q are parallel compositions; (vx)P are restrictions; !P are replications.
- 社団法人電子情報通信学会の論文
- 1997-03-06
著者
関連論文
- 資源適合型アプリケーション統合開発環境の提案(ソフトウェア工学の基礎)
- 狭帯域電力線搬送でのGUIによる家電の遠隔操作の試み
- 移動エージェントモデルを用いた家電の自律制御の試み
- 情報技術に基づく大学事務支援の情報化に関する基礎と実践研究 (平成13年度情報学部研究プロジェクト報告)
- リモートディスプレイフレームワークによる家電ネッワークの試み
- M-pi計算 : 移動エージェントのための計算体系
- 並行計算の最前線 : タイプシステム
- モーバイルプロセス計算へのいざない
- モービルプロセス計算の型システムについて(計算理論とその応用)
- Polyadicπ計算の型計算システムについて
- π計算に対する視覚化システム
- システム要求仕様化のための状態遷移システム表示インターフェースの開発
- 効果的なソフトウェア開発のためのシステムシミュレータ
- 静岡大学受けた側の立場から
- システム要求記述と形式仕様の導出 : デバッグ結果の反映方法
- π計算に対する様相証明システム
- システム要求からの形式仕様の導出方法(マルチメディア通信と分散処理)