--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a01/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,80 @@
+-title: オートマトンの概要
+
+オートマトンは自動的に動く人形という意味だが、ここでは文字列に対して自動的にできることを理論的に解析する。
+入力は有限の種類の文字が有限個並んだ文字列である。それを機械が読み込み、答えを返す。つまり、計算機そのものである。
+機械が文字列を返す場合もあるし、受け入れたかどうかを真偽で返す場合もある。
+機械はメモリと、メモリと入力によって次のメモリの状態が決まるとする。つまり、状態遷移機械(state transition)である。
+
+この機械の様々な形の実装を調べて、それを比較する。また、受けれる文字列の集合を使って特徴づける。さらに、
+計算にかかるメモリと時間に付いて考察する。
+
+--証明と関数言語
+
+証明は、命題の集まりと、それを結ぶ推論からなるネットワーク構造であることを学ぶ。
+関数言語は、集合である型と、それを結ぶ関数からなるネットワーク構造である。
+
+証明と関数言語が対応することを学び、証明を関数型言語(型つきλ計算)で表す。(カーリーハワード対応)
+
+オートマトンの様々な概念をカーリーハワード対応に基づく証明支援系であるAgdaで記述しいていく。
+
+いくつかの例題を通して、Agdaに慣れる。
+
+--実装方法による区別
+
+---決定性有限オートマトン
+
+メモリが有限で、一文字読む毎に状態が進む
+
+---非決定性有限オートマトン
+
+進む状態が複数ある
+
+---ε有限オートマトン
+
+文字を読み込まないでも状態遷移することができるオートマトン
+
+---push down オートマトン
+
+無限長のスタックを一つ持つオートマトン
+
+---Turing Machin
+
+無限長のスタックを二つ(あるいはテープを一つ)持つオートマトン
+
+--文字列集合による区別
+
+--正規集合
+
+文字の選択、文字の結合、そして、その繰り返しによって作られる文字列の集合
+
+--正規表現からオートマトンへの変換
+
+--正規表現の効率的な実装
+
+--決定性オートマトンと非決定性オートマトンの関係
+
+--Turing Machin の性質
+
+--万能 Turing Machin 
+
+--Turing Machin の停止性
+
+--計算量
+
+非決定性Turing Machine
+
+P と NP
+
+--時相論理とモデル検査
+
+プログラムのInteractiveな仕様記述方法である時相論理を学び、そのモデルとして
+無限長の入力を扱うωオートマトンを使用する。
+
+オートマトンが時相論理式を満たしているかどうかを調べるモデル検査に付いて学ぶ。
+
+SMVなどのモデル検査系を使えるようにする。
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,588 @@
+-title: 証明と関数型言語、Agda
+
+問題は、メールでSubjectを (a01 の 問題2.5ならば)
+    Subject: Report on Automan Lecture 2.5 
+として、問題毎に提出すること。
+
+kono@ie.u-ryukyu.ac.jp まで送ること。
+番号のついてない問題はオプションです。
+
+学籍番号をメールの中に記述すること。
+問題番号は正確に記述すること。
+出席しない場合でも、問題解答を送れば出席扱いとします。
+
+提出期限は ura.ie.classes.automaton で知らせます。
+
+
+--証明と関数型言語の関係
+
+証明とは、論理式それを結ぶ推論からなる数学的な構造である。また、関数型言語は集合である型とそれを結ぶ関数からなる数学的構造である。
+
+型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより
+
+論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。
+
+
+--あらすじ
+
+1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する
+    これは構文定義、あるいは、論理式の作り方に相当する
+
+2) 演算子を導入する推論と、除去する推論を定義する。
+　　これには証明図を使う
+
+3) 推論に対応する関数を表す項を考える
+   項は関数型言語の要素になる
+
+　　項の導入 ...  データ構造のconstructor
+　　項の除去 ...  データ構造のaccesor
+
+    導入は関数の出力の型に現れる
+    除去は関数の入力の型に現れる
+
+これを演算子の数の分だけ繰り返す。
+
+次に等式論理を学ぶ。
+
+4) x = x の導入と除去
+
+5) 項が等しいとはとういうことかを学ぶ　　
+    正規形
+
+    正規形を得ることが関数型言語の計算(項の操作)
+
+以上のことを Agda (Haskell に似た構文を持つ証明支援系)で記述する。
+
+--証明の基本
+
+A は論理式を表す変数。あるいは型Aという集合。論理式は変数と論理演算子で表される木構造。変数や演算子は構文要素。
+
+     A → B
+
+これは「AならばB」というのに対応する。関数の視点からは、Aという型からBという型への関数。
+AとBは型を表す論理式。
+
+      A
+  -----------
+      B
+
+Aを仮定して、Bが証明されたことを表す図。証明図。
+
+--関数適用による証明
+
+導入                          除去
+
+       A                   
+       :
+       B                    A       A → B
+   -------------         ------------------
+      A → B                     B
+
+対応する項。項とは、関数型プログラムを構成する構文要素。木構造で表される。
+
+
+    λ x → y
+
+x は変数、y は項。y は複雑な項(関数のbody)でも良い。これは構文定義でもある。変数 x と項yから 
+λ x → y という項を作れる。 x は構文的にスコープを持っている。つまり、関数の引数と同じ扱いとする。
+
+項には型が対応する。これは、再帰的に定義される
+
+    x : A
+
+は、x という項が型Aを持つと言うのを表している。
+
+x : A かつ y : B の時に、
+
+    λ x → y : A → B
+
+と定義する。
+
+---問題2.1 Agdaによる関数と証明
+
+
+以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
+
+<a href="agda/lambda.agda"> lambda </a> <!---  Exercise 2.1 --->
+
+
+---Agdaの構文
+
+型と値
+
+名前の作り方
+
+indent
+
+implicit variable
+
+infix operator and operator order
+
+<a href="agda.html"> agda の細かい構文の話 </a> 
+
+--record または ∧
+
+導入                          除去
+
+     A    B                 A ∧ B           A ∧ B 
+   -------------         ----------- π1   ---------- π2
+      A ∧ B                   A               B
+
+除去は複数あるので名前を区別する必要がある。つまり、それぞれに項を用意する必要がある。
+
+A ∧ B は新しく導入した型である。
+型Aと型Bから作るデータ構造であり、オブジェクトあるいは構造体だと思って良い。
+π1 π2 は構造体から  field を抜き出す accesor によって実装できる。
+
+
+
+record によって  
+
+   record _∧_ A B : Set
+     field
+         π1 : A
+         π2 : B
+
+_∧_　は中置演算子を表す。
+
+     _∧_ A B
+
+は
+
+     A ∧  B
+
+とかける。(Haskell では (∧) を使う)
+
+は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。
+
+   record { π1 = x ; π2 = y }    
+
+
+---例題
+
+     A → B  ∧  B → C  →  A → C 
+
+まず、正しくかっこを付ける。
+
+     (( A → B ) ∧  ( B → C )) → ( A → C  )
+
+線を上に引く。
+
+              :
+  -------------------------------------------------
+     (( A → B ) ∧  ( B → C )) → ( A → C  )
+
+: はこれから埋めていく部分。まず適用するのは→のintro duction である。 ( A → B ) ∧  ( B → C )を仮定で使えるようになる。 
+
+             :
+           A → C  
+  -------------------------------------------------
+     (( A → B ) ∧  ( B → C )) → ( A → C  )
+
+さらに→introを使う。Aを仮定で使えるようになる。
+
+             :
+             C
+  -------------------------------------------------
+           A → C  
+  -------------------------------------------------
+     (( A → B ) ∧  ( B → C )) → ( A → C  )
+
+仮定でCを生成できるのは  B → C しかない。
+
+         B       B → C
+      ---------------------
+             C
+
+これは→elim である。 B → C は仮定( A → B ) ∧  ( B → C )の左側が使える
+
+      ( A → B ) ∧  ( B → C )
+      ---------------------   π2
+            B → C
+
+B の方もがんばると、最終的に
+
+      [ ( A → B ) ∧  ( B → C )]*1
+  --------------------------------- π1
+      [A]*2    A → B                      [ ( A → B ) ∧  ( B → C ) ]*1
+     ---------------- →elim              -------------------------------   π2
+             B                                 B → C
+          ----------------------------------------------- →elim
+                      C
+  ------------------------------------------------- →intro 2
+                     A → C
+  ------------------------------------------------- →intro 1
+     (( A → B ) ∧  ( B → C )) → ( A → C  )
+
+となる。
+
+Agda では、
+
+    lemma : (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma = ?
+
+とすると、A B C が未定義だと言われる。
+
+    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma = ?
+
+引数が一つあるので、それに名前を付ける。
+
+    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma f∧g = ?
+
+いや引数は二つだった。
+
+    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma f∧g a = ?
+
+f∧g は直積なので、
+
+    π1 f∧g :  A → B
+    π2 f∧g :  B → C
+
+なことを考えると、
+
+    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma f∧g a = π2 f∧g ?
+
+ここで、π2 f∧g ? は (π2 f∧g) ? であることを思い出そう。最終的に、
+
+    lemma : {A B C : Set } → (( A → B ) ∧  ( B → C )) → ( A → C  )
+    lemma f∧g a = π2 f∧g (π1 f∧g) a
+
+(ここで、(π2 f∧g (π1 f∧g)) a と書かなくても良いのは何故か?)
+
+前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。
+
+---問題2.2 Agdaのrecord
+
+以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
+
+<a href="agda/record1.agda"> record </a> <!---  Exercise 2.2 --->
+
+
+--data または 排他的論理和(Sum)
+
+ここで扱っている論理(直観主義論理)では∧に対称的な形で∨を定義することはしない。導入は対称的になるが除去はおかしくなってしまう。
+そこで次のように定義することになっている。
+
+除去                           導入
+               A      B
+               :      :
+      A ∨ B    C      C            A               B
+   ------------------------  ----------- p1   ---------- p2
+           C                     A ∨ B           A ∨ B 
+
+
+    data _∨_ (A B : Set) : Set where
+      p1 : A → A ∨ B
+      p2 : B → A ∨ B
+
+dataはCで言えばcase文とunion に相当する。Scala のCase Classもこれである。Cと違いunionにはどの型が入っているかを区別するtagが付いている。
+
+p1 と p2 は A ∨ B を構成する constructor (推論ではintroduction)であり、case 文が eliminator に相当する。
+
+Haskellと同様にp1/p2はパターンマッチで場合分けする。
+
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 = ?
+
+場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。
+
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 (p1 x) = ?
+    ex3 (p2 x) = ?
+
+
+---問題2.3 Agdaのdata
+
+
+<a href="agda/data1.agda"> data </a> <!---  Exercise 2.3 --->
+
+--有限な集合と Nat 
+
+data は有限な要素を持つ集合を構成できる。
+
+    data Three : Set where
+      t1 : Three
+      t2 : Three
+      t3 : Three
+
+    open Three
+
+    data 3Ring : (dom cod : Three) → Set where
+       r1 : 3Ring t1 t2
+       r2 : 3Ring t2 t3
+       r3 : 3Ring t3 t1
+
+これは、三つのVertexとEdgeを持つグラフをdataで表してみたものである。
+
+任意の個数を表すためには自然数(Natural Number)を作る必要がある。ペアノの公理が有名だが、dataを使って以下のように構成する。
+
+    data Nat : Set where
+      zero : Nat
+      suc  : Nat →  Nat
+
+    add : ( a b : Nat ) → Nat
+    add zero x = x
+    add (suc x) y = suc ( add x y )
+
+    mul : ( a b : Nat ) → Nat
+    mul zero x = ?
+    mul (suc x) y = ?
+
+--問題1.4 Nat 
+
+? を埋めて掛け算を完成させよう。
+
+--Equality
+
+自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は
+
+   ---------------
+      x == x
+
+だが、ここには隠れた仮定がある。x は何かの集合の要素なはず。
+
+     { x : A }
+   ---------------
+      x == x
+
+さらに左辺と右辺は等しいが、
+
+     add zero zero == zero
+
+では左辺と右辺は項として同じではない。計算して同じということにして欲しい。つまり、
+
+　　Agdaの項には計算していくと決まった形に落ちる
+
+という性質があって欲しい。この計算はλ項に対して定義する必要がある。この計算をreduction(縮約)、
+決まった形をnormal form(正規形)と言う。
+
+<a href="reduction.html">Reduction</a>
+
+Agda での定義は以下のようになる。
+
+    data _==_ {A : Set } : A → A → Set where
+       refl :  {x : A} → x == x
+
+refl は reflection (反映) の略である。refl は 等式のconstructorになる。
+
+Elmination は変数の置き換えになる。
+
+      x == y    f x y
+   ------------------------
+          f x x
+
+x == y は入力の型であり、refl とうパターンでしか受けられない。この時に、x と y が等しい必要がある。
+
+しかし、x と y は項なので変数を含むことがある。Agda に等しいことを確信させる必要がある。
+この問題はパターンマッチの時にもすででていた。これは項(正規化された)を再帰的に比較していく
+手順が必要になる。これは単一化(Unification)と呼ばれる。
+
+<a href="unification.html">Unification</a>
+
+    ex1 : {A : Set} {x : A } → x == x
+    ex1  = ?
+
+    ex2 : {A : Set} {x y : A } → x == y → y == x
+    ex2 = ?
+
+    ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
+    ex3 = ?
+
+    ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
+    ex4 = ?
+
+以上の証明を refl を使って完成させてみよう。
+
+<a href="agda/equality.agda"> equality </a> <!---  Exercise 2.4 --->
+
+--集合のLevel 
+
+論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。
+
+    ex1 : { A B : Set} → Set
+    ex1 {A} {B} =  A → B
+
+Agda は高階論理なので、論理式自体を返す論理式も作ることができる。
+
+    ex2 : { A B : Set} →  ( A → B ) → Set
+    ex2 {A} {B}  A→B  =  ex1 {A} {B}
+
+
+では、これを論理式を要素として持つ直積を作ってみよう。
+
+    record FuncBad (A B : Set) : Set where
+      field
+         func : A → B → Set
+
+Agda は以下のように文句をいう。
+
+    The type of the constructor does not fit in the sort of the
+    datatype, since Set₁ is not less or equal than Set
+    when checking the definition of FuncBad
+
+自己参照的な集合の定義を避けるために集合には階(level)という概念が導入されている。
+
+    open import Level
+    record Func {n : Level} (A B : Set n ) : Set (suc n) where
+      field
+        func : A → B → Set n
+
+のように集合の階(Level)を明示する必要がある。
+
+--問題1.5 集合のLevel 
+
+level が合うように ? を埋めよ。
+
+<a href="agda/level1.agda"> level </a> <!---  Exercise 2.5 --->
+
+--問題2.6 List
+
+List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。
+
+    postulate A : Set
+
+    postulate a : A
+    postulate b : A
+    postulate c : A
+
+
+    infixr 40 _::_
+    data  List  (A : Set ) : Set  where
+       [] : List A
+       _::_ : A → List A → List A
+
+
+    infixl 30 _++_
+    _++_ :   {A : Set } → List A → List A → List A
+    []        ++ ys = ys
+    (x :: xs) ++ ys = x :: (xs ++ ys)
+
+    l1 = a :: []
+    l2 = a :: b :: a :: c ::  []
+
+    l3 = l1 ++ l2
+
+等式の変形を利用して、List の結合法則を証明してみよう。
+
+    open  import  Relation.Binary.PropositionalEquality
+
+    ++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
+    ++-assoc A [] ys zs = let open ≡-Reasoning in
+      begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
+       ( [] ++ ys ) ++ zs
+      ≡⟨ refl ⟩
+        ys ++ zs
+      ≡⟨⟩
+        [] ++ ( ys ++ zs )
+      ∎
+    ++-assoc A (x :: xs) ys zs = let open  ≡-Reasoning in ?
+
+≡⟨⟩ などの定義はどこにあるのか?
+
+--問題2.6 List
+
+lemma を等式の変形を利用して証明してみよ。
+
+<a href="agda/list.agda"> List </a> <!---  Exercise 2.6 --->
+
+--DAGと否定
+
+グラフには接続されてない二点が存在する。それを表現するために否定¬と矛盾⊥を導入する。
+
+       ⊥
+    ------------- ⊥-elim
+       A
+
+矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。
+
+これは、contructor のない data で表すことができる。
+
+    data ⊥ : Set where
+
+⊥-elim は以下のように証明できる。
+
+    ⊥-elim : {A : Set } -> ⊥ -> A
+    ⊥-elim ()
+
+() は「何にもmatchしないパターン」である。これは型を指定した時に「可能な入力がない」必要がある。つまり、このケースは起こり得ない
+ことを Agda が納得する必要がある。納得できないと error message がでる。
+
+    λ ()
+
+という構文も存在する。
+
+⊥ を使って否定は以下のように定義される。
+
+    ¬_ : Set → Set
+    ¬ A = A → ⊥
+
+否定には入力があることを意識しておこう。
+
+         f0
+      -----→
+   t0         t1
+      -----→
+         f1
+
+というグラフは以下のように記述する。
+
+    data  TwoObject   : Set  where
+           t0 : TwoObject
+           t1 : TwoObject
+
+
+    data TwoArrow  : TwoObject → TwoObject → Set  where
+           f0 :  TwoArrow t0 t1
+           f1 :  TwoArrow t0 t1
+
+ループのあるグラフを作ってみよう。
+
+         r0
+       -----→
+    t0         t1
+       ←-----
+         r1
+
+    data Circle  : TwoObject → TwoObject → Set  where
+           r0 :  Circle t0 t1
+           r1 :  Circle t1 t0
+
+矢印をたどって繋がっている点は接続(connected)されていると言う。
+
+    data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
+        direct :   E x y -> connected E x y
+        indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
+
+直接繋がっているか、間接的に繋がっているかどちからになる。この構造は自然数に似ている。
+
+t0 と t1 が TwoArrow の場合に繋がっていることを証明してみる。
+
+    lemma1 : connected TwoArrow t0 t1
+    lemma1 =  ?
+
+t1 から t0 にはいけない。
+
+    lemma2 : ¬ ( connected TwoArrow t1 t0 )
+    lemma2  = ?
+
+dag (Directed Acyclic Graph) は、すべての点(Vertex)で自分自身につながる経路(Edge)がないグラフ
+
+    dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+    dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+--問題2.7 DAGと否定
+
+TwoArrow が dag で、Circle が dag ではないことを証明してみよう。
+
+    lemma4 : dag TwoArrow
+    lemma4 = ?
+
+    lemma5 :  ¬ ( dag Circle )
+    lemma5 = ?
+
+<a href="agda/dag.agda"> DAG </a> <!---  Exercise 2.7 --->
+

--- /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 --->
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a04/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,117 @@
+-title: 非決定性オートマトン
+
+決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
+
+例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
+
+この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。
+
+    record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              nδ : Q → Σ → List Q
+              sid : Q  →  ℕ
+              nstart : Q
+              nend  : Q → Bool
+
+これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
+
+次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
+
+少し複雑がだが、insert と merge を定義して、
+
+<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
+
+    insert : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) →  List Q  → Q  → List Q
+    insert  M  [] q =  q ∷ []
+    insert  M  ( q  ∷ T ) q' with  (sid M q ) ≟ (sid M q')
+    ... | yes _ = insert  M  T q'
+    ... | no _ = q  ∷ (insert  M  T q' )
+
+    merge : { Q : Set } {  Σ : Set } → ( NAutomaton Q  Σ  ) → List Q  → List Q  → List Q
+    merge  M L1 [] = L1
+    merge  M L1 ( H  ∷ L  ) =  insert M (merge M L1 L ) H
+
+    Nmoves : { Q : Set } { Σ : Set  }
+        → NAutomaton Q  Σ
+        → List Q → List  Σ → List Q
+    Nmoves {Q} { Σ} M q L = Nmoves1 q L []
+       where
+          Nmoves1 : (q : List Q ) ( L : List  Σ ) → List Q → List Q
+          Nmoves1 q  [] _ = q
+          Nmoves1 []  (_  ∷ L) LQ = Nmoves1 LQ L []
+          Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge M  ( nδ M q H ) LQ )
+
+    Naccept : { Q : Set } { Σ : Set  }
+        → NAutomaton Q  Σ
+        →  List  Σ → Bool
+    Naccept {Q} { Σ} M L =
+           checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
+       where
+          checkAccept : (q : List Q ) → Bool
+          checkAccept [] = false
+          checkAccept ( H ∷ L ) with (nend M) H
+          ... | true = true
+          ... | false = checkAccept L
+
+とする。 
+
+--部分集合を使うと簡単になる
+
+<a href="../agda/nfa-list.agda"> nfa-list.agda </a>
+
+
+    record NAutomaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+              Nδ : Q → Σ → Q → Bool
+              Nstart : Q → Bool
+              Nend  :  Q → Bool
+
+
+    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 )  ))
+
+
+    Naccept : { Q : Set } { Σ : Set  } 
+        → NAutomaton Q  Σ
+        → {n : ℕ } → FiniteSet Q {n}
+        → List  Σ  → Bool
+    Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
+       where
+          Naccept1 : NAutomaton Q  Σ → ( Q → Bool ) →  List  Σ  →  Bool
+          Naccept1 M sb []  = exists fin ( λ q → sb q ∧ Nend M q )
+          Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M  fin sb i ) t
+
+--例題
+
+    transition3 : States1  → In2  → States1 → Bool
+    transition3 sr i0 sr = true
+    transition3 sr i1 ss = true
+    transition3 sr i1 sr = true
+    transition3 ss i0 sr = true
+    transition3 ss i1 st = true
+    transition3 st i0 sr = true
+    transition3 st i1 st = true
+    transition3 _ _ _ = false
+
+    fin1 :  States1  → Bool
+    fin1 st = true
+    fin1 ss = false
+    fin1 sr = false
+
+    start1 : States1 → Bool
+    start1 sr = true
+    start1 _ = false
+
+    am2  :  NAutomaton  States1 In2
+    am2  =  record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
+
+    example2-1 = Naccept am2 finState1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
+    example2-2 = Naccept am2 finState1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a05/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,261 @@
+-title: 正規表現
+
+--受理集合と演算
+
+automaton で受理されるのは文字列。あるautomatonnは受理される文字列の集合を決める。
+
+文字列の集合への演算を考えよう
+
+   x      文字列そのもの
+   x+y    文字列の結合
+   *      文字列の繰り返し
+   x|y    文字列の選択
+
+これらを使って文字列の集合を決めると、それは文字列に対するパターンマッチとなる。
+
+これを正規表現という。
+
+---正規表現の例
+
++ は省略しても良いことにしよう。a+b+c  の代わりに、
+
+   abc
+
+文字集合の要素を全部選択したものを . と書くことにしよう。(Shell では?が多い。* は .* を意味する)
+
+   .*abc
+
+   .*abcabc
+
+曖昧さを避けるために()を使う。
+
+   (abc|bcd)
+
+   .*(abc|bcd)
+
+--問題5.1
+
+egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?
+
+C の regcomp を使ってみよ。
+
+Option : 実行時間を測定してみよう。
+
+--正規表現を表すデータ構造
+
+再帰的な構文木を表すには data を使うことができる。
+
+    data Regex   ( Σ : Set  ) : Set  where
+       _*    : Regex  Σ → Regex  Σ
+       _&_   : Regex  Σ → Regex  Σ → Regex Σ
+       _||_  : Regex  Σ → Regex  Σ → Regex Σ
+       <_>   : Σ → Regex  Σ
+
+List Σ を用いて < 文字列 > とすることもできるが、基本的なデータ構造をなるべく簡単にすることにしよう。
+
+<a href="../agda/regex1.agda"> regex1.agda </a>
+
+上の例題は、
+
+   < a > & < b > & < c >
+
+   any = a || b || c
+
+   ( any * ) & ( < a > & < b > & < c > )
+
+   ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > )
+
+   ( < a > & < b > & < c > ) || ( < b > & < c > & < d > )
+
+   ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > )
+
+となる。
+
+--正規言語
+
+ある正規表現が受け付ける文字列の集合を正規言語という。これは文字列の集合全体 ( List Σ )の部分集合になる。
+部分集合は Bool への関数として表すことができる。
+
+    List Σ → Bool
+
+正規言語は以下の論理式で表すことができる。
+
+   regular-language : {Σ : Set} → Regex Σ → List Σ → Bool
+
+Regex Σはdataなので場合分けとなる。
+
+例えば、
+
+    _‖_ : {Σ : Set} ( x y : List Σ → Bool) → List Σ → Bool
+    x ‖ y = λ s → x s ∨ y s
+
+    regular-language (x || y) f = ( regular-language x f ) ‖ ( regular-language y f )
+
+-- < a >
+
+もし、Σがデータなら (例えば In2 )
+
+    regular-language < h > f (i0  ∷ [] ) = true
+    regular-language < h > f (i1  ∷ [] ) = true
+    regular-language < h > f _ = false
+
+で良い。そうっでないなら、
+
+    cmp : (x y : Σ )→ Dec ( x ≡ y )
+
+みたいなのがあれば、
+
+    regular-language < h > (h1  ∷ [] ) with cmp h h1
+    ... | yes _ = true
+    ... | no _  = false
+    regular-language < h > _ = false
+
+と書ける。Dec は、条件分岐を理由付きで得るためのもの。理由がないと証明できない。
+
+in Relation.Nullary
+
+    ¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
+    ¬ P = P → ⊥
+
+    -- Decidable relations.
+
+    data Dec {p} (P : Set p) : Set p where
+      yes : ( p :   P) → Dec P
+      no  : (¬p : ¬ P) → Dec P
+
+--Finite Set
+
+有限集合 Fin n は、
+
+    test1 : Fin 2 → Bool
+    test1 0 → true
+    test1 1 → true
+    test1 2 → true
+
+などのように使いたい。0,1,2 は Data.Nat なのでだめである。Agda には Data.Fin が用意されている。
+
+    data Fin : ℕ → Set where
+      zero : {n : ℕ} → Fin (suc n)
+      suc  : {n : ℕ} (i : Fin n) → Fin (suc n)
+
+実際に test1 がどのようになるかを Agda で確認すると、
+
+    test4 : Fin 2 → Bool
+    test4 zero = { }0
+    test4 (suc zero) = { }1
+    test4 (suc (suc ()))
+
+ここで () はあり得ない入力を表す。あり得ないので body は空である。
+
+(Agda での否定を思い出そう)
+
+--Finite Set の構成
+
+<a href="../agda/nfa.agda"> nfa.agda </a>
+
+    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
+
+    finState1 : FiniteSet States1
+    finState1 = record {
+            Q←F = Q←F
+          ; F←Q  = F←Q
+          ; finiso→ = finiso→
+          ; finiso← = finiso←
+       } where
+           Q←F : Fin 3 → States1
+           Q←F zero = sr
+           Q←F (suc zero) = ss
+           Q←F (suc (suc zero)) = st
+           Q←F (suc (suc (suc ())))
+           F←Q : States1 → Fin 3
+           F←Q sr = zero
+           F←Q ss = suc (zero)
+           F←Q st = suc ( suc zero )
+           finiso→ : (q : States1) → Q←F (F←Q q) ≡ q
+           finiso→ sr = refl
+           finiso→ ss = refl
+           finiso→ st = refl
+           finiso← : (f : Fin 3) → F←Q (Q←F f) ≡ f
+           finiso← zero = refl
+           finiso← (suc zero) = refl
+           finiso← (suc (suc zero)) = refl
+           finiso← (suc (suc (suc ())))
+
+
+
+-- x & y
+
+これは 
+
+    split : {Σ : Set} → (List Σ → Bool)
+          → ( List Σ → Bool) → List Σ → Bool
+
+があれば、
+
+    _・_ : {Σ : Set} → ( x y : List Σ → Bool) → List Σ → Bool
+    x ・ y = λ z → split x y z
+
+    regular-language (x & y) f = ( regular-language x f ) ・ ( regular-language y f )
+
+-- x & y
+
+    repeat : {Σ : Set} → (List Σ → Bool) → List Σ → Bool
+    repeat x [] = true
+    repeat {Σ} x ( h  ∷ t ) = split x (repeat {Σ} x) ( h  ∷ t )
+
+    regular-language (x *) f = repeat ( regular-language x f )
+
+
+--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
+
+
+--問題5.2 - 5.7
+
+いくつかの正規表現に関する例題
+
+<a href="../exercise/002.html"> 問題5.2 - 5.7 </a>  <!---  Exercise 5.2 --->
+
+<a href=""> </a>  <!---  Exercise 5.3 --->
+<a href=""> </a>  <!---  Exercise 5.4 --->
+<a href=""> </a>  <!---  Exercise 5.5 --->
+<a href=""> </a>  <!---  Exercise 5.6 --->
+<a href=""> </a>  <!---  Exercise 5.7 --->
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a06/lecture.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,68 @@
+-title: 正規表現とオートマトン
+
+--ε遷移とオートマトンの組合せ
+
+文字の入力がなくても状態遷移が可能であるとすると、オートマトンの組合せが楽になる。
+
+文字を消費しない遷移を ε遷移と言う。ε遷移可能な状態をまとめて一つの状態と見れば、ε遷移のないNFAに変換できる。
+
+<a href="../agda/epautomaton.agda"> ε automatocn </a>
+
+--正規表現とオートマトンの組合せ
+
+<a href="../agda/regex.agda"> regex.agda </a>
+
+--微分法
+
+--オートマトンから正規表現を生成する
+
+状態遷移の条件を正規表現した一般化オートマトンを考える。
+
+普通のオートマトンから始めて、状態を組み合わせて遷移条件を正規表現にしていく。
+
+状態が一つになったら正規表現が得られる。
+
+--実際の正規表現エンジン
+
+grep のソースコード
+
+--Boyer-Moore Search
+
+固定文字列を検索するなら、正規表現よりも高速な手法がある。
+
+例えば、engine を検索するとする。
+
+　　6文字目がeでなければ、先頭の文字列からengineであることはない
+
+なので、6文字見なくてもだめなことはわかる。しかし、7文字目からengineを探すと、
+
+　　xxxxxn
+　　the engine
+
+を見落とす可能性がある。つまり、
+
+　　6文字目が検索文字列に含まれる文字列だと途中からマッチする可能性がある
+
+何文字目からマッチする可能性があるかは、あらかじめ調べることができる。
+
+　　e   6文字目
+　　n   2文字目
+　　g   3文字目
+　　i   4文字目
+　　?   7文字目
+
+これを繰り返せば良い。
+
+　　.*engine
+
+をDFAに変換して探す場合とどれくらい速度が違うか調べてみよう。
+
+--複数文字列に対する Boyer-Moore Search
+
+
+
+
+
+
+
+

--- a/agda/regex1.agda	Wed Nov 28 21:15:49 2018 +0900
+++ b/agda/regex1.agda	Wed Dec 05 16:17:28 2018 +0900
@@ -4,6 +4,7 @@
 open import Data.Fin
 open import Data.Nat hiding ( _≟_ )
 open import Data.List hiding ( any )
+import Data.Bool using ( Bool ; true ; false ; _∧_ )
 open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
 open import  Relation.Binary.PropositionalEquality as RBF hiding ( [_] ) 
 open import Relation.Nullary using (¬_; Dec; yes; no)
@@ -109,6 +110,11 @@
        Subterm : Regex Σ
        sub     : issub R Subterm fin ≡ true
 
+open import Data.Product
+
+regex2nfa' : {Σ : Set} → Regex Σ → {n m : ℕ } (fin : FiniteSet Σ {n}) → ( NAutomaton (Regex Σ) Σ  ×   FiniteSet (Regex Σ) {m} )
+regex2nfa' = {!!}
+
 regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ
 regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
           nr0 = regex2nfa r fin
@@ -153,6 +159,22 @@
 
 -- testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )
 
+reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
+     → ( regex : Regex Σ )
+     → ( rfin : FiniteSet (Regex Σ) {m} )
+     → ( In : List Σ )
+     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} ( regex2nfa {Σ} regex  fin  ) rfin In
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) rfin In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) rfin In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) rfin In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > rfin In = {!!}
 
 
 
+
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercise/001.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,142 @@
+-title: 関数適用による証明
+
+    A → B → A
+
+を証明してみよう。
+
+まず、証明する式の上に線分を引く。これは「推論して、 A → B → A を導く」ということである。
+
+ ----------------
+    A → B → A
+
+まず、かっこを正しく付ける。
+
+ --------------------
+    A → ( B → A )
+
+であることを思い出そう。ここで使える推論規則は、
+
+      A
+      :
+      B
+ ------------ →-intro
+    A →  B
+
+である。これのBの部分が ( B → A ) になっている。これにより、Aを仮定として使って良くなる。つまり、
+
+     A
+
+は無条件に使って良い。
+
+         A
+         :
+       B → A 
+ --------------------
+    A → ( B → A )
+
+: の部分は自分で埋める必要がある。
+
+       B → A 
+
+の部分に集中しよう。
+
+ --------------------
+       B → A 
+
+となる。同じ推論規則から、
+
+         B
+         :
+         A
+ --------------------
+       B → A 
+
+となる。A は無条件に使って良かった。まとめると、
+
+         A
+ --------------------
+       B → A 
+ --------------------
+    A → ( B → A )
+
+これで証明がつながった。→-intro は二回使ったので番号を付けて区別する。
+→-intro が生成した仮定には同じ番号を付けて[]を付加する。これは、
+discharge と呼ばれる。
+
+        [A]1
+ -------------------- →-intro 2
+       B → A 
+ -------------------- →-intro 1
+    A → ( B → A )
+
+[B]は使ってないが、使わなくて良い。これで証明が完成した。
+
+         B 
+         :
+         A 
+ -------------------- →-intro 
+       B → A
+
+は、a : A があった時に、λ (x : B) → a が B → A という型を持つことに相当する。
+
+     b : B 
+         :
+     a :  A 
+ ------------------------------- 
+     λ (x : B) → a :  B → A
+
+: の左側は値であり、右側が型になる。
+
+証明すべき式は、型
+    f :  B → A
+
+
+
+
+
+
+
+
+
+
+<a href="../s02/lambda.agda"> lambda.agda </a>
+
+
+
+module lambda ( T : Set) ( t : T ) where
+
+
+A→A : (A : Set ) → ( A → A )
+A→A = λ A → λ ( a : A ) → a
+
+lemma2 : (A : Set ) →  A → A 
+lemma2 A a = {!!}
+
+
+ex1 : {A B : Set} → Set 
+ex1 {A} {B} = ( A → B ) → A → B
+
+ex2 : {A : Set} → Set 
+ex2 {A}  =  A → ( A  → A )
+
+ex3 : {A B : Set} → Set 
+ex3 {A}{B}  =  A → B
+
+ex4 : {A B : Set} → Set 
+ex4 {A}{B}  =  A → B → B
+
+ex5 : {A B : Set} → Set 
+ex5 {A}{B}  =  A → B → A
+
+proof5 : {A B : Set } → ex5 {A} {B}
+proof5 a b = a 
+
+postulate S : Set
+postulate s : S
+
+ex6 : {A : Set} → A → S
+ex6 a = s
+
+ex7 : {A : Set} → A → T
+ex7 a = t
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercise/002.ind	Wed Dec 05 16:17:28 2018 +0900
@@ -0,0 +1,60 @@
+-title: 正規表現とAutomaton の問題 5.2 - 5.7
+
+--2
+
+ASCII code の [a-z][a-z0-9]* を Σ={a,b,c...z,0,1...,9}を使って DFA で実現してみよ。
+
+これだと大きいので
+
+   [d-g][d-g4-7]*
+
+を使う。
+
+ASCII code の [d-g][d-g4-7]* を binary の正規表現で表すとどうなるか。
+
+Σ={0,1}を使ったこれに対応するDFAを構成せよ。
+
+--3
+
+以下の正規表現に対応するNFAを計算せよ。
+
+
+a   (00|11)*
+
+b   (01|10)*
+
+c   (01|10)*|111
+
+d   (10|11)*
+
+e   (0|1)*010
+
+--4
+
+上の正規表現に対応するDFAを計算せよ。
+
+--5
+
+上のDFAの否定を与えるDFAを構成してみる。
+
+--6
+
+NFAの否定を構成してみよ
+
+NFAの否定をNFAで計算するにはどうすれば良いか?
+
+--7
+
+Σ = {0,1} で 
+
+    .*1.{n}1.*
+
+を考えよう。.{n} は n 個の任意の文字が入る。
+
+Σ = {0,1} で NFAを構成せよ。(n=0..3)
+
+Σ = {0,1} で DFAを構成せよ。(n=0..3)
+
+一般的にDFAの状態数は n に対していくつになるか?
+
+