停止性問題 in Idris

Halt.idr

-- $ idris
-- > :l Halt
module Halt

%default total


namespace Hal
  postulate H : (f : a) -> Bool

  data Halt : (f : a) -> Bool -> Type where
    NoHalt   : H f = False -> Halt f False
    YesHalt  : H f = True  -> Halt f True

  -- 関数m は、if の中身（コンストラクタTrueHalt の第一条件）が True の時、無限ループする
  data IfInner : Type -> Type where
    TrueHalt   : True  = H f -> Halt f False -> IfInner $ Halt f False
    FalseHalt  : False = H f -> Halt f True  -> IfInner $ Halt f True

  partial
  m : Bool
  m = if H m
    then m    -- inf loop
    else True -- halt

  -- m が停止するとしても停止しないとしても矛盾する
  partial
  theorem1 : IfInner $ Halt Hal.m True  -> Void
  theorem1 (FalseHalt hmF (YesHalt hmT)) = absurd $ trans hmF hmT
  partial
  theorem2 : IfInner $ Halt Hal.m False -> Void
  theorem2 (TrueHalt hmT (NoHalt hmF))   = absurd $ trans hmT hmF

Halt2.idr

-- $ idris
-- > :l Halt2
module Halt2

%default total

{-
namespace Tar
  postulate T : (n : Nat) -> Bool -- True(g(A)) ↔ A
  postulate g : (f : Type) -> Nat
  postulate phi : Type
  postulate hoo : Not $ MyTrue phi

  data MyTrue : Type -> Type where
    Yes : T (g f) = f -> MyTrue f

  --data Halt : (f : a) -> Bool -> Type where
  --  NoHalt   : H f = False -> Halt f False
  --  YesHalt  : H f = True  -> Halt f True

-- 証明 — 示すべきことに反し、L-式 True(n) が存在して以下を満たすと仮定する：N で真である L-文のゲーデル数が n であるときかつそのときに限り True(n) が真である。
-- このとき、True(n) を用いて新しい L-式 S(m) を次のように定義することができる：
-- m が式 φ(x) （x は自由変数）のゲーデル数であって φ(m) が N において偽であるときかつそのときに限り S(m) が真である
-- （すなわち、自身のゲーデル数を代入したときに偽になる式 φ(x) を考える）。
-- ここで、S(m) のゲーデル数 g を考え、S(g) は N で真かどうかを問うと矛盾を生ずる（これはいわゆる対角線論法である）。
  --partial
  s : Type -> Nat -> Bool
  s t n = n == g t

  -- s (g s) が真だとしても偽だとしても矛盾する
  --partial
  theorem1 : s s (g s) = True  -> Void
  theorem1 (FalseHalt hmF (YesHalt hmT)) = absurd $ trans hmF hmT
  --partial
  theorem2 : s (g s) = False -> Void
  theorem2 (TrueHalt hmT (NoHalt hmF))   = absurd $ trans hmT hmF
-}

namespace Tar
  postulate φ : Nat -> Nat -> Bool

  g : Nat -> Bool
  g x = not $ φ x x

  diagonal : (x0 ** φ x0 x0 = g x0) -> void
  diagonal (x0 ** p) with (φ x0 x0)
    | False = absurd p
    | True  = absurd p


namespace D
  interface Diagonal a where
    φ : Nat -> Nat -> Bool
    g : Nat -> Bool
    g x = not $ φ x x

  dVoid : (x0 ** φ x0 x0 = g x0) -> void
  dVoid (x0 ** p) with (φ x0 x0)
    | False = absurd p
    | True  = absurd p

  --implementation Diagonal Nat where