ネロード正規化関手、振る舞い観測関手、実現関手
なんらかの意味でオートマトンの圏があるとき、次の操作がある。
- オートマトンの最小化、最適化、正規化などと呼ばれる操作
- 「観測可能な振る舞い」という概念があり、オートマトンにその観測可能な振る舞いを対応させる操作
- 指定された振る舞いを実際に行うオートマトンを構成する操作
これらは関手で、次のように書ける。
- B:Aut→Beh 振る舞い関手、観測関手、くどい言い方では振る舞い観測関手
- N:Aut→Aut 最小化関手、正規化関手、ネロード関手、くどい言い方ではネロード正規化関手
- R:Beh→Aut 実現関手
関手Nの像であるAutの部分圏をMinとする。
- 関手Nはベキ等である。
- J:Min→Aut を包含埋め込みとすると、N':Auto→Mint とJは随伴ペアである。
- 関手Bのセクションとなる関手を実現関手と呼ぶ。
- 実現関手が1つでもあれば、Nと組み合わせて最小実現関手を構成できる。
- 関手Bと最小実現関手は随伴ペアとなる。
- MinとBehは圏同値になる。
Aut、Min、Beh で構成される三角形を仮にネロード三角形と呼ぶと：
- AutとMinのあいだは随伴な埋め込みと射影で結ばれる。
- AutとBehのあいだは随伴な観測と実現で結ばれる。
- MinとBehのあいだは圏同値で結ばれる。
