Mercurial > hg > Members > kono > Proof > automaton
changeset 332:6f3636fbc481
fix
line wrap: on
line diff
--- 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<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p - - exists : ( Q → Bool ) → Bool - exists p = exists1 n (lt0 n) p - -という形で、 exists を記述することができる。 - -<a href="../agda/finiteSet.agda"> finiteSet.agda </a> - --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 を作成することができた。ここで、状態の有限性を使っていることを確認しよう。 - -<a href=" ../agda/sbconst2.agda"> subset construction </a> - ---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 @@ - -
--- 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 @@ <?xml version="1.0" encoding="UTF-8" standalone="no"?> <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> -<svg xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" xmlns="http://www.w3.org/2000/svg" version="1.1" viewBox="45 155 400 395" width="400" height="395"> +<svg xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" viewBox="45 155 400 395" width="400" height="395"> <defs> - <font-face font-family="Helvetica Neue" font-size="14" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400"> - <font-face-src> - <font-face-name name="HelveticaNeue"/> - </font-face-src> - </font-face> <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"> <g> <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> @@ -17,14 +12,8 @@ <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> </g> </marker> - <font-face font-family="Hiragino Sans" font-size="14" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300"> - <font-face-src> - <font-face-name name="HiraginoSans-W3"/> - </font-face-src> - </font-face> </defs> - <metadata> Produced by OmniGraffle 7.18\n2020-12-23 01:04:40 +0000</metadata> - <g id="Canvas_1" stroke-opacity="1" fill-opacity="1" stroke-dasharray="none" fill="none" stroke="none"> + <g id="Canvas_1" fill="none" stroke-opacity="1" stroke="none" stroke-dasharray="none" fill-opacity="1"> <title>Canvas 1</title> <rect fill="white" x="45" y="155" width="400" height="395"/> <g id="Canvas_1_Layer_1"> @@ -33,7 +22,7 @@ <circle cx="97.23" cy="335" r="42.0000671118797" fill="white"/> <circle cx="97.23" cy="335" r="42.0000671118797" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> <text transform="translate(68.63 326.804)" fill="black"> - <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="5.9060004" y="13">1*(01*)*</tspan> + <tspan font-family="Helvetica Neue" font-size="14" fill="black" x="8.37" y="13">1*(01)*</tspan> </text> </g> <g id="Graphic_3"/> @@ -41,7 +30,7 @@ <circle cx="202" cy="270" r="42.0000671118797" fill="white"/> <circle cx="202" cy="270" r="42.0000671118797" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> <text transform="translate(173.4 261.804)" fill="black"> - <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="19.661" y="13">fail</tspan> + <tspan font-family="Helvetica Neue" font-size="14" fill="black" x="19.661" y="13">fail</tspan> </text> </g> <g id="Line_6"> @@ -54,24 +43,24 @@ <circle cx="315" cy="327" r="42.0000671118797" fill="white"/> <circle cx="315" cy="327" r="42.0000671118797" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> <text transform="translate(286.4 318.804)" fill="black"> - <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="8.37" y="13">1(01*)*</tspan> + <tspan font-family="Helvetica Neue" font-size="14" fill="black" x="10.834" y="13">1(01)*</tspan> </text> </g> <g id="Graphic_11"> <circle cx="315" cy="464" r="42.0000671118797" fill="white"/> <circle cx="315" cy="464" r="42.0000671118797" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> <text transform="translate(286.4 455.804)" fill="black"> - <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="12.262" y="13">(01*)*</tspan> + <tspan font-family="Helvetica Neue" font-size="14" fill="black" x="14.726" y="13">(01)*</tspan> </text> </g> <g id="Graphic_14"> <text transform="translate(199.115 343)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">０</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="0" y="12">０</tspan> </text> </g> <g id="Graphic_15"> <text transform="translate(125.032 415)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="15987212e-20" y="12">1</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="15987212e-20" y="12">1</tspan> </text> </g> <g id="Line_17"> @@ -79,7 +68,7 @@ </g> <g id="Graphic_18"> <text transform="translate(289 217)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">０</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="0" y="12">０</tspan> </text> </g> <g id="Line_20"> @@ -87,7 +76,7 @@ </g> <g id="Graphic_21"> <text transform="translate(359 385)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="15987212e-20" y="12">1</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="15987212e-20" y="12">1</tspan> </text> </g> <g id="Line_25"> @@ -95,7 +84,7 @@ </g> <g id="Graphic_26"> <text transform="translate(283 393)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">０</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="0" y="12">０</tspan> </text> </g> <g id="Graphic_27"> @@ -109,14 +98,17 @@ </g> <g id="Graphic_30"> <text transform="translate(430.198 399)" fill="black"> - <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="15987212e-20" y="12">1</tspan> + <tspan font-family="Hiragino Sans" font-size="14" fill="black" x="15987212e-20" y="12">1</tspan> </text> </g> <g id="Graphic_31"> <text transform="translate(162.666 528)" fill="black"> - <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="1.946" y="13">derivating method </tspan> + <tspan font-family="Helvetica Neue" font-size="14" fill="black" x="1.946" y="13">derivating method </tspan> </text> </g> + <g id="Graphic_32"> + <circle cx="97.23" cy="335" r="36.0000575244682" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> </g> </g> </svg>
--- a/a07/lecture.ind Wed Dec 07 14:51:25 2022 +0900 +++ b/a07/lecture.ind Sun Mar 12 22:49:59 2023 +0900 @@ -6,7 +6,9 @@ Q → Bool -と表すことができる。つまり、その部分集合に含まれるかどうかを表す関数が部分集合そのものになる。これを、Bool +と表すことができる。つまり、その部分集合に含まれるかどうかを表す関数が部分集合そのものになる。 + +これを、Bool <sup>Q</sup> と書くことがある。Bool は二つの要素がある。状態数4からBoolへの関数は、2 <sup>4</sup>個ある。集合のべき乗をこのようにして定義することができる。 @@ -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 (有限性または部分集合の決定性)を使っていることに注意しよう。 + +<a href=" ../agda/sbconst2.agda"> subset construction </a> + + ---問題7.1 以下の非決定性オートマトンを決定性オートマトンへ変換せよ <a href="../exercise/003.html"> 例題 </a> <!--- Exercise 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 を実行することになる。 + +
--- 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 を停止することが分かっているアルゴリズムで決めれば良い。
--- /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 ) Σ + + +
--- 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 ) + +
--- 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 - <to<s : {x y : ℕ } → x < y → x < suc y <to<s {zero} {suc y} (s≤s lt) = s≤s z≤n <to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) @@ -285,7 +282,7 @@ y-x<y : {x y : ℕ } → 0 < x → 0 < y → y - x < y y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y) -... | tri< a ¬b ¬c = +-cancelʳ-< {x} (y - x) y ( begin +... | tri< a ¬b ¬c = +-cancelʳ-< x (y - x) y ( begin suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩ suc y ≡⟨ +-comm 1 _ ⟩ y + suc 0 ≤⟨ +-mono-≤ ≤-refl 0<x ⟩ @@ -427,6 +424,31 @@ m*1=m {zero} = refl m*1=m {suc m} = cong suc m*1=m +*-cancel-left : {x y z : ℕ } → x > 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
--- 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 -
--- 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 ∷ [] ) +
--- 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 = ?
--- 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δ
--- 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 + + +
--- 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<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p)) -MI σ i j lt (i-not p) = ¬ ( MI σ i j lt p ) -MI σ i j lt (p i\/ p₁) = MI σ i j lt p ∧ MI σ i j lt p₁ -MI σ i j lt (p i/\ p₁) = MI σ i j lt p ∨ MI σ i j lt p₁ +MI σ i j lt (P & Q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k P ∧ MI σ k j k<j P)) +MI σ i j lt (i-not P) = ¬ ( MI σ i j lt P ) +MI σ i j lt (P i\/ Q) = MI σ i j lt P ∧ MI σ i j lt Q +MI σ i j lt (P i/\ Q) = MI σ i j lt P ∨ MI σ i j lt Q data QBool ( V : Set ) : Set where qb : Bool → QBool V @@ -76,19 +140,19 @@ SQ1 {V} dec (qv x) v t with dec x v ... | yes _ = qb t ... | no _ = qv x -SQ1 {V} dec (exists x p) v t = SQ1 dec (SQ1 dec p x true) v t b\/ SQ1 dec (SQ1 dec p x false) v t -SQ1 {V} dec (b-not p) v t = b-not (SQ1 dec p v t ) -SQ1 {V} dec (p b\/ p₁) v t = SQ1 dec p v t b\/ SQ1 dec p₁ v t -SQ1 {V} dec (p b/\ p₁) v t = SQ1 dec p v t b/\ SQ1 dec p₁ v t +SQ1 {V} dec (exists x P) v t = SQ1 dec (SQ1 dec P x true) v t b\/ SQ1 dec (SQ1 dec P x false) v t +SQ1 {V} dec (b-not P) v t = b-not (SQ1 dec P v t ) +SQ1 {V} dec (P b\/ Q) v t = SQ1 dec P v t b\/ SQ1 dec Q v t +SQ1 {V} dec (P b/\ Q) v t = SQ1 dec P v t b/\ SQ1 dec Q v t {-# TERMINATING #-} MQ : { V : Set } → (V → Bool) → ((x y : V) → Dec ( x ≡ y)) → QBool V → Bool MQ {V} val dec (qb x) = x MQ {V} val dec (qv x) = val x -MQ {V} val dec (exists x p) = MQ val dec ( SQ1 dec p x true b\/ SQ1 dec p x false ) -MQ {V} val dec (b-not p) = not ( MQ val dec p ) -MQ {V} val dec (p b\/ p₁) = MQ val dec p \/ MQ val dec p₁ -MQ {V} val dec (p b/\ p₁) = MQ val dec p /\ MQ val dec p₁ +MQ {V} val dec (exists x P) = MQ val dec ( SQ1 dec P x true b\/ SQ1 dec P x false ) +MQ {V} val dec (b-not P) = not ( MQ val dec P ) +MQ {V} val dec (P b\/ Q) = MQ val dec P \/ MQ val dec Q +MQ {V} val dec (P b/\ Q) = MQ val dec P /\ MQ val dec Q data QPTL ( V : Set ) : Set where qt : Bool → QPTL V @@ -112,23 +176,23 @@ SQP1 {V} dec (qs x) v t with dec x v ... | yes _ = qt t ... | no _ = qs x -SQP1 {V} dec (q-exists x p) v t = SQP1 dec (SQP1 dec p x true) v t q\/ SQP1 dec (SQP1 dec p x false) v t -SQP1 {V} dec (q○ p) v t = q○ p -SQP1 {V} dec (q□ p) v t = SQP1 {V} dec p v t q/\ q□ p -SQP1 {V} dec (q⋄ p) v t = q-not ( SQP1 dec (q□ (q-not p)) v t) -SQP1 {V} dec (q-not p) v t = q-not ( SQP1 dec p v t ) -SQP1 {V} dec (p q\/ p₁) v t = SQP1 {V} dec p v t q\/ SQP1 {V} dec p₁ v t -SQP1 {V} dec (p q/\ p₁) v t = SQP1 {V} dec p v t q/\ SQP1 {V} dec p₁ v t +SQP1 {V} dec (q-exists x P) v t = SQP1 dec (SQP1 dec P x true) v t q\/ SQP1 dec (SQP1 dec P x false) v t +SQP1 {V} dec (q○ P) v t = q○ P +SQP1 {V} dec (q□ P) v t = SQP1 {V} dec P v t q/\ q□ P +SQP1 {V} dec (q⋄ P) v t = q-not ( SQP1 dec (q□ (q-not P)) v t) +SQP1 {V} dec (q-not P) v t = q-not ( SQP1 dec P v t ) +SQP1 {V} dec (P q\/ Q) v t = SQP1 {V} dec P v t q\/ SQP1 {V} dec Q v t +SQP1 {V} dec (P q/\ Q) v t = SQP1 {V} dec P v t q/\ SQP1 {V} dec Q v t {-# TERMINATING #-} MQPTL : { V : Set } → (ℕ → V → Bool) → ℕ → ((x y : V) → Dec ( x ≡ y)) → QPTL V → Set MQPTL σ i dec (qt x) = x ≡ true MQPTL σ i dec (qs x) = σ i x ≡ true MQPTL σ i dec (q○ x) = MQPTL σ (suc i) dec x -MQPTL σ i dec (q□ p) = (j : ℕ) → i ≤ j → MQPTL σ j dec p -MQPTL σ i dec (q⋄ p) = ¬ ( MQPTL σ i dec (q□ (q-not p) )) -MQPTL σ i dec (q-not p) = ¬ ( MQPTL σ i dec p ) -MQPTL σ i dec (q-exists x p) = MQPTL σ i dec ( SQP1 dec p x true q\/ (SQP1 dec p x false)) -MQPTL σ i dec (p q\/ p₁) = MQPTL σ i dec p ∧ MQPTL σ i dec p₁ -MQPTL σ i dec (p q/\ p₁) = MQPTL σ i dec p ∨ MQPTL σ i dec p₁ +MQPTL σ i dec (q□ P) = (j : ℕ) → i ≤ j → MQPTL σ j dec P +MQPTL σ i dec (q⋄ P) = ¬ ( MQPTL σ i dec (q□ (q-not P) )) +MQPTL σ i dec (q-not P) = ¬ ( MQPTL σ i dec P ) +MQPTL σ i dec (q-exists x P) = MQPTL σ i dec ( SQP1 dec P x true q\/ (SQP1 dec P x false)) +MQPTL σ i dec (P q\/ Q) = MQPTL σ i dec P ∧ MQPTL σ i dec Q +MQPTL σ i dec (P q/\ Q) = MQPTL σ i dec P ∨ MQPTL σ i dec Q
--- a/automaton-in-agda/src/turing.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/turing.agda Sun Mar 12 22:49:59 2023 +0900 @@ -77,6 +77,11 @@ taccept L = move0 tend tnone tδ tstart L [] open import automaton + +-- ATuring : {Σ : Set } → Automaton (List Σ) Σ +-- ATuring = record { δ = {!!} ; aend = {!!} } + +open import automaton open Automaton {-# TERMINATING #-}
--- a/automaton-in-agda/src/utm.agda Wed Dec 07 14:51:25 2022 +0900 +++ b/automaton-in-agda/src/utm.agda Sun Mar 12 22:49:59 2023 +0900 @@ -203,7 +203,7 @@ Copyδ-encode : List utmΣ Copyδ-encode = ０ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ ０ ∷ -- s1 0 = H , wnone , mnone - * ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ -- s1 1 = s2 , write 0 , right + * ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ -- s0 1 = s2 , write 0 , right * ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ -- s2 0 = s3 , write 0 , right * ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ １ ∷ -- s2 1 = s2 , write 1 , right * ∷ ０ ∷ １ ∷ １ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ １ ∷ ０ ∷ ０ ∷ -- s3 0 = s4 , write 1 , left @@ -244,7 +244,7 @@ ... | nq , nL , nR | reads = loop n nq nL nR ... | nq , nL , nR | _ = loop (suc n) nq nL nR -t1 = utm-test2 20 short-input +t1 = utm-test2 3 short-input t : (n : ℕ) → utmStates × ( List utmΣ ) × ( List utmΣ ) -- t n = utm-test2 n input+Copyδ