Mercurial > hg > Members > kono > Proof > automaton

changeset 179:f226c21d61bf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
halting problem done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Mar 2021 00:16:42 +0900
parents 27dbee9c292c
children 4c5d26c149fa
files agda/halt.agda
diffstat 1 files changed, 29 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/agda/halt.agda	Wed Mar 17 10:24:49 2021 +0900
+++ b/agda/halt.agda	Thu Mar 18 00:16:42 2021 +0900
@@ -64,13 +64,12 @@
 
 open import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n : Level}  → Axiom.Extensionality.Propositional.Extensionality n n 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong ) 
 
 record Halt : Set where
    field
       halt :  (t : TM ) → (x : List Bool ) → Bool
-      -- is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
-      -- is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
+      is-halt :     (t : TM ) → (x : List Bool ) → (halt t x ≡ true )  ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
+      is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
 
 record HaltIsTM (ha : Halt) (utm : UTM) : Set where
    field
@@ -89,18 +88,33 @@
      h1 h x with h x
      ... | true =  just true
      ... | false = nothing
+     h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing
+     h-nothing h y eq with h y
+     h-nothing h y refl | false = refl
+     h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
+     h-just h y eq with h y
+     h-just h y refl | true = refl
      TN1 :  (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (encode utm (record { tm = h1 h }) ++ y) ≡ h y
      TN1 h y with h y | inspect h y
-     ... | true  | record { eq = eq1 } = {!!}
+     ... | true  | record { eq = eq1 } = begin
+        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) y1 ) (case1 (sym tm-y1)) ⟩
+        true ∎  where
+          open ≡-Reasoning
+          y1 : List Bool
+          y1 = encode utm (record { tm = λ x → h1 h x }) ++ y
+          tm-y1 = begin
+              tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y)  ≡⟨  is-tm utm _ y ⟩
+              h1 h y ≡⟨ h-just h y eq1  ⟩
+              just true  ∎  where
      ... | false | record { eq = eq1 } = begin
-        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ {!!} ⟩
-        false ∎  where open ≡-Reasoning
-
-
--- TNℕ : (halt : Halt ) → (utm : UTM) → HaltIsTM halt utm → HBijection (TM → Bool) TM
--- TNℕ halt utm halt-is-tm = record {
---        fun←  = λ tm tm1 → Halt.halt halt tm (encode utm tm1)
---      ; fun→  = λ h  → record { tm = λ x → just (h {!!} ) } --  TM → Bool → TM
---      ; fiso← = {!!}
---   }
-
+        Halt.halt halt (UTM.utm utm)  (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) y1 ) (sym tm-y1) ⟩
+        false ∎  where
+          open ≡-Reasoning
+          y1 : List Bool
+          y1 = encode utm (record { tm = λ x → h1 h x }) ++ y
+          tm-y1 :  tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y) ≡ nothing
+          tm-y1 = begin
+              tm (UTM.utm utm) (encode utm (record { tm = λ x → h1 h x }) ++ y)  ≡⟨  is-tm utm _ y ⟩
+              h1 h y ≡⟨  h-nothing h y eq1 ⟩
+              nothing  ∎  where
+