Agda による Automaton の実装

Menu Menu

河野真治 (琉球大学)


Continuation based C による MoarVM の実装

来年初頭のプロシンで発表します...


CbC 軽量継続が使えるC

   __code next(INTERP i) {
       goto cbc_expr(i);
   }

C-- とかにも parameterized goto はある。tail call 専用構文があるのが特徴。

LLVM/GCC 実装がある。


Continuation basd C repository

github / bitbucket もあったような気がするが...

http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_gcc http://www.cr.ie.u-ryukyu.ac.jp/hg/CbC/CbC_llvm


MoarVM Perl6/Rakudo のbyte code machine

NQP (Not quite perl)というPerl6のsubset によるRakudo compiler

VMは JVM/MoarVM の二種類。C で記述されている

MoarVMは間接label gotoで実装(switch文もある)

    OP(extend_u8):
        GET_REG(cur_op, 0).u64 = (MVMuint64)GET_REG(cur_op, 2).u8;
        cur_op += 4;
        goto NEXT;

その部分をCbCのCode Segmentで置き換える

    __code cbc_extend_u8(INTERP i){
        GET_REG(i->cur_op, 0,i).u64 = (MVMuint64)GET_REG(i->cur_op, 2,i).u8;
        i->cur_op += 4;
        goto cbc_next(i);
    }


現状は

例題の85%程度が実行可能

速度的なメリットはまだない。置き換えただけ

CbCの LLVM/GCCのバグ取り中〜 (stack修正のコードがでない...)

    _cbc_exit:
    LFB2:
            pushq   %rbp
    LCFI6:
            movq    %rsp, %rbp
    LCFI7:
            movq    %rdi, -8(%rbp)
   詳しいことはプロシンで...


Agda

Haskell に似た構文を持つ依存型言語。Curry Howard 対応に基づく定理証明系。

    data  States1   : Set  where
       sr : States1
       ss : States1
       st : States1
    fin1 :  States1  → Bool
    fin1 st = true
    fin1 _ = false


Haskellとの違い

data (Sum type)と record (Product)が分かれている。

    data Mammal s = Cat { name :: String, color :: s }
        |        Dog { name :: String, color :: s }
        deriving (Show)

Agda
    record MammalP {s : Set } : Set where
      field
         name : String
         color : s
    data Mammal {s : Set } : Set where
      Cat : MammalP {s} → Mammal
      Dog : MammalP {s} → Mammal

{s} は省略可能な引数。適当に推論されて代入される。


Automatonの授業を Agda でやろう

まだ、Automaton の授業って必要なの?

   コンピュータって、そもそもAutomaton
   機械学習のモデルもAutomaton
   PとNPって知ってる?
   正規表現とその実装
   Turing Machine

単に知っているだけでなく、数学的に理解し、それに関する論理的推論ができる必要がある


Automaton の一般的な目標

  DFA 
  Regular language 
  RegularからNFAの変換(普通はε遷移入り)
  NFAからDFAの変換(subset construction)
  Regular language = DFA
  ω Automaton (入力が無限長の場合) (*)
  Model checking (*)

を示す。(*) は普通やりません。


Automaon の記述

    record Automaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
            δ : Q → Σ → Q
            astart : Q
            aend : Q → Bool

Automatonが持つ機能(関数)の直積として表現される。


Automaon のaccept の記述

    accept : { Q : Set } { Σ : Set  }
        → Automaton Q  Σ
        → List  Σ → Bool
    accept {Q} { Σ} M L = move (astart M) L
       where
          move : (q : Q ) ( L : List  Σ ) → Bool
          move q [] = aend M q
          move q ( H  ∷ T ) = move (  (δ M) q H ) T

入力はListで表す。


NFA の記述 (ダメな例)

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              nδ : Q → Σ → List Q
              sid : Q  →  ℕ
              nstart : Q
              nend  : Q → Bool

NFAは複数の状態に非決定的に遷移する。

これだと move の記述が煩雑になる。 nfa-list.agda


NFA の記述 (良い例)

    record NAutomaton ( Q : Set ) ( Σ : Set  )
           : Set  where
        field
              Nδ : Q → Σ → Q → Bool
              Nstart : Q → Bool
              Nend  :  Q → Bool

状態の集合Qの部分集合を表すのに

   Q → Bool

を使う。


NFA の実行

    Nmoves : { Q : Set } { Σ : Set  }
        → NAutomaton Q  Σ
        → {n : ℕ } → FiniteSet Q  {n}
        →  ( Q → Bool )  → Σ → Q → Bool
    Nmoves {Q} { Σ} M fin  Qs  s q  =
          exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q )  ))

exists : ( p : Q → Bool ) → Bool は、p x をtrueにする x : Q があるというのを表す関数。


Subset Construction の記述

    δconv : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} 
        →  ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
    δconv {Q} { Σ} { n} N nδ f i q =  exists N ( λ r → nδ r i q )
    subset-construction : { Q : Set } { Σ : Set  } { n  : ℕ }  → FiniteSet Q {n} →  
        (NAutomaton Q  Σ ) → (Automaton (Q → Bool)  Σ )  
    subset-construction {Q} { Σ} {n} N NFA = record {
            δ = λ q x → δconv N ( Nδ NFA ) q x
         ;  astart = Nstart NFA 
         ;  aend = exists N ( λ q → f q ∧ Nend NFA q )
       } 

超短い。Listや Procedural な言語で実装すると死ねる。


exists をどう記述するか?

∀ x は入力変数で良い

   lemma1 : ∀ (x :  ℕ) → zero ≤ x * x 

∃ x は skolem 関数を使う

   lemma2 : ∀ (x :  ℕ) → (next :  ℕ →  ℕ ) → x < next x

exists : ( Q → Bool ) → Bool

はね... Qが数え上げできれば...

record で要求してしまっても良い。二重否定を使うとできるかも? 入力が増えてしまう..

   exists p = ¬ (  ∀ (x : Q ) → ¬ ( p x  ≡ true )


Finite Set

Data.Fin をそのまま使う方が楽。でも、Data.Fin に iso だということを表す reocrd を使う。

    record FiniteSet ( Q : Set ) { n : ℕ }
            : Set  where
         field
            Q←F : Fin n → Q
            F←Q : Q → Fin n 
            finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
            finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
         lt0 : (n : ℕ) →  n Data.Nat.≤ n
         lt0 zero = z≤n
         lt0 (suc n) = s≤s (lt0 n)
         lt2 : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
         lt2 {zero} lt = z≤n
         lt2 {suc m} {zero} ()
         lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
         exists : ( Q → Bool ) → Bool
         exists p = exists1 n (lt0 n) p where
             exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
             exists1  zero  _ _ = false
             exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) ∨ exists1 m (lt2 m<n) p

不等号の扱いがな〜

exists は linear search なので遅いです。


Regular Expression の記述

構文木は data で表す

    data Regex   ( Σ : Set  ) : Set  where
       _*    : Regex  Σ → Regex  Σ
       _&_   : Regex  Σ → Regex  Σ → Regex Σ
       _||_  : Regex  Σ → Regex  Σ → Regex Σ
       <_>   : Σ → Regex  Σ


Regular Language の記述

選択は簡単

    regular-language (x || y) f = λ s → ( regular-language x f s ) ∨ ( regular-language y f s )

結合は難しい

    regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
    _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
    x ・ y = λ z → ?


文字列の分割の数え上げ split を使う

    split : {Σ : Set} → (List Σ → Bool)
          → ( List Σ → Bool) → List Σ → Bool
    split x y  [] = x [] ∧ y []
    split x y (h  ∷ t) = (x [] ∧ y (h  ∷ t)) ∨
      split (λ t1 → x ( ( h ∷ [] ) ++ t1 ))  (λ t2 → y t2 ) t
    _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
    x ・ y = λ z → split x y z
    {-# TERMINATING #-}
    repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
    repeat x [] = true
    repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
    regular-language : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) →  List Σ → Bool
    regular-language (x *) f = repeat ( regular-language x f )
    regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
    regular-language (x || y) f = λ s → ( regular-language x f s ) ∨ ( regular-language y f s )
    regular-language < h > f [] = false
    regular-language < h > f (h1  ∷ [] ) with F←Q fin h ≟  F←Q fin h1
    ... | yes _ = true
    ... | no _  = false
    regular-language < h > f _ = false


ω Augomaton の記述

    ω-run : { Q  Σ : Set } → (Ω : Automaton Q Σ ) →  ℕ → ( ℕ → Σ )  → Q
    ω-run Ω zero s = astart Ω
    ω-run Ω (suc n) s = δ Ω (ω-run Ω n s) ( s n )
    record Buchi { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
        field
            from : ℕ
            stay : (n : ℕ ) → n > from → aend Ω ( ω-run Ω n S ) ≡ true
    open Buchi
           
        
    record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
        field
            next     : (n : ℕ ) → ℕ 
            infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 


結論

証明のためのプログラムの記述と実装のためのプログラムの記述は異なる

    データ型の実装を記述しない

  関数でデータ型の性質を記述する

なので、

  証明からプログラムを生成するのは良くない  実装が証明向きの記述と同等であることを示すのが良い

∃ x はめんどくさい。

    定番とか方法ありますか?

河野真治 (琉球大学) / Sat Nov 17 14:29:38 2018