--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda-install.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,68 @@
+-title: Agda の install の方法
+
+Homebrew を使うのが良いそうです。
+
+Emacs を先に入れます。
+
+  brew tap caskroom/cask
+  brew cask install emacs
+
+その後、
+
+   brew install agda
+
+GHCが入ってないなら、
+
+   brew install ghc
+
+install 先がどこかは、
+
+    /usr/local/Cellar/agda/2.5.2/lib/agda
+
+などになるので、
+
+~/.agda に以下のファイルを置きます
+
+    defaults   libraries
+
+defaults の中には
+
+   standard-library
+
+libraries の中には
+    /usr/local/Cellar/agda/2.5.2/lib/agda/standard-library.agda-lib
+
+~/.emacs.d/init.el に以下のファイルを置きます。あるいは自分のinit.el に適当に追加します。
+中のpathは正しいものに置き換えます。
+
+<a href="init.el"> init.el </a>
+
+GUI 側で使わないと文字化けすることがあるようです。Terminal で使いたい時には、
+
+<a href="https://github.com/hamano/locale-eaw"> locale eaw </a>
+
+が必要です。
+
+Emacs から使うので、Emacs も勉強しよう。
+
+<a href="http://www.ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a>
+
+  C-C  control と C を同時に押す
+  M-X  esc を押してから X を押す
+
+C-X C-F で、Agda1.agda file を開けます。
+
+M-X help-for-help M で、Agda のコマンドの一覧が出ます。C-X o で buffer を切り替えて読みます。
+
+
+--vim
+
+<a ref="https://github.com/derekelkins/agda-vim"> agda-vim</a>
+
+が使えます。
+
+--VS-code
+
+<a href="https://github.com/freebroccolo/vscode-agda"> vscode </a>
+
+があるみたい。試してません。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,164 @@
+-title: Agda
+
+Agda は関数型プログラミング言語で、テキストで記述していく。Haskell に似た構文を持つ。Haskell で実装されている。
+
+プログラムは必ず以下のように始める。
+
+module lambda where
+
+この時に、このファイルは、
+
+     lambad.agda      
+
+と同じ名前を持つ必要がある。
+
+プログラムは、
+
+    name : type
+    name = value
+
+という形で関数型言語での関数の型と定義を与える形式。
+
+仮定なしに使えるのは Set という型しかない。あとは、これから構成していく。構成する要素には、
+
+　　関数  ( 型は A → B、値は λ x → y )
+　　record 
+　　data
+
+の三種類。この三種類だけ憶えればよい。
+
+Agdaの操作は、
+
+　　load と型のチェック       何か入力して、C-C C-L
+　　値の計算                  C-C C-N の後に式を入力 (プログラムの実行に相当する)
+
+の二つだけ。その他には、C-C C-C (case文の生成)などがある。
+
+Agda は indent でblockを構成する文法を持ち、Haskell に近い。しかし、以下のことに気をつけよう。
+
+  (){}. は変数名には使えない(それ以外は全部使える = とかも)
+  : と = と　→ の前後には空白が必要
+
+空白がないと「ひと続きの名前」として扱われたり、エラーになったりする。-> でも→でも良い。\ x -> y でも λ x → y でも良い。統一しよう。
+
+    A → B → C は、 A → ( B → C )  のこと
+
+　　f x y は (f x) y のこと
+
+これは複数引数の関数を「少ない引数の関数を返す高階関数」と見るカーリー化に対応している。
+
+   f : A → B → C
+
+の時に f x は  B → C という型を持つ関数を返していると考える。これは Haskell でも同じ。
+
+
+型と値は組で書く。型は省略できるが、Agda で重要なのは論理式に相当する型の方である。
+
+    name : type
+    name = value
+
+定義抜きに使えるのは Set のみである。(正確には Set と、レベルの付いた Set n 。Set は Set zero の省略形)
+
+引数には{}を付けることができる。
+
+    id : ( A : Set ) → A → A
+    id x =  x
+
+は引数の数があっていないので怒られる。
+
+    id : ( A : Set ) → A → A
+    id A x =  x
+
+しかし、A は使われていない。使われてない変数は _ で省略できる。
+
+    id : ( A : Set ) → A → A
+    id _ x =  x
+
+ここでAに{}を付ける。
+
+    id : { A : Set } → A → A
+    id {_} x =  x
+
+推論できる{}な変数は省略することが可能である。
+
+    id : { A : Set } → A → A
+    id x =  x
+
+省略された呼出を明示することもできる。
+
+    f1 : Nat → Nat
+    f1 = id {Nat}
+
+Haskell で id x = x で定義された id の型を調べてみよう。
+
+--Agda の infix operator
+
+    _・_ 
+
+と書くことにより、
+
+   a ・ b
+
+は
+
+   _・_ a b
+
+と同じに扱われる。infix により演算子の順位などを制御することができる。(・の代わりに.を使うと構文エラーになる)
+
+--Agda での?
+
+わからない部分には ? と書くことができる。
+
+   _・_ : {A : Set } → ?
+   f ・ g = λ x → f ( g x )    
+
+この? を埋めていく作業が証明になる。
+
+--Agda でのエラー
+
+C-C C-L の時に、Agda は
+
+    赤     型が衝突していることを示す (書き直しが必要)
+    黄     十分に引数が具体化(instanciate)されてないことを示す
+　　緑     ? で、まだ決めてない部分
+
+などのerrorを出す。これをなくすごとが証明の目標である。
+
+黄色の場合は、{}で省略された型変数を指定するとなおることがある。
+
+エラーが残っている modulde を import することはできない。
+
+他にも
+
+    f = f
+    Termination checking failed for the following functions:
+      f
+
+などのerrorがでる。
+
+--Agda の設定
+
+    % brew info agda
+
+を見ると、
+
+    ==> Caveats
+    To use the Agda standard library by default:
+      mkdir -p ~/.agda
+      echo /usr/local/lib/agda/standard-library.agda-lib >>~/.agda/libraries
+      echo standard-library >>~/.agda/defaults
+
+とある。~/.agda がちゃんと設定されているかどうかを確認しよう。
+
+文字がずれる場合は、
+
+<a href="https://attonblog.blogspot.com/2016/11/homebrew-agda-2512.html"> atton のblog </a>
+
+を参考にして、eaw.el を入れます。
+
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/reduction.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,84 @@
+--Lambda Calculusの簡約
+
+ここでは、Haskell の式をそのまま使う。record と data は使わない
+
+---Types
+
+1. a,b,c などは型である。Haskell の Integer や Char も型である。
+
+2. U,V が型なら  U -> V も型である。(関数)
+
+3. U,V が型なら  (U , V) も型である。(Pair、直積)
+
+ここでは、これらによって作られる型のみを考える。
+
+---Term
+
+Term は以下の規則によって型と一緒に構築される。
+
+1.  Haskell の変数 x,y,z は項。つまり let a = ... で宣言された小文字で始まる記号。対応する型(変数で指定された)を持つ。
+    1 や 'a' も対応する型を持つ項である。
+
+2.  u が型U、v が型V を持てば、(u,v) は型(U,V)を持つ項である。
+
+3.  型(U,V)を持つ項 t に対して、fst t は型U を持つ項、snd t は型 V を持つ項である。
+
+4. v が型V を持つ項で、x0,x1,...,xn が型Uを持てば、 \x0 x1 ..., xn -> v は項である。
+    Haskell によって変数の名前のスコープは適切に扱われるとする。
+
+5. t が型 U->V を持ち、u が 型U を持てば、 t u は型V を持つ項である。
+
+これら項は、Haskell によって評価される。これらは変換規則と提供する。
+
+1. 変数は変数の値
+
+2. (u,v) は pair
+
+3.  fst と snd は pair の最初と次を取ってくる関数
+
+4.  lambda 式は、与えられた引数により変数の置き換えを行う
+
+5.  関数の適用を行う。
+
+---等式
+
+    fst (x,y) == x
+    snd (x,y) == y
+    (\x y -> v) u == v
+
+さらに
+
+   ((fst v),(snd v))==v
+   (\x t x) = t
+
+---正則形 (Normal form)
+
+Haskell の計算は、これらの項をなるべく簡単に変換していくもの。
+
+    fst (u,v)
+    snd (u,v)
+    (\x -> v) u
+
+のような形が式に含まれていなければ、式はこれ以上計算できない。
+
+逆に含まれていれば、次のように変換できる。
+
+    fst (u,v)       -> u
+    snd (u,v)       -> v
+    (\x -> v) u     -> v[u/x]   (v の中のxをuで置き換える)
+
+置き換えによって、さらに計算が進む場合もある。
+
+--問題
+
+以下の式を計算せよ
+
+    (\x -> (snd x,fst x))  (1,2)
+
+以下の式は Haskkel がエラーを出す。
+
+    (\x -> (snd x,fst x))  ((\x -> t 3 ),2)
+
+適切に実行されるように t に関する修正を加えよ。
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/unificagtion.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,27 @@
+-title: unification
+
+Unification (単一化) は、二つの項が同じになる可能性があるかどうかを調べる。
+
+これは、引数に data 型がある時にも起きる。
+
+可能性がなければ失敗する。
+
+---Term
+
+Term は以下の規則によって型と一緒に構築される。
+
+1.  Haskell の変数 x,y,z は項。つまり let a = ... で宣言された小文字で始まる記号。対応する型(変数で指定された)を持つ。
+    1 や 'a' も対応する型を持つ項である。
+
+2.  u が型U、v が型V を持てば、(u,v) は型(U,V)を持つ項である。
+
+3.  型(U,V)を持つ項 t に対して、fst t は型U を持つ項、snd t は型 V を持つ項である。
+
+4. v が型V を持つ項で、x0,x1,...,xn が型Uを持てば、 \x0 x1 ..., xn -> v は項である。
+    Haskell によって変数の名前のスコープは適切に扱われるとする。
+
+5. t が型 U->V を持ち、u が 型U を持てば、 t u は型V を持つ項である。
+
+--単一化
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a07/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,41 @@
+-title: 非決定性オートマトンから決定性オートマトンへの変換
+
+非決定性オートマトンは、ある状態から複数の可能な状態へ遷移する。そのうちのどれかが受理状態へ遷移すれば accept となる。
+
+状態は有限なので、複数の可能な状態は、状態の部分集合となる。状態Qの部分集合は、
+
+　　Q → Bool
+
+と表すことができる。つまり、その部分集合に含まれるかどうかを表す関数が部分集合そのものになる。これを、Bool
+<sup>Q</sup> と書くことがある。Bool は二つの要素がある。状態数4からBoolへの関数は、2
+<sup>4</sup>個ある。集合のべき乗をこのようにして定義することができる。
+
+非決定性オートマトンを状態Qの部分集合を状態とする決定性オートマトンと考えることができる。
+NAutomaton Q Σ は状態の集合Qと入力文字の集合Σからなる非決定性オートマトンだった。これから、
+
+    Automaton (Q → Bool)  Σ
+
+を作れれば、非決定性オートマトンから決定性オートマトンへの変換ができることになる。
+
+状態Q入力文字Σの決定性オートマトンの状態遷移関数は Q → Σ → Q だったから、
+この状態Qの部分集合を状態とするAutomatonの状態遷移関数は、
+
+　(Q → Bool) → Σ → (Q → Bool)
+
+となる。右のかっこは省略可能である。
+
+　(Q → Bool) → Σ → Q → Bool
+
+つまり、状態遷移関数は三つの入力を持つ。f i q としよう。決定性オートマトンの状態遷移関数は、
+
+　  Nδ : Q → Σ → Q → Bool
+
+だった。f : Q → Bool が入力の状態で、i : Σ が決まっている。出力状態は Q → Bool なので q を入力に持つ。
+
+　　λ q → f q ∧ Nδ q i 
+
+---問題7.1 以下の非決定性オートマトンを決定性オートマトンへ変換せよ
+
+
+<a href="../exercise/003.html"> 例題  </a> <!---  Exercise 7.1 --->
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a08/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,60 @@
+-title: push donwオートマトンと文法クラス
+
+任意のnについて 0{n}1{n} に対応する有限オートマトンはない。
+
+    inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
+    inputnn {zero} {_} _ _ s = s
+    inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )                     
+
+inputnn だけ受け付けて、それ以外を受け付けないということができない。
+
+
+
+かっこの対応が取れないことに相当する。
+
+
+--push down automaton
+
+
+    data PushDown   (  Γ : Set  ) : Set  where
+       pop    : PushDown  Γ
+       push   :  Γ → PushDown  Γ
+
+    record PushDownAutomaton ( Q : Set ) ( Σ : Set  ) ( Γ : Set  )
+           : Set  where
+        field
+            pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
+            pstart : Q
+            pz0 :  Γ
+        pmoves :  Q → List  Σ → ( Q × List  Γ )
+        pmoves q L = move q L [ pz0 ]
+               where
+                  move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × List  Γ )
+                  move q _ [] = ( q , [] )
+                  move q [] S = ( q , S )
+                  move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
+                  ... | (nq , pop )     = move nq T ST
+                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+        paccept : List  Σ → Bool
+        paccept L = move pstart L [ pz0 ]
+               where
+                  move : (q : Q ) ( L : List  Σ ) ( L : List   Γ ) → Bool
+                  move q [] [] = true
+                  move q _ [] = false
+                  move q [] (_ ∷ _ ) = false
+                  move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
+                  ... | (nq , pop )     = move nq T ST
+                  ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
+
+
+--文脈自由文法
+
+
+
+---問題8.1 push down automaton
+
+
+<a href="../exercise/004.html"> 例題  </a> <!---  Exercise 8.1 --->
+
+              
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a09/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,302 @@
+-title: Turing Machine
+
+Turing Machine は無限長のテープを持つAutomatonである。これは、stack を二つ持つ Automaton として構成できる。
+
+<a href="../agda/turing.agda"> turing.agda </a>
+
+テープへの操作は、書き込みと移動である。
+
+    data Write   (  Σ : Set  ) : Set  where
+       write   : Σ → Write  Σ
+       wnone   : Write  Σ
+
+    data Move : Set  where
+       left   : Move  
+       right  : Move  
+       mnone  : Move  
+
+Turing machineは状態と入力で、このコマンド二つを選択する。
+
+    record Turing ( Q : Set ) ( Σ : Set  ) 
+           : Set  where
+        field
+            tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
+            tstart : Q
+            tend : Q → Bool
+            tnone :  Σ
+
+書き込みと移動を二つのstack( List Σ)に対する関数として定義する。
+
+    {-# TERMINATING #-}
+    move : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move q L [] = move q  L  ( tnone  ∷ [] ) 
+    move q [] R = move q  ( tnone  ∷ [] )  R 
+    move q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH  
+    ... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
+    ... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
+    ... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
+    ... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
+    ... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
+    ... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
+    {-# TERMINATING #-}
+    move-loop : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move-loop  q L R with tend q
+    ... | true = ( q , L , R )
+    ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
+      where
+        next = move  q  L  R 
+    {-# TERMINATING #-}
+    move0 : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move0  q L R with tend q
+    ... | true = ( q , L , R )
+    move0 q L [] | false = move0 q  L  ( tnone  ∷ [] ) 
+    move0 q [] R | false = move0 q  ( tnone  ∷ [] )  R 
+    move0 q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
+    ... | nq , write x , left  = move0 nq ( RH ∷ x  ∷ LT ) RT 
+    ... | nq , write x , right = move0 nq LT ( x  ∷ RH  ∷ RT ) 
+    ... | nq , write x , mnone = move0 nq ( x  ∷ LT ) (  RH ∷ RT ) 
+    ... | nq , wnone , left    = move0 nq ( RH  ∷ LH  ∷ LT ) RT  
+    ... | nq , wnone , right   = move0 nq  LT ( LH  ∷ RH  ∷ RT ) 
+    ... | nq , wnone , mnone   = move0 nq ( LH  ∷ LT ) (  RH ∷ RT )  
+    {-# TERMINATING #-}
+    taccept : List  Σ → ( Q × List  Σ × List  Σ )
+    taccept L = move0 tstart L []
+
+--Turing Machine の例題
+
+    data CopyStates : Set where
+       s1 : CopyStates
+       s2 : CopyStates
+       s3 : CopyStates
+       s4 : CopyStates
+       s5 : CopyStates
+       H  : CopyStates
+
+
+    Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move 
+    Copyδ s1 0  = (H    , wnone       , mnone )
+    Copyδ s1 1  = (s2   , write 0 , right )
+    Copyδ s2 0  = (s3   , write 0 , right )
+    Copyδ s2 1  = (s2   , write 1 , right )
+    Copyδ s3 0  = (s4   , write 1 , left )
+    Copyδ s3 1  = (s3   , write 1 , right )
+    Copyδ s4 0  = (s5   , write 0 , left )
+    Copyδ s4 1  = (s4   , write 1 , left )
+    Copyδ s5 0  = (s1   , write 1 , right )
+    Copyδ s5 1  = (s5   , write 1 , left )
+    Copyδ H  _  = (H    , wnone   , mnone )
+    Copyδ _  (suc (suc _))      = (H    , wnone       , mnone )
+
+    copyMachine : Turing CopyStates ℕ
+    copyMachine = record {
+            tδ = Copyδ
+         ;  tstart = s1
+         ;  tend = tend
+         ;  tnone =  0
+      } where
+          tend : CopyStates →  Bool
+          tend H = true
+          tend _ = false
+
+    test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
+    test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
+
+    test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
+    test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
+
+
+-- Turing machine の停止問題
+
+---Universal Turing Machine
+
+文字列 x を判定する Turinging machine tm(x) があるとする。
+
+tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine
+
+   utm(tm , x)
+
+を構成することができる。utm(tm,x) は引数を二つ持つが、tm+x と結合した単一の文字列だと思えば単一引数になる。
+
+utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。
+
+  utm(tm,x) = 0  受け入れない
+             1  受け入れる
+             ⊥  止まらない
+
+utm の構成の詳細には立ち入らない。実際に utm を構成するのは良い演習になる。
+
+tm に対応する文字列を tm とすると、tm 自体を tm の入力とすることができる。utm は、そのためだけに導入したので、もう使わない。
+
+--Turinng Machine の停止性の判定
+
+halt(tm,x) は、以下のように定義される。これはまだ、Turing machine であるとは限らない。
+
+  halt(tm,x) = 0  tm(x) が止まらない (halt が停止しない)    (1)
+  halt(tm,x) = 1  tm(x) が止まる                            (2)
+
+halt(tm+x) 自体は ⊥ 、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?
+
+--halt が tm ではあり得ないこの証明
+
+halt の否定を考えよう。
+
+  neg(tm) = 1  halt(tm,tm) が0                     (3)
+  neg(tm) = ⊥  halt(tm,tm) が1                     (4)
+
+つまり、halt(tm,tm) が1 の時、つまり、tm(tm) が停止する時には、neg(tm) は停止しない。neg 自体は halt があればtmとして簡単に作れる。
+
+  neg(neg) = 1
+
+かどうか調べよう。ここで 引数の neg は Turing machine neg を表す文字列である。
+
+まず、neg(neg) =1 と仮定する。(3) から、
+
+  halt(neg,neg) が 0
+
+なことがわかる。つまり、neg(neg) は停止しない。neg(neg) = ⊥ 。これは最初の仮定 neg(neg)=1に矛盾する。
+
+逆に、
+
+  neg(neg) = ⊥
+
+とすると、(4) から、
+
+  halt(neg,neg) = 1
+
+つまり、neg(neg) は止まる。つまり、neg(neg)=1。これも矛盾。
+
+つまり、halt(tm,x) が⊥にならないようなものは存在しない。
+
+つまり、Turinng machine が停止するかどうかを、必ず判定できる停止する Turing machine は存在しない。
+
+--証明の考察
+
+ここで用いているのは、Turing machine の詳細ではなく、
+
+   Turing machine に対応する文字列 tm がある
+   tm を入力として用いることができる
+
+ということと、
+
+   tm が停止する、停止しない
+   tm が停止して、1から0
+
+を返すという性質である。
+
+    neg(neg) 
+
+は自分自身を参照しているので、自己参照と呼ばれる。
+
+halt は、neg が Turing machine になるためには、Turing machine である必要がある。
+
+tm(x) は停止するかしないかどちらかだから、halt(tm,x) という述語自体はある。
+
+しかし、halt(neg,neg) は 0 か 1 かを決めることはできない。
+
+これは述語を定義しても、それが0か1かを決めることができない場合があるということである。
+
+これは、述語論理の不完全性定理に対応する。
+
+この証明は自己参照を用いて矛盾を導く方法である。
+
+--対角線論法
+
+0,1 からなる無限長の文字列を考えよう。これを順に拾っていく。どんな順序で拾っても、自然数の範囲では拾い切れないことをしまそう。
+
+拾った順に、文字列を並べる。
+
+    00000000000000000000000000100000....
+    01000000000000000000000000001000....
+    01100000000000000000000000000100....
+    01110000000000000000000000000010....
+    01111000000000000000000000000000....
+    01111100000000000000000000000000....
+    01011100000000000000000000000000....
+            ...
+            ...
+            ...
+
+行y列xの文字を v(x,y) とする。これは 0 か 1 である。上の文字列の対角線の要素は v(x,x) となる。以下の . が対角線要素になる。
+
+    .0000000000000000000000000100000....
+    0.000000000000000000000000001000....
+    01.00000000000000000000000000100....
+    011.0000000000000000000000000010....
+    0111.000000000000000000000000000....
+    01111.00000000000000000000000000....
+    010111.0000000000000000000000000....
+            ...
+            ...
+            ...
+
+1-v(x,x) を考えると、
+
+    1000001 ...
+
+となる。この文字列は、最初に拾った文字列のどれとも、v(x,x)のところで異なる。つまり拾った文字列とは異なる文字列が必ず存在する。
+
+これは、順に取ってくるという方法では、無限長の文字列は尽くせないということを意味する。可算回と呼ぶ。
+
+--2^N
+
+この無限長の文字列は、自然数Nから{0,1} の写像と考えられる。あるいは、自然数Nの部分集合に1、それ以外に0を割り振ったものである。これを 2^N と書く。
+
+    自然数の部分集合全体
+    自然数から{0,1}への写像の全体
+
+である。自然数に1対1対応する集合を可算集合という。これらの集合は可算集合ではないことが対角線論法からわかる。
+
+この文字列の先頭に 0. を付けると、0から1 の実数を表す。実数の集合は可算集合でないことがわかる。
+
+また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。
+
+--対角線論法と Turing machine の対応
+
+halt(tm,x) は、文字列 tm+x から、{0,1 } への写像を与える。文字列は、bit pattern と考えると、巨大な自然数となる。 tm であれば、文字列表現を持つ。
+
+つまり、halt は 入力 x に対して Turing machine を、その表現の自然数順に並べた時に、止まるものを1、そうでないものを0とする文字列を与える。
+
+入力 x も文字列なので、halt(tm,x) は二次元の0,1のパターンになる。横軸が tm で、縦軸が x として、
+
+    00000000000000000000000000100000....
+    01000000000000000000000000001000....
+    01100000000000000000000000000100....
+    01110000000000000000000000000010....
+    01111000000000000000000000000000....
+    01111100000000000000000000000000....
+    01011100000000000000000000000000....
+            ...
+            ...
+            ...
+
+この文字列の表が halt(tm,x) を決めている。特性関数などと呼ばれる。
+
+halt(x,x) は対角線要素になる。その否定を考えよう。
+
+  not(tm) = 1  halt(tm,tm) が0                     (5)
+  not(tm) = 0  halt(tm,tm) が1                     (6)
+
+not(x) は、haltを入力順にした表の対角線要素を反転したものになる。(前の neg とは少し異なる)
+この文字列は、x 番目の入力文字列に対するnot(x)の値を示している。
+
+対角線論法から、not(x) の文字列は、haltを特徴付ける可算個のパターンに含まれてない。
+
+もし、halt(tm,x) の x に not(x) が含まれていれば、同じパターンが出てくるはずである。
+つまり、not(x) は、halt(tm,x) が判定できる範囲に含まれてないことがわかる。
+
+--対角線論法に対する考察
+
+tm(x) を実行して停止すれば、それは判定できる。しかし、停止しないかどうかはわからない。実際に、わからない tm を構成することはできて、それが not(x) である。
+
+neg(neg) の議論は ⊥ を使っていたが、not(x) では、halt(tm,x) の特徴関数の入力に not(x) が含まれるかどうかに変わっている。
+
+Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。
+
+--さまざまな決定不能問題
+
+多くの問題は Turing machine の停止性に帰着できる。
+
+    ディオファントス方程式
+    文脈依存文法
+    Automaton を含む方程式
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a10/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,90 @@
+-title: Turing Machine と計算量
+
+--計算量
+
+入力の長さ n に対して、どれくらいの計算時間やメモリが要求されるかを表す方法を考える。
+
+計算を Turing machine で行ない、その Turing machine が計算終了までに費すステップと使用したテープの長さを使う。
+
+計算量は、n の式で表す。係数は問わない。
+
+　　o(n)             入力に比例した計算時間
+　　o(n^2)           入力の長さの二乗の計算時間
+　　o(n * log n)         
+　　o(exp n)         入力の長さの指数的な計算時間
+　　o(exp (exp n))   入力の長さの指数的な計算時間
+
+Turing machine ではなく、もっと高級なモデル(例えばメモリを持つもの)を考えても、計算量は同じ。
+
+それは、テープの長さを考慮しても結局は係数しか違わないから。o(1) は入力を受け付ける時間を考慮してない時に意味がある。
+
+実際には係数も問題になることが多い。
+
+--P
+
+Turing machine で多項式時間がかかる計算量。
+
+Pの例。
+
+　　単純サーチ
+　　数え上げ
+
+--Non deteministic turing machine
+
+Automaton と同じように非決定的なTuring machine (NTM)を考える。Deterministic turing machine (DTM)の遷移関数は
+
+    tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } 
+
+だったが、
+
+    tnδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } → Bool
+
+と複数の動作が可能となる。次のテープの状態も複数あることになる。
+
+例えば、1からn までの素数を計算するのに DTMでは1から順番に計算していくが、NTMでは全部一度に調べることができる。
+
+NTMで多項式時間がかかる計算量を NP という。
+
+大雑把に言えば、NTMはCPUが無限にある並列計算機である。
+
+--NTMをDTMで simulation する。
+
+非決定性の数が定数つまりCPUの数が固定なNTMは、DTMと定数分しか差がない。従って計算量的には同じ。
+
+非決定性の数は入力の長さよりは使用したテープの長さに依存する。NTMでPということは、並列に動く個々のTMのテープの使用量はPで押さえられる。
+
+選択は有限(kとする)なので、k^P の分岐が起きている可能性がある。
+
+つまり、NP(NTMでP)な計算では指数的にCPUが使われる可能性がある。従って、一般的には NTMをDTMでsimulationするには指数的なステップがかかる。
+
+--NPの例
+
+   SAT 
+
+--P=NP?
+
+NP はあまりに強力だが、EXP(指数的な計算量)では押さえられる。
+
+--NP hard
+
+任意のNPの問題をとくことができる一般的な問題を NP complete という。
+
+最低でもNPな計算量を要求する計算を NP hard という。NP hard は NP complete とは限らない。
+
+--P space
+
+量化記号を含むSAT。
+
+--o(n)
+
+--o(n^2)
+
+    naive append
+
+--o(n*log n)
+
+    quick sort
+
+--o(exp n)
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a11/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,103 @@
+-title: ωオートマトン
+
+オートマトンは入力を受け付けるかどうかを問題にするので計算は有限時間に終わる。
+
+しかし、サーバなどの計算は終了することは想定されてない。入力が無限にある場合を考えたい。
+
+例えば、信号機は停まらずにずーっと動くことが期待されていて、正しい信号機の動作とそうでない動作がある。そして信号機はオートマトン的に動作している。
+
+--ωオートマトンの定義
+
+オートマトンの定義は同じものを用いる。ただし、入力は無限にある。
+
+    record Automaton ( Q : Set ) ( Σ : Set  )
+           : Set  where
+        field
+            δ : Q → Σ → Q
+            astart : Q
+            aend : Q → Bool
+
+automaton の定義にはもともと入力の実装が何かは記述されていない。
+
+Agda では無限の長さのリストを扱うことはできない。その代わり、自然数 n から入力Σを生成する関数( ℕ → Σ )を用いる。
+これを用いて、
+
+
+    ω-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
+
+    record Muller { Q  Σ : Set } (Ω : Automaton Q Σ ) ( S : ℕ → Σ ) : Set where
+        field
+            next     : (n : ℕ ) → ℕ 
+            infinite : (n : ℕ ) →  aend Ω ( ω-run Ω (n + (next n)) S ) ≡ true 
+
+Buchi ではある時刻から先では、aend で定義される状態の集合にずーっと留まる。Muller ではaendで定義されるある状態の集合を無限回通る。
+
+--ωオートマトンと様相論理
+
+これらは時間の様相を表す論理に関係している。
+
+　　　　[] p      ずーっとpが成立する
+　　　　<> p      いつかpが成立する
+
+これを組み合わせると
+
+　　　　<> [] p      いつからか、ずーっとpが成立するようになる
+　　　　[] <> p      ずーっと、いつかpが起きる
+
+[] はbox、<>はdiamonと呼ばれたりする。
+
+        [] p = ¬ ( <> ¬ p )
+        <> p = ¬ ( [] ¬ p )
+
+である。[] <> p をωオートマトンとして考えることができる。
+
+                       ¬ p
+                   ------------>
+        [] <> p *                 [] <> p 
+                   <-----------
+                       p
+
+p と ¬ p で二つの状態 ( [] <> p * と [] <> p)を行き来する。
+
+
+    data  States3   : Set  where
+       ts* : States3
+       ts  : States3
+
+    transition3 : States3  → Bool  → States3
+    transition3 ts* true  = ts*
+    transition3 ts* false  = ts
+    transition3 ts true  = ts*
+    transition3 ts false  = ts
+
+    mark1 :  States3  → Bool
+    mark1 ts* = true
+    mark1 ts = false
+
+    ωa1 : Automaton States3 Bool
+    ωa1 = record {
+            δ = transition3
+         ;  astart = ts*
+         ;  aend = mark1
+      }  
+
+ここで、[] <> p *  ( 上では ts* ) を無限回通れば、 [] <> p が成立していることになる。(Muller automaton )
+
+これの否定は、<> [] ( ¬ p ) ということになる。これは、ある時点からずーっと ¬ p が続く。(Buchi automaton )
+
+
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a12/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,21 @@
+-title: 時相論理とCTL
+
+--LTTL
+
+[]<> に○p(次の時刻でpが成立)と p until q (q が成立するまでずーっとp)を付け加えた論理をLTTL( Linear Time Temporal Logic )という。
+
+任意のLTTL式はωオートマトンに変換することができる。
+
+変数に対する量化記号を許すと QPTL と呼ばれる。
+
+--CTL
+
+Computational Tree Logic は、非決定性を含む計算に対して、計算の経路を含む状況を記述する。
+
+非決定性は入力の非決定性による。
+
+    EF p requires that there exists a path starting from a state, such that property p holds in a future time 
+    AF p requires that for all paths starting from a state, property p holds in a future time 
+    EG p requires that there exists a path starting from a state, such that property p holds in all future time instants 
+    AG p requires that for all paths starting from a state, property p holds in all future time instants 
+

Binary file a13/fig/semaphore.graffle has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/lecture.ind	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,95 @@
+-title: モデル検査とSAT
+
+--モデル検査
+
+--SAT
+
+--nuXmv
+
+<a href="https://nuxmv.fbk.eu">nuXmv  </a> <br>
+
+<a href="http://nusmv.fbk.eu/NuSMV/tutorial/index.html"> tutorial </a> <br>
+
+a か b のどちらかを非決定的に取る automaton を考える。
+
+    MODULE main
+    VAR
+      state : {a, b};
+    ASSIGN
+      init(state) := a;
+      next(state) := {a, b}; 
+
+状態 a から始まって、任意のaとb の木構造な可能な実行がある。
+
+それぞれの可能な実行を path という。
+
+--CTL
+
+A はすべてのpath、E はあるpath について成り立つ。
+
+G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
+
+a U b は、b になるまでずーっとa 。b になる必要はある。
+
+        SPEC AG state=a
+        SPEC EG state=a
+        SPEC AF state=a
+        SPEC EF state=a
+        SPEC A [ state=a U state=b ]
+        SPEC E [ state=a U state=b ]
+
+--LTL
+
+一つの時間軸についてだけの様相論理。
+
+G はすべての時間(□)、F はいつか(<>)。これの組み合わせになる。
+
+a U b は、b になるまでずーっとa 。b になる必要はある。
+
+nuXmv は false になる可能性を調べる。
+
+        LTLSPEC G state=a
+        LTLSPEC F state=a
+        LTLSPEC G [ state=a U state=b ]
+        LTLSPEC F [ state=a U state=b ]
+
+--smv example
+
+<center><img src="fig/semaphore.svg"></center>
+
+このセマフォは、critical にずーっと入れるので成り立たない性質がある。
+
+
+    % nuXmv -int test7.smv
+
+<a href="smv/test7.smv"> test7.smv </a>
+
+    % nuXmv test8.smv
+
+<a href="smv/test8.smv"> test8.smv </a>
+
+    % nuXmv test9.smv
+
+<a href="smv/test9.smv"> test9.smv </a>
+
+    % nuXmv test10.smv
+
+    % nuXmv -bmc -bmc_length 4 test10.smv
+
+<a href="smv/test10.smv"> test10.smv </a>
+
+--その他の例題
+
+<a href="http://nusmv.fbk.eu/examples/examples.html"> http://nusmv.fbk.eu/examples/examples.html
+
+---問題13.1 
+
+Turing machine の停止性のように、プログラムの正しさは原理的に証明することはできない。
+それにも関わらずシステムの信頼性を高めるにはどうすれば良いか? 定理証明やモデル検査器
+に触れつつ800文字程度で考察せよ。
+
+<a href=""> 例題  </a> <!---  Exercise 13.1 --->
+
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test1.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,10 @@
+MODULE main
+VAR
+  request : boolean;
+  state : {ready, busy};
+ASSIGN
+  init(state) := ready;
+  next(state) := case
+                   state = ready & request : busy;
+                   TRUE : {ready, busy}; esac;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test10.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,11 @@
+MODULE main
+VAR
+  y : 0..15;
+ASSIGN
+  init(y) := 0;
+TRANS
+  case
+    y=7: next(y)=0;
+    TRUE : next(y) = ((y + 1) mod 16);
+  esac
+LTLSPEC G ( y=4 -> X y=6 )

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test2.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,13 @@
+MODULE counter_cell(carry_in)
+ VAR
+   value : boolean;
+ ASSIGN
+   init(value) := FALSE;
+   next(value) := value xor carry_in;
+ DEFINE
+  carry_out := value & carry_in;
+MODULE main
+ VAR
+   bit0 : counter_cell(TRUE);
+   bit1 : counter_cell(bit0.carry_out);
+   bit2 : counter_cell(bit1.carry_out);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test3.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,13 @@
+MODULE inverter(input)
+ VAR
+   output : boolean;
+ ASSIGN
+   init(output) := FALSE;
+   next(output) := !input;
+MODULE main
+ VAR
+   gate1 : process inverter(gate3.output);
+   gate2 : process inverter(gate1.output);
+   gate3 : process inverter(gate2.output);
+FAIRNESS
+  running

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test4.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,11 @@
+MODULE inverter(input)
+ VAR
+   output : boolean;
+ ASSIGN
+  init(output) := FALSE;
+  next(output) := (!input) union output;
+MODULE main
+ VAR
+   gate1 : inverter(gate3.output);
+   gate2 : inverter(gate1.output);
+   gate3 : inverter(gate2.output);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test5.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,27 @@
+MODULE main
+ VAR
+   semaphore : boolean;
+   proc1     : process user(semaphore);
+   proc2     : process user(semaphore);
+ ASSIGN
+   init(semaphore) := FALSE;
+MODULE user(semaphore)
+ VAR
+   state : {idle, entering, critical, exiting}; 
+ASSIGN
+  init(state) := idle;
+  next(state) :=
+  case
+  state = idle : {idle, entering}; state = entering & !semaphore : critical;
+       state = critical
+       state = exiting
+       TRUE
+     esac;
+   next(semaphore) :=
+     case
+       state = entering : TRUE;
+       state = exiting  : FALSE;
+       TRUE             : semaphore;
+     esac;
+ FAIRNESS
+  running

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test6.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,13 @@
+MODULE main
+ VAR
+   gate1 : inverter(gate3.output);
+   gate2 : inverter(gate1.output);
+   gate3 : inverter(gate2.output);
+MODULE inverter(input)
+ VAR
+   output : boolean;
+ INIT
+   output = FALSE
+ TRANS
+   next(output) = !input | next(output) = output
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test7.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,9 @@
+MODULE main
+VAR
+  request : boolean;
+state : {ready,busy}; ASSIGN
+  init(state) := ready;
+  next(state) := case
+                   state = ready & request : busy;
+TRUE : {ready,busy}; esac;
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test8.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,30 @@
+MODULE main
+ VAR
+   semaphore : boolean;
+   proc1     : process user(semaphore);
+   proc2     : process user(semaphore);
+ ASSIGN
+   init(semaphore) := FALSE;
+ SPEC AG ! (proc1.state = critical & proc2.state = critical)
+ SPEC AG (proc1.state = entering -> AF proc1.state = critical)
+MODULE user(semaphore)
+ VAR
+   state : {idle, entering, critical, exiting};
+ ASSIGN
+   init(state) := idle;
+   next(state) :=
+    case
+     state = idle : {idle, entering}; 
+     state = entering & !semaphore : critical;
+     state = critical : {critical, exiting};
+     state = exiting : idle;
+     TRUE    : state ;
+     esac;
+    next(semaphore) :=
+  case
+    state = entering : TRUE;
+    state = exiting  : FALSE;
+       TRUE             : semaphore;
+     esac;
+ FAIRNESS
+   running

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/test9.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,29 @@
+MODULE main
+ VAR
+   semaphore : boolean;
+   proc1     : process user(semaphore);
+   proc2     : process user(semaphore);
+ ASSIGN
+   init(semaphore) := FALSE;
+ LTLSPEC G ! (proc1.state = critical & proc2.state = critical)
+ LTLSPEC G (proc1.state = entering -> F proc1.state = critical)
+MODULE user(semaphore)
+VAR
+state : {idle, entering, critical, exiting};
+ ASSIGN
+   init(state) := idle;
+   next(state) :=
+    case
+       state = idle : {idle, entering}; state = entering & !semaphore : critical;
+       state = critical : {critical, exiting};
+       state = exiting : idle;
+       TRUE : state;
+     esac;
+   next(semaphore) :=
+     case
+       state = entering : TRUE;
+       state = exiting  : FALSE;
+       TRUE             : semaphore;
+     esac;
+ FAIRNESS
+   running

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/testa.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,12 @@
+MODULE main
+VAR
+  state : {a, b};
+ASSIGN
+  init(state) := a;
+  next(state) := {a, b}; 
+    SPEC AG state=a
+    SPEC EG state=a
+    SPEC AF state=a
+    SPEC EF state=a
+    SPEC A [ state=a U state=b ]
+    SPEC E [ state=a U state=b ]

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a13/smv/testb.smv	Sat Nov 23 12:59:45 2019 +0900
@@ -0,0 +1,15 @@
+MODULE main
+VAR
+  state : {a, b};
+ASSIGN
+  init(state) := a;
+  next(state) := case 
+     state = a : b ;
+     state = b : a ;
+    esac; 
+SPEC AG state=a
+SPEC EG state=a
+SPEC AF state=a
+SPEC EF state=a
+SPEC A [ state=a U state=b ]
+SPEC E [ state=a U state=b ]

Binary file exercise/fig/nfa01.graffle has changed

Binary file exercise/fig/nfa02.graffle has changed