`inductive` コマンドに対する制約: strictly positive 性

[Seasawher]

エラーになる例。

/-
(kernel) arg #2 of 'HFS.power' has a non positive occurrence of the datatypes being declared
-/
inductive HFS : Nat → Type where
| empty : HFS 0
| power {n : Nat} : (HFS n → Prop) → HFS (n + 1)

strictly positive の制約を守らないと矛盾が示せるという例

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

unsafe def Bad.toFun (b : Bad) : Bad → Bad :=
  match b with
  | Bad.mk f => f

unsafe def selfApply (b : Bad) : Bad := b.toFun b

unsafe def omega : Bad := selfApply (Bad.mk selfApply)

unsafe def bad_contradiction (b : Bad) : False := by
  induction b
  case mk f ih =>
    exact ih omega

unsafe example : False := bad_contradiction omega

[spinylobster]

エラーメッセージ

(kernel) arg #2 of 'HFS.power' has a non positive occurrence of the datatypes being declared

から察するに、TPiLの7.帰納型の公理の詳細 が関係ありそうですね。

コンストラクタの引数の型に現在定義中の帰納族の要素が現れる場合、それはstrictly positivelyに出現しなければならないという要件がある

[Seasawher]

strict positive という制約は Free モナドの実装時にも表れる。このあたりを調査すればわかりやすく説明できそう。

How to define free monads and cofree comonads in Lean4?

[Seasawher]

https://cs.stackexchange.com/questions/55646/strict-positivity

この Q and A は参考になりそう
日本語訳を載せておく

---

まず、用語の説明です。論理学では「負の位置」と「正の位置」という概念があります。これは論理結合子における非対称性に関連しています。例えば ( A \Rightarrow B ) の場合、( A ) は ( B ) とは異なる振る舞いをします。同様のことが圏論にも見られ、そこでは「負」と「正」の代わりに、それぞれ「反変」と「共変」と呼ばれます。物理学では、「共変的」および「反変的」に振る舞う量について語られることもあります。このように、これは非常に一般的な現象です。プログラマーの視点では、「入力」と「出力」と考えると分かりやすいかもしれません。

それでは、帰納的データ型について説明します。

帰納的データ型 ( T ) を、一種の代数構造として考えてみましょう。コンストラクタは ( T ) の要素を引数として受け取り、新しい ( T ) の要素を生成する操作です。これは通常の代数に非常に似ています。たとえば、加算は2つの数値を受け取り、新しい数値を生成します。

代数では、操作は有限個の引数を取るのが一般的であり、ほとんどの場合、その引数の数は0（定数）、1（単項）、または2（二項）です。この考え方をデータ型のコンストラクタにも一般化するのが便利です。データ型 ( T ) に対するコンストラクタ ( c ) を考えてみましょう。

• ( c ) が定数の場合、それを関数 ( \text{unit} \to T )（または同等に ( (\text{empty} \to T) \to T )）と見なせます。
• ( c ) が単項の場合、それを関数 ( T \to T )（または同等に ( (\text{unit} \to T) \to T )）と見なせます。
• ( c ) が二項の場合、それを関数 ( T \to T \to T )、同等に ( T * T \to T )、またはさらに ( (\text{bool} \to T) \to T ) と見なせます。
• ( c ) が7つの引数を取るコンストラクタであれば、それを $(\text{seven} \to T) \to T$ と見なすことができ、ここで ( \text{seven} ) は7つの要素を持つ型とします。
• ( c ) が可算無限個の引数を取る場合、それは $(\text{Nat} \to T) \to T$ という関数となります。

これらの例からわかるように、コンストラクタの一般的な形は次のように表せます。

$$ c : (A \to T) \to T $$

ここで、( A ) を ( c ) の 引数のアリティ（arity） と呼びます。そして、( c ) を「型 ( T ) の要素を ( A )-多く受け取り、型 ( T ) の要素を生成するコンストラクタ」として考えることができます。

broken: (T -> T) -> T

それでは、「broken はいくつの引数を取るのか？」という問いには、明確な答えがありません。「それは ( T )-個の引数を取る」と答えようとするかもしれませんが、これは適切ではありません。なぜなら、( T ) はまだ定義されていないからです。この難問を解決しようとして、高度な不動点理論を使い、型 ( T ) と単射 ( (T \to T) \to T ) を見つけようとすれば、確かに成功するかもしれません。しかし、その過程で ( T ) に関する帰納法の原理が破綻してしまいます。このようなことを試みるのは、単に悪いアイデアです。

完全性のために、話をもう少し詳しく説明しましょう。上記のコンストラクタの形を少し一般化する必要があります。場合によっては、パラメータを取る操作やコンストラクタがあります。たとえば、スカラー倍はスカラー ( \lambda ) とベクトル ( v ) を受け取り、新しいベクトル ( \lambda \cdot v ) を生成します。これはベクトルに対する単項操作ですが、スカラーによってパラメータ化されています。このスカラー倍を、各スカラーに対する無数の単項操作の集合とみなすこともできますが、それは面倒です。したがって、コンストラクタ ( c ) の一般的な形は、ある型 ( B ) のパラメータを許容する必要があります。

[
c : B * (A \to T) \to T
]

実際、多くのコンストラクタはこの形に書き直すことができますが、それでも十分ではありません。もう一歩進んで、( A ) を ( B ) に依存させる必要があります。これを実現する形は次のようになります。

[
c : \left( \sum_{x : B} A(x) \to T \right) \to T
]

これが帰納的型のコンストラクタの最終形です。この形式は、まさに W型 と呼ばれるものと一致します。この形式は非常に一般的であるため、実際には単一のコンストラクタ ( c ) だけで十分です。実際、もし以下のような2つのコンストラクタ

[
d' : \left( \sum_{x : B'} A'(x) \to T \right) \to T
]
[
d'' : \left( \sum_{x : B''} A''(x) \to T \right) \to T
]

がある場合、それらを1つのコンストラクタに統合できます。

[
d : \left( \sum_{x : B} A(x) \to T \right) \to T
]

ここで、

[
B := B' + B''
]
[
A(\text{inl } x) := A'(x)
]
[
A(\text{inr } x) := A''(x)
]

ちなみに、この一般形をカリー化すると、次のような形式と等価になります。

[
c : \prod_{x : B} \left( (A(x) \to T) \to T \right)
]

この形式の方が、実際に証明支援系（proof assistants）で記述されるものに近いです。証明支援系では、コンストラクタを便利な形で記述できますが、それらは上記の一般形と等価です（これは読者への練習問題です！）。

[Seasawher]

strictly positive についてどのように説明するにせよ、なぜこれは許されるのかが説明できなければならない

これは Nat' を定義するのに Nat' の項が必要なので、項が定義できないのだが unsafe ではない。

-- 許される
inductive Nat' : Type where
  | succ : Nat' → Nat'

[Seasawher]

import Mathlib.Logic.Equiv.Defs

example (T : Type) : (Empty → T) ≃ Unit where
  toFun f := ()
  invFun u := Empty.elim (C := T)
  left_inv f := by ext x; cases x
  right_inv u := by cases u; rfl

example (T : Type) : (Unit → T) ≃ T where
  toFun f := f ()
  invFun f := fun _ => f
  left_inv f := by simp
  right_inv t := rfl

example (T : Type) : (Fin 2 → T) ≃ T × T where
  toFun f := (f 0, f 1)
  invFun p i :=
    match i with
    | 0 => p.1
    | 1 => p.2
  left_inv f := by
    ext x
    simp
    split <;> rfl
  right_inv p := by simp