Mercurial > hg > Members > kono > Proof > automaton

changeset 20:6032a2317ffa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add halt
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 29 Aug 2018 10:28:25 +0900
parents e5d67f06aca8
children ddf5f2f5fde8
files agda/turing.agda
diffstat 1 files changed, 116 insertions(+), 26 deletions(-) [+]
line wrap: on
line diff
--- a/agda/turing.agda	Mon Aug 27 17:17:00 2018 +0900
+++ b/agda/turing.agda	Wed Aug 29 10:28:25 2018 +0900
@@ -4,7 +4,7 @@
 open import Data.Nat hiding ( erase )
 open import Data.List
 open import Data.Maybe
-open import Data.Bool using ( Bool ; true ; false )
+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 )
@@ -16,10 +16,10 @@
    wnone   : Write  Σ
    --   erase write tnone
 
-data Move   (  Σ : Set  ) : Set  where
-   left   : Move  Σ
-   right  : Move  Σ
-   mnone  : Move  Σ
+data Move : Set  where
+   left   : Move  
+   right  : Move  
+   mnone  : Move  
 
 -- at tδ both stack is poped
 
@@ -33,7 +33,7 @@
 record Turing ( Q : Set ) ( Σ : Set  ) 
        : Set  where
     field
-        tδ : Q →  Σ → Q × ( Write  Σ ) × ( Move  Σ )
+        tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move 
         tstart : Q
         tend : Q → Bool
         tnone :  Σ
@@ -55,8 +55,22 @@
     ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
       where
         next = move  q  L  R 
+    {-# TERMINATING #-}
+    move0 : (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
+    move0  q L R with tend q
+    ... | true = ( q , L , R )
+    move0 q L [] | false = move0 q  L  ( tnone  ∷ [] ) 
+    move0 q [] R | false = move0 q  ( tnone  ∷ [] )  R 
+    move0 q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH  
+    ... | nq , write x , left  = move0 nq ( RH ∷ x  ∷ LT ) RT 
+    ... | nq , write x , right = move0 nq LT ( x  ∷ RH  ∷ RT ) 
+    ... | nq , write x , mnone = move0 nq ( x  ∷ LT ) (  RH ∷ RT ) 
+    ... | nq , wnone , left    = move0 nq ( RH  ∷ LH  ∷ LT ) RT  
+    ... | nq , wnone , right   = move0 nq  LT ( LH  ∷ RH  ∷ RT ) 
+    ... | nq , wnone , mnone   = move0 nq ( LH  ∷ LT ) (  RH ∷ RT )  
+    {-# TERMINATING #-}
     taccept : List  Σ → ( Q × List  Σ × List  Σ )
-    taccept L = move-loop tstart L []
+    taccept L = move0 tstart L []
 
 data CopyStates : Set where
    s1 : CopyStates
@@ -67,38 +81,114 @@
    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 )
+Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move 
+Copyδ s1 0  = (H    , wnone       , mnone )
+Copyδ s1 1  = (s2   , write 0 , right )
+Copyδ s2 0  = (s3   , write 0 , right )
+Copyδ s2 1  = (s2   , write 1 , right )
+Copyδ s3 0  = (s4   , write 1 , left )
+Copyδ s3 1  = (s3   , write 1 , right )
+Copyδ s4 0  = (s5   , write 0 , left )
+Copyδ s4 1  = (s4   , write 1 , left )
+Copyδ s5 0  = (s1   , write 1 , right )
+Copyδ s5 1  = (s5   , write 1 , left )
+Copyδ H  _  = (H    , wnone   , mnone )
+Copyδ _  (suc (suc _))      = (H    , wnone       , mnone )
 
-copyMachine : Turing CopyStates Bool
+copyMachine : Turing CopyStates ℕ
 copyMachine = record {
         tδ = Copyδ
      ;  tstart = s1
      ;  tend = tend
-     ;  tnone =  false
+     ;  tnone =  0
   } where
       tend : CopyStates →  Bool
       tend H = true
       tend _ = false
 
-test1 : CopyStates × ( List  Bool ) × ( List  Bool )
-test1 = Turing.taccept copyMachine  ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  )
+test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
+test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )
 
-test2 : ℕ  → CopyStates × ( List  Bool ) × ( List  Bool )
-test2 n  = loop n (Turing.tstart copyMachine) ( true  ∷ true  ∷ false  ∷ false  ∷  false ∷ []  ) []
+test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
+test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
   where
-        loop :  ℕ → CopyStates → ( List  Bool ) → ( List  Bool ) → CopyStates × ( List  Bool ) × ( List  Bool )
+        loop :  ℕ → CopyStates → ( List  ℕ ) → ( List  ℕ ) → CopyStates × ( List  ℕ ) × ( List  ℕ )
         loop zero q L R = ( q , L , R )
         loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) )  ( proj₂  ( proj₂ t1 ) )
           where
               t1 = Turing.move copyMachine q L R
+
+
+---
+--     utm char
+--         head         head  position
+--         send         state description end
+--         del          state delimitor
+--         sstart       state description start
+--         0
+--         1
+--     utm state description 
+--          state-num      ℕ    ( 0 accept, 1 reject )
+--          print          0 write 0, 1 write 1, 2 none
+--          move           0 left   , 1 none     2 write
+--     utm state
+--          head-value    : ℕ
+--          current-state : ℕ
+--          direction     : ℕ
+--          head-dir      : ℕ
+--
+--    --------------- head sstart ( state description ) * send input --------------
+--
+--    loop    search  sstart ( depend on head position )
+--            if state description end reject
+--            if state-num eq current state
+--                if accept end
+--                set current-state, direction and head-value by utm state description
+--                goto exec
+--            else goto loop
+--     exec   
+--           if head-dir = left
+--              search head towrards letf
+--           else
+--              search head towards  write
+--           put head-value
+--           move head ( considering state description )
+--           back to sstart
+--           goto loop
+
+
+
+postulate UTM : Turing ℕ ℕ 
+postulate encode-for-utm : Turing ℕ ℕ → List ℕ
+postulate enumerate-tm : Turing ℕ ℕ → ℕ
+postulate utm-simulate : ( tm : Turing ℕ ℕ ) → ( In : List ℕ ) →  Turing.taccept UTM  ((encode-for-utm tm) ++ In) ≡ Turing.taccept tm In
+
+record Halt : Set where
+    field
+       halt :  List ℕ → Bool
+       TM : Turing ℕ ℕ 
+
+open Halt
+
+record NotHalt ( H : Halt ) : Set where
+    field
+       nothalt :  List ℕ → Bool
+       NegTM : Turing ℕ ℕ 
+       neg :  (n : List ℕ ) → nothalt n  ≡ negate ( halt H n )
+
+open NotHalt
+
+-- neg : ( tm : Turing ℕ ℕ ) → ( h : Halt ) →  Bool
+-- neg tm h = negate ( halt h ( encode-for-utm tm ) )
+
+open import Data.Empty
+
+lemma1 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH ))  ≡ true  →  ⊥
+lemma1 h nh negneg=1 with halt h (encode-for-utm ( NegTM nh )) | nothalt nh (encode-for-utm ( NegTM nh )) | neg nh (encode-for-utm ( NegTM nh ))
+... | true | false  | refl = {!!}
+... | false | true  | refl = {!!}
+
+lemma2 : (H : Halt ) → (NH : NotHalt H ) → nothalt NH (encode-for-utm ( NegTM NH ))  ≡ false  →  ⊥
+lemma2 h nh negneg=1 with halt h (encode-for-utm ( NegTM nh )) | nothalt nh (encode-for-utm ( NegTM nh )) | neg nh (encode-for-utm ( NegTM nh ))
+... | true  | false  | refl = {!!}
+... | false | true  | refl = {!!}