項書換えシステム記述言語maude
背景
大学の分散情報システムという講義で, maudeという項書換えシステムを使うことになったので, コードを書きました. コードを書いたので, せっかくなのでgistにuploadしました. gistにuploadしたので, せっかくなのでここで解説したいと思います.
途中から大学に提出したレポートの写しになっているので, なんだかちぐはぐです.注意してください.
maude
公式サイトはThe Maude System. マニュアルはMaude Manual and Examples - The Maude System のHTMLのリンクを読みましょう. バージョンが上がるとURLが変わるため直接リンクは貼りません. また, wikipediaにも記事があります, 誰か翻訳してください. Maude system - Wikipedia
maudeの数の取り扱いはペアノの公理 - Wikipediaを直接触ることになります. ペアノの公理については型システム入門 −プログラミング言語と型の理論− | Benjamin C. Pierce, 住井 英二郎, 遠藤 侑介, 酒井 政裕, 今井 敬吾, 黒木 裕介, 今井 宜洋, 才川 隆文, 今井 健男 |本 | 通販 | Amazonを読むと理解が深まるのではないでしょうか. こちらは項書換えシステムではなくラムダ計算ですが.
インストール方法
gentooを使っていれば,
公式リポジトリにパッケージが存在するのでsudo emerge maudeで一発でインストールできます.
この機会にgentooをインストールしましょう.
開発環境
emacsならmaude-modeがmelpaに存在します. これを使えばシンタックスチェック, REPLの統合, みんな出来ます. ただし, maudeの文法はガバガバなため, maude-modeのシンタックスチェックでエラーになっててもmaude実装では動いたりすることに注意してください.
階乗計算
普通の言語ですね.
フィボナッチ数計算
fibletを書いてイテレーションすることで,
再帰の爆発を避けて計算量を下げています.
これを書いた後に気が付いたのですが,
maudeもメタ的な操作をすることでジェネリックなletを使うことが出来るようなので,
fibletのように項で変数束縛をエミュレーションすることは本来は不要のようですね.
川渡り問題のリゾルバ
いわゆる川渡り問題のリゾルバです. 条件は
- あなた, 狼, 羊, キャベツがある
- あなただけがボートを操作できる
- ボートにはあなたともう1つが乗ることが出来る
- 狼と羊を孤立させるとゲームオーバー
- 羊とキャベツを孤立させるとゲームオーバー
この問題だと, あなたはボートに固定されます.
deadで死ぬ条件をずらずらと書き,
crlのrewrite ruleで死ぬ場合以外をずらずらと書くだけで,
maudeはSetから全てのパターンをマッチして,
川渡り問題を解いてくれます.
面白い言語ですね.
emptyはItemよりItemSetのコンストラクタとした方がHaskellやLispを経験すると自然に感じますが,
どうもどちらでも良いようです.
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7 built: May 25 2016 19:16:07
Copyright 1997-2014 SRI International
Thu Jul 21 15:07:53 2016
Maude> ==========================================
mod RIVER
Maude> search init =>* river(empty, you wolf sheep cabbage) .
search in RIVER : init =>* river(empty,you wolf sheep cabbage) .
Solution 1 (state 9)
states: 10 rewrites: 46
empty substitution
No more solutions.
states: 10 rewrites: 51
Maude> show path 9 .
state 0, River: river(you wolf sheep cabbage,empty)
===[ crl river(you L I,R) => river(L,you R I) if dead(L) = false [label right]
. ]===>
state 1, River: river(wolf cabbage,you sheep)
===[ crl river(L,you R I) => river(you L I,R) if dead(R) = false [label left] .
]===>
state 2, River: river(you wolf cabbage,sheep)
===[ crl river(you L I,R) => river(L,you R I) if dead(L) = false [label right]
. ]===>
state 3, River: river(cabbage,you wolf sheep)
===[ crl river(L,you R I) => river(you L I,R) if dead(R) = false [label left] .
]===>
state 5, River: river(you sheep cabbage,wolf)
===[ crl river(you L I,R) => river(L,you R I) if dead(L) = false [label right]
. ]===>
state 7, River: river(sheep,you wolf cabbage)
===[ crl river(L,you R I) => river(you L I,R) if dead(R) = false [label left] .
]===>
state 8, River: river(you sheep,wolf cabbage)
===[ crl river(you L I,R) => river(L,you R I) if dead(L) = false [label right]
. ]===>
state 9, River: river(empty,you wolf sheep cabbage)
Maude>
ちなみにmaudeはshow search graphで何かのグラフ言語用のグラフを吐き出してくれます.
しかし,
その吐き出しフォーマットがなんなのか調べても調べてもわからないので諦めました.
graphviz用に書き換えるpythonコードなどは出てきましたが.
どういうソフトウェア用のグラフ言語なのか,
知っている方はコメントをお願いします.
簡単なエレベータパズル
- 3階建ての建物, エレベータ, 違う階に移動したい人達がある
- 人達はそれぞれの階に並んでいる, 以下に人達の初期配置を, その人の目的階だけで表す
- 1階: [2, 3, 2, 2]
- 2階: [1, 1, 3]
- 3階: [1, 2]
- エレベータの初期位置は1階である
- エレベータは移動, 先頭に人の挿入, 先頭の人の排出ができる
- 移動したい人達を全て目的の階に移動させよ
人の配置は解ける程度の量で乱数で適当に決めました.
人は目的階以外の情報を持っていないので,
単なるNatとして表現できるため,
People型などは作りませんでした.
C言語でいうtypedef, Haskellでいうtypeのような,
弱いalias機能があればそれで済ませたのですが,
普通にPeople型を作るとList{Nat}が使えなくなったりして大変なので,
素直にNatで表現しています.
Generic Moduleの使い方を少し読むと,
1から作った型にもviewなどを定義すればTRIVとして要件を満たせるようですが,
残念ながら,
私はmaudeのマニュアルをを大学のレポートの提出期限に間に合うほど早く読めませんでした.
こういう型変数の渡し方は OCamlの第1級モジュールと似てると感じましたが, OCamlはあまり書いたことがないため, 本当に似てるかはよくわかりません.
本当はFloorMapもpreludeのMapが使いたかったのですが,
どうもprotecting MAP{Nat, List{Nat}}するとsyntax errorになるので出来ませんでした.
これをどうにかする方法も提出期限的に無理なので素直にFloorMapを定義することとしました.
今回も停止条件をendルールとして書いていますが,
crlは使っていません.
Haskellでいうas patternはないのかと探しまわった結果見つからなかったので,
crlを連発すると全体パターンのコピペが大量発生してコードが大変冗長になるからです.
searchにsuch that end(B)を付けて判定することで対処することにしました.
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude 2.7 built: May 25 2016 19:16:07
Copyright 1997-2014 SRI International
Thu Jul 21 23:03:30 2016
Maude> ==========================================
mod ELEVATOR
Maude> search init =>* B:Bill such that end(B) .
search in ELEVATOR : init =>* B such that end(B) = true .
Solution 1 (state 698073)
states: 698074 rewrites: 3844304
B --> bill(elevator(2, nil), floor(1, 1 1 1) : floor(2, 2 2 2 2) : floor(3, 3
3))
Solution 2 (state 745303)
states: 745304 rewrites: 4222006
B --> bill(elevator(1, nil), floor(1, 1 1 1) : floor(2, 2 2 2 2) : floor(3, 3
3))
Solution 3 (state 761216)
states: 761217 rewrites: 4357412
B --> bill(elevator(3, nil), floor(1, 1 1 1) : floor(2, 2 2 2 2) : floor(3, 3
3))
No more solutions.
states: 831600 rewrites: 5031118
Maude> show path 698073 .
state 0, Bill: bill(elevator(1, nil), floor(1, 2 3 2 2) : floor(2, 1 1 3) :
floor(3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 2, Bill: bill(elevator(1, 2), floor(1, 3 2 2) : floor(2, 1 1 3) : floor(
3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(s N, PS)) => bill(elevator(s N, EPS),
FS : floor(s N, PS)) [label up] . ]===>
state 5, Bill: bill(elevator(2, 2), floor(1, 3 2 2) : floor(2, 1 1 3) : floor(
3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 12, Bill: bill(elevator(2, 1 2), floor(1, 3 2 2) : floor(2, 1 3) : floor(
3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 29, Bill: bill(elevator(2, 1 1 2), floor(1, 3 2 2) : floor(2, 3) : floor(
3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(s N, PS)) => bill(elevator(s N, EPS),
FS : floor(s N, PS)) [label up] . ]===>
state 59, Bill: bill(elevator(3, 1 1 2), floor(1, 3 2 2) : floor(2, 3) : floor(
3, 1 2))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 117, Bill: bill(elevator(3, 1 1 1 2), floor(1, 3 2 2) : floor(2, 3) :
floor(3, 2))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 235, Bill: bill(elevator(3, 2 1 1 1 2), floor(1, 3 2 2) : floor(2, 3) :
floor(3, nil))
===[ rl bill(elevator(s N, EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, PS)) [label down] . ]===>
state 467, Bill: bill(elevator(2, 2 1 1 1 2), floor(1, 3 2 2) : floor(2, 3) :
floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 882, Bill: bill(elevator(2, 3 2 1 1 1 2), floor(1, 3 2 2) : floor(2, nil)
: floor(3, nil))
===[ rl bill(elevator(s N, EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, PS)) [label down] . ]===>
state 1624, Bill: bill(elevator(1, 3 2 1 1 1 2), floor(1, 3 2 2) : floor(2,
nil) : floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 2894, Bill: bill(elevator(1, 3 3 2 1 1 1 2), floor(1, 2 2) : floor(2,
nil) : floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 5087, Bill: bill(elevator(1, 2 3 3 2 1 1 1 2), floor(1, 2) : floor(2,
nil) : floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(N, P PS)) => bill(elevator(N, P EPS),
FS : floor(N, PS)) [label pick] . ]===>
state 8695, Bill: bill(elevator(1, 2 2 3 3 2 1 1 1 2), floor(1, nil) : floor(2,
nil) : floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(s N, PS)) => bill(elevator(s N, EPS),
FS : floor(s N, PS)) [label up] . ]===>
state 14417, Bill: bill(elevator(2, 2 2 3 3 2 1 1 1 2), floor(1, nil) : floor(
2, nil) : floor(3, nil))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 23020, Bill: bill(elevator(2, 2 3 3 2 1 1 1 2), floor(1, nil) : floor(2,
2) : floor(3, nil))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 35918, Bill: bill(elevator(2, 3 3 2 1 1 1 2), floor(1, nil) : floor(2, 2
2) : floor(3, nil))
===[ rl bill(elevator(N, EPS), FS : floor(s N, PS)) => bill(elevator(s N, EPS),
FS : floor(s N, PS)) [label up] . ]===>
state 54236, Bill: bill(elevator(3, 3 3 2 1 1 1 2), floor(1, nil) : floor(2, 2
2) : floor(3, nil))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 79841, Bill: bill(elevator(3, 3 2 1 1 1 2), floor(1, nil) : floor(2, 2 2)
: floor(3, 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 113600, Bill: bill(elevator(3, 2 1 1 1 2), floor(1, nil) : floor(2, 2 2)
: floor(3, 3 3))
===[ rl bill(elevator(s N, EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, PS)) [label down] . ]===>
state 157660, Bill: bill(elevator(2, 2 1 1 1 2), floor(1, nil) : floor(2, 2 2)
: floor(3, 3 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 211927, Bill: bill(elevator(2, 1 1 1 2), floor(1, nil) : floor(2, 2 2 2)
: floor(3, 3 3))
===[ rl bill(elevator(s N, EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, PS)) [label down] . ]===>
state 278781, Bill: bill(elevator(1, 1 1 1 2), floor(1, nil) : floor(2, 2 2 2)
: floor(3, 3 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 355382, Bill: bill(elevator(1, 1 1 2), floor(1, 1) : floor(2, 2 2 2) :
floor(3, 3 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 441958, Bill: bill(elevator(1, 1 2), floor(1, 1 1) : floor(2, 2 2 2) :
floor(3, 3 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 530929, Bill: bill(elevator(1, 2), floor(1, 1 1 1) : floor(2, 2 2 2) :
floor(3, 3 3))
===[ rl bill(elevator(N, EPS), FS : floor(s N, PS)) => bill(elevator(s N, EPS),
FS : floor(s N, PS)) [label up] . ]===>
state 620598, Bill: bill(elevator(2, 2), floor(1, 1 1 1) : floor(2, 2 2 2) :
floor(3, 3 3))
===[ rl bill(elevator(N, P EPS), FS : floor(N, PS)) => bill(elevator(N, EPS),
FS : floor(N, P PS)) [label drop] . ]===>
state 698073, Bill: bill(elevator(2, nil), floor(1, 1 1 1) : floor(2, 2 2 2 2)
: floor(3, 3 3))
Maude>
エレベータの停止位置が3箇所あるため, Solutionも3つ出現することになりました. これは実行するまで予想していませんでした.
このプログラムには問題があり, 少し階数や人数を増やすと組み合わせが爆発し, プログラムは停止する気配を見せず, スワップが上限を突破する勢いで溜まっていきます.
もちろん, これを回避するのは簡単で, ハノイの塔のように適当に置いておく階を設定したり, アルゴリズムを変えることで大体効率的に解を出すことができるでしょう.
しかし, それは効率の良い解なのか全くわからないという問題があります.
他の｢効率が良さそうな｣アルゴリズムを使うとしても, 結局はそれは人間の先入観で書いているだけなので, maudeを使う意味がやはり無くなってしまいます.
モデル検査の利点｢定義を書くだけで検査できる｣と, 欠点｢組み合わせ爆発への対策は結局難しい｣を思い知らされました.
しかしモデル検査は単なるしらみつぶし検査と考えることが出来るため, その点maudeは, C言語から入ってきたようなプログラマにもとっつきやすく, coqのような定理証明系よりは意味不明ではありませんでした.
またmaude言語は, ruleが任意箇所に引数を取れることによって, かなり自由に構文を弄れるのは大変面白いと思いましたが, 結局それもmaude内の範疇を抜け出せないので, 構文を弄ろうとするとやはりLisp系のマクロやTemplate Haskellのように, ASTを直接触れる機構があったほうが楽なのではないかと思いました.
maudeの部分的実装
途中で飽きた中途半端なものです. マッチングの参考ぐらいにはなるかもしれません.
hatena-bookmark