Mercurial > hg > Members > kono > Proof > automaton
changeset 407:c7ad8d2dc157
safe halt.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Nov 2023 18:04:55 +0900 |
| parents | a60132983557 |
| children | 3d0aa205edf9 |
| files | automaton-in-agda/src/finiteFunc.agda automaton-in-agda/src/halt.agda automaton-in-agda/src/turing.agda automaton-in-agda/src/utm.agda |
| diffstat | 4 files changed, 214 insertions(+), 79 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/automaton-in-agda/src/finiteFunc.agda Thu Nov 09 18:04:55 2023 +0900 @@ -0,0 +1,75 @@ +{-# OPTIONS #-} + +module finiteFunc where + +open import Data.Nat hiding ( _≟_ ) +open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred ) +open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-refl ; <-irrelevant ) renaming ( <-cmp to <-fcmp ) +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.Definitions +open import Relation.Binary.PropositionalEquality +open import logic +open import nat +open import finiteSet +open import finiteSetUtil +open import fin +open import Data.Nat.Properties as NP hiding ( _≟_ ) + +open import Axiom.Extensionality.Propositional +open import Level hiding (suc ; zero) + +open import Level renaming ( suc to Suc ; zero to Zero) +postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n) +open import Data.Vec hiding ( map ; length ) +import Data.Product + + +-- we cannot simply use f ≡ g for f : Q → A in Bijection of List Bool and (finite → Bool ) +-- what we can say is theres a fuction which elementwise equal + +F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x +F2L-iso {Q} fin x = f2l m a<sa x where + m = FiniteSet.finite fin + f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L fin n<m (λ q q<n → List2Func fin n<m x q ) ≡ x + f2l zero (s≤s z≤n) [] = refl + f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3f where + lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1 + lemma1 refl refl = refl + lemma2 : List2Func fin (s≤s n<m) (h ∷ t) (FiniteSet.Q←F fin (fromℕ< n<m)) ≡ h + lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ< n<m)) ≟ fromℕ< n<m + lemma2 | yes p = refl + lemma2 | no ¬p = ⊥-elim ( ¬p (FiniteSet.finiso← fin _) ) + lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func fin (s≤s n<m) (h ∷ t) q ≡ List2Func fin (NP.<-trans n<m a<sa) t q + lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ< n<m + lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ< n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where + lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n + lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s z≤n + lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl) + lemma4 q _ | no ¬p = refl + lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t + lemma3f = begin + F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) + ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) + (f-extensionality ( λ q → + (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩ + F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) + ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ + t + ∎ where + open ≡-Reasoning + +open Bijection + +fin→ : {A : Set} → FiniteSet A → FiniteSet (A → Bool ) +fin→ {A} fin = iso-fin fin2List iso where + a = FiniteSet.finite fin + iso : Bijection (Vec Bool a ) (A → Bool) + fun← iso x = F2L fin a<sa ( λ q _ → x q ) + fun→ iso x = List2Func fin a<sa x + fiso← iso x = F2L-iso fin x + fiso→ iso f = lemma where + lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f + lemma = f-extensionality ( λ q → L2F-iso fin f q ) + +
--- a/automaton-in-agda/src/halt.agda Wed Nov 08 21:35:54 2023 +0900 +++ b/automaton-in-agda/src/halt.agda Thu Nov 09 18:04:55 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical-compatible #-} +{-# OPTIONS --cubical-compatible --safe #-} module halt where @@ -16,36 +16,35 @@ open import logic -record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where +record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where field - fun← : S → R - fun→ : R → S - fiso← : (x : R) → fun← ( fun→ x ) ≡ x --- normal bijection required below, but we don't need this to show the inconsistency --- fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x + ffun← : S → R → Bool + ffun→ : (R → Bool) → S + ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x -injection' : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) -injection' R S f = (x y : R) → f x ≡ f y → x ≡ y + -- ffun← ( ffun→ f ) ≡ f , if we have functional extensionality but it is unsafe -open HBijection +open FBijection + +fdiag : {S : Set } (b : FBijection S S) → S → Bool +fdiag b n = not (ffun← b n n) -diag : {S : Set } (b : HBijection ( S → Bool ) S) → S → Bool -diag b n = not (fun← b n n) +-- +-- ffun→ b (fiag b) is some S +-- ffun← b (ffun→ b (fdiag b) ) is a function S → Bool +-- is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x ) +-- but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction -diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S -diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where - diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n ) - diagn1 n dn = ¬t=f (diag b n ) ( begin - not (diag b n) - ≡⟨⟩ - not (not (fun← b n n)) - ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩ - not (fun← b (fun→ b (diag b)) n) - ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩ - not (fun← b n n) - ≡⟨⟩ - diag b n - ∎ ) where open ≡-Reasoning +fdiagonal : { S : Set } → ¬ FBijection S S +fdiagonal {S} b = ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where + ff1 : S + ff1 = ffun→ b (fdiag b) + ff2 : S → Bool + ff2 = ffun← b (ffun→ b (fdiag b) ) + ff3 : (x : S) → ffun← b (ffun→ b (fdiag b) ) x ≡ fdiag b x + ff3 x = ffiso← b (fdiag b) x + ff4 : not ( ffun← b (ffun→ b (fdiag b) ) (ffun→ b (fdiag b))) ≡ fdiag b (ffun→ b (fdiag b)) + ff4 = refl -- definition of fdiag b record TM : Set where field @@ -63,9 +62,6 @@ open _∧_ -open import Axiom.Extensionality.Propositional -postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n - record Halt : Set where field halt : (t : TM ) → (x : List Bool ) → Bool @@ -74,11 +70,11 @@ open Halt -TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool) -TNL halt utm = record { - fun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x) - ; fun→ = λ h → encode utm record { tm = h1 h } - ; fiso← = λ h → f-extensionality (λ y → TN1 h y ) +TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool) +TNLF halt utm = record { + ffun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x) + ; ffun→ = λ h → encode utm record { tm = h1 h } + ; ffiso← = λ h y → TN1 h y } where open ≡-Reasoning h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool @@ -111,10 +107,9 @@ tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ h1 h y ≡⟨ h-nothing h y eq1 ⟩ nothing ∎ - -- the rest of bijection means encoding is unique + -- the rest of bijection means encoding is unique, but we don't need it -- fiso→ : (y : List Bool ) → encode utm record { tm = λ x → h1 (λ tm → Halt.halt halt (UTM.utm utm) tm ) x } ≡ y -TNL1 : UTM → ¬ Halt -TNL1 utm halt = diagonal ( TNL halt utm ) +TNLF1 : UTM → ¬ Halt +TNLF1 utm halt = fdiagonal ( TNLF halt utm ) -
--- a/automaton-in-agda/src/turing.agda Wed Nov 08 21:35:54 2023 +0900 +++ b/automaton-in-agda/src/turing.agda Thu Nov 09 18:04:55 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +-- {-# OPTIONS --allow-unsolved-metas #-} module turing where open import Level renaming ( suc to succ ; zero to Zero ) @@ -31,10 +32,7 @@ -- left push SR , pop -- right pop , push SL -{-# TERMINATING #-} move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) -move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q L ( tnone ∷ [] ) -move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q ( tnone ∷ [] ) R move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT ) ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) ) @@ -42,29 +40,67 @@ ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT ) ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) ) ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) ) -{-# TERMINATING #-} -move-loop : {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } +move {Q} {Σ} {tnone} {tδ} q ( LH ∷ LT ) [] with tδ q LH +... | nq , write x , left = ( nq , ( tnone ∷ x ∷ LT ) , [] ) +... | nq , write x , right = ( nq , LT , ( x ∷ tnone ∷ [] ) ) +... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( tnone ∷ [] ) ) +... | nq , wnone , left = ( nq , ( tnone ∷ LH ∷ LT ) , [] ) +... | nq , wnone , right = ( nq , LT , ( LH ∷ tnone ∷ [] ) ) +... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( tnone ∷ [] ) ) +move {Q} {Σ} {tnone} {tδ} q [] ( RH ∷ RT ) with tδ q tnone +... | nq , write x , left = ( nq , ( RH ∷ x ∷ [] ) , RT ) +... | nq , write x , right = ( nq , [] , ( x ∷ RH ∷ RT ) ) +... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( RH ∷ RT ) ) +... | nq , wnone , left = ( nq , ( RH ∷ tnone ∷ [] ) , RT ) +... | nq , wnone , right = ( nq , [] , ( tnone ∷ RH ∷ RT ) ) +... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( RH ∷ RT ) ) +move {Q} {Σ} {tnone} {tδ} q [] [] with tδ q tnone +... | nq , write x , left = ( nq , ( tnone ∷ x ∷ [] ) , [] ) +... | nq , write x , right = ( nq , [] , ( x ∷ tnone ∷ [] ) ) +... | nq , write x , mnone = ( nq , ( x ∷ [] ) , ( tnone ∷ [] ) ) +... | nq , wnone , left = ( nq , ( tnone ∷ tnone ∷ [] ) , [] ) +... | nq , wnone , right = ( nq , [] , ( tnone ∷ tnone ∷ [] ) ) +... | nq , wnone , mnone = ( nq , ( tnone ∷ [] ) , ( tnone ∷ [] ) ) + +move-loop : (i : ℕ) {Q Σ : Set } → {tend : Q → Bool} → { tnone : Σ} → {tδ : Q → Σ → Q × ( Write Σ ) × Move } → (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) -move-loop {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q +move-loop zero {Q} {Σ} {tend} {tnone} {tδ} q L R = ( q , L , R ) +move-loop (suc i) {Q} {Σ} {tend} {tnone} {tδ} q L R with tend q ... | true = ( q , L , R ) -... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) +... | flase = move-loop i {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) ) where next = move {Q} {Σ} {tnone} {tδ} q L R -{-# TERMINATING #-} move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q → Σ → Q × ( Write Σ ) × Move) (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) -move0 tend tnone tδ q L R with tend q -... | true = ( q , L , R ) -move0 tend tnone tδ q L [] | false = move0 tend tnone tδ q L ( tnone ∷ [] ) -move0 tend tnone tδ q [] R | false = move0 tend tnone tδ q ( tnone ∷ [] ) R -move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH -... | nq , write x , left = move0 tend tnone tδ nq ( RH ∷ x ∷ LT ) RT -... | nq , write x , right = move0 tend tnone tδ nq LT ( x ∷ RH ∷ RT ) -... | nq , write x , mnone = move0 tend tnone tδ nq ( x ∷ LT ) ( RH ∷ RT ) -... | nq , wnone , left = move0 tend tnone tδ nq ( RH ∷ LH ∷ LT ) RT -... | nq , wnone , right = move0 tend tnone tδ nq LT ( LH ∷ RH ∷ RT ) -... | nq , wnone , mnone = move0 tend tnone tδ nq ( LH ∷ LT ) ( RH ∷ RT ) +move0 tend tnone tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH +... | nq , write x , left = nq , ( RH ∷ x ∷ LT ) , RT +... | nq , write x , right = nq , LT , ( x ∷ RH ∷ RT ) +... | nq , write x , mnone = nq , ( x ∷ LT ) , ( RH ∷ RT ) +... | nq , wnone , left = nq , ( RH ∷ LH ∷ LT ) , RT +... | nq , wnone , right = nq , LT , ( LH ∷ RH ∷ RT ) +... | nq , wnone , mnone = ( q , ( LH ∷ LT ) , ( RH ∷ RT ) ) +move0 tend tnone tδ q ( LH ∷ LT ) [] with tδ q LH +... | nq , write x , left = nq , ( tnone ∷ x ∷ LT ) , [] +... | nq , write x , right = nq , LT , ( x ∷ tnone ∷ [] ) +... | nq , write x , mnone = nq , ( x ∷ LT ) , ( tnone ∷ [] ) +... | nq , wnone , left = nq , ( tnone ∷ LH ∷ LT ) , [] +... | nq , wnone , right = nq , LT , ( LH ∷ tnone ∷ [] ) +... | nq , wnone , mnone = nq , ( LH ∷ LT ) , ( tnone ∷ [] ) +move0 tend tnone tδ q [] ( RH ∷ RT ) with tδ q tnone +... | nq , write x , left = nq , ( RH ∷ x ∷ [] ) , RT +... | nq , write x , right = nq , [] , ( x ∷ RH ∷ RT ) +... | nq , write x , mnone = nq , ( x ∷ [] ) , ( RH ∷ RT ) +... | nq , wnone , left = nq , ( RH ∷ tnone ∷ [] ) , RT +... | nq , wnone , right = nq , [] , ( tnone ∷ RH ∷ RT ) +... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( RH ∷ RT ) +move0 tend tnone tδ q [] [] with tδ q tnone +... | nq , write x , left = nq , ( tnone ∷ x ∷ [] ) , [] +... | nq , write x , right = nq , [] , ( x ∷ tnone ∷ [] ) +... | nq , write x , mnone = nq , ( x ∷ [] ) , ( tnone ∷ [] ) +... | nq , wnone , left = nq , ( tnone ∷ tnone ∷ [] ) , [] +... | nq , wnone , right = nq , [] , ( tnone ∷ tnone ∷ [] ) +... | nq , wnone , mnone = nq , ( tnone ∷ [] ) , ( tnone ∷ [] ) record Turing ( Q : Set ) ( Σ : Set ) : Set where @@ -73,8 +109,14 @@ tstart : Q tend : Q → Bool tnone : Σ - taccept : List Σ → ( Q × List Σ × List Σ ) - taccept L = move0 tend tnone tδ tstart L [] + taccept : (i : ℕ ) → List Σ → ( Q × List Σ × List Σ ) + taccept i L = tloop i tstart [] [] where + tloop : (i : ℕ) (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ ) + tloop zero q L R = ( q , L , R ) + tloop (suc i) q L R with tend q + ... | true = ( q , L , R ) + ... | false with move0 tend tnone tδ q L R + ... | nq , L , R = tloop i nq L R open import automaton @@ -84,20 +126,36 @@ open import automaton open Automaton -{-# TERMINATING #-} -move1 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (δ : Q → Σ → Q ) (tδ : Q → Σ → Write Σ × Move) +move1 : {Q Σ : Set } (tnone : Σ ) (δ : Q → Σ → Q ) (tδ : Q → Σ → Write Σ × Move) (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ -move1 tend tnone δ tδ q L R with tend q -... | true = ( q , L , R ) -move1 tend tnone δ tδ q L [] | false = move1 tend tnone δ tδ q L ( tnone ∷ [] ) -move1 tend tnone δ tδ q [] R | false = move1 tend tnone δ tδ q ( tnone ∷ [] ) R -move1 tend tnone δ tδ q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ (δ q LH) LH -... | write x , left = move1 tend tnone δ tδ (δ q LH) ( RH ∷ x ∷ LT ) RT -... | write x , right = move1 tend tnone δ tδ (δ q LH) LT ( x ∷ RH ∷ RT ) -... | write x , mnone = move1 tend tnone δ tδ (δ q LH) ( x ∷ LT ) ( RH ∷ RT ) -... | wnone , left = move1 tend tnone δ tδ (δ q LH) ( RH ∷ LH ∷ LT ) RT -... | wnone , right = move1 tend tnone δ tδ (δ q LH) LT ( LH ∷ RH ∷ RT ) -... | wnone , mnone = move1 tend tnone δ tδ (δ q LH) ( LH ∷ LT ) ( RH ∷ RT ) +move1 tnone δ tδ q ( LH ∷ LT ) ( RH ∷ RT ) with tδ (δ q LH) LH +... | write x , left = (δ q LH) , ( RH ∷ x ∷ LT ) , RT +... | write x , right = (δ q LH) , LT , ( x ∷ RH ∷ RT ) +... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( RH ∷ RT ) +... | wnone , left = (δ q LH) , ( RH ∷ LH ∷ LT ) , RT +... | wnone , right = (δ q LH) , LT , ( LH ∷ RH ∷ RT ) +... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( RH ∷ RT ) +move1 tnone δ tδ q ( LH ∷ LT ) [] with tδ (δ q LH) LH +... | write x , left = (δ q LH) , ( tnone ∷ x ∷ LT ) , [] +... | write x , right = (δ q LH) , LT , ( x ∷ tnone ∷ [] ) +... | write x , mnone = (δ q LH) , ( x ∷ LT ) , ( tnone ∷ [] ) +... | wnone , left = (δ q LH) , ( tnone ∷ LH ∷ LT ) , [] +... | wnone , right = (δ q LH) , LT , ( LH ∷ tnone ∷ [] ) +... | wnone , mnone = (δ q LH) , ( LH ∷ LT ) , ( tnone ∷ [] ) +move1 tnone δ tδ q [] ( RH ∷ RT ) with tδ (δ q tnone) tnone +... | write x , left = (δ q tnone) , ( RH ∷ x ∷ [] ) , RT +... | write x , right = (δ q tnone) , [] , ( x ∷ RH ∷ RT ) +... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( RH ∷ RT ) +... | wnone , left = (δ q tnone) , ( RH ∷ tnone ∷ [] ) , RT +... | wnone , right = (δ q tnone) , [] , ( tnone ∷ RH ∷ RT ) +... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( RH ∷ RT ) +move1 tnone δ tδ q [] [] with tδ (δ q tnone) tnone +... | write x , left = (δ q tnone) , ( tnone ∷ x ∷ [] ) , [] +... | write x , right = (δ q tnone) , [] , ( x ∷ tnone ∷ [] ) +... | write x , mnone = (δ q tnone) , ( x ∷ [] ) , ( tnone ∷ [] ) +... | wnone , left = (δ q tnone) , ( tnone ∷ tnone ∷ [] ) , [] +... | wnone , right = (δ q tnone) , [] , ( tnone ∷ tnone ∷ [] ) +... | wnone , mnone = (δ q tnone) , ( tnone ∷ [] ) , ( tnone ∷ [] ) record TM ( Q : Set ) ( Σ : Set ) : Set where @@ -105,8 +163,14 @@ automaton : Automaton Q Σ tδ : Q → Σ → Write Σ × Move tnone : Σ - taccept : Q → List Σ → ( Q × List Σ × List Σ ) - taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L [] + taccept : (i : ℕ) → Q → List Σ → ( Q × List Σ × List Σ ) + taccept i q L = tloop i q L [] where + tloop : (i : ℕ) → (q : Q ) ( L : List Σ ) ( R : List Σ ) → Q × List Σ × List Σ + tloop i q L R with aend automaton q + ... | true = ( q , L , R ) + tloop zero q L R | false = ( q , L , R ) + tloop (suc i) q L R | false with move1 tnone (δ automaton) tδ q L R + ... | q' , L' , R' = tloop i q' L' R' data CopyStates : Set where s1 : CopyStates @@ -153,7 +217,7 @@ tend _ = false test1 : CopyStates × ( List ℕ ) × ( List ℕ ) -test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) +test1 = Turing.taccept copyMachine 10 ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ ) test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) []
--- a/automaton-in-agda/src/utm.agda Wed Nov 08 21:35:54 2023 +0900 +++ b/automaton-in-agda/src/utm.agda Thu Nov 09 18:04:55 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module utm where open import turing @@ -232,9 +234,8 @@ ^ ∷ ０ ∷ ０ ∷ １ ∷ １ ∷ [] utm-test1 : List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ ) -utm-test1 inp = Turing.taccept U-TM inp +utm-test1 inp = Turing.taccept U-TM 10 inp -{-# TERMINATING #-} utm-test2 : ℕ → List utmΣ → utmStates × ( List utmΣ ) × ( List utmΣ ) utm-test2 n inp = loop n (Turing.tstart U-TM) inp [] where @@ -242,7 +243,7 @@ loop zero q L R = ( q , L , R ) loop (suc n) q L R with move {utmStates} {utmΣ} {０} {utmδ} q L R | q ... | nq , nL , nR | reads = loop n nq nL nR - ... | nq , nL , nR | _ = loop (suc n) nq nL nR + ... | nq , nL , nR | _ = loop n nq nL nR t1 = utm-test2 3 short-input