読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

正規表現エンジン制作入門(2): いろいろなDFA

Haskell

オートマトンの単位を落としてしまいましたが、正規表現エンジンは作っていきたいと思います。

前回定義したDFAを思い出してみましょう。

inkar-us-i.hatenablog.com

DFAは状態を持ち、入力された文字によってその状態を変えていく機械でした。

f:id:cloudear8:20170224082156p:plain

この図はsが初期状態であり、文字'0'を受け取れば状態aに、'1'を受け取れば状態bに、'2'を受け取れば状態cに遷移し、bが受理状態であるオートマトンを表しています。

このオートマトンを使って、簡単な正規表現を表してみましょう。

[abc]+を受理するオートマトン

f:id:cloudear8:20170224082931p:plain
上図のオートマトン正規表現[abc]+を受理します。初期状態はs0であり、そこからa, b, cのいずれかの文字を受け取ると受理状態s1に遷移します。
矢印が省略されている場合は失敗を意味します。すなわち、このオートマトンは実際は以下のオートマトンの省略になっています。
f:id:cloudear8:20170224083321p:plain
ちなみに、この暗黙的に用意される非受理状態fは前回実装したDFAではNothingで表されます。

このオートマトンを前回実装したDFA型の値として表してみましょう。

-- Examples.hs
-- [abc]+
abcPlus :: DFA Int Char
abcPlus = DFA {
    dfaTransTable = [
        (s0, 'a') --> s1
      , (s0, 'b') --> s1
      , (s0, 'c') --> s1
      , (s1, 'a') --> s1
      , (s1, 'b') --> s1
      , (s1, 'c') --> s1
      ]
  , dfaStart = s0
  , dfaAccepts = [s1]
  } where s0:s1:_ = [0..]

前回も説明しましたが、状態s0, s1の実体は区別できれば何でもいいので、

s0:s1:_ = [0..]

として適当な数値を割り当てています。

試しに実行してみましょう。

>>> abcPlus `accepts` "a"
True
>>> abcPlus `accepts` "b"
True
>>> abcPlus `accepts` "c"
True
>>> abcPlus `accepts` "accabbccbcbc"
True
>>> abcPlus `accepts` "accabbccbcbcd"
False
>>> abcPlus `accepts` "accabbdccbcbc"
False

abcPlusが正規表現[abc]+を表していることがわかると思います。

a(b|cd)*eを受理するオートマトン

このようなオートマトンは以下のように作ることができます。
f:id:cloudear8:20170224091002p:plain
また、このようなオートマトンを表すDFA型の値は以下のように定義することができます。

-- Example.hs
-- a(b|cd)*e
abcde :: DFA Int Char
abcde = DFA {
    dfaTransTable = [
        (s1, 'a') --> s2
      , (s2, 'b') --> s2
      , (s2, 'c') --> s3
      , (s3, 'd') --> s2
      , (s2, 'e') --> s4
      ]
  , dfaStart = s1
  , dfaAccepts = [s4]
  } where s1:s2:s3:s4:_ = [0..]

実行結果:

>>> abcde `accepts` "abcde"
True
>>> abcde `accepts` "ae"
True
>>> abcde `accepts` "abbbbe"
True
>>> abcde `accepts` "acdcdbcde"
True
>>> abcde `accepts` "acbde"
False
>>> abcde `accepts` "abcdcd"
False
>>> abcde `accepts` "abbeb"
False

このようにして実例を見ていくと、正規表現オートマトンで表せそうなことが何となくわかるのではないでしょうか。
それでは次回に続きます。

Haskellでtest/**/*Spec.hsを全部拾ってテストしてくれるやつ

Haskell

よく忘れるのでメモ

{-# OPTIONS_GHC -F -pgmF hspec-discover #-}

test/Spec.hsにこの1行を書くだけで、test/内の全部のテストを拾い集めて実行してくれるmainを生成してくれます。


明日は正規表現エンジンのこと書きます。

rsyncでポート番号を指定する

本当は正規表現エンジンについての話を書きたかったのですが、最近まとまった時間が取れないので関係ないことを書きます。

タイトルの通り。

$ rsync -e "ssh -p 12345" hoge@fuga.com:/foo/bar/baz/ /piyo/rofi/

これでok

正規表現エンジン制作入門(1): 正規表現とDFA

Haskell

オートマトンの単位は落としそうですが、今日から数回に分けてHaskell正規表現エンジンを自作していきたいと思います。

完成図

実は既に手元に完成品があるのですが、今回はHaskell正規表現DSLを構築したいと思います。動作例は以下の通り。

>>> str "hoge" `matches` "hoge"
True
>>> str "hoge" `matches` "fuga"
False
>>> ((str "hoge" |: str "fuga") *:) `matches` "hogefugahogefuga"
True
>>> ((str "hoge" |: str "fuga") *:) `matches` "hogefugahogefugafoobar"
False

str "hoge" が文字列 hogeを、|:が論理和を、*:が任意回の繰り返しを表します。

完成品は以下のリポジトリに上げる(予定)です。

github.com

オートマトン

正規表現エンジンを実装するには、まずオートマトンを作る必要があります。
オートマトンは理論上正規表現と等価な表現力を持っており、通常は正規表現をそのまま解析するのではなく、等価なオートマトンに変換してから文字列のマッチなどの処理を行います(たぶん)。
オートマトンは有限種類の状態からなり、入力文字によってその状態を変化させていく仮想的な機械です。文字列の各文字を先頭から順に入力していき、最終的に到達した状態の種類によって入力文字列が正規表現にマッチしたかどうかを判定します。

オートマトンにも種類はいろいろありますが、基本的に以下のような形で表すことができます。

-- Automaton.hs
module Automaton where

-- 以下2つは後でMapのキーにしたりするので、Ordのインスタンスになっています。
type Alphabet a = (Eq a, Ord a) -- アルファベット
type State s = (Eq s, Ord s) -- 状態

-- 後で使う
(-->) :: a -> b -> (a, b)
a --> b = (a, b)
infix 5 -->

-- オートマトン
class Automaton fa where
  type F fa s :: *
  step :: (State s, Alphabet a) => fa s a -> F fa s -> a -> F fa s
  initStates :: (State s, Alphabet a) => fa s a -> F fa s
  isAcceptStates :: (State s, Alphabet a) => fa s a -> F fa s -> Bool

これが状態型sを持ち、文字aの列[a]を認識するオートマトンfa s aの定義になります。
オートマトンは初期状態と呼ばれる値initStatesと、受理状態と呼ばれる値isAcceptStates, 遷移関数と呼ばれる関数stepの3種類からなります。

それぞれの定義にはF fa sという謎の型が使われていますが、これはとりあえずs自体と同等だと思ってください。オートマトンの種類によってはこのsが同時に複数存在したりする可能性があるので、抽象的な定義になっているだけです。

そうやってAutomatonの定義を読み替えると、以下のようになります。

-- 遷移関数
step :: (State s, Alphabet a) => fa s a -> s -> a -> s
-- 初期状態
initStates :: (State s, Alphabet a) => fa s a -> s
-- 受理状態
isAcceptStates :: (State s, Alphabet a) => fa s a -> s -> Bool

オートマトンfaはそれぞれ自分の状態sを持っており、その状態で文字aが入力されると、次の状態が

s' = step fa s a

となるs'に移ります。
初期状態s0のオートマトンfaに文字列a0:a1:a2:..:an:[]を与えた時、オートマトンは以下のように状態を遷移していきます。

s1 = step fa s0 a0
s2 = step fa s1 a1
...
sn = step fa s(n-1) a(n-1)
s(n+1) = step fa sn an

こうして最後にたどり着いた状態s(n+1)がisAcceptStatesを満たせば、その状態は受理状態であり、入力文字列は受理されたと言います。
最終的には、文字列が受理されることとその文字列が正規表現にマッチしていることが同値になるようなオートマトンを構成していくことになります。

今の説明に従って、オートマトンが文字列を「受理」するかどうかを判定する関数を書いてみましょう。

-- Automaton.hs
run :: (Automaton fa, State s, Alphabet a) => fa s a -> F fa s -> [a] -> F fa s
run fa ss [] = ss
run fa ss (a:as) = run fa (step fa ss a) as

-- dfa `accepts` str : dfa が列 str を受理すれば True, そうでなければ False
accepts :: (Automaton fa, State s, Alphabet a) => fa s a -> [a] -> Bool
fa `accepts` as = isAcceptStates fa (run fa (initStates fa) as)

次に、オートマトンの実際の実装例を一つ見てみましょう。以下のデータ型DFAは、オートマトンの中でも最も簡単なものである決定性有限オートマトン(Deterministic Finite Automaton)と言われるものです*1

-- Automaton/DFA.hs
module Automaton.DFA
import qualified Data.Map as M
import qualified Data.Set as S

data DFA state alpha = DFA {
    dfaTransTable :: M.Map (state, alpha) state
  , dfaStart :: state
  , dfaAccepts :: S.Set state
  } deriving (Show, Read)

instance Automaton DFA where
  type F DFA s = Maybe s
  step _ Nothing _ = Nothing
  step dfa (Just s) a = M.lookup (s, a) $ dfaTransTable dfa
  initStates dfa = Just (dfaStart dfa)
  isAcceptStates _ Nothing = False
  isAcceptStates dfa (Just s) = isAcceptState dfa s

isAcceptState :: (State s, Alphabet a) => DFA s a -> s -> Bool
isAcceptState dfa s = S.member s $ dfaAccepts dfa

DFAは初期状態をdfaStart, 受理状態を集合dfaAcceptsで表しており、状態sと文字aが来た時に次に遷移する状態をMapの形で持っています。
DFAの状態(F DFA s)はMaybe s型で表され、Nothingは常に失敗となりますが、これは単にMapに遷移先が書かれていなかった場合に無条件で失敗にするための実装上の都合です。

これを使って、簡単なオートマトンを作ってみましょう。
以下は"ab"の任意回の繰り返しを受理するオートマトンです。

-- Example.hs
{-# LANGUAGE
    OverloadedLists #-}
import Automaton
import Automaton.DFA (DFA(..))

n_times_of_ab :: DFA Int Char
n_times_of_ab = DFA {
    dfaTransTable = [
        (s, 'a') --> a
      , (a, 'b') --> b
      , (b, 'a') --> a
      ]
  , dfaStart = s
  , dfaAccepts = [b]
  } where s:a:b:_ = [0..]

OverloadedListsというGHC拡張が使われていますが、これはMapやSet等*2をリストリテラルと同様の表記で書けるようにするための拡張です。


s, a, bは状態です。区別できれば何でも良いので、s:a:b:_ = [0..]というように適当な数値を代入しています。

初期状態はsで、そこから入力文字'a'を受け取ると状態aになります。状態aから入力文字'b'を受け取ると状態bに移り、状態bから入力文字'c'を受け取ると状態aに戻ります。それ以外の場合は失敗(受理されない)です。

f:id:cloudear8:20170209170509p:plain

最終的に状態bにたどり着いていれば、その文字列は受理されたこととなります。

>>> n_times_of_ab `accepts` "" -- 空文字列は受理しない
False
>>> n_times_of_ab `accepts` "ab" -- "ab" の1回の繰り返しなのでok
True
>>> n_times_of_ab `accepts` "abababab" -- "ab" の4回の繰り返しなのでok
True
>>> n_times_of_ab `accepts` "ababababa" -- aで終わってるのでダメ
False
>>> n_times_of_ab `accepts` "aababab" -- 先頭がaaとなっているのでダメ
False
>>> n_times_of_ab `accepts` "bababab" -- bから始まっているのでダメ
False

*1:DFA自体の厳密な定義についてはここでは触れません。気になる方はWikipediaとかに載っているので読んでみてください。 決定性有限オートマトン - Wikipedia

*2:GHC.Exts.IsListのインスタンスである任意の型

Coqで型クラスで群論

Coq

群論に関する定義をするのであれば、型クラスを使うのが一番うまくいくと思います。

Class Group G :=
  {
    gunit : G;
    gadd : G -> G -> G;
    ginv : G -> G;
    gadd_unit_l : forall g : G, gadd gunit g = g;
    gadd_unit_r : forall g : G, gadd g gunit = g;
    gadd_assoc : forall a b c : G, gadd (gadd a b) c = gadd a (gadd b c);
    gadd_inv : forall g : G, gadd g (ginv g) = gunit /\ gadd (ginv g) g = gunit
  }.

Infix "<+>" := gadd (at level 40, left associativity).

何より、このgaddを演算子にできるのが便利です。他の方法で、例えば

Definition is_group (G : Type) (gadd : G -> G -> G) (gunit : G) ...

としても、gaddは単なる束縛変数なので、別な名前を付けることはできません。

群の定義だけして終わるのもつまらないので、簡単な定理を証明してみましょう。

単位元の一意性。

Theorem group_unit_unique:
  forall (G : Type) (Grp : Group G),
  forall u : G,
    (forall g : G, g <+> u = g /\ u <+> g = g)
    -> u = gunit.
Proof.
  intros G Grp u H.
  specialize (H gunit).
  destruct H.
  rewrite -> gadd_unit_l in H.
  assumption.
Qed.

逆元の一意性。

Theorem ginv_unique:
  forall (G : Type) (Grp : Group G) (g h : G),
    g <+> h = gunit /\ h <+> g = gunit
    -> h = ginv g.
Proof.
  intros G Grp g h H.
  destruct H.
  assert (Hinv := gadd_inv).
  specialize (Hinv g).
  destruct Hinv.
  rewrite <- H1 in H.
  assert (H3: ginv g <+> (g <+> h) = ginv g <+> (g <+> ginv g)).
  {
    rewrite -> H. reflexivity.
  }
  rewrite <- gadd_assoc in H3.
  rewrite -> H2 in H3.
  rewrite <- gadd_assoc in H3.
  rewrite -> H2 in H3.
  rewrite -> gadd_unit_l in H3.
  rewrite -> gadd_unit_l in H3.
  assumption.
Qed.

自明な群は任意の群の部分集合

Definition hom {G H : Type} {Grp : Group G} {Hrp : Group H} (f : G -> H) :=
  forall a b : G, f (a <+> b) = f a <+> f b.

Definition mono {A B : Type} (f : A -> B) :=
  forall a b : A, f a = f b -> a = b.

Definition subgroup (H G : Type) {Grp : Group G} {Hrp : Group H} (f : H -> G) :=
  mono f /\ hom f.

Inductive trivial : Type := T.

Instance trivial_group : Group trivial :=
  {
    gunit := T;
    gadd := fun _ _ => T;
    ginv := fun _ => T
  }.
Proof.
  (* gadd_unit_l *)
  intros g.
  destruct g.
  reflexivity.
  (* gadd_unit_r *)
  intros g.
  destruct g.
  reflexivity.
  (* gadd_assoc *)
  intros.
  reflexivity.
  (* gadd_inv *)
  intros.
  split.
  reflexivity.
  reflexivity.
Qed.

Definition trivial_to_grp {G : Type} {Grp : Group G} (z : trivial) : G := gunit.

Theorem trivial_subgroup:
  forall (G : Type) (Grp : Group G),
  exists f : trivial -> G,
    subgroup trivial G f.
Proof.
  intros G Grp.
  exists trivial_to_grp.
  unfold subgroup.
  split.
  - (* mono f *)
    unfold mono.
    intros a b H.
    destruct a.
    destruct b.
    reflexivity.
  - (* hom f *)
    unfold hom.
    intros a b.
    destruct a.
    destruct b.
    unfold trivial_to_grp.
    rewrite -> gadd_unit_l.
    reflexivity.
Qed.

Coqだと「部分群」などの概念をうまく記述できないので、より圏論的な同等の定義(monoな射の存在とか)で代替したほうがうまく書けるものが多い気がします。

Coqで型クラスでモナド

Coq

Haskell大好きなので、モナドを実装できそうな言語があればとりあえず実装してしまう癖があります。
Coqでモナド使うほどのことを書くのか、と言われればアレですが。

Class Monad (M : Type -> Type) :=
  {
    point {A : Type} : A -> M A;
    bind {A B : Type} : M A -> (A -> M B) -> M B
  }.


Infix ">>=" := bind (at level 65, left associativity).

試しにoptionでインスタンス定義してみます。

Definition option_point {T : Type} (x : T) : option T := Some x.
Definition option_bind {A B : Type}
           (m : option A) (f : A -> option B) : option B :=
  match m with
    | None => None
    | Some x => f x
  end.

Instance option_monad : Monad option :=
  {
    point := @option_point;
    bind := @option_bind
  }.

たぶん使わないけどCoqでoptionモナドができました。

Coqなので、例えば m >>= f = Some x なら m = Some a のようなことも証明できてしまいます。すごい。

Theorem option_bind_some:
  forall (A B : Type) (m : option A) (f : A -> option B),
    (exists b : B, m >>= f = Some b)
    -> (exists a : A, m = Some a).
Proof.
  intros A B m f H.
  destruct H as [b].
  destruct m as [m' | ].
  - exists m'.
    reflexivity.
  - simpl in H.
    congruence.
Qed.

Coqで型クラス

Coq

Coqにも型クラスがあるらしいです。

Class Ord a :=
  {
    le : a -> a -> bool
  }.

これでleというメソッドを持つ型クラスOrdを定義できます。

インスタンス定義は以下のように行います。

Fixpoint le_nat (n m : nat) : bool :=
  match n, m with
    | O, O => true
    | O, S _ => true
    | S _, O => false
    | S n', S m' => le_nat n' m'
  end.

Instance nat_ord : Ord nat :=
  {
    le := le_nat
  }.

複数のインスタンスを定義することもできます。

Instance nat_rev_ord : Ord nat :=
  {
    le := fun x y => le_nat y x
  }.

どのインスタンスを選択するかは、

@le nat nat_rev_ord

のように明示的に与えてやればOKです。

Coqにはそもそも暗黙引数があるので、型クラスがあるからと言って無い場合に比べてめちゃくちゃ便利になるかと言われるとそういうことも無さそうです。暗黙引数でレコード型を渡すのと書き方的にもそんなに変わりません。