Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/halt.agda @ 407:c7ad8d2dc157
safe halt.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 09 Nov 2023 18:04:55 +0900 |
| parents | af8f630b7e60 |
| children | 3d0aa205edf9 |
| rev | line source |
|---|---|
| 407 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 405 | 2 |
| 141 | 3 module halt where |
| 4 | |
| 5 open import Level renaming ( zero to Zero ; suc to Suc ) | |
| 6 open import Data.Nat | |
| 142 | 7 open import Data.Maybe |
| 141 | 8 open import Data.List hiding ([_]) |
| 9 open import Data.Nat.Properties | |
| 10 open import Relation.Nullary | |
| 11 open import Data.Empty | |
| 12 open import Data.Unit | |
| 142 | 13 open import Relation.Binary.Core hiding (_⇔_) |
| 141 | 14 open import Relation.Binary.Definitions |
| 15 open import Relation.Binary.PropositionalEquality | |
| 16 | |
| 17 open import logic | |
| 18 | |
| 407 | 19 record FBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where |
| 141 | 20 field |
| 407 | 21 ffun← : S → R → Bool |
| 22 ffun→ : (R → Bool) → S | |
| 23 ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x | |
| 141 | 24 |
| 407 | 25 -- ffun← ( ffun→ f ) ≡ f , if we have functional extensionality but it is unsafe |
| 164 | 26 |
| 407 | 27 open FBijection |
| 28 | |
| 29 fdiag : {S : Set } (b : FBijection S S) → S → Bool | |
| 30 fdiag b n = not (ffun← b n n) | |
| 141 | 31 |
| 407 | 32 -- |
| 33 -- ffun→ b (fiag b) is some S | |
| 34 -- ffun← b (ffun→ b (fdiag b) ) is a function S → Bool | |
| 35 -- is pointwise equal to fdiag b , which means not (ffun← b (ffun→ b (fdiag b) ) x ≡ (fdiag b) x ) | |
| 36 -- but is also means not (fdiag b) x ≡ (fdiag b) x , contradiction | |
| 164 | 37 |
| 407 | 38 fdiagonal : { S : Set } → ¬ FBijection S S |
| 39 fdiagonal {S} b = ¬t=f _ (trans ff4 (sym (ff3 _) ) ) where | |
| 40 ff1 : S | |
| 41 ff1 = ffun→ b (fdiag b) | |
| 42 ff2 : S → Bool | |
| 43 ff2 = ffun← b (ffun→ b (fdiag b) ) | |
| 44 ff3 : (x : S) → ffun← b (ffun→ b (fdiag b) ) x ≡ fdiag b x | |
| 45 ff3 x = ffiso← b (fdiag b) x | |
| 46 ff4 : not ( ffun← b (ffun→ b (fdiag b) ) (ffun→ b (fdiag b))) ≡ fdiag b (ffun→ b (fdiag b)) | |
| 47 ff4 = refl -- definition of fdiag b | |
| 141 | 48 |
| 164 | 49 record TM : Set where |
| 50 field | |
| 51 tm : List Bool → Maybe Bool | |
| 52 | |
| 53 open TM | |
| 54 | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
55 record UTM : Set where |
| 164 | 56 field |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
57 utm : TM |
|
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
58 encode : TM → List Bool |
|
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
59 is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x |
| 164 | 60 |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
61 open UTM |
| 164 | 62 |
| 141 | 63 open _∧_ |
| 173 | 64 |
| 142 | 65 record Halt : Set where |
| 66 field | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
67 halt : (t : TM ) → (x : List Bool ) → Bool |
| 179 | 68 is-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ true ) ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) ) |
| 69 is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x ) | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
70 |
| 142 | 71 open Halt |
| 72 | |
| 407 | 73 TNLF : (halt : Halt ) → (utm : UTM) → FBijection (List Bool) (List Bool) |
| 74 TNLF halt utm = record { | |
| 75 ffun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x) | |
| 76 ; ffun→ = λ h → encode utm record { tm = h1 h } | |
| 77 ; ffiso← = λ h y → TN1 h y | |
|
177
375e1dcba6aa
TNL in halting problem
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
176
diff
changeset
|
78 } where |
| 180 | 79 open ≡-Reasoning |
| 178 | 80 h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool |
| 81 h1 h x with h x | |
| 82 ... | true = just true | |
| 83 ... | false = nothing | |
| 180 | 84 tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool |
| 85 tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y | |
| 179 | 86 h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing |
| 87 h-nothing h y eq with h y | |
| 88 h-nothing h y refl | false = refl | |
| 89 h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true | |
| 90 h-just h y eq with h y | |
| 91 h-just h y refl | true = refl | |
| 180 | 92 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y |
| 405 | 93 TN1 h y with h y in eq1 |
| 94 ... | true = begin | |
| 180 | 95 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩ |
| 179 | 96 true ∎ where |
| 180 | 97 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true |
| 98 tm-tenc = begin | |
| 99 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ | |
| 179 | 100 h1 h y ≡⟨ h-just h y eq1 ⟩ |
| 180 | 101 just true ∎ |
| 405 | 102 ... | false = begin |
| 180 | 103 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩ |
| 179 | 104 false ∎ where |
| 180 | 105 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing |
| 106 tm-tenc = begin | |
| 107 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ | |
| 179 | 108 h1 h y ≡⟨ h-nothing h y eq1 ⟩ |
| 180 | 109 nothing ∎ |
| 407 | 110 -- the rest of bijection means encoding is unique, but we don't need it |
| 180 | 111 -- fiso→ : (y : List Bool ) → encode utm record { tm = λ x → h1 (λ tm → Halt.halt halt (UTM.utm utm) tm ) x } ≡ y |
| 179 | 112 |
| 407 | 113 TNLF1 : UTM → ¬ Halt |
| 114 TNLF1 utm halt = fdiagonal ( TNLF halt utm ) | |
| 332 | 115 |