Turing Machine の停止問題を Agda で

割とやぶれさっていたんですが、10日くらい前にふっとできました。

record HBijection {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

diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S

くらいまではできてて、List Bool と Nat` とかと戦ってたんですが、

　　S を List Bool で良いんじゃないの?

で、確かにそう。あとは、

record TM : Set where
field
tm : List Bool → Maybe Bool

record UTM : Set where
field
utm : TM
encode : TM → List Bool
is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x

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 )

と書き下してしまえば、Bijection を作るだけで終わりだ。

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 ) }
where
TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y

Halt が TM である必要はない。TMのencodingのuniqnessも不要。ただ halt は bool を返すけど、
TM は Maybe Bool なので、それを変換することが必要なわけね。確かに、そう書いてある。
理解したつもりでも書き下してみると確認できて良いです。

なんで、こんなに時間がかかったのかは謎。一つは Bijection の対角線論法と halt の定義が入り混じっててて分離できなかったからだな。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/halt.agda