Friday, 9 July 2021

超準解析を Agda で

うっかり書き始めてしまったわけですが、わりと順調。

超自然数は

  HyperNat = ℕ → ℕ

整数は差を取れば良い。

  data HyperZ : Set where
    hz : HyperNat → HyperNat → HyperZ

で分数と。

  data HyperR : Set where
    hr : HyperZ → (k : HyperNat ) → ((i : ℕ) → 0 < k i) → HyperR

等号とか不等号の決定はTrichotomous は排中律な仮定になるわけですけどね。

  record _n≤_ (i j : HyperNat ) : Set where
    field
     ≤-map : Bijection ℕ ℕ
     ≤-m : ℕ
     is-n≤ : (k : ℕ ) → k > ≤-m → i k ≤ j (fun→ ≤-map k)

ってな感じか。これで、できそうなんですが、

Transfer principle ってのがあって「実数で証明できる性質は、超実数でも証明される」ってのがあるらしい。

確かに、自然数から上の方法で分数まで作って体になるので、そうなるんだが、それ自体をどう Agda で書くのかわからん。

  transferN : ( p : ℕ → Set ) → HyperNat → Set
  transferN p n = (k : ℕ ) → p (n k)

  transfer : {R H : Set} → ( p : R ∨ H → Set )
     → ((x : R ) → p (case1 x) )
     → ((x : H ) → p (case2 x))
  transfer {R} {h} p rp x = ?

ってなのを思いついたが、それで通るのかは謎だな。

No comments: