これは停止するらしい

module IndHatena where

open import Data.Nat
import Level
open import Induction.Nat using (<-rec)

f : (x : &#8469;) -> &#8469;
f zero = zero
f x = f x'
  where
    postulate x' : &#8469;
    postulate pr : x' < x

f改' : (x : &#8469;) -> ((y : &#8469;) -> y <′ x -> &#8469;) -> &#8469;
f改' zero _ = zero
f改' x f改 = f改 x' pr
  where
    postulate x' : &#8469;
    postulate pr : x' <′ x

f改 : &#8469; -> &#8469;
f改 = <-rec (λ _ -> &#8469;) f改'

g' : (x : &#8469;) -> ((y : &#8469;) -> y <′ x -> &#8469;) -> &#8469;
g' x g = g x' pr
  where
    postulate x' : &#8469;
    postulate pr : x' <′ x

g : &#8469; -> &#8469;
g = <-rec (λ _ → &#8469;) g'

まぁコードはどうでも良くて、気分としては、自然数を取る関数fがあり、今xについて定義しようとしている。

どこからか、xより小さいと分かっている数x'が現れて、f x = f x'である。あと、f zero = zero

と定義したいなーと思ったとしても、Agda2でfを上の通りそのまんま定義してもダメデスよ、と言われます。なぜなら、停止するかどうかが分からないから。

そこで、自然数っていうのは小なりな関係でWell-foundedなので、という事を利用して、兎に角停止性を言ってみたのがf改です。

どんどん小さくなって言って、自然数で一番小さいzeroには最終的になって、zeroは明らかに停まるので多分いけそうだ！という雰囲気そのままなのですが(つまり帰納法の基底が存在している)。

ところが、基底が存在していないgでも停止性が言えてしまいます。

こういうのはOKなのかなぁ。