Maude

最近Maudeにはまっている。
項書き換えシステムなんですが、等式論理や、書換論理を取り込み
なんかパーサーから実行からなんから全部出来るシステムにみえます。

当面、ACPおよびACPを使ったProces Termの簡略化なんかをTRSで
書いてみるというのに使えるかな。

あとは、BlueSpecのように、ルールからFSMを生成するような仕掛け
との関連を整理したいなあ。

LTLの集合をいれるとFSMを作ってくれるってものにならないかなあ?
なんかこれって退避モード?