Canvas 1

# HG changeset patch # User Shinji KONO # Date 1678628999 -32400 # Node ID 6f3636fbc481d3d430419cd090dc72bbb7dbcfc6 # Parent 9324852d3a1767f4ebfabd125614baa9d13fc14f fix diff -r 9324852d3a17 -r 6f3636fbc481 .hgtags diff -r 9324852d3a17 -r 6f3636fbc481 a01/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda-install.ind diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda.ind diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/dag.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/data1.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/equality.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/lambda.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/level1.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/list.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/logic.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/practice-logic.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/practice-nat.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/agda/record1.agda diff -r 9324852d3a17 -r 6f3636fbc481 a02/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a02/reduction.ind diff -r 9324852d3a17 -r 6f3636fbc481 a02/unification.ind diff -r 9324852d3a17 -r 6f3636fbc481 a03/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a04/fig/concat.graffle diff -r 9324852d3a17 -r 6f3636fbc481 a04/fig/concat.svg diff -r 9324852d3a17 -r 6f3636fbc481 a04/fig/nfa.graffle diff -r 9324852d3a17 -r 6f3636fbc481 a04/fig/nfa.svg diff -r 9324852d3a17 -r 6f3636fbc481 a04/lecture.ind --- a/a04/lecture.ind Wed Dec 07 14:51:25 2022 +0900 +++ b/a04/lecture.ind Sun Mar 12 22:49:59 2023 +0900 @@ -164,36 +164,6 @@ もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。 ---finiteSet - -有限な集合を表すのに、個々の data を使えばよいが、統一的に扱いたい。Agda には Data.Fin が用意されている。 - -Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。 - - 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 - -という感じで、Data.Fin と状態を対応させる。そうすると、 - - lt0 : (n : ℕ) → n Data.Nat.≤ n - lt0 zero = z≤n - lt0 (suc n) = s≤s (lt0 n) - - exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool - exists1 zero _ _ = false - exists1 ( suc m ) m finiteSet.agda - --NAutomatonの受理と遷移 @@ -201,25 +171,24 @@ Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ - → {n : ℕ } → FiniteSet Q {n} - → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool - Nmoves {Q} { Σ} M fin Qs s q = - exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) + → (exists : ( Q → Bool ) → Bool) + → ( Qs : Q → Bool ) → (s : Σ ) → ( Q → Bool ) + Nmoves {Q} { Σ} M exists Qs s = λ q → exists ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば遷移可能になる。(だいぶ簡単になった) + Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ - → {n : ℕ } → FiniteSet Q {n} + → (exists : ( Q → Bool ) → Bool) → (Nstart : Q → Bool) → List Σ → Bool - Naccept M fin sb [] = exists fin ( λ q → sb q /\ Nend M q ) - Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t + Naccept M exists sb [] = exists ( λ q → sb q /\ Nend M q ) + Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。 - --例題例題1.36 を考えよう。状態遷移関数は以下のようになる。 @@ -261,99 +230,6 @@ ---非決定性オートマトンと決定性オートマトン - - record Automaton ( Q : Set ) ( Σ : Set ) - : Set where - field - δ : Q → Σ → Q - aend : Q → Bool - -の Q に Q → Bool を入れてみる。 - - δ : (Q → Bool ) → Σ → Q → Bool - aend : (Q → Bool ) → Bool - -これを、 - - record NAutomaton ( Q : Set ) ( Σ : Set ) - : Set where - field - Nδ : Q → Σ → Q → Bool - Nend : Q → Bool - -これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。 - -NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。 - -遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は - - Nδ : Q → Σ → Q → Bool - -だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。 - - f q /\ Nδ NFA q i nq - -これが true になるものを exists を使って探し出す。 - - δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool) - δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q ) - -ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。 - -終了条件は - - f q /\ Nend NFA q ) - -で良い。これが true になるものを exists を使って探し出す。 - -Q が FiniteSet Q {n} であれば - - subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → - (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ ) - subset-construction {Q} { Σ} {n} fin NFA astart = record { - δ = λ f i → δconv fin ( Nδ NFA ) f i - ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q ) - } - -という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。 - - λ f i → δconv fin ( Nδ NFA ) f i -は - λ f i q → δconv fin ( Nδ NFA ) f i q - -であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。 - -これで実際に、NFAから DFA を作成することができた。ここで、状態の有限性を使っていることを確認しよう。 - - subset construction - ---subset constructionの状態数 - -実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを -自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、 - - q1 q2 q3 - false false false - false false true - false true false - false true true - true false false - true false true - true true false - true true true - -という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。 - -アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。 -前もって、可能な状態を Automaton として探し出そうとすると、指数関数的な爆発になってしまう。 - -実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。 - ---NFAの実行 - -subset construction した automaton はすべての状態を生成する前でも実行することができる。 -ただし、毎回、nest した exists を実行することになる。 @@ -364,5 +240,3 @@ - - diff -r 9324852d3a17 -r 6f3636fbc481 a05/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a06/fig/derivation.graffle Binary file a06/fig/derivation.graffle has changed diff -r 9324852d3a17 -r 6f3636fbc481 a06/fig/derivation.svg --- a/a06/fig/derivation.svg Wed Dec 07 14:51:25 2022 +0900 +++ b/a06/fig/derivation.svg Sun Mar 12 22:49:59 2023 +0900 @@ -1,12 +1,7 @@ -^Q と書くことがある。Bool は二つの要素がある。状態数4からBoolへの関数は、2 ⁴個ある。集合のべき乗をこのようにして定義することができる。 @@ -34,8 +36,116 @@ 　　λ q → f q ∧ Nδ q i + +--状態の部分集合を使う + +true になるものは複数あるので、やはり部分集合で表される。つまり、 + + exists : ( P : Q → Bool ) → Q → Bool + +このような関数を実装する必要がある。 + +--非決定性オートマトンと決定性オートマトン + + record Automaton ( Q : Set ) ( Σ : Set ) + : Set where + field + δ : Q → Σ → Q + aend : Q → Bool + +の Q に Q → Bool を入れてみる。 + + δ : (Q → Bool ) → Σ → Q → Bool + aend : (Q → Bool ) → Bool + +これを、 + + record NAutomaton ( Q : Set ) ( Σ : Set ) + : Set where + field + Nδ : Q → Σ → Q → Bool + Nend : Q → Bool + +これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。 + +NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。 + +遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は + + Nδ : Q → Σ → Q → Bool + +だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。 + + f q /\ Nδ NFA q i nq + +これが true になるものを exists を使って探し出す。 + + δconv : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) + → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) + δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q ) + +ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。 + +終了条件は + + f q /\ Nend NFA q ) + +で良い。これが true になるものを exists を使って探し出す。 + +Q が FiniteSet Q {n} であれば + + subset-construction : { Q : Set } { Σ : Set } → + ( ( Q → Bool ) → Bool ) → + (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) + subset-construction {Q} { Σ} exists NFA = record { + δ = λ q x → δconv exists ( Nδ NFA ) q x + ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) + } + +という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。 + + λ f i → δconv exists ( Nδ NFA ) f i +は + λ f i q → δconv exists ( Nδ NFA ) f i q + +であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。 + +これで実際に、NFAから DFA を作成することができた。 +ここで、状態の exists (有限性または部分集合の決定性)を使っていることに注意しよう。 + + subset construction + + ---問題7.1 以下の非決定性オートマトンを決定性オートマトンへ変換せよ例題 +--subset constructionの状態数 + +実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを +自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、 + + q1 q2 q3 + false false false + false false true + false true false + false true true + true false false + true false true + true true false + true true true + +という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。 + +アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。 +前もって、可能な状態を Automaton として探し出そうとすると、指数関数的な爆発になってしまう。 + +実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。 + +--NFAの実行 + +subset construction した automaton はすべての状態を生成する前でも実行することができる。 +ただし、毎回、nest した exists を実行することになる。 + + diff -r 9324852d3a17 -r 6f3636fbc481 a08/lecture.ind --- a/a08/lecture.ind Wed Dec 07 14:51:25 2022 +0900 +++ b/a08/lecture.ind Sun Mar 12 22:49:59 2023 +0900 @@ -136,51 +136,14 @@ しかし、文法自体は CFG で定義されることが多い。 -文法定義には BNF (Buckas Noar Form)を使う。ここでは Agda で以下のように定義する。 - - data Node (Symbol : Set) : Set where - T : Symbol → Node Symbol - N : Symbol → Node Symbol - - data Seq (Symbol : Set) : Set where - _，_ : Symbol → Seq Symbol → Seq Symbol - _． : Symbol → Seq Symbol - Error : Seq Symbol - - data Body (Symbol : Set) : Set where - _｜_ : Seq Symbol → Body Symbol → Body Symbol - _； : Seq Symbol → Body Symbol - - record CFGGrammer (Symbol : Set) : Set where - field - cfg : Symbol → Body Symbol - top : Symbol - eq? : Symbol → Symbol → Bool - typeof : Symbol → Node Symbol +文法定義には BNF (Buckas Noar Form)を使う。 -これを split を使って言語として定義できる。 - - cfg-language0 : {Symbol : Set} → CFGGrammer Symbol → Body Symbol → List Symbol → Bool - - {-# TERMINATING #-} - cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool - cfg-language1 cg Error x = false - cfg-language1 cg (S ， seq) x with typeof cg S - cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' /\ cfg-language1 cg seq t - cfg-language1 cg (_ ， seq) [] | T x = false - cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x - cfg-language1 cg (S ．) x with typeof cg S - cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x' - cfg-language1 cg (_ ．) _ | T x = false - cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x - - cfg-language0 cg _ [] = false - cfg-language0 cg (rule ｜ b) x = - cfg-language1 cg rule x \/ cfg-language0 cg b x - cfg-language0 cg (rule ；) x = cfg-language1 cg rule x - - cfg-language : {Symbol : Set} → CFGGrammer Symbol → List Symbol → Bool - cfg-language cg = cfg-language0 cg (cfg cg (top cg )) + expr : EA | EB | EC ; + statement : + SA | SB | SC + | IF expr THEN statement + | IF expr THEN statement ELSE statement + ; これらを実際に parse するのには再帰下降法が便利なことが知られている。 @@ -190,13 +153,14 @@ --文脈依存文法 - cfg : Symbol → Body Symbol + expr : EA | EB | EC ; の部分を - cdg : List Symbol → Body Symbol + delcare exprt : EA | EB | EC ; -とすると、文脈依存文法になる。これを判定して停止するプログラムは、stack を二つ持つ Automaton になるが、 +のように : の左側に複数の要素を許す +と、文脈依存文法になる。これを判定して停止するプログラムは、stack を二つ持つ Automaton になるが、 Turing Machine と呼ばれる。その停止性を判定することはできない。それを次の講義で示す。実用的には文法規則の適当な subset を停止することが分かっているアルゴリズムで決めれば良い。 diff -r 9324852d3a17 -r 6f3636fbc481 a09/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a10/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a11/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a12/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a13/fig/semaphore.graffle diff -r 9324852d3a17 -r 6f3636fbc481 a13/fig/semaphore.svg diff -r 9324852d3a17 -r 6f3636fbc481 a13/lecture.ind diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test1.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test10.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test2.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test3.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test4.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test5.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test6.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test7.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test8.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/test9.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/testa.smv diff -r 9324852d3a17 -r 6f3636fbc481 a13/smv/testb.smv diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/LICENSE diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/README.md diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/automaton-in-agda.agda-lib diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/automaton-in-agda.agda-pkg diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/automaton-ex.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/automaton.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/bijection.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/cfg.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/cfg1.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/chap0.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/derive.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/deriveUtil.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/even.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/extended-automaton.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/automaton-in-agda/src/extended-automaton.agda Sun Mar 12 22:49:59 2023 +0900 @@ -0,0 +1,80 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module extended-automaton where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat -- hiding ( erase ) +open import Data.List +open import Data.Maybe hiding ( map ) +-- open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate ) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Product hiding ( map ) +open import logic + +record Automaton ( Q : Set ) ( Σ : Set ) : Set where + field + δ : Q → Σ → Q + aend : Q → Bool + +open Automaton + +accept : { Q : Set } { Σ : Set } + → Automaton Q Σ + → Q + → List Σ → Bool +accept M q [] = aend M q +accept M q ( H ∷ T ) = accept M ( δ M q H ) T + +NAutomaton : ( Q : Set ) ( Σ : Set ) → Set +NAutomaton Q Σ = Automaton ( Q → Bool ) Σ + +Naccept : { Q : Set } { Σ : Set } + → Automaton (Q → Bool) Σ + → (exists : ( Q → Bool ) → Bool) + → (Nstart : Q → Bool) → List Σ → Bool +Naccept M exists sb [] = exists ( λ q → sb q /\ aend M sb ) +Naccept M exists sb (i ∷ t ) = Naccept M exists (λ q → exists ( λ qn → (sb qn /\ ( δ M sb i q ) ))) t + +PDA : ( Q : Set ) ( Σ : Set ) → Set +PDA Q Σ = Automaton ( List Q ) Σ + +data Write ( Σ : Set ) : Set where + write : Σ → Write Σ + wnone : Write Σ + -- erase write tnone + +data Move : Set where + left : Move + right : Move + mnone : Move + +record OTuring ( Q : Set ) ( Σ : Set ) + : Set where + field + tδ : Q → Σ → Q × ( Write Σ ) × Move + tstart : Q + tend : Q → Bool + tnone : Σ + taccept : List Σ → ( Q × List Σ × List Σ ) + taccept L = ? + +open import bijection + +b0 : ( Q : Set ) ( Σ : Set ) → Bijection (List Q) (( Q × ( Write Σ ) × Move ) ∧ ( Q × List Σ × List Σ )) +b0 = ? + +Turing : ( Q : Set ) ( Σ : Set ) → Set +Turing Q Σ = Automaton ( List Q ) Σ + +NDTM : ( Q : Set ) ( Σ : Set ) → Set +NDTM Q Σ = Automaton ( List Q → Bool ) Σ + +UTM : ( Q : Set ) ( Σ : Set ) → Set +UTM Q Σ = Automaton ( List Q ) Σ + +SuperTM : ( Q : Set ) ( Σ : Set ) → Set +SuperTM Q Σ = Automaton ( List Q ) Σ + + + diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/fin.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/finiteSet.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/finiteSetUtil.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/flcagl.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/gcd.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/halt.agda --- a/automaton-in-agda/src/halt.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/halt.agda Sun Mar 12 22:49:59 2023 +0900 @@ -114,3 +114,5 @@ TNL1 : UTM → ¬ Halt TNL1 utm halt = diagonal ( TNL halt utm ) + + diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/index.ind diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/induction-ex.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/lang-text.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/libbijection.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/logic.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/nat.agda --- a/automaton-in-agda/src/nat.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/nat.agda Sun Mar 12 22:49:59 2023 +0900 @@ -189,9 +189,6 @@ *< {zero} {suc y} lt = s≤s z≤n *< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) -*-cancel-left : {x y z : ℕ } → x > 0 → x * y ≡ x * z → y ≡ z -*-cancel-left {suc x} {y} {z} x>0 eq = *-cancelˡ-≡ x eq - 0 → x * y ≡ x * z → y ≡ z +*-cancel-left {suc x} {zero} {zero} lt eq = refl +*-cancel-left {suc x} {zero} {suc z} lt eq = ⊥-elim ( nat-≡< eq (s≤s (begin + x * zero ≡⟨ *-comm x _ ⟩ + zero ≤⟨ z≤n ⟩ + z + x * suc z ∎ ))) where open ≤-Reasoning +*-cancel-left {suc x} {suc y} {zero} lt eq = ⊥-elim ( nat-≡< (sym eq) (s≤s (begin + x * zero ≡⟨ *-comm x _ ⟩ + zero ≤⟨ z≤n ⟩ + _ ∎ ))) where open ≤-Reasoning +*-cancel-left {suc x} {suc y} {suc z} lt eq with cong pred eq +... | eq1 = cong suc (*-cancel-left {suc x} {y} {z} lt ( proj₂ +-cancel-≡ x _ _ (begin + y + x * y + x ≡⟨ +-assoc y _ _ ⟩ + y + (x * y + x) ≡⟨ cong (λ k → y + (k + x)) (*-comm x _) ⟩ + y + (y * x + x) ≡⟨ cong (_+_ y) (+-comm _ x) ⟩ + y + (x + y * x ) ≡⟨ refl ⟩ + y + suc y * x ≡⟨ cong (_+_ y) (*-comm (suc y) _) ⟩ + y + x * suc y ≡⟨ eq1 ⟩ + z + x * suc z ≡⟨ refl ⟩ + _ ≡⟨ sym ( cong (_+_ z) (*-comm (suc z) _) ) ⟩ + _ ≡⟨ sym ( cong (_+_ z) (+-comm _ x)) ⟩ + z + (z * x + x) ≡⟨ sym ( cong (λ k → z + (k + x)) (*-comm x _) ) ⟩ + z + (x * z + x) ≡⟨ sym ( +-assoc z _ _) ⟩ + z + x * z + x ∎ ))) where open ≡-Reasoning + record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set (n Level.⊔ m) where field fzero : {p : P} → f p ≡ zero → Q p diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/nfa.agda --- a/automaton-in-agda/src/nfa.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/nfa.agda Sun Mar 12 22:49:59 2023 +0900 @@ -38,14 +38,15 @@ existsS1 : ( States1 → Bool ) → Bool existsS1 qs = qs sr \/ qs ss \/ qs st --- extract list of q which qs q is true -to-listS1 : ( States1 → Bool ) → List States1 -to-listS1 qs = ss1 LStates1 where - ss1 : List States1 → List States1 - ss1 [] = [] - ss1 (x ∷ t) with qs x - ... | true = x ∷ ss1 t - ... | false = ss1 t +-- given list of all states, extract list of q which qs q is true + +to-list : {Q : Set} → List Q → ( Q → Bool ) → List Q +to-list {Q} x exists = to-list1 x [] where + to-list1 : List Q → List Q → List Q + to-list1 [] x = x + to-list1 (q ∷ qs) x with exists q + ... | true = to-list1 qs (q ∷ x ) + ... | false = to-list1 qs x Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ @@ -63,7 +64,7 @@ {-# TERMINATING #-} NtraceDepth : { Q : Set } { Σ : Set } → NAutomaton Q Σ - → (Nstart : Q → Bool) → List Q → List Σ → List (List ( Σ ∧ Q )) + → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → List (List ( Σ ∧ Q )) NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] [] where ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (List ( Σ ∧ Q ) ) → List (List ( Σ ∧ Q ) ) ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( List ( Σ ∧ Q )) → List ( List ( Σ ∧ Q )) @@ -77,17 +78,40 @@ ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) ... | false = ndepth qs sb (i ∷ is) t t1 +NtraceDepth1 : { Q : Set } { Σ : Set } + → NAutomaton Q Σ + → (Nstart : Q → Bool) → (all-states : List Q ) → List Σ → Bool ∧ List (List ( Σ ∧ Q )) +NtraceDepth1 {Q} {Σ} M sb all is = ndepth all sb is [] [] where + exists : (Q → Bool) → Bool + exists p = exists1 all where + exists1 : List Q → Bool + exists1 [] = false + exists1 (q ∷ qs) with p q + ... | true = true + ... | false = exists1 qs + ndepth : List Q → (q : Q → Bool ) → List Σ → List ( Σ ∧ Q ) → List (Bool ∧ List ( Σ ∧ Q ) ) → Bool ∧ List (List ( Σ ∧ Q ) ) + ndepth1 : Q → Σ → List Q → List Σ → List ( Σ ∧ Q ) → List ( Bool ∧ List ( Σ ∧ Q )) → List ( Bool ∧ List ( Σ ∧ Q )) + ndepth1 q i [] is t t1 = t1 + ndepth1 q i (x ∷ qns) is t t1 = ? -- ndepth all (Nδ M x i) is (⟪ i , q ⟫ ∷ t) (ndepth1 q i qns is t t1 ) + ndepth [] sb is t t1 = ? -- ⟪ exists (λ q → Nend M q /\ sb q) ? ⟫ + ndepth (q ∷ qs) sb [] t t1 with sb q /\ Nend M q + ... | true = ndepth qs sb [] t ( ? ∷ t1 ) + ... | false = ndepth qs sb [] t t1 + ndepth (q ∷ qs) sb (i ∷ is) t t1 with sb q + ... | true = ndepth qs sb (i ∷ is) t (ndepth1 q i all is t t1 ) + ... | false = ndepth qs sb (i ∷ is) t t1 + -- trace in state set -- Ntrace : { Q : Set } { Σ : Set } → NAutomaton Q Σ + → (all-states : List Q ) → (exists : ( Q → Bool ) → Bool) - → (to-list : ( Q → Bool ) → List Q ) → (Nstart : Q → Bool) → List Σ → List (List Q) -Ntrace M exists to-list sb [] = to-list ( λ q → sb q /\ Nend M q ) ∷ [] -Ntrace M exists to-list sb (i ∷ t ) = - to-list (λ q → sb q ) ∷ - Ntrace M exists to-list (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t +Ntrace M all-states exists sb [] = to-list all-states ( λ q → sb q /\ Nend M q ) ∷ [] +Ntrace M all-states exists sb (i ∷ t ) = + to-list all-states (λ q → sb q ) ∷ + Ntrace M all-states exists (λ q → exists ( λ qn → (sb qn /\ ( Nδ M qn i q ) ))) t data-fin-00 : ( Fin 3 ) → Bool data-fin-00 zero = true @@ -117,7 +141,7 @@ fin1 sr = false test5 = existsS1 (λ q → fin1 q ) -test6 = to-listS1 (λ q → fin1 q ) +test6 = to-list LStates1 (λ q → fin1 q ) start1 : States1 → Bool start1 sr = true @@ -130,8 +154,8 @@ example2-2 = Naccept am2 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) t-1 : List ( List States1 ) -t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ [] -t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ [] +t-1 = Ntrace am2 LStates1 existsS1 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ (sr ∷ ss ∷ st ∷ []) ∷ (st ∷ []) ∷ [] +t-2 = Ntrace am2 LStates1 existsS1 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) -- (sr ∷ []) ∷ (sr ∷ []) ∷ (sr ∷ ss ∷ []) ∷ [] ∷ [] t-3 = NtraceDepth am2 start1 LStates1 ( i1 ∷ i1 ∷ i1 ∷ [] ) t-4 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ i0 ∷ [] ) t-5 = NtraceDepth am2 start1 LStates1 ( i0 ∷ i1 ∷ [] ) @@ -237,47 +261,3 @@ existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) ) existsS1-valid n = ¬-bool refl ( n ( λ x → false )) --- --- using finiteSet --- - -open import finiteSet -open import finiteSetUtil -open FiniteSet - -allQ : {Q : Set } (finq : FiniteSet Q) → List Q -allQ {Q} finq = to-list finq (λ x → true) - -existQ : {Q : Set } (finq : FiniteSet Q) → (Q → Bool) → Bool -existQ finq qs = exists finq qs - -eqQ? : {Q : Set } (finq : FiniteSet Q) → (x y : Q ) → Bool -eqQ? finq x y = equal? finq x y - -finState1 : FiniteSet States1 -finState1 = record { - finite = finite0 - ; Q←F = Q←F0 - ; F←Q = F←Q0 - ; finiso→ = finiso→0 - ; finiso← = finiso←0 - } where - finite0 : ℕ - finite0 = 3 - Q←F0 : Fin finite0 → States1 - Q←F0 zero = sr - Q←F0 (suc zero) = ss - Q←F0 (suc (suc zero)) = st - F←Q0 : States1 → Fin finite0 - F←Q0 sr = # 0 - F←Q0 ss = # 1 - F←Q0 st = # 2 - finiso→0 : (q : States1) → Q←F0 ( F←Q0 q ) ≡ q - finiso→0 sr = refl - finiso→0 ss = refl - finiso→0 st = refl - finiso←0 : (f : Fin finite0 ) → F←Q0 ( Q←F0 f ) ≡ f - finiso←0 zero = refl - finiso←0 (suc zero) = refl - finiso←0 (suc (suc zero)) = refl - diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/nfa136.agda --- a/automaton-in-agda/src/nfa136.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/nfa136.agda Sun Mar 12 22:49:59 2023 +0900 @@ -4,7 +4,6 @@ open import nfa open import automaton open import Data.List -open import finiteSet open import Data.Fin open import Relation.Binary.PropositionalEquality hiding ( [_] ) @@ -17,31 +16,6 @@ a0 : A2 b0 : A2 -finStateQ : FiniteSet StatesQ -finStateQ = record { - Q←F = Q←F - ; F←Q = F←Q - ; finiso→ = finiso→ - ; finiso← = finiso← - } where - Q←F : Fin 3 → StatesQ - Q←F zero = q1 - Q←F (suc zero) = q2 - Q←F (suc (suc zero)) = q3 - F←Q : StatesQ → Fin 3 - F←Q q1 = zero - F←Q q2 = suc zero - F←Q q3 = suc (suc zero) - finiso→ : (q : StatesQ) → Q←F (F←Q q) ≡ q - finiso→ q1 = refl - finiso→ q2 = refl - finiso→ q3 = 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 ()))) - transition136 : StatesQ → A2 → StatesQ → Bool transition136 q1 b0 q2 = true transition136 q1 a0 q1 = true -- q1 → ep → q3 @@ -62,41 +36,28 @@ exists136 : (StatesQ → Bool) → Bool exists136 f = f q1 \/ f q2 \/ f q3 -to-list-136 : (StatesQ → Bool) → List StatesQ -to-list-136 f = tl1 where - tl3 : List StatesQ - tl3 with f q3 - ... | true = q3 ∷ [] - ... | false = [] - tl2 : List StatesQ - tl2 with f q2 - ... | true = q2 ∷ tl3 - ... | false = tl3 - tl1 : List StatesQ - tl1 with f q1 - ... | true = q1 ∷ tl2 - ... | false = tl2 - nfa136 : NAutomaton StatesQ A2 nfa136 = record { Nδ = transition136; Nend = end136 } +states136 = q1 ∷ q2 ∷ q3 ∷ [] + example136-1 = Naccept nfa136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) -t146-1 = Ntrace nfa136 exists136 to-list-136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) +t146-1 = Ntrace nfa136 states136 exists136 start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) + +test111 = ? example136-0 = Naccept nfa136 exists136 start136( a0 ∷ [] ) example136-2 = Naccept nfa136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) -t146-2 = Ntrace nfa136 exists136 to-list-136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) - -open FiniteSet +t146-2 = Ntrace nfa136 states136 exists136 start136( b0 ∷ a0 ∷ b0 ∷ a0 ∷ b0 ∷ [] ) nx : (StatesQ → Bool) → (List A2 ) → StatesQ → Bool nx now [] = now nx now ( i ∷ ni ) = (Nmoves nfa136 exists136 (nx now ni) i ) -example136-3 = to-list-136 start136 -example136-4 = to-list-136 (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] )) +example136-3 = to-list states136 start136 +example136-4 = to-list states136 (nx start136 ( a0 ∷ b0 ∷ a0 ∷ [] )) open import sbconst2 @@ -111,3 +72,96 @@ → Naccept nfa136 exists136 states x ≡ accept fm136 states x lemma136-1 [] _ = refl lemma136-1 (h ∷ t) states = lemma136-1 t (δconv exists136 (Nδ nfa136) states h) + +data Σ2 : Set where + ca : Σ2 + cb : Σ2 + cc : Σ2 + cf : Σ2 + +data Q2 : Set where + a0 : Q2 + a1 : Q2 + ae : Q2 + b0 : Q2 + b1 : Q2 + be : Q2 + +-- a.*f + +aδ : Q2 → Σ2 → Q2 → Bool +aδ a0 ca a1 = true +aδ a0 _ _ = false +aδ a1 cf ae = true +aδ a1 _ a1 = true +aδ _ _ _ = false + +a-end : Q2 → Bool +a-end ae = true +a-end _ = false + +a-start : Q2 → Bool +a-start a0 = true +a-start _ = false + +nfa-a : NAutomaton Q2 Σ2 +nfa-a = record { Nδ = aδ ; Nend = a-end } + +nfa-a-exists : (Q2 → Bool) → Bool +nfa-a-exists p = p a0 \/ p a1 \/ p ae + +test-a1 : Bool +test-a1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ [] ) + +test-a2 = map reverse ( NtraceDepth nfa-a a-start (a0 ∷ a1 ∷ ae ∷ []) ( ca ∷ cf ∷ cf ∷ [] ) ) + +-- b.*f + +bδ : Q2 → Σ2 → Q2 → Bool +bδ ae cb b1 = true +bδ ae _ _ = false +bδ b1 cf be = true +bδ b1 _ b1 = true +bδ _ _ _ = false + +b-end : Q2 → Bool +b-end be = true +b-end _ = false + +b-start : Q2 → Bool +b-start ae = true +b-start _ = false + +nfa-b : NAutomaton Q2 Σ2 +nfa-b = record { Nδ = bδ ; Nend = b-end } + +nfa-b-exists : (Q2 → Bool) → Bool +nfa-b-exists p = p b0 \/ p b1 \/ p ae + +-- (a.*f)(b.*f) + +abδ : Q2 → Σ2 → Q2 → Bool +abδ x i y = aδ x i y \/ bδ x i y + +nfa-ab : NAutomaton Q2 Σ2 +nfa-ab = record { Nδ = abδ ; Nend = b-end } + +nfa-ab-exists : (Q2 → Bool) → Bool +nfa-ab-exists p = nfa-a-exists p \/ nfa-b-exists p + +test-ab1 : Bool +test-ab1 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] ) + +test-ab2 : Bool +test-ab2 = Naccept nfa-a nfa-a-exists a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) + +test-ab3 = map reverse ( NtraceDepth nfa-ab a-start (a0 ∷ a1 ∷ ae ∷ b0 ∷ b1 ∷ be ∷ []) ( ca ∷ cf ∷ ca ∷ cb ∷ cf ∷ [] )) + +test112 : Automaton (Q2 → Bool) Σ2 +test112 = subset-construction nfa-ab-exists nfa-ab + +test114 = Automaton.δ (subset-construction nfa-ab-exists nfa-ab) + +test113 : Bool +test113 = accept test112 a-start ( ca ∷ cf ∷ ca ∷ cb ∷ cb ∷ [] ) + diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/non-regular.agda --- a/automaton-in-agda/src/non-regular.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/non-regular.agda Sun Mar 12 22:49:59 2023 +0900 @@ -204,7 +204,7 @@ open import nat lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2) → isRegular inputnn1 s r ) -lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) {!!} (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) ) +lemmaNN r Rg = tann {TA.x TAnn} (TA.non-nil-y TAnn ) (TA.xyz=is TAnn) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyz TAnn) ) (tr-accept→ (automaton r) _ (astart r) (TA.trace-xyyz TAnn) ) where n : ℕ n = suc (finite (afin r)) @@ -237,56 +237,16 @@ length nntrace ∎ where open ≤-Reasoning nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04) nn06 = dup-in-list>n (afin r) nntrace nn05 + TAnn : TA (automaton r) (astart r) nn TAnn = pumping-lemma (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06) - count : In2 → List In2 → ℕ - count _ [] = 0 - count i0 (i0 ∷ s) = suc (count i0 s) - count i1 (i1 ∷ s) = suc (count i1 s) - count x (_ ∷ s) = count x s - nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t - nn11 {x} [] t = refl - nn11 {i0} (i0 ∷ s) t = cong suc ( nn11 s t ) - nn11 {i0} (i1 ∷ s) t = nn11 s t - nn11 {i1} (i0 ∷ s) t = nn11 s t - nn11 {i1} (i1 ∷ s) t = cong suc ( nn11 s t ) - nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s - nn10 s p = nn101 s (subst (λ k → k ≡ true) (sym (Rg s)) p ) where - nn101 : (s : List In2) → inputnn1 s ≡ true → count i0 s ≡ count i1 s - nn101 [] p = refl - nn101 (x ∷ s) p = {!!} - i1-i0? : List In2 → Bool - i1-i0? [] = false - i1-i0? (i1 ∷ []) = false - i1-i0? (i0 ∷ []) = false - i1-i0? (i1 ∷ i0 ∷ s) = true - i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1) - nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 ) - nn20 {s} {s0} {s1} p np = {!!} - mono-color : List In2 → Bool - mono-color [] = true - mono-color (i0 ∷ s) = mono-color0 s where - mono-color0 : List In2 → Bool - mono-color0 [] = true - mono-color0 (i1 ∷ s) = false - mono-color0 (i0 ∷ s) = mono-color0 s - mono-color (i1 ∷ s) = mono-color1 s where - mono-color1 : List In2 → Bool - mono-color1 [] = true - mono-color1 (i0 ∷ s) = false - mono-color1 (i1 ∷ s) = mono-color1 s - record Is10 (s : List In2) : Set where - field - s0 s1 : List In2 - is-10 : s ≡ s0 ++ i1 ∷ i0 ∷ s1 - not-mono : { s : List In2 } → ¬ (mono-color s ≡ true) → Is10 (s ++ s) - not-mono = {!!} - mono-count : { s : List In2 } → mono-color s ≡ true → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s) - mono-count = {!!} + tann : {x y z : List In2} → ¬ y ≡ [] → x ++ y ++ z ≡ nn → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z) ≡ true ) - tann {x} {y} {z} ny eq axyz axyyz with mono-color y - ... | true = {!!} - ... | false = {!!} + tann {x} {y} {z} ny eq axyz axyyz = ¬-bool (nn10 x y z (trans (Rg (x ++ y ++ z)) axyz ) ) (trans (Rg (x ++ y ++ y ++ z)) axyyz ) where + nn11 : (x y z : List In2 ) → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) + nn11 = ? + nn10 : (x y z : List In2 ) → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false + nn10 = ? diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/omega-automaton.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/prime.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/pushdown.agda --- a/automaton-in-agda/src/pushdown.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/pushdown.agda Sun Mar 12 22:49:59 2023 +0900 @@ -47,6 +47,11 @@ ... | ⟪ nq , none ⟫ = paccept nq T (SH ∷ ST) ... | ⟪ nq , push ns ⟫ = paccept nq T ( ns ∷ SH ∷ ST ) +-- +-- Automaton Q Σ +-- Automaton (Q → Bool ) Σ +-- Automaton (Q ∧ List Q) Σ + record PDA ( Q : Set ) ( Σ : Set ) ( Γ : Set ) : Set where field @@ -108,6 +113,7 @@ data States1 : Set where ss : States1 st : States1 + pn1 : PushDownAutomaton States1 In2 States1 pn1 = record { pδ = pδ diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/puzzle.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/regex.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/regex1.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/regular-concat.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/regular-language.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/regular-star.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/root2.agda diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/sbconst2.agda --- a/automaton-in-agda/src/sbconst2.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/sbconst2.agda Sun Mar 12 22:49:59 2023 +0900 @@ -14,7 +14,11 @@ open Bool -δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool) +-- exits : check subset of Q ( Q → Bool) is not empty +--- ( Q → Σ → Q → Bool ) transition of NFA +--- (Q → Bool) → Σ → (Q → Bool) generate transition of Automaton + +δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q ) subset-construction : { Q : Set } { Σ : Set } → @@ -53,3 +57,6 @@ → Naccept NFA exists states x ≡ true lemma2 [] states saccept = saccept lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept + + + diff -r 9324852d3a17 -r 6f3636fbc481 automaton-in-agda/src/temporal-logic.agda --- a/automaton-in-agda/src/temporal-logic.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/temporal-logic.agda Sun Mar 12 22:49:59 2023 +0900 @@ -1,6 +1,6 @@ -module temporal-logic where +open import Level renaming ( suc to succ ; zero to Zero ) +module temporal-logic {n : Level} where -open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Data.List open import Data.Maybe @@ -14,12 +14,41 @@ open Automaton - open import nat open import Data.Nat.Properties +open import Data.Unit + +-- Linear Time Temporal Logic (clock base, it has ○ (next)) + +record TL : Set (Level.suc n) where + field + at : ℕ → Set n + +open TL + +always : (P : Set n) → TL +always P = record { at = λ t → P } + +now : (P : Set n) → TL +now P = record { at = λ t → t ≡ 0 → P } + +record Sometime : Set n where + field + some : ℕ + +open Sometime + +sometimes : (P : Set n) → TL +sometimes P = record { at = λ t → (s : Sometime) → P } + +TLtest00 : {t : ℕ } (P : Set n) → at (always P) t → at (now P) t +TLtest00 P all refl = all + +TLtest01 : {t : ℕ } (P : Set n) → ¬ ( (t : ℕ ) → (at (sometimes (¬ P) ) t )) → at (always P) t +TLtest01 {t} P ns = ⊥-elim ( ns (λ s sm p → ? ) ) data LTTL ( V : Set ) : Set where - s : V → LTTL V + s : V → LTTL V -- proppsitional variable p is true on this time ○ : LTTL V → LTTL V □ : LTTL V → LTTL V ⋄ : LTTL V → LTTL V @@ -29,15 +58,50 @@ _t/\_ : LTTL V → LTTL V → LTTL V {-# TERMINATING #-} -M1 : { V : Set } → (ℕ → V → Bool) → ℕ → LTTL V → Set +M1 : { V : Set } → (σ : ℕ → V → Bool) → (i : ℕ ) → LTTL V → Set M1 σ i (s x) = σ i x ≡ true M1 σ i (○ x) = M1 σ (suc i) x M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1 σ j p M1 σ i (⋄ p) = ¬ ( M1 σ i (□ (t-not p) )) M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) ) M1 σ i (t-not p) = ¬ ( M1 σ i p ) -M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ -M1 σ i (p t/\ p₁) = M1 σ i p ∨ M1 σ i p₁ +M1 σ i (p t\/ p₁) = M1 σ i p ∨ M1 σ i p₁ +M1 σ i (p t/\ p₁) = M1 σ i p ∧ M1 σ i p₁ + +data Var : Set where + p : Var + q : Var + +test00 : ℕ → Var → Bool +test00 3 p = true +test00 _ _ = false + +test01 : M1 test00 3 ( s p ) +test01 = refl + +test02 : ¬ M1 test00 4 ( s p ) +test02 () + +-- We cannot write this +-- +-- LTTL? : { V : Set } → (σ : ℕ → V → Bool) → (i : ℕ ) → (e : LTTL V ) → Dec ( M1 σ i e ) +-- LTTL? {V} σ zero (s x) with σ zero x +-- ... | true = yes refl +-- ... | false = no ( λ () ) +-- LTTL? {V} σ zero (○ e) with LTTL? {V} σ 1 e +-- ... | yes y = yes y +-- ... | no n = no n +-- LTTL? {V} σ zero (□ e) = ? +-- LTTL? {V} σ zero (⋄ e) = ? +-- LTTL? {V} σ zero (e U e₁) = ? +-- LTTL? {V} σ zero (t-not e) = ? +-- LTTL? {V} σ zero (e t\/ e₁) = ? +-- LTTL? {V} σ zero (e t/\ e₁) = ? +-- LTTL? {V} σ (suc i) e = ? + +-- check validity or satisfiability of LTTL formula +-- generate Buchi or Muller automaton from LTTL formula +-- given some ω automaton, check it satisfies LTTL specification data LITL ( V : Set ) : Set where iv : V → LITL V @@ -57,10 +121,10 @@ ... | tri< a ¬b ¬c = MI σ (suc i) j a x ... | tri≈ ¬a b ¬c = ⊤ ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c) -MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i