--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a03/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,135 @@
+-title: 決定性オートマトン
+
+-- Automaton オートマトンの定義 ( Q, Σ, σ, q0, F )
+
+    1. Q is a finte set calles states
+    2. Σ is a finte set calles alphabet
+    3. δ : Q x Σ is the transition function
+    4. q0 ∈ Q is the start state
+    5. F ⊆ Q is the set of accept states
+
+これを Agda で表すには record を使う。
+
+    record Automaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+            δ : Q → Σ → Q
+            astart : Q
+            aend : Q → Bool
+
+<a href="../agda/automaton.agda"> automaton.agda </a>
+
+record は名前のついた数学的構造で、二つの集合 Q と Σの関係定義する関数からなる。
+
+record は直積で複数の集合の組だが、ここでは関係を表す論理式/関数の型の組になっている。
+
+      astart : Q
+
+Q の要素一つを表している。このrecordが一つあると、astart で一つQの要素を特定できる。
+
+      δ : Q → Σ → Q
+
+は関数で、引数を二つ持っている。ここでは論理式ではない。入力となるaplhabet(文字) とstate (状態)から次の状態を指定する関数である。
+transition function (状態遷移関数)と呼ばれる。
+
+       aend : Q → Bool
+
+これはQの部分集合を指定している。Bool は
+
+     data Bool : Set where
+        true   : Bool
+        false  : Bool
+
+で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか?)
+
+--オートマトンの入力
+
+オートマトンの入力は文字列である。文字列を表すには List を用いる。
+
+    data  List  (A : Set ) : Set  where
+       [] : List A
+       _∷_ : A → List A → List A
+
+    l2 = a ∷ b ∷ a ∷ c ∷  []
+
+だったことを思い出そう。(Agda のbuiltinのListは ∷ を使う)
+
+
+--状態遷移
+
+状態遷移関数をListに適用する。
+
+    moves : { Q : Set } { Σ : Set  }
+        → Automaton Q  Σ
+        → Q → List  Σ → Q
+    moves {Q} { Σ} M q L = move q L
+       where
+          move : (q : Q ) ( L : List  Σ ) → Q
+          move q [] = q
+          move q ( H  ∷ T ) = move (  (δ M) q H ) T
+
+List に沿って、状態が変わる。
+
+    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
+
+最後の状態が aend ならば accept される。これらを、record Automaton 内で定義しても良い。
+
+---具体的なオートマトン
+
+reccord Automaton は抽象的なオートマトンで実装がない。(Java/C++ の abstract classと同じ)
+実装を与えるには、record のfield の型を持つ関数を与えれば良い。
+
+まず、状態と文字を定義する。
+
+    data  States1   : Set  where
+       sr : States1
+       ss : States1
+       st : States1
+
+    data  In2   : Set  where
+       i0 : In2
+       i1 : In2
+
+状態遷移関数と accept state を作ろう。
+
+    transition1 : States1  → In2  → States1
+    transition1 sr i0  = sr
+    transition1 sr i1  = ss
+    transition1 ss i0  = sr
+    transition1 ss i1  = st
+    transition1 st i0  = sr
+    transition1 st i1  = st
+
+    fin1 :  States1  → Bool
+    fin1 st = true
+    fin1 _ = false
+
+st になればok。record は以下のように作る。
+
+    am1  :  Automaton  States1 In2
+    am1  =  record {  δ = transition1 ; astart = sr ; aend = fin1   }
+
+これを動かすには、
+
+    example1-1 = accept am1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+    example1-2 = accept am1 ( i1  ∷ i1  ∷ i1  ∷ [] )
+
+とする。( example1-1 の型は何か?)
+
+--問題 3.1
+
+教科書のAutomatonの例のいくつかを Agda で定義してみよ。
+
+accept される入力と accept されない入力を示し、Agda で true false を確認せよ。
+
+<a href=""> </a>  <!---  Exercise 3.1 --->
+
+
+