ぷちます、買いました?? 

-- "A Tutorial on [Co-]Inductive Types in Coq"
-- 3.4 Case Analysis and Logical Paradoxes の Agda2版です。
-- Strictly Positiveが要請される１つの理由

module Paradox where

open import Data.String

data False : Set0 where

data Nat : Set0 where
  zero : Nat
  succ : Nat → Nat

one = succ zero
two = succ one
three = succ two
four = succ three

data Id {A : Set0} : A → A → Set0 where
  refl : (a : A) → Id a a

f : False → Id zero one
f () -- 矛盾出て来たらもう諦めよう... という書き方

postulate false : False

Theorem : Id zero one
Theorem = f false -- 実際にはこう使う

-- もうちょっとくどい方法でこれと同じ事をする！！

{-
data Lambda : Set0 where
  lambda : (Lambda -> False) -> Lambda

strictly-positiveでないので定義出来ない
-}

-- ので postulateを使って定義する
postulate Lambda : Set0
postulate lambda : (Lambda → False) → Lambda

-- lambdaに対してはこのような定義が出来ない
pred : Nat → Nat
pred zero = zero
pred (succ a) = a

-- 本当は次のようにmatchを定義したいのよ！！?
{-
match : Lambda -> False
match lam ~ (lambda h) = h lam -- ここで h ∈ Lambda -> False となる これは lambdaの定義から明らか
-}

-- でも出来ないので次のようにする
postulate match : Lambda → ((Lambda → False) → False) → False

-- 後は準備
apply : Lambda → Lambda → False
apply f x = match f (λ(l : Lambda → False) → l x)

Delta : Lambda
Delta = lambda (λ(x : Lambda) → apply x x)

loop : False -- False作れました！！
loop = apply Delta Delta

ぷろくし : False → Id "春香さん" "はるかさん"
ぷろくし ()

せおれむ : Id "春香さん" "はるかさん"
せおれむ = ぷろくし loop

...それで??

例えば、HaskellでHOASを書きたいなーとかになると

data Exp where
  ELam :: (Exp -> Exp) -> Exp

みたいな事が書きたく成るのですが、これはNot Strictly Positiveなので駄目です、って感じになります。

(HOASの参考は http://twelf.plparty.org/wiki/Higher-order_abstract_syntax 他)

... ... それで??

not strictly positiveということは、strictly positiveだと困る理由があるからで、取りあえず上に挙げた例はそうなのですがちょっと特殊な気もします。

で、一般的にstrictly positiveを許すと、即ちなにを覚悟しないといけないのかが知りたいっていうのと、strictlyがあるならpositiveもあるわけで、positiveを許すと何を覚悟しなければならないかを知りたい。

知りたいというのは、実際書けないわけで、書けない理由を知らずにはいそうですかと言うのはなぁというのが少しあるので。

参考文献

ぷちます!(1) (電撃コミックス EX)

ぷちます!(1) (電撃コミックス EX)