bisimulation checker モドキ

Haskell

なんだろうこれ。1時間くらいで適当に作ったやつ。bisimulation かどうかを確かめる(?)もの。bisimulation じゃない場合には実行時エラーになります。
checker 関数に状態を2つ入れると計算が開始されます。"a.b.stop" は、"a***b***STOP"と書きます。

先輩によると、基底みたいなやつがない場合もあるとか(coinduction?)。このコードだと、そんなんは判定できません。
それと、tau はtau遷移(?)とかいうやつ。意味がわかってないので使い方が思いっきり間違ってる可能性があります。
このコードでは、tau はアクションを実行するんじゃなくて、選択になってる部分をリストに展開する操作を行う関数になってます。

import Control.Monad
import Data.List

type TWO = (Process, Process)
type Action = Int
data Process = STOP |
               DOT Action Process |
               PLUS Process Process deriving (Eq, Show)
a *** b = DOT a b
a +++ b = PLUS a b
infixr 7 ***
infixr 6 +++

tau :: Process -> [Process]
tau (PLUS p1 p2) = msum [tau p1, tau p2]
tau p            = return p

check :: [TWO] -> TWO -> [TWO]
check bis (left, right) =
    do l <- tau left
       r <- tau right
       case (l, r) of
         (STOP, STOP)         -> (STOP, STOP) : bis
         (DOT a p1, DOT b p2) -> check ((p1,p2) : bis) $ check' (l,r)
check' (DOT a p1, DOT b p2) | a==b = (p1, p2)
add a l | elem a l  = l
        | otherwise = a:l
checker l r = nub $ check [(l,r)] (l,r)

left, right :: Process
left  = 1***(2***STOP+++2***STOP) +++ 1***2***STOP
right = 1***2***STOP
test  = checker left right

実行結果はこんな感じに。

Main> test
[(STOP,STOP),(PLUS (DOT 2 STOP) (DOT 2 STOP),DOT 2 STOP),(PLUS (DOT 1 (PLUS (DOT 2 STOP) (DOT 2 STOP))) (DOT 1 (DOT 2 STOP)),DOT 1 (DOT 2 STOP)),(DOT 2 STOP,DOT 2 STOP)]
Main>

結果をみる限りでは、本と同じのが返ってきてるみたい。