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

ハイパーグラフ書き換え系への構文駆動でcompositional な構文・意味論の提案
佐野 仁

上田 和紀

グラフ書換え系における一般的なハイパーグラフの定義は，頂点集合，辺集合，頂点から辺への対応とラベリング
関数などからなり，サブグラフへのマッチングや生成はそれらへの射を用いて定義される．ただし，これは λ 計算
や π 計算のように構文駆動な意味論とは言い難い．そこで，本研究ではグラフ書き換えに基づく計算モデル Flat
LMNtal にプロセス代数における名前の隠蔽の構文・意味論を組み込むことで，ハイパーグラフ書き換え系の構文駆動で compositional な構文・意味論を提案する．また，さらにこの上でいくつかの性質について証明を行い，その妥当性を確認した．

らを形式的に扱うには，ハイパーグラフを第一級に扱

1 はじめにうシンプルで精密な計算モデルがあるのが望ましい．

ハイパーグラフ [3] とは，頂点と 2 つの頂点を接続（ハイパー）グラフを第一級に扱うプログラミングする辺の集合からなるグラフを，辺がそれぞれ 1 つ

言語または計算モデルのパラダイムとしてグラフ書き

以上の頂点を結ぶことができるように拡張したもの

換え系 [4] [13] [12] がある．グラフ書き換え系は，書きである．ハイパーグラフはコンピュータサイエンスに換え規則に基づき，グラフのマッチング及びマッチン

普遍的に出現するデータ構造であり，インターネット

グしたサブグラフの書き換えを行って計算を進める．

などに代表されるようなマクロなネットワーク構造

文献 [3] にあるように，ハイパーグラフは一般的にはから，言語処理系の実装などの低レイヤに至るまで，

頂点 ID の集合（頂点集合）と頂点 ID の集合の多重

多くのものがハイパーグラフを用いて抽象化可能で集合（辺集合）の組で定義される．グラフ書き換え系ある．例えば，C 言語などでのポインタは n (n ≥ 0)における（ハイパー）グラフの定義は様々なバリエー

個のポインタが一つのアドレスを共有するという意味

ションがあるが，典型的には前述したハイパーグラフ

で n (+1) 個の端点を結ぶ，（有向）ハイパーリンクにの定義の派生であり，頂点 ID の集合と辺 ID の集合なっている．関数型言語においては，これらの言語上と辺から頂点への対応に加えて，頂点や辺のラベリで提供されるデータ構造としては木しかないもののング関数などが付随する [4]．書き換え規則は典型的（とはいえ，木もグラフである），その実装においてには (L, K, R) のように，マッチングを行うサブグラ

は，基本的にハイパーグラフを扱う必要がある．これ

フ，書き換え規則における左辺と右辺の頂点や辺の対∗ Introducing a syntax-driven and compositional syn-tax and semantics to hypergraph rewriting system
This is an unrefereed paper. Copyrights belong to
the Author(s).
Jin Sano, Kazunori Ueda, 早稲田大学基幹理工学研究科
情報理工・情報通信専攻, Dept. of Computer Science
and Communications Engineering, Graduate Schoolof Fundamental Science and Engineering, Waseda
University.

応，生成するサブグラフの三つ組からなり，書き換えは，グラフへの射を用いて L とマッチし，K によって保存する頂点や辺やラベルを対応させながら R によって新たなグラフを生成する pushout を行う．
ただし，これは Structural Operational Semantics（SOS） [11] とは大きく異なり，• 構文から直接的に操作的意味論が定義できているわけではない，つまり構文駆動でないため，実

1. 1 本稿の構成際のプログラムとの対応がそこまで自明でない．

まず，2 節で関連研究について述べ，3 節で提案す• 圏論などの数学的素養を要求し，少なくとも一般

る Flat HyperLMNtal の意味論の概要を述べる．次のプログラマにとっては複雑である．

に，4 節でこれを精密に定義する．また，5 節でこの• compositional でない．ここで，compositional

意味論が構文駆動な計算モデルに普遍的に見られる性とは部分から全体を構成可能だという意味であ質を満たすことを検証する．そして，6 節では，これる．先述のようなグラフの定義では，例えば頂点を応用して階層ハイパーグラフ書き換え言語である

集合と辺集合の組からなるグラフを二つ持ってき

HyperLMNtal の形式化を行う．最後に，7 節で本稿たときに，それらの合成がどのように定義されをまとめる．

るのかは自明でないため，素直に compositionalとは言い難い．また，グラフ書き換え系における2 関連研究グラフのマッチングに用いる射は，部分から全グラフ書き換えに基づくプログラミング言語とし体を構成するようなものではないため，これもて，GP 2 [1]，Dactl [6] などが存在する．GP 2 はグcompositional でない．

ラフのマッチングと書き換え以外にもいくつかの制対して，広く受け入れられている計算モデル（λ 計

御構造を持ち，それらに関しては SOS が定義されて算や π 計算 [14] など）はほとんど全て，構文駆動な

いるが，グラフのマッチング及び書き換えは，典型的SOS に基づいて定義されており，構文と直結していなグラフ書き換え系の意味論である double-pushoutてシンプルで，構造的帰納法などを用いることによりapproach [13] に基づくもので，1 節で触れた通り，構性質の証明が比較的しやすいという特徴がある．

文駆動でない．

階層グラフ書き換えに基づく SOS を持つプログラ

Dactl は論理型言語や関数型言語などの項書き換え

ミング言語として，LMNtal が存在する [16]．ただし，に基づく言語のコンパイラのターゲット言語（CTL）

LMNtal におけるグラフの辺（リンク）はハイパーを目指したグラフ書き換え言語である．ここで，Dactl

リンクではないため，端点を高々二つしかもてない．

が計算に用いるグラフは，辺の始点（ノードが持つLMNtal の拡張として，これにハイパーリンクの機能

ポインタ）に全順序のついた有向グラフであり，複数を加えた HyperLMNtal [17] が存在している．ただし，の辺が同じ頂点を始点としてもつことが許されるた

LMNtal には形式的な定義があるが，HyperLMNtal

め，ハイパーグラフとなっている．Dactl においても[17] では LMNtal からの拡張を非形式的に述べていグラフのマッチング及び書き換えはグラフへの射を援るだけにとどまり，精密な意味論を与えているわけで用するものとなっており，構文駆動でない [2]．ここはない．ここで，HyperLMNtal は LMNtal 独自ので，注目に値するのは matching （ルール左辺のマッ機能であるグラフの階層化（膜）などにも対応しておチ），building （ルール右辺のグラフ生成）を行った

り，また通常のリンクとハイパーリンクは区別され，後に redirection を行うことである．Redirection とそれらの接続も可能など，相当に複雑である．

は，他のノードが持つ参照をあるアドレスの方へ向け

そこで，本研究では，LMNtal から階層化の機能を直すことで，これは，無向グラフ書き換え系において省いた計算モデルである Flat LMNtal のリンクを，は，ある辺を他の辺と融合させることに対応する．

プロセス代数の名前の隠蔽の構文・意味論を導入する

Redirection は特に論理型言語や関数型言語の実装

ことで，構文駆動性を保ったままハイパーリンクに拡において普遍的に見られる概念であり，例えば遅延評張した計算モデルとして Flat HyperLMNtal を定義

価を行う関数型言語の仮想機械 G-Machine [8] におい

し，提案する．これはミニマルなハイパーグラフ書きても重要な役割を果たす．G-Machine の実装をハイ換え系の形式的定義になっていると主張する．

パーグラフ書き換え言語 HyperLMNtal [17] を用いて行った研究 [15] では redirection を行うためのノード，

indirection ノードをハイパーリンクの融合を用いてくリンクに関する意味論は相応に複雑になっている．

簡潔に実装できることを示した．従って，ハイパーグ

また，プログラムも複雑化する．

ラフ書き換え系を定式化するにあたって，ハイパーリ
ンクの融合が精密に形式化できることは重要である

3 提案する意味論の概要と言える．

本研究では階層化の機能を省いた LMNtal（Flat

ネットワークを扱う SOS で定義される並行計算モ

LMNtal） をベースに拡張する形でハイパーグラフ書

デルとして， π 計算などが存在する．π 計算はモバ

き換え系を形式化した．LMNtal には connector とイルネットワークをモデル化するために提案された呼ばれる，= を名前（ラベル）に持つ特殊なアトム計算モデルであるから，この意味論がハイパーグラ（ノード）が存在する．これは構造合同規則 (E9) にフ書き換え系と共通項を持つのは自然である．実際，

よって，以下のようにリンクの融合を行う．

文献 [9] においては multi-arc な（ハイパーリンクで

X = Y, P ≡ P [Y /X]

あることを許す） ﬂow graph を用いて例題の説明が（ただし X は P の自由リンク，P はアトム）

なされている．しかし，π 計算はあくまでネットワー
クを介した通信をモデル化する計算モデルであり，グ

ここで，P [Y /X] はリンク代入で，P に出現する全ラフのマッチングや書き換えを行うグラフ書き換えてのリンク X を Y で置き換えるものである．また，系とは異なる．ここで，π 計算を先述した典型的なグあるプロセスにおける自由リンクとはそのプロセスにラフ書き換え系の意味論を用いて定義した研究は存

1 回のみ出現するリンクである．プロセスに 2 回出現

在している [5] ものの，ハイパーグラフ書き換え系をしたリンクは局所リンクと呼ばれる．LMNtal のリ

π 計算の意味論を援用して定式化したという研究はンクはハイパーリンクではないため．高々2 回しか出著者の知る限り存在しない．

現できないという構文制約がある．そのため，このよ

また，π 計算の派生として，Fusion calculus があうに，リンクの出現回数を数えるだけで局所リンク

る [10]．Fusion calculus では π 計算とは異なり，チャ（局所変数）と自由リンク（自由変数）を見分けるこネルを受信する際に受信したチャネルを局所的に束縛とができる．ただし，ハイパーリンクは出現回数に制するのではなく，大域的にそれらのチャネルを同じも限がないため，このように見分けることはできない．

のとする，チャネルの融合（fusion） を行う．Fusion

ハイパーリンク代入もハイパーでないリンクと同様

calculus における fusion はハイパーリンクの融合とに P ⟨Y /X⟩ で，P に出現する全てのハイパーリンク

直に対応する概念であるので，これは重要な関連研

X を Y で置き換えるものと定義したとする．ここ究である．ただし，これはあくまで π 計算の派生でで，ハイパーリンクに局所性を定義できていなかった

あって，グラフ書き換え系の定式化と直に結びつくわ場合は，ハイパーリンクの融合（fusion）がハイパー

けではない．

リンク代入を行うとき，代入すべき全てのハイパーリ

グラフ書き換えに基づく構文駆動な計算モデルかンクを代入し終えたかどうかが判別できない．このたつプログラミング言語として，LMNtal が存在する

め，fusion， ▷◁ に関する構造合同規則を，単純にX ▷◁ Y, P ≡ P ⟨Y /X⟩[16]．ただし，LMNtal におけるグラフの辺（リンク）はハイパーリンクではないため，端点を高々二つしかのように定義すると，例えば，

もてない．LMNtal にはグラフや書き換え規則からなるプロセスを階層化する膜と呼ばれる機能が存在し，この機能を用いてリンクの端点のノードを集約させる
ことによって，ハイパーリンクをエンコードすること(a(X), (X ▷◁ Y, b(X, Y )))(1)(a(Y ), b(Y, Y ))(2)はと構造合同であるべきだが，は可能である．ただし，階層化は単なるハイパーリン(a(X), b(Y, Y ))クの表現よりも強力な機能であるために，特に膜を貫とは構造合同であってはならないはずなのに，これが(3)導出できてしまう．ここで，(2) ≡ (1) ≡ (3) を認めてしまうと，任意の異なるハイパーリンク（この例では X, Y ）を同じハイパーリンクへ書き換えたものと

プロセス

P

構造合同だと言えてしまい，プログラムに出現する全てのハイパーリンクが等しいことが導出できてしまって，グラフ書き換え系としての意味をなさなくなる．
これを防ぐためには，X を Y と融合する（ハイパーリンク代入を行う）ときに P の外で X が出現

::=

0

Null

|

p(X1 , . . . , Xm )Atom, m ≥ 0|(P, P )

Molecule|

νX.P

Hyperlink creation|(P :- P )

Rule

図1

Flat HyperLMNtal の構文

しないという保証 が必要である. ただし，これは「プログラム全体」について言及してしまっているため，

def

fn(0) = ∅m∪deffn(p(X1 , . . . , Xm )) ={Xi }部分だけで意味を定義することができておらず，このままでは compositional でない．また，これは Pi=1の構文から導かれる制約となっておらず，構文駆動で

def

fn((P, Q)) = fn(P ) ∪ fn(Q)

ない．

def

fn(νX.P ) = fn(P ) \ {X}LMNtal では (E9) の付帯条件「ただし X は P の

def

fn((P :- Q)) = ∅自由リンク」が，X が X = Y , P のどちらにも出現していることを要求し，X = Y, P において 局所リ

図2

Flat HyperLMNtal のプロセスの自由ハイパー

ンク であることを保証するので，この問題は発生しリンクの集合ない．
そこで，本研究では，局所リンクと自由リンクと4. 1 Flat HyperLMNtal の構文いう概念を構文駆動かつ compositional にハイパー

4. 1. 1 プロセス

リンクに持ち込むために，λ 計算における λx.E や

Flat HyperLMNtal は二つの構文要素から成り

π 計算における (νx)P (channel creation) のように.

立つ：

明示的なスコープ（hyperlink creation ）を新たな構• X はハイパーリンクを表す．

文として導入することにした．

• p はアトム名を表す. 唯一の予約名は ▷◁ である.

提案する構文・意味論においては，構文 νX.P がFlat HyperLMNtal の構文は図 1 に示される . ア

ハイパーリンク X が P において局所ハイパーリン

トム X ▷◁ Y は fusion と呼び，直感的には引数のハクであることを保証する. そして，LMNtal におけるイパーリンク同士を繋げる機能を持つ. プロセス P(E9) に対応する規則， (E6) はにおける自由ハイパーリンクの集合を fn(P ) で表し，

νX.(X ▷◁ Y, P ) ≡ νX.P ⟨Y /X⟩（ただし X または Y が P に自由出現する）のようになる．

図 2 のように帰納的に定義する.

4. 1. 2 ルール
ルール (P :- Q) において，P はルールの左辺と呼び， Q はルールの右辺と呼ぶ. ルール (P :- Q) は以下に示す条件を満たす必要がある.

4 提案するハイパーグラフ書き換え系の構文と操作的意味論

1. ルールは P に出現してはならない.
2. fn(P ) ⊇ fn(Q).

構文駆動かつ compositional なハイパーグラフ書

二つ目の条件は，直感的には，右辺で新しく出現す

き換え系のミニマムな形式的定義として，以下に述べるハイパーリンクは ν (new) で宣言してやる必要がる Flat HyperLMNtal を提案する．

あると読める．

def

0⟨Y /X⟩ = 0
p(X1 , . . . , Xm )⟨Z/Y ⟩def= p(X1 ⟨Z/Y ⟩, . . . , Xm ⟨Z/Y ⟩) Z
if Xi = Y
def
ただし Xi ⟨Z/Y ⟩ = Xi if Xi ̸= Y

(E1)

(0, P ) ≡ P(E2)(P, Q) ≡ (Q, P )(E3)(P, (Q, R)) ≡ ((P, Q), R)(E4)

P ≡ Q ⇒ (P, R) ≡ (Q, R)(E5)

P ≡ Q ⇒ νX.P ≡ νX.Q

(E6)

(P, Q)⟨Y /X⟩ = (P ⟨Y /X⟩, Q⟨Y /X⟩)
def

(νX.P )⟨Z/Y ⟩ =
νX.P
if X = YνX.P ⟨Z/Y ⟩if X ̸= Y ∧ X ̸= Z
νW.(P ⟨W/X⟩)⟨Z/Y ⟩ if X ̸= Y ∧ X = Z




∧W ∈
/ fn(P ) ∧ W ̸= Z
def

(P :- Q)⟨Y /X⟩ = (P :- Q)
図3

Flat HyperLMNtal のハイパーリンク代入

νX.(X ▷◁ Y, P ) ≡ νX.P ⟨Y /X⟩（ただし X ∈ fn(P ) ∨ Y ∈ fn(P )）

def

(E7)

νX.νY.X ▷◁ Y

≡ 0

νX.0 ≡ 0

(E8)
(E9)

νX.νY.P≡ νY.νX.P

νX.(P, Q) ≡ (νX.P, Q)(E10)（ただし X ∈/ fn(Q)）
図4

Flat HyperLMNtal プロセスの構造合同

たときのためで，これがないと，例えば

νX.(X ▷◁ X, a(X)) ≡ a(X)
4. 2 Flat HyperLMNtal の操作的意味論となり，この例では，左辺では自由ハイパーリンクはまず，プロセス間の構造合同規則 (≡) を定義し，出現しないが，右辺では X が自由ハイパーリンクとそれを用いて遷移関係 (−→) を定義する.

なり，≡ の両辺で自由ハイパーリンク（自由変数）の集合が変化してしまう．これは構文駆動な計算モデル

4. 3 構造合同規則

においては望ましくない性質であるため，νX. を規≡ を図 4 の関係を満たすプロセス上の最小の同値則の右辺にも補っている．

関係として定義する. ただし， P ⟨Y /X⟩ はハイパー

同様に，付帯条件「ただし X ∈ fn(P )∨Y ∈ fn(P )」リンク代入であり，これは図 3 に示されるように，全も構造合同なプロセス間で自由ハイパーリンクの集ての自由出現する X を Y で置き換えるものである.

合が等しくなるようにするためである．この付帯条件

ここで， X が Y に置き換えられた時に自由出現しがないと，例えば，ない場所に出現しているときは，事前に α 変換が必

νX.(X ▷◁ Y, a) ≡ a

要になる可能性があることに注意する. また， 以降，が導出でき，この例では左辺では自由ハイパーリンク

Flat HyperLMNtal の意味論の記述においては， =Y が出現するが，右辺では自由ハイパーリンクは出をプロセスや構文要素が構文的に等しいという意味

現せず，≡ の両辺で自由ハイパーリンクの集合が変で用いる.

化してしまう．

(E1)–(E4) は LMNtal と全く同様である．(E5) は
ν を構造合同関係にするための規則である(E6)，(E7) は fusion のための規則で，これが本研究における核心部分である．(E6) の左辺において，

こういったコーナーケースがいくつか存在したため，≡ の関係にあるプロセス間において，自由ハイパーリンクの集合が等しいということは，定理 3 において証明した．

νX. が必要な理由はすでに第 3 節において説明した

ただし，この付帯条件のために，ハイパーリンク

通りである．この右辺において νX. が必要なのは，が ▷◁ の両辺にしか出現しない場合に，(E6) のみで

X と Y がどちらも同じ名前のハイパーリンクであっは fusion を吸収できない．そこで，このケースに対応するためにさらに (E7) を用意した．ここで，(E7)P −→ P ′(P, Q) −→ (P ′ , Q)

(R1)

P −→ P ′νX.P −→ νX.P ′(R2)P −→ P ′Q −→ Q′P ′ ≡ Q′

(R3)

Q≡P

(R4)

(P, (P :- Q)) −→ (Q, (P :- Q))

図5

Flat HyperLMNtal プロセスの遷移関係

用いて νY.(Y ▷◁ X, p(X, Y )) の形に変換できる．
従って，これは以下のように遷移が可能である(p(X, X), (p(X, Y ) :- q(X, Y )))≡補題 1 νY.(p(X, X), (p(X, Y ) :- q(X, Y )))≡E6 νY.(Y ▷◁ X, (p(X, Y ), (p(X, Y ) :- q(X, Y ))))−→ νY.(Y ▷◁ X, (q(X, Y ), (p(X, Y ) :- q(X, Y ))))
≡E6 νY.(q(X, X), (p(X, Y ) :- q(X, Y )))≡補題 1 (q(X, X), (p(X, Y ) :- q(X, Y )))このように，fusion に関する構造合同関係を援用することによって，自由ハイパーリンクのマッチン

も X と Y が同じハイパーリンク名のときも適用可グ，特に非単射的マッチングも可能である．

能であることに注意されたい．

(E8)–(E10) は ν のための規則で，これらは π 計
算などの並行計算モデルにおいて普遍的に見られる

5 Flat HyperLMNtal の性質
λ 計算や π 計算は，α 変換が（構造）合同性を保つことや，自由変数の集合が（構造）合同なプロセ規則である．

変換による合同関係は他の定義から導出可能であったス間で変化しないこと，自由変数の集合が遷移に伴い広義単調に減少することといった性質を満たす †1 ．

のであえて定義せず，定理 1 としてのちに証明する．

これらは構文駆動な計算モデルにおいて普遍的な性

Flat HyperLMNtal では局所ハイパーリンクの α

質だと言える．そこで，この節では，これらの性質が4. 4 遷移関係

Flat HyperLMNtal においても成り立つことを証明

プロセス間の遷移関係 −→ を図 5 を満たす最小のする．

関係として定義する.
計算モデル，プログラミング言語の意味論においては，関数の仮引数と実引数，ルールとグラフのハ
イパーリンクの対応などの，マッチングする際の変数の対応がきちんと定義できていることが重要である．Flat HyperLMNtal の場合は局所ハイパーリン

5. 1 構造合同規則に関する性質の証明
提案した Flat HyperLMNtal の構造合同規則ではLMNtal における構造合同規則と比較して• (E4) P ≡ P [Y /X](ただし X は P の自由リンク)

クは α 変換可能であることを後で示すものの，自由• (E8) X = Y ≡ Y = X

ハイパーリンクは α 変換できないため，これが正しに対応するものが欠けている．

くマッチングできるように定義されているかが鍵とこれはこれらの規則が他の規則から導出できるこなってくる．

と，すなわち admissible であることがわかったため

では，ルールである．これらを定理 1 と定理 2 に示す. また，そ(p(X, Y ) :- q(X, Y ))れらの定理を用いて自由ハイパーリンクの集合が合がアトム p(X, X) を書き換えることは可能であろう

同なプロセス間で変化しないことを定理 3 に示す.

か．より正確には，

補題 1 (自由出現しないハイパーリンクを束縛する ν(p(X, X), (p(X, Y ) :- q(X, Y )))は遷移することが可能か．ルールは(p(X, X) :- . . .)のような形に α 変換することはできない．しかし，アトム p(X, X) は (E7) とのちに証明する補題 1 をの除去).

νX.P ≡ P where X ∈/ fn(P )†1 ただし，π 計算では，構造合同規則 Sc-Mat においてのみ，構造合同なプロセス間で自由変数の集合が変化する可能性がある [14]

Proof.

νX.νY.(Y ▷◁ X, (X ▷◁ Y, P ))
νX.P
≡E5

νX.(0, P )∵ P ≡E1 (0, P )≡E10(νX.0, P )∵X∈/ fn(P )≡E4(0, P )

∵ νX.0 ≡E8 0≡E1

P≡E5, E3 νX.νY.((Y ▷◁ X, X ▷◁ Y ), P )≡E5, E10 νX.(νY.(Y ▷◁ X, X ▷◁ Y ), P )∵Y ∈/ fn(P )≡E5, E6 νX.(νY.X ▷◁ X, P )∵ (X ▷◁ Y )⟨X/Y ⟩ = X ▷◁ X

補題 2 (同じハイパーリンクを代入しても構文的に等しい).

≡E5, E10 νX.νY.(X ▷◁ X, P )∵Y ∈/ fn(P )≡E9 νY.νX.(X ▷◁ X, P )P ⟨X/X⟩ = P
これは見かけほどは自明ではない．なぜなら，ハ
イパーリンク代入を行う際に α 変換をされてしまい，
合同ではあるが構文的には異なるプロセスになってしまう可能性が素朴には否定できないからである．

≡E6, 補題 2 νY.νX.P∵ P ⟨X/X⟩ = P≡補題 1 νX.P
∵Y ∈/ fn(P )であり，またProof. プロセスにおいて，構造帰納法を用いて証明する．ここで， 0， p(X1 , . . . , Xm )，(P, Q)，(P :- Q)の場合は帰納法の仮定より明らかである．

Case νY.P :def(νY.P )⟨X/X⟩ = νY.P

if Y = X

νY.P ⟨X/X⟩ if Y ̸= X
 = νY.P ∵ 帰納法の仮定

Y ̸= X ∧ Y = X は絶対に起こり得ないた
め, 変数捕捉の回避のために α 変換（これにνX.νY.(Y ▷◁ X, (X ▷◁ Y, P ))≡E2, E3, E5, E9 νY.νX.(X ▷◁ Y, (Y ▷◁ X, P ))≡E5, E6 νY.νX.(Y ▷◁ Y, P ⟨Y /X⟩)
≡E5, 補題 1 νY.(Y ▷◁ Y, P ⟨Y /X⟩)∵X∈
/ fn((Y ▷◁ Y, P ⟨Y /X⟩))≡E6 νY.P ⟨Y /X⟩∵ 補題 2 より (P ⟨Y /X⟩)⟨Y /Y ⟩ = P ⟨Y /X⟩
であるため，νX.P ≡ νY.P ⟨Y /X⟩

Case X ∈/ fn(P ) :より構文的な等しさが失われる可能性があっこの場合においては，(E7) を用いて，まずた）を行う可能性はない．

自由ハイパーリンク X を付加させることで，先の証明を活用する．

定理 1 (α 同値).

νX.P ≡ νY.P ⟨Y /X⟩ where Y ∈/ fn(P )Proof. この証明には補題 1 と補題 2 を用いる.

νX.P≡補題 1 P
≡E1 (0, P )代入される自由ハイパーリンクが出現している場≡E4, E7 (νX.νX.X ▷◁ X, P )合としていない場合に分けて証明を行う．後者は自明≡E4, 補題 1 (νX.X ▷◁ X, P )に思えるが，ハイパーリンク代入による α 変換が起∵X∈
/ fn(νX.X ▷◁ X)

きる可能性があるため，これは自明ではない．前者を先に証明し，前者を用いることのできる形に変形してやることで証明を行う．

Case X ∈ fn(P ) :≡E10 νX.(X ▷◁ X, P )∵X∈/ fn(P )≡先の証明 νY.(X ▷◁ X, P )⟨Y /X⟩∵ X ∈ fn((X ▷◁ X, P ))= νY.(Y ▷◁ Y, P ⟨Y /X⟩)≡E10 (νY.Y ▷◁ Y, P ⟨Y /X⟩)∵X∈
/ fn(P ) なので Y ∈/ fn(P ⟨Y /X⟩)
≡E4, 補題 1 (νY.νY.Y ▷◁ Y, P ⟨Y /X⟩)

定理 3 (構造合同なプロセスにおける自由ハイパーリ
ンクの集合の等価性).

fn(P ) = fn(Q) if P ≡ Q≡E7 (0, P ⟨Y /X⟩)

Proof. 構造合同規則とプロセスにおいて構造帰納法≡E1 P ⟨Y /X⟩

を用いて証明を行う．

≡補題 1 νY.P ⟨Y /X⟩
ここで，定理 1 の証明に (E1)–(E10) の全ての構
造合同規則を用いていることは注目に値する．定理 1
やこれから述べる定理 2 が構造合同規則から導出できることにより，LMNtal における規則（グラフ書き
換え系に必要な規則）が全て導出できること，つまCase (0, P ) ≡ P :fn((0, P )) = fn(0) ∪ fn(P ) = fn(P )Case (P, Q) ≡ (Q, P ) :fn((P, Q)) = fn(P ) ∪ fn(Q) = fn(Q) ∪fn(P ) = fn((Q, P ))Case (P, (Q, R)) ≡ ((P, Q), R) :り，定義した構造合同規則が十分であることはわかる．

fn((P, (Q, R))) = fn(P ) ∪ fn(Q) ∪ fn(R) =が，これらが必要であること，つまり admissible なfn(((P, Q), R))

規則が存在しないことを証明するのは難しい．実際に，Case P ≡ P ′ ⇒ (P, Q) ≡ (P ′ , Q) :LMNtal においては構造合同規則 (E8) が admissible

帰納法の仮定より fn(P ) = fn(P ′ ) if P ≡ P ′であることは，本研究で初めて示された（以下に述べであるのでる定理 2 とほぼ同じように証明できる）．しかし，定fn((P, Q)) = fn(P ) ∪ fn(Q) = fn(P ′ ) ∪理 1 の導出において定義した全ての構造合同規則を

fn(Q) = fn((P ′ , Q))

用いたことは，提案する意味論における構造合同規則
がどれも必要であるということの直感的な根拠を与えるものである．
定理 2 (▷◁ の対称性).

X ▷◁ Y ≡ Y ▷◁ X
Proof.

Case P ≡ P ′ ⇒ νX.P ≡ νX.P ′ :
帰納法の仮定より fn(P ) = fn(P ′ ) if P ≡ P ′であるのでfn(νX.P ) = fn(P )\{X} = fn(P ′ )\{X} =fn(νX.P ′ )Case νX.(X ▷◁ Y, P ) ≡ νX.P ⟨Y /X⟩ （ た だ しνZ.(Z ▷◁ X, Z ▷◁ Y )≡E6 νZ.(X ▷◁ Y )∵ (Z ▷◁ Y )⟨X/Z⟩ = X ▷◁ Y
≡補題 1 X ▷◁ Y
であり，またνZ.(Z ▷◁ X, Z ▷◁ Y )≡E2, E5 νZ.(Z ▷◁ Y, Z ▷◁ X)≡E6 νZ.(Y ▷◁ X)∵ (Z ▷◁ X)⟨Y /Z⟩ = Y ▷◁ X
≡補題 1 Y ▷◁ X
従って，X ▷◁ Y ≡ Y ▷◁ X.

X ∈ fn(P ) ∨ Y ∈ fn(P )） :付帯条件より, fn(P ⟨Y /X⟩) は(fn(P ) \ {X}) ∪ {Y } と等しい．
従って,fn(νX.(X ▷◁ Y, P ))= (fn(P ) ∪ {Y }) \ {X}= ((fn(P ) \ {X}) ∪ {Y }) \ {X}= fn(P ⟨Y /X⟩) \ {X} = fn(νX.P ⟨Y /X⟩)
Case νX.νY.X ▷◁ Y ≡ 0 :fn(νX.νY.X ▷◁ Y )= fn(X ▷◁ Y ) \ {X, Y }= {X, Y } \ {X, Y } = ∅ = fn(0)Case νX.0 ≡ 0 :fn(νX.0) = ∅ \ {X} = ∅ = fn(0)Case νX.νY.P ≡ νY.νX.P :Case (P, (P :- Q)) −→ (Q, (P :- Q)) :fn(νX.νY.P ) = (fn(P ) \ {Y }) \ {X} =ルールの二つ目の構文条件により fn(P ) ⊇(fn(P ) \ {X}) \ {Y } = fn(νY.νX.P )fn(Q) であるのでCase νX.(P, Q) ≡ (νX.P, Q) （ただし X ∈/ fn(Q)）:
fn(νX.(P, Q))

fn((P, (P :- Q))) = fn(P ) ⊇ fn(Q) =fn((Q, (P :- Q)))= (fn(P ) ∪ fn(Q)) \ {X}= (fn(P ) \ {X}) ∪ fn(Q)∵X∈/ fn(Q)= fn((νX.P, Q))

6 HyperLMNtal の構文・意味論
この節では構文駆動な意味論を持つ階層グラフ書き
換え言語 LMNtal へハイパーリンクを形式的に組み込む．Flat LMNtal は非常にミニマルな計算モデル

5. 2 遷移規則に関する性質の証明
提案する意味論において，プロセスの自由ハイパー
リンクは遷移に伴い，単調に減少することを 定理 4で示す. つまり，これは新たな自由ハイパーリンクが遷移に伴い出現することがないことを保証するものである．
定理 4 (プロセスの遷移に伴う自由ハイパーリンクの広義単調減少性).

であったが，LMNtal は「実用プログラミング言語」
としての側面が強く [18]，（ほとんどの他の実用プログ
ラミング言語よりは遥かに簡明であるものの）表現力の高さと引き換えに意味論は相応に複雑になっている．

LMNtal には，Flat LMNtal の諸機能に加えて，「膜」と呼ばれるプロセスの階層化の機能が存在する．
膜を貫く自由リンクに関する意味論は相応に複雑でfn(P ) ⊇ fn(Q) if P −→ Q

あり，また膜の中の書き換え規則の集合にマッチする

Proof. プロセスと遷移関係において構造帰納法を用

ルール文脈や膜の中の残りのグラフにマッチするプロ

いて証明する．

セス文脈などの複雑なパッターンマッチのための構文

P −→ P ′Case:(P, Q) −→ (P ′ , Q)や意味論が付随する．

帰納法の仮定より fn(P ) ⊇ fn(P ′ ) if P −→P ′ であるのでfn((P, Q)) = fn(P ) ∪ fn(Q) ⊇ fn(P ′ ) ∪fn(Q) = fn((P ′ , Q))

実装したものであり，これは通常のリンクの直接的な拡張ではない．この特殊なアトムはハイパーリンク

性判定 [7] などを行う．これは処理系からすると単な帰納法の仮定より fn(P ) ⊇ fn(P ′ ) if P −→P ′ であるのでfn(νX.P ) = fn(P )\{X} ⊇ fn(P ′ )\{X} =fn(νX.P ′ )Casetal に特殊な単引数のアトムとしてハイパーリンクをの ID を持ち，これを用いてマッチングやグラフ同型

P −→ P ′Case:
νX.P −→ νX.P ′Q≡P

さらに，現実装の HyperLMNtal は 通常の LMN-

るアトムとも取れるため，通常のリンクと接続することも可能であるし，通常の自由リンクで，通常のリンクの先でハイパーリンクと接続されたグラフをマッチングすることも可能である．これを定式化するためには，ハイパーリンクをリンクの拡張ではなく，アトP −→ P ′Q −→ Q′P ′ ≡ Q′:

帰納法の仮定よりfn(P ) ⊇ fn(P ′ ) if P −→ P ′ であり，また定理 3 から fn(Q) = fn(P ) if Q ≡ P かつ

fn(P ′ ) = fn(Q′ ) if P ′ ≡ Q′ であるのでfn(Q) = fn(P ) ⊇ fn(P ′ ) = fn(Q′ )ムと同じような構文要素として定義する必要がある．
本節ではそのように複雑な SOS を持つプログラミ
ング言語においても，提案する意味論が容易に組み込めることを確認する．

6. 1 HyperLMNtal の抽象構文
HyperLMNtal の構文要素を三つで定める：• 通常のリンク名 X ．
• ハイパーリンク名 H ．ただし，ハイパーリンク
は通常のリンクと区別するために基本的に ! をつけて表記される．

• アトム名 p．アトム名の予約名は = と ▷◁ である.
抽象構文を図 6 で与える. ここで，LMNtal に新しく追加された構文要素を † で示す. また，LMNtal とプロセス

P ::= 0Null

| p(X1 , . . . , Xm )Atom, m ≥ 0| (P, P )Molecule| {P }Cell| νH.P

Hyperlink creation †| !H(X)

Hyperlink †| (T :- T )Rule

同様の略記法を扱えるものとする．詳細は文献 [16] をプロセステンプレート

参照されたい．例えば，省略しても曖昧さの残らない括

T ::= 0Null

弧は省略可能である．また， !H1 (X), X ▷◁ Y, !H2 (Y )| p(X1 , . . . , Xm )Atom, m ≥ 0

は !H1 ▷◁ !H2 のように略記できる．

| (T, T )Molecule

HyperLMNtal のプロセスに出現する自由ハイパー| {T }

Cell

リンクの集合を図 7 のように定義する．また，プロ| νH.T

Hyperlink creation †セステンプレートにおける自由ハイパーリンクも同| !H(X)

Hyperlink †様に定義する．ここで，通常のリンクとハイパーリン| (T :- T )Ruleクの名前空間は別であることに注意されたい．例えば| @p

Rule context「X が P の自由リンクである」といったときは，プ| $p [X1 , . . . , Xm |A]

Process context,m≥0

ロセス P において通常のリンクがただ一回のみ出現
したことを表し，そのプロセスにおけるハイパーリンクの出現に関しては全く言及していない．
また，LMNtal と Flat HyperLMNtal における構
文条件をどちらとも満たさなくてはいけない．例えば，通常のリンクの出現数は高々2 回のみでなくてはリンク束

A ::= [ ]

Empty

| *X

Bundle
図6

HyperLMNtal の構文ならない．また，ルール T :- U は fn(T ) ⊇ fn(U )を満たさなくてはならない.

ス文脈やルール文脈などのマッチングに利用される．
この詳細は文献 [16] を参照されたい．ただし，ここ

6. 2 HyperLMNtal の構造合同規則

で，プロセス文脈はハイパーリンクにマッチ可能であ

図 9 は HyperLMNtal のプロセスにおける構造合るが，hyperlink creation を含むプロセスにはマッチ

同規則を示す. LMNtal から新しく追加された規則

可能でないものと定義する．これによって，プロセスは † で示した. ここで，P [Y /X] は通常のリンクの文脈を用いたプロセスのコピーにおいてハイパーリ

代入を示し，通常のリンク X を通常のリンク Y でンクは新しく生成されることなく，元のものから共有置き換えるものである．対して，P ⟨H2 /H1 ⟩ は 表 8されることになる．

に定義されるようなハイパーリンク代入である．Flat

HyperLMNtal において既に議論されたように事前の7 まとめ

α 変換が要求される可能性があることに注意する.

本論文では，プロセス代数における隠蔽の構文・

図 10 は HyperLMNtal の遷移関係を示す. 新しく意味論をグラフ書き換えに基づく計算モデル Flat

追加された遷移規則は † で示す. 規則 (R7) における

LMNtal に組み込むことで，ハイパーグラフ書き換

θ はルールのマッチングにおける置換を表し，プロセ

え言語 Flat HyperLMNtal の構文・意味論を定義しdef

fn(0) = ∅deffn(p(X1 , . . . , Xm )) = ∅def

fn((P, Q)) = fn(P ) ∪ fn(Q)deffn({P }) = fn(P )(E1)0, P ≡ P(E2)

P, Q ≡ Q, P

(E3)

P, (Q, R) ≡ (P, Q), R(E4)

P ≡ P [Y /X]

def

fn(νH.P ) = fn(P ) \ {H}deffn(!H(X)) = {H}def

fn((P :- Q)) = ∅
図7

HyperLMNtal プロセスの自由ハイパーリンクの集合（ただし X は P の局所リンク）(E5)

P ≡ P ′ ⇒ P, Q ≡ P ′ , Q(E6)

P ≡ P ′ ⇒ {P } ≡ {P ′ }(E7) †P ≡ Q ⇒ νH.P ≡ νH.Q

(E8)

X=X≡0

(E9)

X = Y, P ≡ P [Y /X]（ただし P はアトム，X は P の自由
リンク）

def

0⟨H2 /H1 ⟩ = 0{X = Y, P } ≡ X = Y, {P }

(E10)
def

p(X1 , . . . , Xm )⟨H2 /H1 ⟩ = p(X1 , . . . , Xm )（ただし X または Y のどちらか一方が P の自由リンク）

def(P, Q)⟨H2 /H1 ⟩ = (P ⟨H2 /H1 ⟩, Q⟨H2 /H1 ⟩)(νH.P )⟨H2 /H1 ⟩
νH.P
if H = H1νH.P ⟨H2 /H1 ⟩




def
if H ̸= H1 ∧ H ̸= H2
=


νH
.(P
⟨H
/H⟩)⟨H
3
3
2 /H1 ⟩

if H ̸= H1 ∧ H = H2

∧ H3 ∈/ fn(P )∧H3 ̸= H2
 !H (X) if H = H
21
def!H(X)⟨H2 /H1 ⟩ = !H(X) if H ̸= H1
def(P :- Q)⟨H2 /H1 ⟩ = (P :- Q)
図8

HyperLMNtal のハイパーリンク代入(E11) † νH1 .(!H1 ▷◁ !H2 , P ) ≡ νH1 .P ⟨H2 /H1 ⟩（ただし H1 ∈ fn(P ) ∨ H2 ∈ fn(P )）(E12) † νH1 .νH2 .(!H1 ▷◁ !H2 ) ≡ 0(E13) † νH.0 ≡ 0(E14) † νH1 .νH2 .P ≡ νH2 .νH1 .P(E15) † νH.{P } ≡ {νH.P }(E16) † νH.(P, Q) ≡ (νH.P, Q)（ただし H ∈/ fn(Q)）
図9

HyperLMNtal プロセスの構造合同

ると思われるが，一番の原因はそのコア部分に広く普及している計算モデルの意味論（SOS）が適用できていなかったことだと考える．しかし，このようにハイパーリンクの融合も第一級に扱う強力なハイパーグ

た．これは構文から直接的に操作的意味論を定義でき

ラフ書き換え言語として，ミニマムな SOS を定義しており，圏論などの深い数学的素養を要求せず，一般

たことによって，ハイパーグラフ書き換え系の普及及のプログラマにとってもシンプルでわかりやすい定義

び，SOS を持つ他の計算モデルやプログラミング言となっていると主張する．また，これが他の構文駆動

語への組み込みが容易になると主張する．

な計算モデルに普遍的に見られる性質を持つことを謝 辞 本 研 究 の 一 部 は ，科 学 研 究 費 基 盤 研 究 (B)証明し，SOS を持つより複雑なプログラミング言語

18H03223 の助成を受けて実施した．

に容易に組み込むことが可能であることを示した．
グラフ書き換え言語は現状，研究者にとっても，広く受け入れられているプログラミングパラダイムとは言いがたい．これには実装上の効率などの要因もあ

参 考 文 献[ 1 ] Bak, C.: GP 2: Eﬃcient Implementation of a
Graph Programming Language, PhD Thesis, Uni-

(R1)P −→ P ′P, Q −→ P ′ , Q(R2)

P −→ P ′{P } −→ {P ′ }(R3) †

P −→ P ′νH.P −→ νH.P ′

(R4)

Q≡P

P −→ P ′ P ′ ≡ Q′
Q −→ Q′(R5){X = Y, P } −→ X = Y, {P }（ただし X と Y は {X = Y, P }の自由リンク）(R6)

X = Y, {P } −→ {X = Y, P }（ただし X と Y は P の自由リンク）(R7)

T θ, (T :- U ) −→ U θ, (T :- U )図 10HyperLMNtal プロセスの遷移関係

versity of York, September 2015.
[ 2 ] Banach, R.: DACTL Rewriting is Categorical,
Computer Science Department, Manchester University, 1991.
[ 3 ] Claude, B.: Hypergraphs: Combinatorics of Finite Sets, Elsevier Science Publishers B.V., USA,1989.
[ 4 ] Ehrig, H., Ehrig, K., Prange, U., and Taentzer,
G.: Fundamentals of Algebraic Graph Transformation (Monographs in Theoretical Computer Science.
An EATCS Series), Springer, 2006.
[ 5 ] Gadducci, F.: Graph rewriting for the πcalculus, Mathematical Structures in Computer Science, Vol. 17, No. 3(2007), pp. 407–437.
[ 6 ] Glauert, J., Kennaway, J., and Sleep, M.: Dactl an Experimental Graph Rewriting Language, Proc.

Graph Grammars 1990, LNCS, Vol. 532, Springer,
1991, pp. 378–395.
[ 7 ] Gocho, M., Hori, T., and Ueda, K.: Evolution of
the LMNtal Runtime to a Parallel Model Checker,
Computer Software, Vol. 28, No. 4(2011), pp. 4 137–
4 157.
[ 8 ] Kieburtz, R. B.: The G-machine: A fast, graphreduction evaluator, Functional Programming Languages and Computer Architecture, Springer Berlin
Heidelberg, 1985, pp. 400–413.
[ 9 ] Milner, R., Parrow, J., and Walker, D.: A calculus of mobile processes, I, Information and Computation, Vol. 100, No. 1(1992), pp. 1–40.
[10] Parrow, J. and Victor, B.: The fusion calculus:
expressiveness and symmetry in mobile processes,
Proc. LICS 1998, 1998, pp. 176–185.
[11] Plotkin, G.: A Structural Approach to Operational Semantics, J. Log. Algebr. Program., Vol. 6061(2004), pp. 17–139.
[12] Raoult, J. C.: On graph rewritings, TheoreticalComputer Science, Vol. 32, No. 1(1984), pp. 1–24.
[13] Rozenberg, G.: Handbook of Graph Grammars
and Computing by Graph Transformation, World
Scientiﬁc, 1997.
[14] Sangiorgi, D. and Walker, D.: The Pi-Calculus:
A Theory of Mobile Processes, Cambridge University Press, 2001.
[15] Sano, J.: Implementing G-Machine in HyperLMNtal, Bachelor’s thesis, Waseda University,
2021. https://arxiv.org/abs/2103.14698.
[16] Ueda, K.: LMNtal as a hierarchical logic programming language, Theoretical Computer Science,Vol. 410, No. 46(2009), pp. 4784–4800.
[17] Ueda, K. and Ogawa, S.: HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model,
KI - Künstliche Intelligenz, Vol. 26, No. 1(2012),
pp. 27–36.
[18] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal, コンピュータ ソフトウェア, Vol. 25,
No. 1(2008), pp. 124–150.