Mercurial > hg > Members > kono > Proof > automaton

changeset 63:abfeed0c61b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 30 Oct 2019 12:07:29 +0900
parents 797dd1369472
children 475923938f50
files a03/lecture.ind agda/puzzle.agda
diffstat 2 files changed, 89 insertions(+), 90 deletions(-) [+]
line wrap: on
line diff
--- a/a03/lecture.ind	Mon Oct 28 09:05:13 2019 +0900
+++ b/a03/lecture.ind	Wed Oct 30 12:07:29 2019 +0900
@@ -14,7 +14,6 @@
            : Set  where
         field
             δ : Q → Σ → Q
-            astart : Q
             aend : Q → Bool
 
 <a href="../agda/automaton.agda"> automaton.agda </a>
@@ -23,10 +22,6 @@
 
 record は直積で複数の集合の組だが、ここでは関係を表す論理式/関数の型の組になっている。
 
-      astart : Q
-
-Q の要素一つを表している。このrecordが一つあると、astart で一つQの要素を特定できる。
-
       δ : Q → Σ → Q
 
 は関数で、引数を二つ持っている。ここでは論理式ではない。入力となるaplhabet(文字) とstate (状態)から次の状態を指定する関数である。
@@ -42,6 +37,8 @@
 
 で、true false の二つの要素を持つ集合である。(これでどうして部分集合になるのか? F ⊆ Q を Agda ではどう定義するべきか?)
 
+start state はrecordで定義しない方が便利だと言うことがこの後わかる。
+
 --オートマトンの入力
 
 オートマトンの入力は文字列である。文字列を表すには List を用いる。
@@ -72,13 +69,15 @@
 
     accept : { Q : Set } { Σ : Set  }
         → Automaton Q  Σ
+        → (astart : Q)
         → List  Σ → Bool
-    accept {Q} { Σ} M L = move (astart M) L
+    accept {Q} { Σ} M astart L = move astart 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 内で定義しても良い。
 
 ---具体的なオートマトン
@@ -114,7 +113,7 @@
 st になればok。record は以下のように作る。
 
     am1  :  Automaton  States1 In2
-    am1  =  record {  δ = transition1 ; astart = sr ; aend = fin1   }
+    am1  =  record {  δ = transition1 ; aend = fin1   }
 
 これを動かすには、
 
--- a/agda/puzzle.agda	Mon Oct 28 09:05:13 2019 +0900
+++ b/agda/puzzle.agda	Wed Oct 30 12:07:29 2019 +0900
@@ -38,7 +38,7 @@
         lemma1 (case2 g) = ¬g g
 
     problem1 : Goat → ¬ Dog
-    problem1 g d = ⊥-elim ( fact1 p (case2 d) g )
+    problem1 g d = fact1 p (case2 d) g 
   
     problem2 : Goat → Rabbit
     problem2 g with lem Cat | lem Dog
@@ -52,16 +52,16 @@
         lemma2 (case2 g) with fact2 p ¬c
         lemma2 (case2 g) | case1 d = ¬d d
         lemma2 (case2 g) | case2 r = ¬r r
-  
+
     problem3 : (¬ Rabbit ) → Cat
     problem3 ¬r with lem Cat | lem Goat 
     problem3 ¬r | case1 c | g = c
     problem3 ¬r | case2 ¬c | g = ⊥-elim ( ¬r ( fact3 p lemma3 )) where
-       lemma3 :  ¬ ( Cat ∨ Goat )
-       lemma3 (case1 c) = ¬c c
-       lemma3 (case2 g) with fact2 p ¬c
-       lemma3 (case2 g) | case1 d = fact1 p (case2 d ) g
-       lemma3 (case2 g) | case2 r = ¬r r
+        lemma3 :  ¬ ( Cat ∨ Goat )
+        lemma3 (case1 c) = ¬c c
+        lemma3 (case2 g) with fact2 p ¬c
+        lemma3 (case2 g) | case1 d = fact1 p (case2 d ) g
+        lemma3 (case2 g) | case2 r = ¬r r
 
 module pet-research1 ( Cat Dog Goat Rabbit : Set ) where
 
@@ -116,79 +116,79 @@
   problem3 false true false false = refl
   problem3 false true true false = refl
 
-module pet-research2 ( Cat Dog Goat Rabbit : Set ) where
-
-  open import Data.Bool hiding ( _∨_ )
-  open import Relation.Binary
-  open import Relation.Binary.PropositionalEquality 
-
-  ¬_ : Bool → Bool
-  ¬ p = p xor true
-
-  infixr 5 _∨_ 
-  _∨_ :  Bool → Bool → Bool
-  a ∨ b = ¬ ( (¬ a) ∧ (¬ b ) )
-
-  _=>_ :  Bool → Bool → Bool
-  a => b = (¬ a ) ∨ b 
-
-  open import Data.Bool.Solver using (module xor-∧-Solver)
-  open xor-∧-Solver
-
-  problem0' :  ( Cat : Bool ) → (Cat xor Cat ) ≡ false
-  problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl
-
-  problem1' :  ( Cat : Bool ) → (Cat ∧ (Cat xor true ))  ≡ false 
-  problem1' = solve 1 (λ c → ((c :* (c :+ con true )) ) := con false ) {!!}
-
-  open import Data.Nat
-  :¬_ : {n : ℕ} → Polynomial n → Polynomial n
-  :¬ p = p :+ con true
-
-  _:∨_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
-  a :∨ b = :¬ ( ( :¬ a ) :* ( :¬ b ))
-
-  _:=>_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
-  a :=> b = ( :¬ a ) :∨ b 
-
-  _:∧_ = _:*_
-
-  infixr 6 _:∧_
-  infixr 5 _:∨_ 
-
-  problem0 :  ( Cat Dog Goat Rabbit : Bool ) →
-    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
-    => (Cat ∨ Dog ∨ Goat ∨ Rabbit) ≡ true
-  problem0 = solve 4 ( λ Cat Dog Goat Rabbit → (
-    ( ((Cat :∨ Dog ) :=> (:¬ Goat)) :∧ ( ((:¬ Cat ) :=>  ( Dog :∨ Rabbit )) :∧ (( :¬ ( Cat :∨ Goat ) ) :=>  Rabbit)  ))
-    :=> ( Cat :∨ (Dog :∨ ( Goat :∨ Rabbit))) ) := con true ) {!!}
-
-  problem1 :  ( Cat Dog Goat Rabbit : Bool ) →
-    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
-    => ( Goat => ( ¬ Dog )) ≡ true
-  problem1 c false false r = {!!}
-  problem1 c true false r = {!!}
-  problem1 c false true r = {!!}
-  problem1 false true true r = refl
-  problem1 true true true r = refl
-
-  problem2 :  ( Cat Dog Goat Rabbit : Bool ) →
-    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
-    => ( Goat => Rabbit ) ≡ true
-  problem2 c d false false = {!!}
-  problem2 c d false true = {!!}
-  problem2 c d true true = {!!}
-  problem2 true d true false = refl
-  problem2 false false true false = refl
-  problem2 false true true false = refl
-
-  problem3 :  ( Cat Dog Goat Rabbit : Bool ) →
-    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
-    => ( (¬ Rabbit ) => Cat ) ≡ true
-  problem3 false d g true = {!!}
-  problem3 true d g true = {!!}
-  problem3 true d g false = {!!}
-  problem3 false false false false = refl
-  problem3 false false true false = refl
-  problem3 false true false false = refl
-  problem3 false true true false = refl
+-- module pet-research2 ( Cat Dog Goat Rabbit : Set ) where
+-- 
+--   open import Data.Bool hiding ( _∨_ )
+--   open import Relation.Binary
+--   open import Relation.Binary.PropositionalEquality 
+-- 
+--   ¬_ : Bool → Bool
+--   ¬ p = p xor true
+-- 
+--   infixr 5 _∨_ 
+--   _∨_ :  Bool → Bool → Bool
+--   a ∨ b = ¬ ( (¬ a) ∧ (¬ b ) )
+-- 
+--   _=>_ :  Bool → Bool → Bool
+--   a => b = (¬ a ) ∨ b 
+-- 
+--   open import Data.Bool.Solver using (module xor-∧-Solver)
+--   open xor-∧-Solver
+-- 
+--   problem0' :  ( Cat : Bool ) → (Cat xor Cat ) ≡ false
+--   problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl
+-- 
+--   problem1' :  ( Cat : Bool ) → (Cat ∧ (Cat xor true ))  ≡ false 
+--   problem1' = solve 1 (λ c → ((c :* (c :+ con true )) ) := con false ) {!!}
+-- 
+--   open import Data.Nat
+--   :¬_ : {n : ℕ} → Polynomial n → Polynomial n
+--   :¬ p = p :+ con true
+-- 
+--   _:∨_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+--   a :∨ b = :¬ ( ( :¬ a ) :* ( :¬ b ))
+-- 
+--   _:=>_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+--   a :=> b = ( :¬ a ) :∨ b 
+-- 
+--   _:∧_ = _:*_
+-- 
+--   infixr 6 _:∧_
+--   infixr 5 _:∨_ 
+-- 
+--   problem0 :  ( Cat Dog Goat Rabbit : Bool ) →
+--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+--     => (Cat ∨ Dog ∨ Goat ∨ Rabbit) ≡ true
+--   problem0 = solve 4 ( λ Cat Dog Goat Rabbit → (
+--     ( ((Cat :∨ Dog ) :=> (:¬ Goat)) :∧ ( ((:¬ Cat ) :=>  ( Dog :∨ Rabbit )) :∧ (( :¬ ( Cat :∨ Goat ) ) :=>  Rabbit)  ))
+--     :=> ( Cat :∨ (Dog :∨ ( Goat :∨ Rabbit))) ) := con true ) {!!}
+-- 
+--   problem1 :  ( Cat Dog Goat Rabbit : Bool ) →
+--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+--     => ( Goat => ( ¬ Dog )) ≡ true
+--   problem1 c false false r = {!!}
+--   problem1 c true false r = {!!}
+--   problem1 c false true r = {!!}
+--   problem1 false true true r = refl
+--   problem1 true true true r = refl
+-- 
+--   problem2 :  ( Cat Dog Goat Rabbit : Bool ) →
+--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+--     => ( Goat => Rabbit ) ≡ true
+--   problem2 c d false false = {!!}
+--   problem2 c d false true = {!!}
+--   problem2 c d true true = {!!}
+--   problem2 true d true false = refl
+--   problem2 false false true false = refl
+--   problem2 false true true false = refl
+-- 
+--   problem3 :  ( Cat Dog Goat Rabbit : Bool ) →
+--     ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+--     => ( (¬ Rabbit ) => Cat ) ≡ true
+--   problem3 false d g true = {!!}
+--   problem3 true d g true = {!!}
+--   problem3 true d g false = {!!}
+--   problem3 false false false false = refl
+--   problem3 false false true false = refl
+--   problem3 false true false false = refl
+--   problem3 false true true false = refl