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 compilerVMは 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 xexists : ( 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 はめんどくさい。
定番とか方法ありますか?