strictly positive 性についての補足

[Seasawher]

A が Inhabited ならば、 T → A は Inhabited.

つまり (T → A) → T をコンストラクタとする帰納型 T を想定したとき、 T は inhabited.

しかし T はコンストラクタのアリティが T 自身になっていて不定なので、T の項が存在すると仮定すると矛盾になる。

したがって、矛盾が導かれる…のではないか？？
これで説明になっているのでは。

[Seasawher]

残念ながら説明にはなっていない。A の Inhabited 性を仮定するのは変で、やはり元々の文脈である「停止しない計算の型チェックが通ってしまう」ことを問題にするべき。

停止しない計算の存在から矛盾を示せるのは理論としては知っているが、どうやるとコード例としてわかりやすいだろうか？

[Seasawher]

矛盾が生じることの説明はできた。無限に計算が続くことを、コードを慎重に読まなくても分かるようにしたいが、それは難しいだろうか…？

opaque A : Type

unsafe inductive Bad where
  | mk (f : Bad → A)

unsafe def selfApply (b : Bad) : A :=
  match b with
  | Bad.mk f => f b

-- omega を計算すると omega 自身が出てくるから、omega の計算は無限に続く
-- 計算が無限に続くような項を定義できてしまった
unsafe def omega : A := selfApply (Bad.mk selfApply)

-- A は任意の型なのに、Inhabited インスタンスが構築できてしまった！
unsafe instance : Inhabited A := ⟨omega⟩