今回は(one way) tree automataの話です. ざっくり直感的な説明をするなら、木構造をした入力テープ上を走査(ただし今回はone wayなので逆走したりはしない)して、そこに書かれたアルファベットを入力として読んでいき状態遷移するようなオートマトンなのですが、チ○ンラーメンで出来た*1私の貧相な脳みそでは理解するまでに苦戦を強いられてしまいました。そこで、同じチキ○ラーメンで出来た脳みそを持つ同士が心置きなく○キンラーメンを食べることができるようにちょっとした説明記事を書こうと思います。

話の流れとしてはまず定義を示し、その後意味のない例を用いて動きを確認していきます。

定義

定義 1 :

非負整数の初めのN個を0回以上繰り返して作れる列 $T_N = \left\{ 0,1,\dots,N-1 \right\} ^{*}$ をN分木とみなす. この時空列 $\Lambda$ は木のルートである. また, 各ノード $x \in T_N$ は後者(successors)として $x0,\dots,x(N-1)$ をもつ.

定義2:

$T_N$ の要素の列 $\pi = \left\{ x_n \right\}$ ですべての $n$ について $x_{n+1}$ が $x_n$ の後者になっているようなものをパスと呼ぶ.

定義3:

$\Sigma$ が有限のアルファベットであるとき, 関数 $f : T_N \rightarrow \Sigma$ を無限 $N$ 分 $\Sigma$ 木と呼ぶ.

定義4:

無限 $N$ 分 $\Sigma$ 木上の(非決定的)ツリーオートマトン $A$ は次の要素からなる4つ組 $(S, s_0, M, G)$ で定義される.

$S$ は状態の集合
$s_0 \in S$ は初期状態
$M : S\times \Sigma \rightarrow 2^{S^N}$ は次状態関数
$G \subset 2^{S}$ は受理部分集合

定義5:

$A$ の実行 $\rho : T_N \rightarrow S$ は $\rho (\Lambda)=s_0$ かつ任意の $x \in T_N$ について $(\rho (x0),\dots , \rho (x(n-1))) \in M(\rho (x), f(x))$ となるような関数

定義6:

$\rho$ が $f$ 上の $A$ の実行かつ $\pi$ が無限パスであるとき, $Inf(\rho, \pi) = \left\{ s \in S \mid \pi\ \texttt{上の無限にある} x \texttt{について}\ \rho (x) = s \right\}$

定義7:

すべての無限パス $\pi$ について $Inf(\rho, \pi) \in G$ となるような $f$ 上の $A$ の実行 $\rho$ が存在するとき、そしてその時に限り, オートマトン $A$ は無限 $N$ 分 $\Sigma$ 木 $f$ を受理する.

例:

定義は一通り示したわけですが、困ったことに脳みそがチキン○ーメンで出来ていると定義からその意味をイメージすることが出来ないわけです。ところが幸いなことにオートマトンの話なので動かしてみることが出来ます！というわけで具体的な例を考えていきます。

定義1で言っているのは, 木の各ノードを非負整数の列により表すことができるという事です。例として以下に皆が大好きな2分木の画像を張ります。 f:id:kashiwagi513:20161202201332p:plain

左からそれぞれ $T_2 = \left\{ \Lambda , 0, 1 \right\}$ , $T_2 = \left\{ \Lambda , 0, 1, 00 \right\}$ のようにして表すことができます. 左右の図中0,1はどちらも各々の $\Lambda$ の後者です。ここで, 右図中00は0の後者ではない, という事に注意してください。

この木の上でのたどり方をパスと呼びますがパスは定義2のようにして定義されます。たった今右図中の00は0の後者ではないといったのはパスの定義の際に0から直ぐに00へと移動するようなたどり方を許さないようにするためです。

さて、本題のオートマトンの話に移りましょう。例として次のようなオートマトンを考えます。

$S = \left\{ s_0, s_1, s_2, s_3 \right\}$
$M(s_0, a) = \left\{ (s_1, s_2) \right\}$
$M(s_0, b) = \left\{ (s_2, s_1) \right\}$
$M(s_1, a) = \left\{ (s_2, s_3) \right\}$
$M(s_1, b) = \left\{ (s_3, s_2) \right\}$
$M(s_2, a) = \left\{ (s_2, s_3) \right\}$
$M(s_2, b) = \left\{ (s_3, s_2) \right\}$
$M(\_, \_) = \left\{ \right\}$
$G= \left\{ s_0, s_1, s_2, s_3 \right\}$

簡単のためすべての状態を受理状態に含めました。つまりこれで非決定的な遷移の結果可能な遷移先がなくならなければ(実行が無限に続きさえすれば)受理するようになるはずです。また、簡単のため各次状態関数の遷移先の個数を0個か1個にしました。ここで、定義5をもう一度見てみましょう。

定義5:

$A$ の実行 $\rho : T_N \rightarrow S$ は $\rho (\Lambda)=s_0$ かつ任意の $x \in T_N$ について $(\rho (x0),\dots , \rho (x(n-1))) \in M(\rho (x), f(x))$ となるような関数

ここがすっきりとわかればもう実行の様子はイメージ出来るようになるはずです(少なくとも私の混乱の原因はここでした)。定義5に基づいて次の図の様な入力を与えた時の具体的な実行を求めてみましょう。

f:id:kashiwagi513:20161203011416p:plain

点々で表した以降の部分は直前のノード上のアルファベットと同じものが続くと考えてください。この時,定義5より実行 $\rho (\Lambda)$ は $s_0$ となりますね。では、ノード0,1時点での実行はどうなるでしょうか。ノード $\Lambda$ に対応するアルファベットは $a$ です。次状態関数より $M(\rho (\Lambda),f(\Lambda))=M(s_0,a) = \left\{ (s_1, s_2) \right\}$ となるので,ノード0,1に対応する実行はそれぞれ $\rho (0) = s_1, \rho (1) = s_2$ となります。同様にして各ノード時点での実行を求めていくと次のようになります。

$\rho (00) = s_2, \rho (000) = s_2, \dots$

$\rho (01) = s_3, \rho (001) = s_3, \dots$

$\rho (11) = s_2, \rho (111) = s_2, \dots$

$\rho (10) = s_3, \rho (110) = s_3, \dots$

もう、お分かりですね。無印のオートマトンでは一つの次状態を返していたのが、ツリーオートマトンでは、入力木の分岐の数だけ次状態を返すように拡張されています。それだけです。どうして初め理解に手間取ったのか………。

ただし、話を簡単にするために次状態関数の返す状態の個数を制限していたことは忘れないでください。実際には非決定的な遷移をするので、もちろん状態数はさらに膨れ上がります。とはいえ、今の簡単な例で一度理解してしまえば非決定的な遷移の例もなんとなくイメージ出来るようになったのではないでしょうか。

参考文献

Propositional dynamic logic of looping and converse is elementarily decidable

定義は⇧の論文のものを参照しました。

*1:チキンラ○メンを中傷する意図はありません。むしろチキンラーメンに生かされているといっても過言ではないほど毎日チキンラーメンばかりたべています

2016-11-30

Propositional Dynamic Logic of Looping and Converse

論文等紹介用語記事の体をなさぬメモ

Propositional Dynamic Logic of Looping and Converse

注意 : 本記事は記事の体をなさぬ自分用メモです。したがってわかりやすさ等について一切の配慮をしておりません。内容を整理し記事の体をなすようになれば「記事の体をなさぬメモ」タグを外します。

Intro

fact

すべての充足可能な式は有限生成可能なモデルをもつ(モデルは有限グラフのunravelingによって得られる)
⇧のことがPDL with loopingが有限モデル性を失わない理由.

有限モデル性

PDL式pの(無限かもしれない)任意のモデルは,全く同じpの部分式を満たすような状態を一つにまとめる事で, pの小さな有限モデルへ縮小することができる
PDLの決定手続きにおいて重要な性質(Fischer and Ladner 1979; Pratt, 1979)

1対1モデル性

任意の充足可能な式が1対1モデルで満足される.
1対1モデル : 構造Sが1対1であるとは任意の原子プログラムAについて関係 $\prec A\succ_S$ が1対1であること

SnS

Second order theory of n successors
SnSへの変換が素直に与えられる条件:
そのモデルをグラフから木に変換できるような論理
決定可能
決定可能性の証明は無限木上のオートマトンのemptinessへの帰着による

PDL

regular programにおける無限ループの概念を捉えるのに十分な力を持っていない(Pratt, 1978)
有限モデル性を満たす

PDL+natural formula construct (?)

Propositional Algorithmic Logic (Mirkowska, 1980)のすべての式を表現可能
Temporal Logic of Branching Time (Ben-Ari, Manna and Pnueli, 1981)のすべての式を表現可能
無限ループのpropositionalな概念を表現可能

PDL with Looping

状態のマージによって無限モデルから有限モデルへと縮小することのできない式が存在する(=>PDLより真に表現力が高い)
決定可能
SnSへの埋め込みにより決定可能性を証明できるが、complexityの上界がelementaryでない(SnSがelementary timeで決定可能でない(Mayer, 1974))
(少し弱い)有限モデル性を満たす(Street, 1980, 1982)
モデルをグラフから木にできる(下位ノードにしか繋がっていない)
elementary timeでの決定手続きは, SnSを経由せず無限木上のオートマトンのemptinessに直接帰着させることで得られる(Streett 1980, 1982)
1対1モデル性を満たす

PDL with converse

PDLと同じ有限モデル性を満たす
決定手続き(Fischer and Ladner, 1979; Pratt, 1979)
converse の構成についてのSnSへの自明な変換はまだ無い
1対1モデル性を満たさない

PDL with looping and converse

有限モデル性を満たさない(任意の有限モデルで充足可能でない式が存在する)
しかし、決定可能(elementary decidable)
グラフから木へと解こうとする際に, converseのせいでプログラムが任意のノードとつながってしまうため無限木上のオートマトンのemptinessへ帰着できない.(有限モデル性を満たさない理由)
deterministic two way automata on infinite treeを使えば決定可能性を言える.

SOAPL (Second Order Acyclic Process Logic)

決定可能(SnSへの埋め込みによる)
モデルをグラフから木にできる(下位ノードにしか繋がっていない)

参考文献

Pratt, 1978

Application of modal logic to programming | SpringerLink

Parikh, 1978

A decidability result for a second order process logic - IEEE Xplore Document

Propositional dynamic logic of looping and converse is elementarily decidable

http://ruthenia.info/txt/pavlo/03B/harel_kozen_tiuryn_2000.pdf

2016-10-28

チキチキ表現力天下一武道会

未整理

論理とか文法とかあれこれの表現力のメモ[未整理]

regular language < linear language < context free

2016-10-28

クリプキフレーム Kripke frame

用語

クリプキフレーム Kripke frame

そう言えばクリプキフレームの話を書いていなかった事を思い出したり(クリプキフレームの話なんて素敵なpdf (http://www.is.titech.ac.jp/~kashima/manuscript/03Sept.pdf )がネット上に溢れているので、わざわざ書くようなことでもないような気もしますが………)

定義

クリプキフレーム $\mathfrak{K}$ は次の２つ組で定義される.

$\mathfrak{K}=(K, \mathfrak{m}_{\mathfrak{K}})$

ここで、 $K$ は状態と呼ばれる集合、 $\mathfrak{m}_{\mathfrak{K}}$ は意味付け関数(meaning function)と呼ばれる.

例えばこの定義のもとで動的命題論理の意味論を考えてみる. 命題 $p\in\Phi$ 、プログラム $a\in\Pi$ について意味付け関数 $\mathfrak{m}_{\mathfrak{K}}$ が次のように与えられる.

$\mathfrak{m}_{\mathfrak{K}}(p) \subseteq K, \mathfrak{m}_{\mathfrak{K}}(a) \subseteq K \times K$

このとき、意味付け関数の直感的な意味は、ある命題pを満たすような状態の集合、あるプログラムaの実行に相当する遷移関係の集合を与えているようなものであると考えることが出来る.

[そのうち加筆修正]

参考文献

amazonリンクで恐縮ですが

www.amazon.co.jp

2016-10-10

2-way 決定性有限オートマトン[2DFA]

用語

2-way 決定性有限オートマトン[2DFA]

直感的な説明をすると, 入力文字列を2方向に走査できるオートマトン。通常のオートマトンでは, キャラクタを受け取るとそのキャラクタと, 現在の状態から次の状態を決定する。その流れは2DFAでも同様に行われるが, 2DFAでは入力として与えられるキャラクタに, アルファベットの他, 方向付きの終端記号が含まれる。あたえられた文字列ををテープ, 今ちょうど読んでいるキャラクタが, テープ中のヘッドが指している部分に記されている図をイメージする。初めヘッドはテープの左端からスタートし1文字づつ右側へと進んでいく。終端器号 $\dashv$ に到達すると, ヘッドは進む向きを反転させ, テープ左端へと向かい始める。左側にも同様の終端器号 $\vdash$ が存在し, ここに到達すればヘッドは再び右側へと進み始める。形式的な定義は次のように与えられる。

定義

2DFA Mは次の8つ組で与えられる.

$(Q, \Sigma , \vdash , \dashv , \delta , s , t , r)$

where

$Q$ は状態の有限集合
$\Sigma$ は入力文字の有限集合(アルファベット)
$\vdash,\dashv$ はそれぞれ左終端器号,右終端器号( $\vdash,\dashv\not\in\Sigma$ )
$\delta : Q\times\{\Sigma\cup\{\vdash,\dashv \}\}\rightarrow Q\times\{L,R\}$ は遷移関数(L,Rはそれぞれヘッドが次に左に進むか右に進むかを表す)
$s, t, r \in Q$ はそれぞれ初期状態, 受理状態, リジェクト状態を表す

また遷移関数は次の条件を満たす

任意の $q\in Q$ について
$\delta(q,\vdash) = (u, R) for some u\in Q$
$\delta(q,\dashv) = (v, L) for some v\in Q$
任意の $b\in\Sigma\cup\{\vdash\}$ について
$\delta(t, b) = (t, R),\ \delta(r, b) = (r, R)$
$\delta(t, \dashv) = (t, L)\ \delta(r, \dashv) = (r, L)$

条件1の直感的な意味は,テープのヘッドが終端記号読み込み時にその移動方向を逆転させることを,条件2は受理,またはリジェクト時にヘッドをテープの右端に除けてしまう事を表している.

参考

http://www.cs.cornell.edu/courses/cs682/2008sp/Handouts/2DFA.pdf

pdfへの直リンクです, すみません。あとでちゃんとしたソースを貼り直します。

2016-09-29

Visibly Pushdown Automaton

用語

Visibly Pushdown Automaton (VPA)

nested wordをアクセプトするオートマトンをnested wordオートマトンという。VPAはnested wordオートマトンと等価な普通の(nested wordでない)語を受理するオートマトン。

nested wordオートマトンと関係がありそうだなあ…位のことは、遷移関数の定義を見ると、(直感的には)直ぐわかる。その辺りの対応に関する証明の詳細は調べてない。

普通、VPAと言った場合は決定的なものを指すっぽい(未確認)

定義

VPAは6つ組 $(Q,\hat{\Sigma},\Gamma,\delta,q_0,F)$ の形で定義されれる。

ここで、

$Q$ は状態の有限集合
$\hat{\Sigma}$ は入力アルファベットを表す。 $\hat{\Sigma}$ は $\Sigma_c,\Sigma_r,\Sigma_{int}$ の3つの部分からなり、それぞれcall記号,ret記号,内部記号を含む.
$\Gamma$ はスタックアルファベットと呼ばれる有限集合で、空のスタックを表す特別な記号 $\bot\in\Gamma$ を含む.
は遷移関数.ここで
- $\delta_c : Q\times\Sigma_c\rightarrow Q\times\Gamma$ (call遷移関数)
- $\delta_r : Q\times\Sigma_r\times\Gamma\rightarrow Q$ (ret遷移関数)
- $\delta_{int} : Q\times\Sigma_{int}\rightarrow Q$ (内部遷移関数)
$q_0\in Q$ は初期状態
$F\subseteq Q$ は受理状態の集合