Finding Patterns Common to a Set of Strings

Angluin
Finding Patterns Common to a Set of Strings
ACM 1979 pp.130-141
ang79.md

いわゆるパターン言語であって、 与えられた文字列集合を言語に含められるようなパターンを "pattern common" と呼ぶ.

Angluin's problem (aka. MINL)

Example

S={S=\{ 1011, 110111 }\}

定義

About Pattern

  1. A pattern is any finite string over (ΣX)(\Sigma \cup X).
  2. PP
  3. substitution
  4. ,\equiv, \preceq
  5. 個別に数えた変数が kk 個あるパターンを k-variable パターンといって、それ全体を PkP_k とする
  6. L(p)L(p)
  7. canonical form p^\hat{p}

About Inductive Identification

  1. positive presentation
  2. 添字付き言語族について、そのなかの全ての言語について、任意の正提示から、ある一つの推論マシーンで極限同定できるとき、その言語族を同定する、という

3.1 Equivalence

Thm 3.1.5

pqL(p)=L(q)p \equiv q \iff L(p) = L(q)

証明には Thm 3.3.5 が必要.

3.2 Membership

Thm 3.2.1

Given p,qp,q, pqp \preceq q の判定はNP.

qq が k-variable だとすると、qq から部分列を kk 個、非決定的に引っ張ってきて、 マッチすることをチェックすればよい. 従って、 |p|O(k)|p|^{O(k)} の計算量で、決定的に計算できる. |p||p|pp の長さ.

Thm 3.2.2

Given s,ps, p, sL(p)s \in L(p) の判定はNP完全.

3-SAT からパターンマッチへの帰着による証明

3.3 Containment

3.3.3

\preceq が半順序

3.3.2

pqL(p)L(q)p \preceq q \Rightarrow L(p) \subseteq L(q)

3.3.4

3.3.2 の逆は偽.

反例

Σ={0,1},p=0x10xx1,q=xxy\Sigma=\{0,1\}, p=0x10xx1, q=xxy

pqp \npreceq q

sL(p)s=0t10tt1s \in L(p) \iff s=0t10tt1. t=0u,1ut=0u, 1u の二通りの場合を考える. 前者の場合 s=00(u100u0u1)qs = 00(u100u0u1) \preceq q. 後者の場合 s=(01u1)(01u1)u1qs = (01u1)(01u1)u1 \preceq q. したがつて sL(q)s \in L(q).

Thm 3.3.5

If |p|=|q||p|=|q| then pqL(p)L(q)p \preceq q \iff L(p) \subseteq L(q).

Thm 3.3.6

qq が one-variable pattern なら、 pqL(p)L(q)p \preceq q \iff L(p) \subseteq L(q).

3.3.7

Given p,qp,q, L(p)L(q)L(p) \subseteq L(q) の判定は NP困難.

4.1 帰納推定のための条件

添字付き言語族 𝒞=L1,L2...\mathcal{C} = L_1, L_2 ... であって、効率的に sLis \in L_i が判定できるとする (帰納言語).

条件 C1

i,finiteTLi,j,TLjLi\forall i, \exists \text{finite} T \subseteq L_i, \nexists j, T \subseteq L_j \subsetneq L_i

この TT はいわゆる、LiL_i の 有限証拠 (tell-tail) と呼ばれる.

条件 EC1 (C1のenum版)

LiL_i の有限証拠を TiT_i とする. L1,L2...L_1, L_2 ... という indexing に対して T1,T2...T_1, T_2 ... という列挙を効率良く行う手続きが存在すること.

4.1.1

EC1 を満たす iff 極限同定可能

EC1 \Rightarrow 極限同定

  1. S{}S \leftarrow \{\}
  2. g0=g_0 = \bot
  3. For each time t=1,2..t=1,2..
    1. SS{st}S \leftarrow S \cup \{ s_t \}

条件 C2

条件 C3