Mercurial > hg > Members > kono > Proof > automaton
changeset 18:6ec8e933ab43
turing wrote but not yet worked
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 27 Aug 2018 15:05:41 +0900 |
| parents | 08b589172493 |
| children | e5d67f06aca8 |
| files | agda/turing.agda |
| diffstat | 1 files changed, 67 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/turing.agda Sun Aug 26 17:48:26 2018 +0900 +++ b/agda/turing.agda Mon Aug 27 15:05:41 2018 +0900 @@ -1,7 +1,7 @@ module turing where open import Level renaming ( suc to succ ; zero to Zero ) -open import Data.Nat +open import Data.Nat hiding ( erase ) open import Data.List open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ) @@ -11,38 +11,81 @@ open import Data.Product -data PushDown ( Σ : Set ) : Set where - pop : PushDown Σ - push : Σ → PushDown Σ +data Write ( Σ : Set ) : Set where + write : Σ → Write Σ + wnone : Write Σ + -- erase write tnone + +data Move ( Σ : Set ) : Set where + left : Move Σ + right : Move Σ + mnone : Move Σ + +-- at tδ both stack is poped + +-- write S push S , push SR +-- erase push SL , push tone +-- none push SL , push SR +-- left push SR , pop +-- right pop , push SL record Turing ( Q : Set ) ( Σ : Set ) : Set where field - tδ : Q → Σ → Q × ( PushDown Σ ) × ( PushDown Σ ) + tδ : Q → Σ → Q × ( Write Σ ) × ( Move Σ ) tstart : Q tend : Q → Bool - tz0 : Σ - tmoves : Q → List Σ → ( Q × List Σ × List Σ ) - tmoves q L = move q L [ pz0 ] + tnone : Σ + {-# TERMINATING #-} + taccept : List Σ → ( Q × List Σ × List Σ ) + taccept L = move tstart L [] where - move : Q → ( List Σ ) → ( List Σ ) → ( Q × List Σ × 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 ) - taccept : List Σ → Bool - taccept 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 ) + move : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) + move q L R with tend q + ... | true = ( q , L , R ) + move q L [] | false = move q L ( tnone ∷ [] ) + move q [] R | false = move q ( tnone ∷ [] ) R + move q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH + ... | nq , write x , left = move nq ( RH ∷ x ∷ LT ) RT + ... | nq , write x , right = move nq L ( x ∷ RH ∷ RT ) + ... | nq , write x , mnone = move nq ( x ∷ LT ) ( RH ∷ RT ) + ... | nq , wnone , left = move nq ( LT ) ( LH ∷ RH ∷ RT ) + ... | nq , wnone , right = move nq ( RH ∷ LH ∷ LT ) ( RT ) + ... | nq , wnone , mnone = move nq ( LH ∷ LT ) ( RH ∷ RT ) + +data CopyStates : Set where + s1 : CopyStates + s2 : CopyStates + s3 : CopyStates + s4 : CopyStates + s5 : CopyStates + H : CopyStates +Copyδ : CopyStates → Bool → CopyStates × ( Write Bool ) × ( Move Bool ) +Copyδ s1 false = (H , wnone , mnone ) +Copyδ s1 true = (s2 , write false , right ) +Copyδ s2 false = (s3 , write false , right ) +Copyδ s2 true = (s2 , write true , right ) +Copyδ s3 false = (s4 , write true , left ) +Copyδ s3 true = (s3 , write true , right ) +Copyδ s4 false = (s5 , write false , left ) +Copyδ s4 true = (s4 , write true , left ) +Copyδ s5 false = (s1 , write true , right ) +Copyδ s5 true = (s5 , write true , left ) +Copyδ H _ = (H , wnone , mnone ) +copyMachine : Turing CopyStates Bool +copyMachine = record { + tδ = Copyδ + ; tstart = s1 + ; tend = tend + ; tnone = false + } where + tend : CopyStates → Bool + tend H = true + tend _ = false +test1 : CopyStates × ( List Bool ) × ( List Bool ) +test1 = Turing.taccept copyMachine ( true ∷ true ∷ false ∷ false ∷ false ∷ [] )