Maudeのお勉強 - keigoiの日記

Maudeは書き換え論理(rewriting logic)だとかメンバシップ等式論理(membership equational logic)の項を書いたり動かしたりできる。今の僕の理解ではMaudeは項書き換え系のめっちゃリッチな実装とだけ思っている。 →の前後が等価であれば CafeOBJ みたいな等価変換だけど、 rewriting logic というのはより一般的な、例えば並行システムの非決定的遷移みたいなのも書けるらしい。

日本語でのMaudeの解説

コンピュータソフトウェアの記事 http://www.jstage.jst.go.jp/article/jssst/25/2/25_2_78/_article/-char/ja/ が役に立つに違いない。(まだ読んでない)

Maudeで変数束縛を含む代数を書くには

いきなりマニアックな話題かもしれないけど、 Maude は一階な項書き換えしか書けない。 λ計算とかπ計算とかプログラミング言語における変数束縛とかsubstitutionみたいな高階(Maude的には変数束縛は全て高階らしい)な構文は項書き換えの規則で作ったり書き換えたりしなければならない。 CINNI - A Generic Calculus of Explicit Substitutions and its Application to λ-; ς- and π-Calculi (著者のサイトのD論の5章) では Maude で変数束縛と代入をいい感じに扱う方法の一つが発明されている。

で、これを動かしてみる。せっかくなのでこの論文の π計算の例を入力してみることにした。

ソース

pi1.maude

*** from M. Oliver Stehr, CINNI - A Generic Calculus of Explicit Substitutions and its Application to $\lambda$- $\varsigma$- and $\pi$-Calculi. In proc. of The 3rd International Workshop on Rewriting Logic and its Applications, ENTCS 36, pp. 70-92, 2000.

fmod QIDLt is
  including QID .
  protecting STRING .
  op _<_ : Qid Qid -> Bool .
  vars A B : Qid .
  eq A < B = string(A) < string(B) .
endfm

fmod SubstChan is
  including NAT .
  including QID .
  vars X Y Z : Qid . 

  sort Chan .
  vars CX CY CZ : Chan . 
  
  sort Subst . 
  var S : Subst . 
  vars n m : Nat . 
  
  op _{_} : Qid Nat -> Chan . 
  op [_:=_] : Qid Chan -> Subst . 
  op [shift_] : Qid -> Subst . 
  op [lift__] : Qid Subst -> Subst . 
  op __ : Subst Chan -> Chan . 
  
  eq ([X := CZ] (X{0})) = CZ . 
  eq ([X := CZ] (X{s(m)})) = (X{m}) . 
  ceq ([X := CZ] (Y{n})) = (Y{n}) if X =/= Y . 
  eq ([shift X] (X{m})) = (X{s(m)}) . 
  ceq ([shift X] (Y{n})) = (Y{n}) if X =/= Y . 
  eq ([lift X S] (X{0})) = (X{0}) . 
  eq ([lift X S] (X{s(m)})) = [shift X] (S (X{m})) . 
  ceq ([lift X S] (Y{m})) = [shift X] (S (Y{m})) if X =/= Y . 
endfm
  
mod PI is
  protecting QIDLt .
  protecting SubstChan .

  sort Trm .
  op __ : Subst Trm -> Trm . 

  vars X Y Z : Qid . 
  vars CX CY CZ : Chan . 
  vars M N P Q : Trm . 
  var S : Subst . 

  *** process constructors
  op nil : -> Trm . 
  op _|_ : Trm Trm -> Trm [assoc comm id: nil] . 
  op new[_]_ : Qid Trm -> Trm . 
  op out_!_._ : Chan Chan Trm -> Trm . 
  op in_[_]._ : Chan Qid Trm -> Trm . 

  *** substitution on processes
  eq S nil = nil . 
  ceq S (M | N) = (S M) | (S N) if N =/= nil and M =/= nil . 
  eq S (out CX ! CZ . M) = out (S CX) ! S CZ . (S M) . 
  eq S (in CX [ Y ] . M) = in (S CX) [ Y ] . ([lift Y S] M) . 
  eq S (new [X] M) = new [X] ([lift X S] M) . 
  
  *** structural equality
  eq new [X] nil = nil . *** (NEW1) 
  ceq (new [X] P) | Q = new [X] (P | [shift X] Q) if P =/= nil and Q =/= nil . *** (NEW2) 
  ceq new [X] new [Y] P = new [Y] new [X] P if Y < X . *** (NEW3) 
  
  *** reduction
  rl [communicate] : (out CX ! CZ . P) | (in CX [ Y ] . Q) => P | [Y := CZ] Q .
endm

*** 例
rew (new['a]new['b]((out 'a{0} ! 'b{0} . nil) | (in 'a{0} ['x]. nil))) .

最後の rew で π計算の項の簡約を試している。ここで 'a とか 'b というのはソート Qidをもつ。 'a{0} とか 'b{0} は演算子 _{_} を使っていてソート Chan である。
この {0} とかいうのはCINNI の記法で、その場所から項の外側に向かって数えて何番目の変数束縛を参照しているのかを示す。例えば λx.λx.λx.x{2} なら 2番目のx を参照している。この表現は変数名を変えずにcapture-avoidingな代入を行うのに一役買っている。

Maude

		     \||||||||||||||||||/
		   --- Welcome to Maude ---
		     /||||||||||||||||||\
	    Maude 2.4 built: Nov  6 2008 16:49:57
	    Copyright 1997-2008 SRI International
		   Wed Nov 12 07:33:27 2008
Advisory: "pi.maude", line 67 (mod PI): collapse at top of Q | new[X]P may
    cause it to match more than you expect.
==========================================
rewrite in PI : new['a]new['b](out 'a{0} ! 'b{0} . nil) | in 'a{0}['x]. nil .
rewrites: 14 in 0ms cpu (0ms real) (114754 rewrites/second)
result Trm: nil
Maude>

動いた。何かadvisoryが出ているけれどよくわからない。 new演算子のスコープを広げる規則が大幅にマッチするのでヤバいよということらしいけどそれは別に意図通りだと思う。

frozen

しかしこのままだと π計算の意味論とは異なり inやoutプレフィクスの下の項も簡約されてしまう。項書き換え系の書き換え規則とはそういうものらしい。
例えば:

Maude> rew out 'c{0} ! 'd{0} . (new['a]new['b]((out 'a{0} ! 'b{0} . nil) | (in 'a{0} ['x]. nil))) .
rewrite in PI : out 'c{0} ! 'd{0} . new['a]new['b](out 'a{0} ! 'b{0} . nil) |
    in 'a{0}['x]. nil .
rewrites: 14 in 0ms cpu (0ms real) (14000000 rewrites/second)
result Trm: out 'c{0} ! 'd{0} . nil
Maude>

c!d.(new a,b)(a!b.nil | a?x.nil) -> c!d.nil となっている。

書き換え規則を subtermに適用しないために、プレフィクスの演算子にfrozenを指定する。

pi2.maude

:
  op out_!_._ : Chan Chan Trm -> Trm [frozen]. 
  op in_[_]._ : Chan Qid Trm -> Trm [frozen]. 
:

すると、outプレフィクスの下の項には書き換え規則が適用されなくなる。

Maude> rew out 'c{0} ! 'd{0} . (new['a]new['b]((out 'a{0} ! 'b{0} . nil) | (in 'a{0} ['x]. nil))) .
rewrite in PI : out 'c{0} ! 'd{0} . new['a]new['b](out 'a{0} ! 'b{0} . nil) |
    in 'a{0}['x]. nil .
rewrites: 10 in 0ms cpu (0ms real) (85470 rewrites/second)
result Trm: out 'c{0} ! 'd{0} . new['a]new['b](out 'a{0} ! 'b{0} . nil) | in
    'a{0}['x]. nil
Maude>

あとは + 演算子を作ったり以前書いた abort を試したり may testしたりなどしたい。参考CiteULike