グラフ書き換え言語 LMNtal の紹介

この記事は Wathematica Advent Calender 2023 のために書かれたものです。

はじめに

こんにちは。ワセマの幽霊サークル員です。というかなにかの申請を出し忘れたので、よそ者の可能性すら大いにあります。へへ

全くゼミに参加していなくて書くものがないため、所属している研究室で扱っている言語を軽く紹介および宣伝しようと思います。

大変おこがましいなとは思っております。でも本当に思いつかなかったのでこれでいかせてくださいすみません......見逃してください...... あと偉大な先輩方の作った紹介資料を参考にしまくってしまいすみません.......もしこれ読んでなんか間違ってると思ったら教えてください......

グラフ書き換え言語 LMNtal とは？

見出しのリンクから飛べるページを読んでわかる人はそっち読んだほうがいいと思います♡♡♡

グラフ書き換え言語とは、グラフを書き換える言語です😀

グラフと言っても、棒グラフとか折れ線グラフとかそういったグラフではなく、ノードとエッジから成るグラフ理論の方のグラフです。

LMNtalはグラフ構造とグラフ構造に対する書き換えルールを記述することで非決定的に書き換えを行うことができます。（ちなみに、エレメンタル、と読みます。）

多分何を言っているかわからないと思うので、具体例を見ていきましょう。

実際にLMNtalを触りながら読みたい人は、統合開発環境であるLaViTを入れてください。（laViTの使い方）

LMNtal の記法

以下ではPrologのシンタックスハイライトを利用しているのでところどころ変ですが、気にしないでください。

アトムとリンク

LMNtalでは、ノードにあたるものはアトム、エッジにあたるものはリンクと呼ばれます。アトム名は小文字から、リンク名は大文字から始まります。

例えば、リンクを持たないアトム a が2つと b が1つほしいとき、以下のように書きます。

a, a, b.

次に、a アトムと b アトムが1本のリンクでつながっているとき、以下のように書きます。

a(X), b(X).

図を見てもらうとわかるように、リンクは無向です。（書き方によって向きを表すこともできます。）

ここで、以下のようにリンク名を変更しても同じグラフが得られます。

a(Y), b(Y).

ここで問題です。以下のように書いた2つのグラフは同じでしょうか？

% graph 1
a(X, Y), b(X), c(Y).
% graph 2
a(X, Y), c(X), b(Y).

実は、アトムにつながっているリンクには順序があります。

graph 1 の場合には a の 0番目のリンクに b、1番目のリンクに c がつながっていますが、graph 2 の場合には a の 0番目のリンクには c, 1番目のリンクには b がつながっています。

したがって、この2つのグラフは異なります。

ルール

書き換え規則は、ルールと呼ばれます。

書き換え前のグラフ :- 書き換え後のグラフ. と書くと、書き換え前のグラフにマッチしたグラフが書き換えられます。

以下のLMNtalコードを実行すると、どんなグラフが得られるでしょうか？

% graph
a. b(X), c(X).
% rule
b(Y), c(Y) :- d.

1本のリンクでつながった b と c が d に書き換わります。前述のように、リンク名は気にしなくてよいです。

  • 書き換え前

  • 書き換え後

では、以下のコードを実行すると何が起こるでしょうか？書き換え前のグラフは先程と同じです。

% graph
a. b(X), c(X).
% rule
b, c :- d.

このコードを実行しても、ルールは発火しません。なぜなら、リンクを持たない b アトムと c アトムにマッチするものはないからです。

したがって、コードを実行しても書き換えは起こらず、グラフはそのままです。

カンマ・ピリオド・:-

カンマ > ピリオド > :- の順に結合力が高くなります。ピリオドは、ルールとそれ以外を区切ることができます。

したがって、以下の2つのコードは同じです。

% graph 1
a. b. c(X), d(X).
% graph 2
a, b. d(Z), c(Z).

しかし、以下の2つのコードは異なるグラフ及びルールを表します。どう違うのでしょうか？

% pattern 1
a. b :- c.
% pattern 2
a, b :- c.

pattern 1を構成するものは、

  • a というアトム
  • b 1つを c 1つに書き換えるルール

であるのに対し、pattern 2を構成するものは、

  • a と b 1つずつを c 1つに書き換えるルール

となっています。カンマのほうがピリオドより結合力が高いためです。

自由リンク・アトムの埋め込み・コネクタ

接続先が指定されていないリンクは自由リンクと呼ばれます。

以下のようにルールを記述することで、リンクのつながっている先が何であっても書き換えることができます。

% graph
a(X), c(X).
% rule
a(X) :- b(X).
  • 書き換え前

  • 書き換え後

ここでの注意点は、普通のリンクは2つのものをつなぐことしかできないということです。

グラフにおいて、同じリンクは3回以上使用できません。 ルールにおいて、同じリンクは左辺または右辺だけに2回登場するか、左辺と右辺に1回ずつだけ登場する形になります。

% OK
a(X), b(X), c(Y), d(Y).
a(X, Y) :- b(X), c(Y).

% NG
a(X), b(X), c(X).
a(X) :- b.
a(X), b(X) :- c(X).
a(X) :- a(Y).

ここで、先程 OK 側に書いたグラフを見てみましょう。アトムの引数には、実はリンクだけではなく、アトムを直接書くこともできます。

また、コネクタ = を使用することで、アトムとリンク、アトムとアトムがつながっていることを表現できます。

したがって、以下はすべて同じグラフを表します。

% graph 1
a(X), b(X), c(Y), d(Y).
% graph 2
a(b), c(d).
% graph 3
a=b, c=X, d=X.
リスト

以下のように記述すると、リスト（linked list）を表現できます。

list = [1,2,3].

グラフは以下のような形になっており、'.' アトムと '[]' アトムを使用してベタ書きすることもできます。

list = '.'(1, '.'(2, '.'(3, '[]'))).

また、 | を使用することで、リストの先頭 n 要素と、残りの部分を指定することができます。したがって、先程のリストを以下のように書いても同じです。

list = [1,2|[3]].

リストの先頭要素に 4 を挿入するようなルールは、例えば以下のように書けます。

list = L :- list = [4|L].

ここで問題です。以下のようなコードを書くと、何が起きるでしょうか。

list = [1,2|[3]].
list = L :- list = [4|L].

実は、このコードは実行が止まりません。

LMNtalは適用できるルールがある限り適用し続けるため、無限ループに陥ってしまいます。

この場合、先頭に4を挿入しても、 "list にリンクで何かがつながったもの" であることには変わりがなく、何度書き換えを適用してもルールの左辺とのパターンマッチが成功してしまいます。

以下のように記述すれば、リストを用いて循環リストや双方向リストを表現できます。

list = [A, 1, 2, 3 | A]. 


list = [A,B,C], list = [D,E,F], 1(A,F), 2(B,E), 3(C,D).

補足

つかれたので、説明を省きます。寝たい

LMNtalのすごさを見てみよう！

公開されているデモプログラムのなかからハノイの塔のシミュレーションを見てみましょう。

なんと、LMNtalではたった1本のルールでハノイの塔をシミュレートできます！ このルールでは、ガードによってルールの適用に条件付けをしています。もし、p の引数のリストの先頭要素が他のリストの先頭よりも小さければ、先頭要素を他のリストの先頭の前に移動できる、というルールになっています。

以下では、盤の数が4枚の場合を示しています。

/*
 * Tower of Hanoi puzzle
 * 2007/06/09(Sat) by okabe
 */

poles(p([1,2,3,4,99]),p([99]),p([99])).
P1=p([H1|T1]), P2=p([H2|T2]) :- H1<H2 | P1=p(T1), P2=p([H1,H2|T2]).

これをLMNtalの統合開発環境LaViTで実行すると、以下の結果が得られました。

'# of States'(stored)   = 81.
'# of States'(end)      = 0.

4段のハノイの塔の状態数は81、終了状態（そこからの遷移が存在しない状態）は0個です。

次に、生成された状態空間を見てみます。

きれいですね。状態を選択することで、その状態におけるグラフを確認できます。

また、説明は省きますが、LTL式 を書くことで モデル検査 もできます。すごいですね。

じゃあ5枚、6枚... で試したいときはどうするかというと、このときもルールを変える必要はありません。poles(p([1,2,3,4,99]),p([99]),p([99])). とグラフを書いたときの引数のリストを変更すればいいだけです。すごいですね。

演習問題

興味が湧いてきて暇だった人がいたらやってみてください。

  1. 下のような三角形を書いてみよう。

  1. 木構造を書いてみよう。
  2. rev([1,2,3], []). を rev([], [3,2,1]) にするような、任意のリストを反転させる1本のルールを書こう。
  3. append([],[1,2,3],[4,5,6]) を append([1,2,3,4,5,6],[],[]) にするような、任意の2本のリストを結合するルールを書こう。
  4. 食事する哲学者の問題をシミュレートしてみよう。

おわりに

LMNtal、おもしろいですね。みなさんも、ぜひLaViTをダウンロードして触ってみてください。

参考文献・関連リンク