完備化の問題をいくつか解いてみたーその2

概要

拙作の完備化ツールをいろいろ使ってみたメモのその2です。 今回は、簡単な状態遷移図に対して用いてみます。 その1はこちらです。115個の完備化の問題を解いています。

zkat.hatenablog.com

やってみた

今回ツールに与える状態遷移図は以下のようにします。 これは、RFC 8555に出てくるとある状態遷移図をアレンジしたものです。

state-transition

ツールに入力できる形式で表すと以下の通りです。 trnという関数が、状態遷移を示しています。第二引数の状態に於いて、第一引数で示すトリガーが生じると、次の状態に遷移するということを表しています。

$ cat data
(VAR x y z)
(RULES

 trn(INIT, INIT)                      -> PENDING
 trn(ERROR, PENDING)                  -> INVALID
 trn(RECEIVEREQUEST, PENDING)         -> READY
 trn(ERROR, READY)                    -> INVALID
 trn(RECEIVEDATA, READY)              -> PROCESSING
 trn(ERROR, PROCESSING)               -> INVALID
 trn(FINISHCREATION, PROCESSING)      -> VALID

 car(cons(x,y)) -> x
 cdr(cons(x,y)) -> y
 cdr(NIL) -> NIL
 apply(NIL, x) -> x
 apply(x, y) -> apply(cdr(x), trn(car(x),y))
 trace(x) -> apply(x, INIT)
)

状態遷移図を辿る際に便利な関数traceを定義する為に、trn以外の諸々の関数を定義しています。 traceは、引数に1つのリストをとります。リストは状態遷移の為のトリガーを並べたものです。 traceは、リスト内のトリガー(操作)を全て実行した際の状態を返す関数です。

上記を完備化した書き換え系の下で、次の2つの項が何になるか確認してみたいと思います。 \begin{align} trace([INIT, RECEIVEREQUEST, RECEIVEDATA])\\ trace([INIT, ERROR]) \end{align}

$ wget https://github.com/moratori/clover/releases/download/v2.4.2/clover-linux-x86_64_v2.4.2 && chmod +x clover-linux-x86_64_v2.4.2
$ ./clover-linux-x86_64_v2.4.2 rewrite data 'trace([INIT, RECEIVEREQUEST, RECEIVEDATA])' 'trace([INIT, ERROR])'
YES

(VAR z x y)
(RULES
 trn(car(NIL),x) -> x
 apply(cons(y,x),z) -> apply(x,trn(y,z))
 apply(cdr(x),trn(car(x),y)) -> apply(x,y)
 trace(x) -> apply(x,INIT)
 apply(NIL,x) -> x
 cdr(NIL) -> NIL
 cdr(cons(x,y)) -> y
 car(cons(y,x)) -> y
 trn(FINISHCREATION,PROCESSING) -> VALID
 trn(ERROR,PROCESSING) -> INVALID
 trn(RECEIVEDATA,READY) -> PROCESSING
 trn(ERROR,READY) -> INVALID
 trn(RECEIVEREQUEST,PENDING) -> READY
 trn(ERROR,PENDING) -> INVALID
 trn(INIT,INIT) -> PENDING
)
(COMMENT
 ERROR < FINISHCREATION < INIT < INVALID < NIL < PENDING < PROCESSING < READY < RECEIVEDATA < RECEIVEREQUEST < VALID < TRN < APPLY < TRACE < CAR < CDR < CONS
)
(COMMENT
 trace([INIT, RECEIVEREQUEST, RECEIVEDATA]) reduced PROCESSING
 trace([INIT, ERROR]) reduced INVALID
)

最後に出力されている通り、 $trace([INIT, RECEIVEREQUEST, RECEIVEDATA])$は、$PROCESSING$となることが分かりました。 また、$trace([INIT, ERROR])$は、$INVALID$となることが分かりました。