日本ソフトウェア科学会第 41 回大会 (2024 年度) 講演論文集

MELL のカット除去規則に基づく階層グラフ書換え言
語の拡張
田久 健人

上田 和紀

階層グラフ書換えとは，グラフ構造に，階層表現やグループ化のための箱状の構造 (Box) を加えた構造と，その書換えにより計算を表現する手法で，高い表現力を有するモデリング・計算手法である．一方で，論理体系との対応が自明ではない．そこで，Box を持つ Multiplicative Exponential Linear Logic (MELL) の Proof Nets に着目した．二者間の対応関係の考察にあたり，階層グラフ書換え言語 LMNtal による MELL Proof Nets のカット除去規則のエンコードを試みたが，接続先を明示しない不特定多数のエッジを含む Box の複製や消去の表現が自明ではな
かった．本研究では，LMNtal 上においてこれらの操作の仕様を定義し，処理系に実装した上で，これらの操作の階層グラフ書換えにおける有用性を論ずる．さらに，LMNtal の状態空間探索機能などを用いて，LMNtal の Proof
Nets のワークベンチとしての有用性を示す．

グラフ書換えと呼ばれ，その体系はいくつか存在して

1 はじめにいる．並行計算の文脈で登場した Chemical Abstract

1. 1 背景Machine (CHAM) [2]，Bigraphical Reactive System

接続構造と階層構造は，コンピュータサイエンスや(BRS) [12]，階層グラフ書換え言語 LMNtal [20] や，

日常の様々な事象のモデリングにおいて普遍的に現

pushout を用いたグラフ変換の定義に階層性を追加しれる．例えば，企業の組織図や，クラスの継承関係，

た Hierarchical Graph Transformation [6]，グラフィシステム構成図やアーキテクチャ図等，様々な事象のカルなポートグラフ書換えツール PORGY [16] 向け

図的表現において，しばしば各構成要素の接続関係をに階層表現を追加した Attributed Hierarchical Port

線で表現し，それとは別に構成要素の階層分けやグ

Graphs (AHP) [7] などが提案されている．また，こループ化に関して円形や四角形で囲む表現方法が用れらの体系の多くには、形式的な定義のほかに実装もいられる．このような，接続構造をグラフで，階層構存在している．中でも LMNtal は，コンパクトな構

造を箱状の構造 (以降 Box と呼ぶ) で表現する，階層グラフと呼ばれるデータ構造がある．上記の通り階層

造的操作的意味論を持ち，オープンソースの処理系を提供している †1 ．

グラフは普遍的な構造であるため，これを形式的に扱

一般に，ある計算モデルの研究としての位置付けを

う計算モデルがあるのが望ましい．

明確にするために，他の計算モデルとの対応関係を階層グラフの書換えを用いて計算を行う手法は階層示すことは重要である．階層グラフ書換えにおいて∗も同様で，各階層グラフ書換え系がそれぞれいくつ

Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination.
This is an unrefereed paper. Copyrights belong to
the Author(s).
Kento Takyu, Kazunori Ueda, 早稲田大学基幹理工学
研究科情報理工・情報通信専攻, Dept. of Computer
Science and Communications Engineering, Graduate School of Fundamental Science and Engineering,
Waseda University.

かの計算モデルとの関係を示している．CHAM では

CCS，BRS では非同期 π 計算や CCS，CSP との関係が示されている．LMNtal では，ラムダ計算，π 計
算，Ambient 計算などの計算モデルのエンコードが†1 https://github.com/lmntal

可能であることが示されている [25] ほか，G-Machine

不特定多数のエッジを扱う構文があるため，大多数の記述 [17] や，C プログラムへの変換 [24] などの実の操作は直接的にエンコードできた．しかしながら，用的なプログラミング言語との対応も示されている．

Box の複製，消去に関しては，ルール前後での Box

また，論理体系との対応関係の整備は，Curry-の内部要素 (ノード，エッジ) の個数の変化が伴うた

Howard 同型等で見られるように，仕様の明瞭化や，め，要素の出現回数に関する構文上の制約によって接論理体系に基づく良い性質が得られるため重要であ続関係の安全性を保証している LMNtal においては，る．しかしながら，階層グラフ書換え系と論理体系の直接的なエンコードが難しい．

対応は非自明である．文献 [20] では，LMNtal プログ
ラムの線形論理式による解釈を試みているが，膜に1. 2 目的

関する扱いは，膜を平坦化し，膜のない ﬂat LMNtal

本研究では，LMNtal において，MELL Proof Netsに帰着させて解釈している．そのため，Box 構造ののカット除去規則で現れる，不特定多数のエッジを含動作に対する直接的な論理学的解釈は依然として自む Box の複製や消去機能を導入することで，LMNtal

明ではない．
階層グラフ書換えと関連があると考えられる論理体と MELL の対応関係を明瞭にする．これらの機能の仕様を形式的に記述し，処理系に実装したうえで，系として，Multiplicative Exponential Linear Logic

1. これらの機能を用いていくつかの例題を記述し，(MELL) が挙げられる．線形論理では，論理式をグ

階層グラフ書換えにおける，MELL Proof Nets

ラフ構造で表現する Proof Nets という手法が存在し，に基づく Box 操作の有用性を論ずる．また，中でも指数的演算子 (exponentials) に関する推論規2. これらの機能を用いて，MELL Proof Nets が則は，Proof Nets においては Promotion Box と呼ば直接的にエンコードできることを示す．これによれる Box 構造で表現される．また，Proof Nets におり，LMNtal の MELL Proof Nets のワークベン

けるカット除去は，グラフの書換えによって表現さチとしての有用性を示す．

れ，中でも指数的演算子に関するカット除去規則は，階層グラフ書換え側だけでなく，MELL Proof Nets

Promotion Box の階層移動，複製，消去を行うものの研究においても有用な成果となることが期待される．

がある．Proof Nets から出発したグラフ書換え系としては，Interaction Nets [11] やその派生の Box を

1. 3 本論文の構成持つ体系 [1]，Hypernet [14] が挙げられる．これらは2 節では，階層グラフ書換え言語 LMNtal につい関数型言語の計算モデルとしては有用であるが，表現て説明する．このとき，4 節および 5 節で用いる構可能なグラフ構造が限定されており，モデリング言語

文や機能に絞って説明する．3 節では，線形論理のとしては十分とはいえない．

一つである Multiplicative Exponential Linear Logic

本研究では，階層グラフ書換え系から出発し，階層(MELL) と，Proof Nets について説明する．4 節でグラフ書換え系と論理体系との対応を考察する．対は，LMNtal の拡張について述べる．また，例題の記象とする階層グラフ書換え系としては，構文や意味

述を通して，導入した機能の有用性を述べる．5 節で論が明瞭であり，多数の計算モデルとの対応が考察さは，拡張 LMNtal を用いた MELL のカット除去規則

れていて，オープンソースの処理系が提供されていのエンコードについて述べる．最後に，6 節でまとめ

る LMNtal を選択した．LMNtal における階層グラを述べる．

フの書換えと，MELL Proof Nets のカット除去の対

なお，本文において，青地の Box を用いた図は応関係を考察するにあたり，LMNtal による MELL

LMNtal グラフ，赤地の Box を用いた図は MELL

Proof Nets のエンコードを試みた [18]．一般に，階Proof Nets を表す．

層グラフ書換えにおいて，不特定多数のエッジを含む Box の操作は自明ではない．LMNtal においては，

プロセス
P ∶∶= 0∣ p(X1 , . . . ,Xm )∣ P ,P∣ {P }∣ [ RuleName @@ ] T :- T

( 空)
(アトム)
(分子)
( 膜)
(ルール)

プロセステンプレート
T ∶∶= 0(空)
∣ p(X1 , . . . ,Xm )(アトム)∣ T ,T(分子)∣ {T }( 膜)∣ [ RuleName @@ ] T :- T
(ルール)
∣ @p
(ルール文脈)∣ $p[X1 , . . . ,Xm |A](プロセス文脈)∣ p(*X1 , . . . ,*Xm )(アトム集団)

a

図2

a

a

多重辺や自己ループを許す，LMNtal グラフの例

文字から始まる名前はリンク名，そうでないものはアトム名として解釈される．同じリンク名の対によってエッジの接続を表す．このため，直感的にはプロセ
ス中に同じリンク名はたかだか 2 回しか出現しない．

LMNtal では，この制約を構文上の制約として次のよ
うに課している (リンク条件)：

剰余引数
A ∶∶= []
∣ *X

(リンク束)

プロセスに同名のリンクは高々2 回出現できる．
このとき，2 回出現するリンクは両端がアトムと繋図1

LMNtal の構文

がっている局所リンクであり，1 回のみ出現するリンクは一端が無接続である (または，外部と接続してい2 階層グラフ書換え言語 LMNtal
本節では，文献 [20] の内容をもとに階層グラフ書
換え言語 LMNtal について簡単に説明する．なお，

LMNtal には，ルール適用に関する操作的意味論や，る) 自由リンクである．この制約により，リンクの不正な接続を排除している．

LMNtal においては，アトムの多重集合によって無向多重グラフを表現する．つまり，多重辺や自己ループの出現を許す．例えば，プロセスに関する構造合同規則があるが，本稿ではこれらに関する説明は文献 [20] 等に委ねる．

a(X,X), a(Y,Z), a(Y,Z).

2. 1 構文
LMNtal の構文を図 1 に示す．言語の基本要素は，アトム，リンク，膜，ルールからなる．

は，図 2 のような無向多重グラフを表す．このとき，図中の矢印は第一引数を指し，そこから矢印の向き

2. 1. 1 アトム，リンク，膜に従って引数に順序がついていることを示す．なお，

LMNtal におけるアトム，リンクは，それぞれグ

図 2 で行ったように，LMNtal のコードはグラフ構

ラフ理論における頂点 (ノード)，辺 (エッジ) に対応

造として図示可能である． アトムやリンクに関するする．

略記法はいくつか存在する．中でもよく用いられる記p という名前で m 本のリンク X1 , . . . , Xm を持つ法として，リンクの左側に + をつけた，+X のようなアトムを p(X1 , . . . ,Xm ) と表記する．これらのリン

表記が挙げられる．これは１価アトム ’+’(X) の前置

クを，アトムの引数といい，引数には全順序がある．

演算子記法である．

例えば，a(X,Y) は，2 価の a アトムで，第一引数はLMNtal における膜は，一般的なグラフ理論には無X，第二引数は Y である．このような，引数が固定個

い，グラフの階層構造やグルーピングを表現するため

で全順序の付いている頂点からなるグラフは，ポートの構造である．この構造は，膜計算 [2] 等に由来して

グラフ (port graph) [7] と呼ばれる．なお，英字の大いる．膜は，{P } という形で表記される．膜は入れである．このとき，リンク束は，自由リンクの集合ではなく，順序のある列を表すことに留意する．また，

a

b

c

記法 ∣*X∣ によって，リンク束とマッチしたリンクの本数を表す．

2. 1. 4 プロセス文脈
図3

膜を貫通するリンクのある LMNtal グラフの例

プロセス文脈は，膜の中のルール以外のプロセスのうち，明示的に指定されていないもの全体とマッチ子構造をなすことができ，リンクは膜の境界を越えてアトムをつなぐことができる．例えば，する．
プロセス文脈は，$p[X1 , . . . ,Xm |A] のような形式で記述する．引数 X1 , . . . ,Xm は，その文脈が持っ{a(X), {b(Y,X)}}, c(Y).

ていなければならない自由リンクであり，これを明示的な自由リンクと呼ぶ．A にはリンク束 *X を記述

は，図 3 のような構造を表す．このような，アトム，
リンクからなる無向多重グラフに膜を加えた構造を，

LMNtal グラフと呼ぶ．
2. 1. 2 ルール

することができ，これは，明示的な自由リンク以外の0 本以上の自由リンクを持つことを表し，このような自由リンクを明示的でない不特定多数の自由リンクと呼ぶ．例えば，ルール：

ルールは，部分グラフから部分グラフへの書換えを表す書換え規則である．例えば，a(X) :- b(X) は，o(B), {i(A,B),$p[A|*X]} :- n(A),$p[A|*X].

1 価の a アトムを，1 価の b アトムに書き換えるルールである．便宜上，ルールの名前として RuleName

は，初期状態：をルールの前に付すこともある．
ルールの左辺と右辺には，部分グラフを記述する．

o(B), {i(A,B),a(A,G1),b(G2)},g(G1),g(G2).

そのため，しばしば自由リンクが現れる．ルール各辺
における自由リンクは，接続先を明記しないものの，
他の部分と接続している．このような自由リンクを含むグラフの変換ルールにおいて，ルール自体には自由リンクが存在しない，つまりルール上に出現する
リンクは，そのルール上にちょうど 2 回出現しなけに対して，図 4 のような書換えを行う．
また，リンク束やプロセス文脈に関しても，リンクと同様に構文上の出現回数の制約が設けられていて，不正な接続を防いでいる．図 4 の例では，*X は，ればならないという制約が設けられている．つまり，ルール上にちょうど 2 回出現していて，これにより左辺に自由リンクとして出現したリンクは，右辺でルール前後での *X リンクの接続が安全に保存されても同様に自由リンクとして出現する必要がある (この構文条件の詳細は [20](Occurrence Conditions) を参照)．直感的には，線形型によるポインタ制御と同様の役割を果たしている．この制約により，書換え時に不正な接続 (ダングリングポインタ) が生成されるのを防いでいる．

2. 1. 3 リンク束
リンク束は，*X のような形式で記述される，不特定多数の自由リンクとマッチするワイルドカード記法

いる．
以上のように，プロセス文脈は，一般的なプログラ
ミング言語におけるワイルドカードのように振る舞
うが，接続関係を指定できるという点が，階層グラフを扱う言語ならではの特徴である．

2. 1. 5 アトム集団
アトム集団 (aggregate) p(*X1 , . . . ,*Xm ) (m > 0)は，リンク束 *Xi が表すリンクの本数と同じ個数のm 価のアトムを表す．アトム集団に関して，リンクの接続関係を安全に保つためのいくかの制約が設け

i A

o

b
a

A

$p

g
g
*X
⋮

n

∶−

b
A

g
a

g

A $p
n

*X
⋮

o

i

図4

プロセス文脈，リンク束を含む書換えの例

図5

状態空間の可視化例

られている [20]．アトム集団によって，不特定多数個

理の最も基本的な (弱い) 断片である Multiplicativeのアトムを表現することができるが，その複雑さか

Linear Logic(MLL) に，指数的演算子 !，? を加えたら，現行の LMNtal 処理系上では代替の機能としてものである．

4. 1 節で述べる nlmem ライブラリを提供している．

定義 3.1 (MELL の論理式). MELL の論理式 F は
以下のように定義される：

LMNtal によるルールの適用は，評価戦略が定めら&

formula F ∶∶= X ∣ F  ∣ F ⊗ F ∣ F

2. 2 非決定性

F ∣ !F ∣ ?F

ここで，X は原子論理式 (atomic formula) を表す．
また，否定  に関して以下のように挙動を定める：(A⊗B) ∶= A B &(A B) ∶= A ⊗B (?A) ∶= !(A )A ⊸ B ∶= A B

a_to_b@@ a :- b.

(!A) ∶= ?(A )a_to_c@@ a :- c.

また，含意 → は，&A ∶= A&

れていないため，非決定的である．例えば，

A → B ↦ (!A ⊸ B)の，2 つのルールがプロセス中に存在し，これを a,a.という初期状態に適用すると，2 つある a アトムはそれぞれ b，c に書換えられる可能性があり，終了状態
は，b,b，b,c，c,c の 3 通りが考えられる．

LMNtal 処理系 SLIM [22] では，このような非決定性を扱うための非決定モードが用意されている．非決定モードでは，全ての可能性を列挙し，状態空間を構築する．また，構築した状態空間は，可視化ツール

StateViewer によって可視化することができる [21]．
例えば，先の例で構築した状態空間は，図 5 のように可視化される．また，構築した状態空間に対して，のように埋め込まれる．

◇

図 6 に，MELL の推論規則 (one-sided) を示す．ここで，A，B は論理式，Γ，∆ は論理式の列である．
構造規則のうち，Exchange 規則は認められているが，Weakening，Contraction は，指数的演算子 !，? を通してのみ定義されている．これにより，Γ，∆ は，!，? 内では集合のように振る舞うが，それ以外では多重集合のように振る舞う．乗法的連言 ⊗ と，一般的な (加法的な) 連言の違いは推論規則を見ると明らか
で，一般的な連言は 1 つの文脈から導出されるのに対して，⊗ は 2 つの文脈から導出される．Weakening，Contraction が認められている場合は，加法的連言とLTL モデル検査を行うことができる [22]．

乗法的連言は同値であるが，これらの構造規則が認められていない場合は，異なる挙動を示す．具体的に

3 MELL と Proof Nets
3. 1 Multiplicative

Exponential

LinearLogic
本研究では，Multiplicative Exponential Linear

Logic (MELL) [8] を対象にする．MELL は，線形論

は，乗法的連言の場合は，それぞれの文脈から A，Bのみを取り出す，すなわち “消費” している．このよ
うに，資源管理の観点から 2 つの連言は異なる意味を持つ．

MELL の証明体系は，カット除去定理が成り立つ

⊢ A, A⊢ Γ, A⊢ ∆, A(cut)⊢ Γ, ∆(ax)⊢ Γ, A, B( )⊢ Γ, A B&&⊢?Γ, A(!)⊢?Γ, !A⊢ Γ, A⊢ ∆, B(⊗)⊢ Γ, ∆, A ⊗ B⊢ Γ, A(?d)⊢ Γ, ?A

図6⊢ Γ, A(?w)⊢ Γ, ?A⊢ Γ, ?A, ?A(?c)⊢ Γ, ?AMELL の推論規則

ことが知られている [8]．図 7 に，MELL のカット除

このとき，ワイヤーは必ずしも閉じている必要はな

去規則の例を示す．なお，全てのカット除去規則はい．これは，自由リンクの存在を許すと言い換えるこ

Appendix に添付する．このとき，推論規則中で二重とができる．

線で示したルール適用は，そのルールを複数回必要な次に，証明構造と証明木の対応関係を定める．証明だけ適用することを意味する．多くの規則は直接カッ

構造は，一般に対応する証明木を持つとは限らない

トを除去していないが，それらの規則は，カットを証が，整合性条件と呼ばれる条件を満たすクラスの証明

明図の上部に移動させることにより正規化を助けて構造に関しては，これに対して解釈されるようなシーいる．

クエント計算の証明が存在する．この，整合性条件を満たす証明構造を Proof Nets と呼ぶ．
整合性条件としては，同値である複数の条件が知ら

3. 2 MELL Proof Nets
3. 2. 1 証明構造と整合性条件れているが，本研究においては，Danon-Regnier

次に，MELL のシークエントに対応する Proof Netsの整合性条件 [5] を採用する．

[8] を定義する．まず，証明構造を定義する．図 8 に，

定義 3.3 (スイッチング). 証明構造 S に対するスイッ

MELL の証明構造の構成要素を示す．各構成要素は，

チング σ とは，S 中の，図 10(a) に示すような， ，MELL の推論規則でラベル付けされたセル (ノード)?c の左右の選択である．スイッチンググラフ Sσ とと MELL 論理式でラベル付けされたワイヤー (エッは，S の全てのジ) からなる．このとき，セル ⊗，図 10(b) のように全ての Promotion Box の外枠を剥&&

のみ 2 つの入力，?c セルを，σ に従って書換え，がしたものである．

◇&&

が順序づけられている．
また，シークエント計算の (!) 規則を扱うための構

スイッチングは， ，?c セルに対して，左右どちら造として，Promotion Box が導入される (図 9)．

かを選択し切断する操作で，非決定的な操作である．

Box の内部を変換から保護し，簡約を順序付ける．

つまり，証明構造 S に対して，スイッチンググラフ

Promotion Box は，必ず互いに分離しているか入れSσ は，S の子になっている必要がある．?Γ は，不特定多数の ?

け存在する．

，?c セルの個数を n として，2n 個だ&

Proof Nets はスイッチングを用いて定義される．

付き論理式の列を表す．
証明構造は，これらの要素を組み合わせることで構

定義 3.4 (Proof Nets). 証明構造 S の任意のスイッ成される．

チング Sσ が非巡回であるとき，S は Proof Net で定義 3.2 (MELL Proof Structure). MELL の証明ある．

構造は，図 8 に示すセル，ワイヤーと，図 9 に示す

Promotion Box からなる，有向非巡回多重グラフで
ある．

◇

◇

Danos-Regnier の整合性条件は，証明構造の幾何的な条件によって Proof Nets を定義する．
図 11 に，MELL Proof Net の例を示す (拡大版は(a) promotion-nested⊢?Γ, !A⊢?Γ, A⊢?∆, B, ?A

(!)

(!)

⊢?∆, !B, ?A(cut)⊢?Γ, ?∆, !B(!)⊢?Γ, !A↝⊢?Γ, ?∆, B⊢?Γ, A⊢∆(!)⊢?Γ, !A⊢ ∆, ?A⊢?Γ, ∆

(?w)

⊢∆

↝

(cut)

⊢?Γ, !A⊢ ∆, ?A , ?A(!)⊢?∆, ?A⊢?Γ, ?∆

(?c)

(cut)

⊢?Γ, A↝⊢?Γ, !A(?w)∗⊢?Γ, ∆⊢?Γ, A⊢?Γ, A(!)⊢?Γ, !A

(!)

A

B

A

B

⊢?Γ, ?Γ, ∆

&
A

A
?A

A

&

?c

!w

?d

!

?A

?A

?A

!A

A

&

B

A
B

B

B

A

?A

"

B

?A
?c

?A

?A

"

&

A
?A

?A

&

A⊗B
?A

A

&

B
"

B
&

cut
A



(cut)

(?c)∗

(a) 選択

A

A
ax

(cut)

MELL のカット除去規則の一部

A⊗⊢?∆, ?A , ?A⊢?Γ, ∆, ?A⊢?Γ, ∆

図7

(cut)

(!)

⊢?Γ?∆, !B(b) promotion-weakening(c) promotion-contraction⊢?∆, B, ?A&⊢?Γ, A

?A

?A

"

?c

?c

?A

?A

(b) Promotion Box の展開

A

!

⋯

図8

証明構造の構成要素：セルとワイヤー

?Γ

図 10

!A

⋯
?Γ

!A

スイッチング操作

を満たしている．対応する証明木は Appendix に添付する．
A

3. 2. 2 カット除去
シークエントと同様に，Proof Nets においてもカッ

!
⋯

?Γ

ト除去が定義される．図 12 に，MELL Proof Nets

!A

におけるカット除去規則の例を示す．それぞれ図 7 の
図9

各規則に対応している．なお，全てのカット除去規則

証明構造の構成要素：Promotion Box

は Appendix に添付する．MELL Proof Nets におけ&

図 24 に添付)．巡回している箇所にはいずれもセルが含まれていて，いずれのスイッチンググラフも非巡回であることから，Danos-Regnier の整合性条件

るカット除去は，このように部分グラフの書換えによって表される．

MELL Proof Nets では，カット除去に関して，以は合流性を持つ．
ax

?d

?w

n

n

?d

n

除去は強正規化性を持つ．

?d
ax

!
?(!n ⊗ n ) ?nn!n

以上のような，Promotion Box で出現するような，

?n

n

⊗

&

?c

不特定多数のエッジを含む階層構造の書換え規則を一!n ⊗ n(?n )

cut

n)

&

&

!(?n

n) ⊗ (!n ⊗ n )n!n ⊗ n(?n )

n

⊗

&
?n

&

&

?(!n ⊗ n )般的なグラフ書換え系で表現する方法は，自明では

ax

!

&

?n

n

&

?c
?(!n ⊗ n )?n&?n ?(!n ⊗ n )定理 3.4 (強正規化性). MELL Proof Nets のカット

ax

n

n

&

?w

ax

?n

&

!n ⊗ n

!(?n

n

ない．

4 LMNtal の拡張

cut

本節では，MELL Proof Nets のカット除去で出現
図 11

する，不特定多数のエッジを含む階層構造や，そのMELL Proof Net の例

書換え規則を，LMNtal 上で記述できるように拡張する．

(a) box-nested
4. 1 nlmem
A

⋯
?Γ

A

B

!

!

⋯
?A

!A

LMNtal の構文において，不特定多数個の自由リン

B

クは記述できるものの，現行の処理系では，アトムや

!
?A

!A

膜が不特定多数存在することを表す記法は提供してし

cut
!

⋯

⋯

?Γ

?∆ !B

?∆ !B

cut

ない．よって，MELL Proof Nets の box-weakening
や box-contraction で出現するような，不特定多数個(b) box-weakeningのセルを用いた書換え規則を記述することはできな
?w

⋯

?w

A

い．関連研究として，量化子を用いた言語拡張 [13](to

?w

⋯
?w

!

appear) が挙げられるが，これは主に不特定多数のア

?Γ

⋯

?Γ

トムに関する表現力の拡張を目的としていて，本研究

?A

!A
cut

で扱う不特定多数の自由リンクに関する表現力の拡(c) box-contraction

?A

?A

A
⋯
?Γ

張は行われていない．

⋯
?Γ

!

?c

!A

?A

A

A

!

!

⋯

!A

?Γ

!A
cut

cut

?c
?c

⋯

SLIM 上には非線形膜ライブラリ nlmem (nonlinear membrane) が実装されている [25]．nlmem ラ
?A

?A

イブラリ自体は，階層グラフ書換えにおける不特定

cut

?c

多数のエッジを含む膜に関する操作のため，MELL

Proof Nets とは無関係の文脈で実装された．nlmem
図 12

MELL Proof Nets のカット除去規則の例

ライブラリには，不特定多数の自由リンクを持つ膜の消去を行う nlmem.kill と，消去を行う nlmem.copy

下の定理が成り立つ [8] [9] [15]．

が実装されている．各機能の動作の概略図を図 13 に定理 3.1 (カット除去定理). MELL Proof Nets にお示す．

いて，任意の Proof Nets に対してカット除去が可能

nlmem.kill では，第一引数に消去対象の膜を，第である．

二引数には，膜の消去後に接続先を失う自由リンクの定理 3.2 (安定性). 任意の MELL Proof Net は，カッ先に繋げるアトム (図中では n アトムを取っている)

ト除去後も MELL Proof Net である．

を取る．nlmem.copy では，第一引数に複製対象の膜定理 3.3 (合流性). MELL Proof Nets のカット除去を，第二引数には，膜の複製後に浮いてしまう自由リ

remove :
*X

n
kill

A

$p

$a

n

⋮

$a

*X

n

⋮

n

A
delete

*X
X

$p

⋮

*X

→ $a

⋮

$a

nlmem.kill(A,n), {$p[A|*X]}
copy :
copy

A

B

*X

$p

⋮

$p

n

*X

図 14

MELL のカット除去に基づく膜の消去 delete

B
n A

n

n
⋮

$p

n

実装に関しても，この記法自体を新たな構文として実装する方法は自明でないが，nlmem の場合と同様に，

nlmem.copy(A,n,B), {$p[A|*X]}

用途を限定することで，ライブラリ機能として実装す
図 13

nlmem ライブラリの動作概略図

ることが可能である．
まず，自由リンクを持つ膜の消去機能を定義する．

ンクを保護するためのアトムを，第三引数には，複製仕様は以下のように記述される．

した主ポート A を第二引数のアトムでまとめた際の，主ポートの元の接続先を保存するための自由リンク
を取る．これらの操作は，アトム集団によって仕様を

mell.delete(X,A), {$p[X|*X]}, {$a[A]}→ $a[*X]

記述することができる．アトム集団の用途をこれらの操作に限定し，ライブラリ機能として提供している．
しかしながら，kill，copy ともに，接続先不定の
自由リンクを塞ぐための構造がアトムに限定されていたり，contraction のカット除去規則で行われている
ような主ポートの扱いができないなど，MELL Proof

Nets のカット除去規則と直接的に対応が取れない部

対応する図を図 14 に示す．delete アトムの第 1 引
数には消去対象の膜を，第 2 引数には膜の消去後に接続先を失う自由リンクの先に繋げる，1 引数の構造$a[A] を取る．$a[A] には，アトムだけでなく，膜や，それらを組み合わせた a(A,B),b(B,C),c(C) のような構造も取ることができることに留意する．このとき，プロセス文脈の型付けに関する問題 [23] を分がある．

回避するため $a[A] は膜で囲む．反応後は，消去対

4. 2 不特定多数の自由リンクを持つ膜の消去
以降では，前節の課題を解決した，新たな自由リン
クの膜の複製，消去機能を持つ LMNtal の拡張について述べる．基本的には，新たな構文は追加せずに，
既存の構文を用いて記述するが，表現記法として [20]のアトム集団 (aggregate) を拡張した以下の記法を

象の膜が消え，*X だけが残り，本来 *X が膜側で接続していた接続していた各リンクが，それぞれ $a[A]のコピーに接続される．このとき，$a[A] を囲っていた膜は剥がされる．このように，mell.delete は，nlmem.kill の第二引数にアトム以外の構造を取れる
ように拡張したものとして定義される．

導入する：$p[*X1 ,*X2 , . . . ,*Xm ](m > 0)

ここで，各 *Xi はすべて同じ名前の (ルール左辺または右辺の) プロセス文脈に現れるリンク束であり，∣*X1 ∣ = ∣*X2 ∣ = . . . = ∣*Xm ∣ である．
これは，アトム集団をプロセス文脈に拡張したもの
で，m 本の自由リンクを持つ ∣*Xi ∣ 個のプロセス文脈を表す．この表現を用いることで，不特定多数個のプ
ロセス文脈を仕様中に記述することができる．また，

4. 3 不特定多数の自由リンクを持つ膜の複製
次に，不特定多数の自由リンクを持つ膜の複製機能を定義する．仕様は以下のように記述される．

4. 4. 1 同期 π 計算
C1$b

同期 π 計算の，通信に関する規則は以下のように

C2

C1

X

copy

*Z

$p

⋮

$b

$p

→

$a

$a
$a

C2

$b

$p

*Z

記述される．

(x(y).P + M ∣ x̄⟨z⟩.Q + N ) → P [z/y] ∣ Q⋮$a

ここで，通信前 (左辺) において，通信を行うプロ
セス P ，Q と同時に出現するプロセス M ，N は，通図 15

信後には消去される．プロセスを膜で表現したとき，MELL のカット除去に基づく膜の複製 copy

M ，N は膜の消去を意味するが，M ，N にも，上記の規則に明示的に現れないチャネルが存在する可能性

mell.copy(X,A1,A2,A3,B1,B2,C1,C2),があるため，不特定多数の自由リンクを持つ膜の消去{$p[X|*Z]}, {$a[A1,A2,A3]} ,{$b[B1,B2]}に対応する．

→ {$p[X’|*Z’]}, {$p[X’’|*Z’’]},

文献 [25] では，nlmem.kill を用いた以下のような$a[*Z’,*Z’’,*Z],

エンコードを行った．

$b[X’,C1], $b[X’’,C2].
対応する図を図 15 に示す．copy アトムの第 1 引数
は複製対象の膜を取る．このとき，copy アトムに直接つながる X の接続元を主ポートと呼ぶ．以降の 5

1
2
3
4

comm@@{$x,+C1,+C2},{get(C1,Y,{$p[Y|*V1]}),$m},{snd(C2,Z,{$q}),$n}:- {$x},$p[Z|*V1],$q,nlmem.kill({$m,$n}).

個の引数は，膜を複製した際に，接続先が浮いてしまう自由リンクに繋げるための構造につながるリンク

nlmem.kill を用いていた部分は，mell.delete を用を取る．いずれも，プロセス文脈の型に関する問題をいて以下のように記述できる．

回避するために，膜で囲む．第 2，3，4 引数は，主ポート以外につながるリンク *X を保護するための構造につながるリンクをとる．第 5，6 引数は，主ポートを保護するための構造につながるリンクを取る．第7，8 引数は，主ポートの外向きのリンクと接続する

1
2
3
4

comm@@{$x,+C1,+C2},{get(C1,Y,{$p[Y|*V1]}),$m},{snd(C2,Z,{$q}),$n}:- {$x},$p[Z|*V1],$q,mell.delete({$m,$n},d).

ためのリンクを取る．反応後は，複製対象の膜が複製され，{$p[X’|*Z’]}，{$p[X’’|*Z’’]} が生成され4. 4. 2 Ambient 計算

る．$a を展開して得られたプロセス文脈群は，*Z’，

Ambient 計算 [3] におけるプロセスの複製を例に示*Z’’ を結び，元の自由リンクである *Z を再現する．

す．Ambient 計算とは，ambient と呼ばれる Box 構$b は，主ポートのリンク X’，X’’ を，それぞれ C1，造を扱う，プロセス計算の一種である．多くのプロセ

C2 に接続する．このように，mell.copy は主ポート

ス計算は，プロセスの複製機能 !P を持つ．(!P は構造とその他の扱いを分離する．

合同規則 !P ≡ P ∣ !P によって定義される)．Ambient
計算においてもプロセスの複製が導入されることが

4. 4 例題

あるが，ほとんど !(open m.P ) の形式でのみ使用さ

プロセス計算における，プロセスの複製や強制終了

れ，以下のような規則で記述される：

で，膜の複製や消去を行う例を示す．なお，mell ラ!(open m.P ) ∣ m[Q] → P ∣ Q ∣ !(open m.P )イブラリは LMNtal 処理系 SLIM 上で実装し，これ直感的には，ambient は膜によってエンコード可能だ

らの例題について動作確認を行なった．

が，名前管理の詳細な解釈のため，文献 [19] では以下のようなエンコードが行われた．

4
5
6

A

B

A⊗B

このエンコードにおいては，膜は ambient 構造のエ

A

B

↧

A

B

A

A

↧

A⊗B

A B
par(A,B,C)

tensor(A,B,C)

cut

B

⊗

A

A
ax

&

9

A

↧
open_repl_aux@@
copies(A,B), copies({$p},remove) :- A=B, $p.

B⊗tensor(A,B,C)

7
8

A

&

3

open_repl@@
open_repl(M,{$p}),{amb(M1),{id,+M1,-M2,$mm},$q,@q},{id,+M,+M2,$m}:- nlmem.copy({$p},A1,A2,A3,B1,B2,remove,P),{cp(A1,A2,A3)},{copies(B1,B2)},$q, {id,+M3,$m,$mm}, open_repl(M3,P).

&

2

&

1

↧
A

A

A
A
ax{+A,+B}

cut{+A,+B}

A

A

ンコードと，名前管理のための構造の，2 とおりの役割を持つ．P ↦ $p，Q ↦ $q である．m に関しては，
名前参照の動的な移動に対応するために，参照を膜?A?A’?c’({+A,+B},C)
?c

?w

?d

’!’(A,B)
!

?A

?A

?A

!A

を用いた木構造で管理している．プロセスの複製は，

nlmem.copy を用いて記述されている．この規則は，mell.copy を用いて以下のように記述できる．

↧

↧

?A

?A
?w

1
2
3
4
5
6

open_repl@@
open_repl(M,{$p}),{amb(M1),{id,+M1,-M2,$mm},$q,@q},{id,+M,+M2,$m}:- mell.copy({$p},A1,A2,A3,B1,B2,remove,P),{cp(A1,A2,A3)},{B1=B2},$q, {id,+M3,$m,$mm}, open_repl(M3,P).

?A’?c’({+A,+B},C)

図 16

?d

!

?A

?A

!A

’?w’(A)’?d’(A,B)’!’(A,B)

セル・ワイヤーのエンコード

LMNtal のモデル検査機能が Proof Nets の性質の検証に利用できるようになり，LMNtal が Proof Nets

以上のように，各種プロセス計算におけるプロセの有用なワークベンチとなることが示される．

スの複製や消去が，Promotion Box の操作と関連する不特定多数の自由リンクを持つ膜の複製や消去で5. 1 エンコード手法

表現できることが示された．Proof Nets における

5. 1. 1 MELL Proof Nets のエンコード

Promotion Box は，内部の構造をアトミックに操作

まず，証明構造の構成要素 (図 8) をエンコードすするため，Optimal Reduction 等の局所的書換えにる．セルとワイヤーは，図 16 のようにエンコードす

基づく書換え系では排除されることが多いが，並行性る．⊗，

が求められる動作の記述や，階層構造を持つ概念の記

る．ax，cut セルは入力に順序がないので，膜で表現

述においては有用である．

する．?c セルは，入出力の区別はアトム，順序のな&

9

open_repl_aux@@
remove({$p}):- $p.

↧
A

?c

7
8

↧
A

セルの入力の順序づけは，アトムで表現す

い入力は膜で表現する．また，論理式を表す閉じてい

5 MELL Proof Nets の LMNtal へのエ
ンコード

ないワイヤーは，後述のエンコード例に示すように，
アトム formula を繋げる．

本節では，MELL Proof Nets を拡張 LMNtal にエ次に，Promotion Box (図 9) は，図 17 のようにンコードする方法について述べる．特に，カット除

エンコードする．Promotion Box の外枠は膜で表現

去規則に関して，4 節で導入した機能を用いて簡潔する．文脈 ?Γ はリンク束 *X で，空白部分はプロセにエンコードできることが期待される．これにより，

ス文脈 $p[X1|*X] で表現する．

で記述される．定義 3.3 では，全てのパターンのス
イッチンググラフが要求されるが，これは，LMNtal$p[X1|*X]の非決定モードにより，図 19 のルールの全ての適用

X1
A

パターンの終了状態より得られる．

!

!

また，Danos-Regnier の整合性条件のような，グ

⋯

⋯

?Γ

!A

*X

X2

ラフの形式に関する規則も，図 20，図 21 のような{’!’(X1,X2),$p[X1|*X]}.

グラフの変換規則としてエンコードできる．♯アトム
は，2 引数のアトム，つまりPromotion Box のエンコード

&

図 17

，!，?d，?c アトムを表す．♭アトムは，1 引数のアトム，つまり ?w，v ，以上のように，全ての構成要素が直接的にエンコーf アトムを表す．t アトムは，グラフ構造に流すトードできた．証明構造は，これらの要素の組み合わせクンを表す．ti アトムは，最初に 1 度だけ場にトーで構成されるので (定義 3.2)，これらのエンコードをクンを生成するための，チケットのような役割を持組み合わせることで，証明構造全体をエンコードでつアトムである．まず最初に，いずれかのアトムが 1

きる．

度だけ ti アトムと反応し，場にトークンを生成する

証明構造のエンコード例を示す．図 11 に示した

(図 20)．その後トークンは，通ったアトムを消費しProof Net は，図 18 の LMNtal コードで表される．

ながらグラフ構造を走査する．最終的に構造の端，つ

このとき，図 11 右端の (?n ) n に対応する自由リ

まり♭アトムに到達すると，そのトークンは 0 価のンクを，アトム formula で終端させる (16 行目)．

ok アトムに変化する．一方で，構造に循環がある場&

合は，いずれ 2 つのトークンが衝突して ng アトムに変化する (図 21)．このように，token-passing ルー
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

ax{+A1,+A2},'?d'(A1,A3),'?w'(A4).
{ax{+B1,+B2},'?d'(B1,B3).
'?w'(B4),'!'(B2,B5).
}.
'?c'({+A3,+B4}+C1),'?c'({+A4,+B3},C2).
tensor(B5,T1,D2),ax{+T1,+T2}.
cut{+A2,+D2}.
par(C2,T2,P1),par(C1,P1,F).
{
ax{+E1,+E2},'?d'(E1,E3).
par(E3,E2,E4),'!'(E4,E5).
}.
tensor(E5,T3,D4),ax{+T3,+T4}.
cut{+F,+D4}.
formula(T4).

ルを用いてグラフ構造の整合性を判定することがで
きる．

1
2
3
4
5

switching_par_l@@par(A,B,AB) :- par(B,AB),v(A).

678switching_contraction@@'?c'({+C1,+C2},X3) :- '?c'(C1,X3),v(C2).

9
10
11

図 18

switching_par_r@@par(A,B,AB) :- par(A,AB),v(B).

switching_box@@{'!'(X1,X2),$p[X1|*X]} :- $p[X2|*X]

Proof Net のエンコード例
図 19

スイッチング規則のエンコード

証明構造に関する整合性判定は，LMNtal 上でエンコード可能である．

5. 1. 2 MELL Proof Nets カット除去規則のエ

図 10 で示したスイッチング操作は，部分グラフのンコード

変換規則なので，LMNtal のルールで図 19 のように続いて，カット除去規則 (図 12) のエンコードを行

簡潔にエンコードできる．このとき，contraction にう．グラフの変換規則は，LMNtal のルールで表現さ関しては，C1，C2 に順序がないため，1 本のルール

れる．

t
♯

ti

t

ti

t

A

t

B

!

A

B

!

♭

t
⊗

ti

t

ti

cut

⋯

?Γ

t

?A

!A

?A

!A

!

⋯

!
⋯

?∆ !B

cut

⋯

?Γ

t

?∆ !B

↧
$p

図 20

token-passing による DR 判定: トークンの初

$p

$q
X1

$q

X3

!

X1

期生成

X3

!
*X

X2

!

⋯

X3
!

⋯

X2

X3

⋯

⋯

*X

*Y X4

*Y X4

t
♯

♯

t

t

図 22

t

box-nested 規則のエンコードtt

ることが保証される．
t⊗t

その他の規則も同様にエンコードできるが (全てのtエンコード結果は Appendix に添付する)，Weaken-ting，Contraction の規則に関しては，前述の通り非

t
t

⊗

t

⊗

t

t

自明な操作を含んでおり，4 節で導入した機能を用いてエンコードする必要がある．

♭
t

図 21

box-weakening 規則は，以下のようにエンコード

t
ng

ok
t

token-passing による DR 判定

する．

box_weakening@@{'!'(X1,X2),$g[X1|*X]},cut{+X2,+X3},'?w'(X3):- mell.kill(X,A),{$p[X|*X]},{'?w'(A)}.

box-nested 規則は，以下のようにエンコードする．
図 23(a) に対応図を示す．mell.delete を用いて，
box_nested@@{'!'(X1,X2),$g1[X1|*X]},{$g2[X3|*Y]},
cut{+X2,+X3}:- {{'!'(X1,X2),$g1[X1|*X]},$g2[X3|*Y]
cut{+X2,+X3}}.

図 22 に対応図を示す．このような，ワイヤーの束や階層構造を含む規則は，LMNtal のリンク束と膜を用いて簡潔に記述できる．また，Occurrence Conditions(2. 1. 1 節) のもとで，このルールはポインタ安全であPromotion Box の内側のリンクに ?w アトムを繋ぐようにする．

box-contraction 規則は，以下のようにエンコード
する．

box_contraction@@{'!'(X1,X2),$g[X1|*X]},'?c'({+C1,+C2},X3)
cut{+X2,+X3},:- mell.copy(X2,A1,A2,A3,B1,B2,C1,C2),{'!'(X1,X2),$g[X1|*X]},{'?c'({+A1,+A2},A3)},{cut{+B1,+B2}}.

(a) box-weakening
?w

?w

A

⋯

↦

⋯
?w

!

X1

X1

?Γ

?w
⋯

⋯

?A

!A

?w

*X

X2

?w

!

?w

!

⋯

?Γ

$p

$p

?w

*X

X3

⋯

X2
?w

deletecut*X(b) box-contraction

A

A

!

?A

⋯

?Γ

A

!A

?Γ

?c

!

?A

!A
cut

⋯

?Γ

!

⋯

?A

cut

?c

?A

!A

?c

⋯

cut

?A

?c

↧
$p
$p
X1

$p
C1

C2

⋯

*X

X2

*X

X4

C1

C2

X2
copy

?c

⋯

*X

!

⋯

C1 C2

⋯

*X

!

X3

!

!

X1

$q
X1

X2

X3

?c
?c

図 23

?c

?c

mell ライブラリを用いたカット除去規則のエンコード

図 23(b) に対応図を示す．mell.copy の第 2，3，4 引

1. 仕様が与えられ，数は contraction に対応する構造を取る．mell.copy

2. それを満たすアルゴリズムを記述し，において自由リンクを保護するための構造として，

3. アルゴリズムの健全性，完全性，決定性などを

アトム以外も取れるようにしたのは，主にこの部分証明する．

のエンコードのためである．第 5，6 引数は Cut にのような議論が行われるが，本研究においては，アル対応する構造を，第 7，8 引数は，カット除去前のゴリズムが限りなく仕様 (証明構造 (定義 3.2)，カッContraction の入力側のリンク 2 つを取る．これによト除去規則 (図 12)) に近い形で記述されている．どり，カット除去後の主ポート周りの構造をエンコード

ちらの体系にも対応する図表現が存在しており，エンする．nlmem.copy では，このようなアトム以外の構

コードの正しさは，非形式的には図の比較より明らか

造による自由リンクの保護や，主ポートの扱いを行である．形式的証明が必要な場合には，それぞれの数

うことができず，エンコードには複数のルールが必要

学的表現の間の対応を取る必要があるが，本論文ではだったが，mell.copy の導入によって，1 つのルール

詳細を省く．

でエンコード可能になった．

5. 2 エンコードの正しさに関する議論
エンコードの正しさに関して，一般的には，

ax
n
?w

?d

?d
ax

!
?(!n ⊗ n ) ?n

n

!n

?n

n

⊗

&

?c

ax
n

!n ⊗ n(?n )

cut
&
&

?n

!(?n
n

n)

(?n )!n ⊗ n

⊗

&
&

?n

!(?n

n

n

?d
?n

ax

&

&

?(!n ⊗ n )

n

!
&

?c
?(!n ⊗ n )?n&?n ?(!n ⊗ n )

n

&

?d

ax
n

n

n
?n

&

n

&

?w

ax

?n

&

!n ⊗ nnn) ⊗ (!n ⊗ n )

cut

図 24

f ∶ n → n, x ∶ n ⊢ f ∶ n → n

T-Var

Proof Net の β 簡約の例

f ∶ n → n, x ∶ n ⊢ x ∶ n

f ∶ n → n, x ∶ n ⊢ f x ∶ n
f ∶ n → n ⊢ λx ∶ n.f x ∶ n → n

T-Var
T-App

T-Abs

⊢ λf ∶ n → n.λx ∶ n.f x ∶ n → n → n → n

T-Abs⊢ (λf ∶ n → n.λx ∶ n.f x)(λx ∶ n.x) ∶ n → n
↝∗

図 25

T-Var
x∶n⊢x∶nT-Abs⊢ λx ∶ n.x ∶ n → n
T-App

T-Var
x∶n⊢x∶nT-Abs⊢ λx ∶ n.x ∶ n → n(λf ∶ n → n . λx ∶ n . f x) (λx ∶ n . x) →β (λx ∶ n . x)

5. 3 実行例：単純型付きラムダ計算の β-簡約
5. 3. 1 カット除去による β-簡約の状態空間構築
単純型付きラムダ計算を Proof Nets で表現する．

&

A → B ↦ ?A

B より，関数型の型付けは MELL

Proof Nets に埋め込むことができる [8] [10]．このとき，カット除去は β-簡約に対応し，カットを全て除去した後の Net は，β-簡約を全て行った，正規形のラムダ式に対応する．
図 24 に ，単 純 型 付 き ラ ム ダ 計 算 (λf ∶ n →
図 26

図 18 へのカット除去適用の状態空間

n . λx ∶ n . f x) (λx ∶ n . x) → (λx ∶ n . x) の Proof Netに よ る 表 現 を 示 す．初 期 状 態 の Net は ，図 11 と同様のものである (そのエンコードは図 18 に示し

(a) contraction-equivalence?A

contraction_equation@@'?c'({+C1,+C2},CC),'?c'({+CC,+C3},C4):- '?c'({+C2,+C3},CC),'?c'({+C1,+CC},C4)

?A
?A

?A
?c

?A
?c

=s

?A

?A

?A
?A
?c

box_contraction_pull@@{'!'(X1,X2),'?c'({+X3,+X4},X5),$p[X1,X3,X4|*X]}:- {'!'(X1,X2),$p[X1,X3,X4|*X]},'?c'({+X3,+X4},X5).

?c?A(b) contraction-pull-equivalence

A

=s

A

?c
!

!

⋯

⋯

?Γ

!A

?c

?Γ

!A

box_weakening_pull@@{'!'(X1,X2),'?w'(X3),$p[X1|*X]}:- {'!'(X1,X2),$p[X1|*X]},'?w'(X3).

(c) weakening-pull-equivalence

A

=s

A

?w
!
⋯

!
⋯

?Γ

!A

box_contraction_push@@{'!'(X1,X2),$p[X1,X3,X4|*X]},'?c'({+X3,+X4},X5):- {'!'(X1,X2),$p[X1,X3,X4|*X]'?c'({+X3,+X4},X5),}.

box_weakening_push@@{'!'(X1,X2),$p[X1|*X]},'?w'(X3):- {'!'(X1,X2),'?w'(X3),$p[X1|*X]}.

?w

?Γ

!A

図 28

図 27

Pull-equivalence

図 27 の各規則の LMNtal エンコード

うな同値関係 =s [4] を導入し，カット除去と同時並行での適用を許した場合の合流性や正規性への影響をた) が，これは図 25 の上側の証明図に対応する．

検証する．

(λf ∶ n → n . λx ∶ n . f x)(λx ∶ n . x) は，β-簡約によっ

図 27 の LMNtal エンコードを図 28 に示す．同値て正規形 λx ∶ n . x に簡約される．λx ∶ n . x に対応す関係を，両向きの書換え規則として表現した．また，る証明図は図 25 の下側であり，それに対応する Net(a) contraction-equivalence に関しては，入力の順序

は，図 24 の右側の Proof Net である．

がないため，1 本のルールで記述した．(b)，(c) にお

図 26 に，図 18 にカット除去規則を適用した状態

いては，右向き (Promotion Box から要素を取り出す

空間図を示す．初期状態の Net は，最短 10 ステップ方向) のルールは pull と，左向き (要素を Promotion

で正規形 λx ∶ n . x に対応する Net に簡約される．まBox に入れる方向) のルールは push と呼ばれることた，全ての簡約ルートが，最終的に一つの終了状態が多いため，それに従って命名した．

(図中の赤いノード) で停止することから，この例題

適 用 対 象 の Proof Nets と し て ，(λf ∶ n →において，定理 3.3，定理 3.4 の性質が満たされていn . λx ∶ n . f (f x)) (λx ∶ n . x) に対応する，図 29 をるのが確認できる．

用いる．これらの規則をカット除去規則に加えてい5. 3. 2 Pull-equivalence の追加

き，図 29 のエンコードに対して適用した際の状態空LMNtal でカット除去規則などの Proof Nets に関間の変化 (全状態の数，終了状態の数) を調査した．

する変換規則を直接的にエンコードできたことの利

表 1 に，各ルールの適用と状態空間の変化を示す．1

点の一つとして，既存の規則の変更や，新たな規則の段目は，ルールを何も追加せずにカット除去規則の追加が容易に行えることが挙げられる．

みを適用したもので，状態数は 476 個で，終了状態

例として，Pull-equivalence と呼ばれる図 27 のよは 1 個であった．2 段目以降は，図 27 のルールを追加していく．2 段目は，(a) contraction-equivalenceを追加した．状態数と終了状態に変化はなかった．

6 まとめ

本エンコードにおいては，?c の入力に順序はない

本研究では，MELL Proof Nets のカット除去規則

ため，図 27(a) の両辺は同じ状態としてカウントさで行われていた，不特定多数の自由リンクを含む Box

れる．そのため，contraction-equivalence を追加し構造の消去，複製操作を，階層グラフ書換え言語 LM-ても，同じ状態から同じ状態への遷移が追加される

Ntal に導入することにより，(i) 階層グラフ書換えにだけであり，状態数は変化しない．3–5 段目は，(b)おいて，並行性や階層性の表現で Promotion Box がcontraction-pull-equivalence を追加した．3 段目は有用であること，(ii) LMNtal が Proof Nets のワーク

push のみ追加したが，1 度も適用されることはな

ベンチとして有用であることを示した．また，MELL

く，状態数はカット除去のみ適用したときと同じ 476

Proof Nets とは無関係な文脈で，同様の操作を実現個であった．4 段目は pull のみ追加した．状態数はするために実装された nlmem.kill，nlmem.copy を，1808 個に増加し，終了状態は変わらず 1 個で，かつProof Nets の観点から整理することができた．

全ての簡約経路は有限であった (定理 3.3，定理 3.4

謝辞 本研究の一部は科学研究費補助金 (23K11057)が成り立っている)．5 段目は両方同時に追加した．状および早稲田大学特定課題研究助成費 (2024C-432)

態数は 1808 個で，終了状態は 1 個であった．状態の助成を得て行われた数に関しては，pull のみ追加した場合と同じである
が，push ルールの適用として，pull ルールの適用の参 考 文 献逆向きのみの遷移が追加された．これにより，無限[ 1 ] Alves, S., Fernández, M., and Mackie, I.: A newgraphical calculus of proofs, Electronic Proceedingsin Theoretical Computer Science, Vol. 48(2011).
[ 2 ] Berry, G. and Boudol, G.: The chemical abstract
machine, Theoretical Computer Science, Vol. 96,
No. 1(1992), pp. 217–248.
[ 3 ] Cardelli, L. and Gordon, A. D.: Mobile ambients, Theoretical Computer Science, Vol. 240,
No. 1(2000), pp. 177–213.
[ 4 ] Danos, V.: La Logique Linéaire appliquée àl’étude de divers processus de normalisation (principalement du Lambda-calcul), 1990.
[ 5 ] Danos, V. and Regnier, L.: The Structure ofMultiplicatives, Archive for Mathematical Logic,
Vol. 28, No. 3(1989), pp. 181–203.
[ 6 ] Drewes, F., Hoﬀmann, B., and Plump, D.: Hierarchical Graph Transformation, Journal of Computer and System Sciences, Vol. 64, No. 2(2002),
pp. 249–283.
[ 7 ] Ene, N. C., Fernández, M., and Pinaud, B.:
Attributed hierarchical port graphs and applications, Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 265(2018), pp. 2–19.
Publisher: Open Publishing Association.
[ 8 ] Girard, J.-Y.: Linear logic, Theoretical Computer Science, Vol. 50, No. 1(1987), pp. 1–101.
[ 9 ] Girard, J.-Y.: Linear Logic: A Survey, 1993.
[10] Guerrini, S.: Proof Nets and the λ-Calculus,
Linear Logic in Computer Science, Ehrhard, T., Girard, J.-Y., Ruet, P., and Scott, P.(eds.), London
Mathematical Society Lecture Note Series, Cambridge University Press, 2004, pp. 65–118.
[11] Lafont, Y.: Interaction Nets, Proceedings ofの簡約経路が現れ，強正規化性 (定理 3.4) が失われた．6–8 段目は，(c) weakening-pull-equivalence を追加した．6 段目は push のみ追加した．状態数は41216 個に増加し，終了状態は 16 個となり，合流性(定理 3.3) が失われる結果となった．ただし，全ての簡約経路は有限であった．状態数が大幅に増加した原因としては，weakening の pull は，対象となる ?w
セルが Promotion Box 内に存在するものに限定されているが，push に関しては，対象となる ?w セルがPromotion Box 内に存在しないということのみを要求していて，適用対象となる ?w セルが増加したためである．7 段目は pull のみ追加した．状態数は 756 個に増加し，終了状態は 1 個で，全ての簡約経路は有限であった (定理 3.3，定理 3.4 が成り立っている)．8段目は両方同時に追加した．ルール適用は止まることがなく，状態数は爆発した．つまり，強正規化性 (定理 3.4) が失われる結果となった．
以上のように，ルールの追加と，それに伴う書換え系としての性質の変化を，LMNtal 上で容易に調査することができた．

ax

ax
?n

&

!n ⊗ n

n

n

ax
n

n

?w

?d

?w

?d

?n

?(!n ⊗ n )?(!n ⊗ n )

?n

n

?d
ax

!
ax
?n

n

!n

?n

n

&

⊗
?c
!n ⊗ n?c?n ?(!n ⊗ n )

?n

&

?d

&
n

cut

?(!n ⊗ n ) 
?n

ax

!
?c

!

n

!n

n

⊗

?(!n ⊗ n )?cax

!n ⊗ n

!(?n

&

?w

&

!n n

n

!n ⊗ n

n)

?n
⊗

cut

&
&

?n

n

&
&

?n

!(?n

n

&

&

?(!n ⊗ n )n) ⊗ (!n ⊗ n )

cut

図 29

?ceq

n

Proof Net: (λf ∶ n → n . λx ∶ n . f (f x)) (λx ∶ n . x)

?cpush

表1

各ルール適用時の状態空間?cpull?wpush?wpull

✓
✓
✓
✓

&

?n

✓

the 17th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’90,
New York, NY, USA, Association for Computing
Machinery, 1989, pp. 95–108.
[12] Milner, R.: Bigraphical Reactive Systems, Proceedings of the 12th International Conference on
Concurrency Theory, CONCUR ’01, Berlin, Heidelberg, Springer-Verlag, 2001, pp. 16–35.
[13] Mishina, H. and Ueda, K.: Introducing Quantiﬁcation into a Hierarchical Graph Rewriting Lan-

終了状態数

476

1

476

1

476

1

1808

1

1808

1

41216

16

✓

756

1

✓

∞

—

✓
✓

状態数

guage, 34th International Symposium on LogicBased Program Synthesis and Transformation(LOPSTR 2024), Milano, Italy, September 2024.
[14] Muroya, K.: Hypernet semantics of programming languages, Ph.D. thesis, University of Birmingham, 2020.
[15] Pagani, M. and Falco, L. T. d.: Strong normalization property for second order linear logic, Theoretical Computer Science, Vol. 411, No. 2(2010),
pp. 410–444.

[16] Pinaud, B., Melançon, G., and Dubois, J.:
PORGY: A Visual Graph Rewriting Environment
for Complex Systems, Computer Graphics Forum,Vol. 31, No. 3(2012), pp. 1265–1274. Publisher: Wiley.
[17] Sano, J.: Implementing G-Machine in HyperLMNtal, CoRR, Vol. abs/2103.14698(2021). arXiv:
2103.14698.
[18] Takyu, K. and Ueda, K.: Encoding MELL Cut
Elimination into a Hierarchical Graph Rewriting
Language, The 21st Asian Symposium on Programming Languages and Systems SRC&Posters, 2023.
[19] Ueda, K.: Encoding Distributed Process Calculi
into LMNtal, Electronic Notes in Theoretical Computer Science, Vol. 209(2008), pp. 187–200.
[20] Ueda, K.: LMNtal as a hierarchical logic programming language, Theoretical Computer Science,Vol. 410, No. 46(2009), pp. 4784–4800.
[21] 綾野貴之, 堀泰祐, 岩澤宏希, 小川誠司, 上田和紀: 統
合開発環境による LMNtal モデル検査, コンピュータ
ソフトウェア, Vol. 27, No. 4(2010), pp. 4 197–4 214.
[22] 後町将人, 堀泰祐, 上田和紀: LMNtal 実行時処理系の並列モデル検査器への発展, コンピュータ ソフトウェ
ア, Vol. 28, No. 4(2011), pp. 4 137–4 157.
[23] 工藤晋太郎, 加藤紀夫, 上田和紀: LMNtal 処理系におけるグラフ構造の操作機能の設計と実装, 情報科学技術レターズ, Vol. 4, August 2005, pp. 9–12.
[24] 冨岡太一, 上田和紀: グラフ書換え言語 LMNtal からの C プログラムの自動生成, 日本ソフトウェア科学会
第 34 回大会, 2017.
[25] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal, コンピュータ ソフトウェア, Vol. 25,
No. 1(2008), pp. 1 124–1 150.

A 図 11 に対応する MELL の証明木
図 30 に，図 11 に対応する証明木を示す．

B 全てのカット除去規則
図 31 に，MELL のシークエント計算の全てのカット除去規則を，図 32 に，MELL Proof Nets における全てのカット除去規則を，図 33 に，その LMNtal
エンコードを示す．

(ax)

(!)

(⊗)
(cut)

⊢?(!n ⊗ n ), ?(!n ⊗ n ), ?n , n

⊢?n

&

( )

⊢!(?n

&

( )
n

&

図 30

ax-cut⊢ Γ, A⊢ Γ, A&&⊢ Γ, A⊢ ∆, AB( )⊢ Σ, B ⊢ ∆, Σ, A ⊗ B ⊢ Γ, ∆, Σ
promotion-nested⊢?Γ, A⊢?∆, B, ?A(!)⊢?Γ, !A⊢?∆, !B, ?A⊢?Γ, ?∆, !B
promotion-dereliction⊢?Γ, A⊢?Γ, !Apromotion-weakening

(!)
(cut)

⊢?Γ, !A↝⊢?Γ, !A(!)⊢ ∆, ?A , ?A⊢?∆, ?A⊢?Γ, ?∆(!)⊢?∆, B, ?A⊢?Γ, ?∆, B⊢?Γ?∆, !B

(?d)
(cut)

⊢∆
(?w)
⊢ ∆, ?A(cut)⊢?Γ, ∆↝⊢∆⊢?Γ, ∆(?c)(cut)⊢?Γ, A↝⊢?Γ, !A(!)⊢?Γ, !A⊢?Γ, ∆

図 31

MELL のカット除去規則

(cut)

(?w)

(!)

⊢?∆, ?A , ?A⊢?Γ, ∆, ?A⊢?Γ, ?Γ, ∆

(cut)

(cut)

⊢?Γ, ∆(!)

⊢ Σ, B (!)⊢ ∆, A⊢?Γ, A↝⊢?Γ, A(cut)⊢ Γ, ∆, Σ

promotion-contraction⊢?Γ, A⊢ ∆, A⊢ Γ, ∆, B⊢?Γ, A⊢?Γ, ∆⊢?Γ, !A(⊗)
n⊢ Γ, A

↝

(cut)

↝

(cut)

⊢ ∆, ?A⊢?Γ, An) ⊗ (!n ⊗ n ), ?n

(ax)
n

n

⊢ Γ, A, B(⊗)⊢ ∆, A(!)⊢!n ⊗ n , ?n

図 11 に対応する証明木(ax)⊢ A, A

(!)

n)

(cut)
&

⊢?n

( )

n

⊢!(?n

&⊢?(!n ⊗ n ) ?n

n&⊢?(!n ⊗ n ), ?n(?d)⊢?n , n(?c)⊢?(!n ⊗ n ), ?n , n(ax)⊢ n , n

(?c)

&

n

⊢?(!n ⊗ n ), ?(!n ⊗ n ), ?n , ?n , ntensor-par⊢ Γ, A, B(ax)⊢ n, n

⊢?(!n ⊗ n ), ?n , n, !n ⊗ n&⊢?(!n ⊗ n ), ?n , ?n

(?w)

&

⊢?(!n ⊗ n ), ?n , !n

n

(?w)

&

(?d)

&

&

⊢?(!n ⊗ n ), ?n

⊢?(!n ⊗ n ), ?n , nn&⊢!n ⊗ n , ?n

(?d)

&

⊢?n , n(ax)&⊢ n , n

(?c)

(cut)

(cut)

ax-cut
A

A

ax
A
cut

A

A

tensor-par
A

B

A

&
B

&

A

A

B
⊗

B

A

cut

B
cut

A⊗B
cut

box-nested

A

B

!

A

B

!

?Γ

?A

!A

!

⋯

cut

⋯

?A

!A

!
⋯

?∆ !B

cut

⋯

?Γ

?∆ !B

box-derelection

A
A

cut

!
⋯

?Γ

A

A
?d
⋯

?A

!A

?Γ

cut

box-weakening
?w

?w

A

⋯

?w

⋯
?w

!

?Γ

⋯

?Γ

?A

!A
cut

box-contraction

A

A

!

?A

?A

⋯

?Γ

A

!A

?Γ

?c

!

!A
cut

⋯

?Γ

!

⋯

?c

?A

!A
cut

図 32

?c

⋯

?c

MELL Proof Nets のカット除去規則

?A
cut

?A

1

//// ax-cut

2

ax_cut@@3cut{+X,+Y},ax{+Y,+Z}

4:- X=Z.

56//// tensor-par7

tensor_par@@8

tensor(X1,Y1,XY1),par(X2,Y2,XY2),cut{+XY1,+XY2}

9:- cut{+X1,+X2},cut{+Y1,+Y2}.

10
11// box12//// box-nested

13box_nested@@

14{'!'(X1,X2),$g1[X1|*X],@r1},cut{+X2,+X3},{$g2[X3|*Y],@r2}

15:- {{'!'(X1,X2),$g1[X1|*X],@r1},cut{+X2,+X3},$g2[X3|*Y],@r2}.

16
17//// box-dereliction

18

box_dereliction@@19{'!'(X1,X2),$g[X1|*X],@r},cut{+X2,+X3},'?d'(X4,X3)

20:- cut{+X1,+X4}, $g[X1|*X],@r.

21
22

////

box-weakening

23

box_weakening@@

24{'!'(X1,X2),$g[X1|*X]},cut{+X2,+X3},'?w'(X3)25:- mell.delete(X1,W),{$g[X1|*X]},{'?w'(W)}.

26
27//// box-contration

28

box_contraction@@29{'!'(X1,X2),$g[X1|*X]},cut{+X2,+X3},'?c'({+C1,+C2},X3)

30
31:- mell.copy(X2,A1,A2,A3,B1,B2,C1,C2),{'!'(X1,X2),$g[X1|*X]},{'?c'({+A1,+A2},A3)},{cut{+B1,+B2}}.

図 33

カット除去規則の LMNtal エンコード (full)