"self type and coinductive type" での依存型に対応した余帰納法の誤りについて

[Hexirp]

"self type and coinductive type" の依存型に対応した余帰納法を導いている所のことである。

ここが怪しいと思っていた。なので、 Stack Overflow で質問してみた。すると、やっぱり間違っていたみたいである。

[Hexirp]

q は pol で実装できるかな？

[Hexirp]

まず、 Push_out を実装しよう。

defined inductive type
  Push_out
      (i : Level & Multiplicity.zero)
      (A : Type i & Multiplicity.zero)
      (B : Type i & Multiplicity.zero)
      (C : Type i & Multiplicity.zero)
      (f : A -> B & Multiplicity.zero)
      (g : A -> C & Multiplicity.zero)
    : Type i
where
  left : B -> Push_out i A B C f g
  right : C -> Push_out i A B C f g
  path
    :
      pi
        x : A & Multiplicity.zero
      ->
        Path
          i
          (lambda _ : Interval => Push_out i A B C f g)
          (left (f x))
          (right (g x))

[Hexirp]

Cubical Type Theory と Quantitative Type Theory を組み合わせたとき、 Path : pi (i : Level & Multiplicity.zero) (A : Interval -> Type i) (x : A Interval.zero & Multiplicity.zero) (y : A Interval.one & Multiplicity.zero) -> Type i を考えると、 Path.id : pi (i : Level & Multiplicity.zero) (A : Type i) (x : A & e) -> Path i (lambda _ : Interval => A) x x の e は何になるべきなのかという問題が出てくる。

[Hexirp]

まあ、 Intheo では Interval と Path は非プリミティブ型であるから、その実装の時に分かるだろう。

[Hexirp]

自分型での Interval の実装は これ に拠っている。これによると、 Path の多重度の指定の仕方によって Path.id の多重度も変わりそうである。

また、これは面白いことに transp というプリミティブを必要とするようだ。これは Cubical Agda でも同様にプリミティブであって内部的には型に対する場合分けで記述されるようである。 Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types の 3.2 を参照せよ。

[Hexirp]

元々の Cubical Agda では comp がプリミティブだったな。それを使って transport を実装していた。

[Hexirp]

次は、余依存型を定義する。

define value Codependent_Type (i : Level) (A : Type i) : Type (Level.succ i) where
  Codependent_Type i A = Product (Level.succ i) (lift i A) (Type i)

[Hexirp]

次は、 _! を定義する。

define value
  Codependent_Type_Wrapper (i : Level) (A : Type i) (Q : Codependent_Type i A)
    : Type (Level.succ i)
where
  Codependent_Type_Wrapper i A Q
    =
      Push_out
        (Level.succ i)
        Q
        (lift i A)
        (Type i)
        (Product.first (Level.succ i) (lift i A) (Type i))
        (Product.second (Level.succ i) (lift i A) (Type i))

[Hexirp]

これ によると、 cofibration を組み込めると Cubical Type Theory の regularity の問題が解決できる可能性があるらしい。

[Hexirp]

q : A -> Q! を定義しよう。

define value
  codisplay (i : Level) (A : Type i) (Q : Codependent_Type i A)
    : A -> Codependent_Type_Wrapper i A Q
where
  codisplay i A Q
    =
      Push_out.left
        (Level.succ i)
        Q
        (lift i A)
        (Type i)
        (Product.first (Level.succ i) (lift i A) (Type i))
        (Product.second (Level.succ i) (lift i A) (Type i))

[Hexirp]

さて、これらが任意の対象 X と任意の射 f : A -> X と push-out を構成することを証明しなければならない。

[Hexirp]

まず、 f : A -> X から Codependent_Type.map i A X f : Codependent_Type i A -> Codependent_Type i X を自明に得ることが出来る。

[Hexirp]

Codependent_Type_Wrapper i X (Codependent_Type.map i A X f Q) が、件の型が任意の対象 X と任意の射 f : A -> X と push-out を成すときの、その push-out そのものなのである！

X -> Codependent_Type_Wrapper i X (Codependent_Type.map i A X Q) は codisplay と同様に Push_out.left により自明に与えられる。これもまた依存型における事情と一致している……

もう一方の Codependent_Type_Wrapper i A Q -> Codependent_Type_Wrapper i X (Codependent_Type.map i A X Q) が必要である。これを実装できるだろうか？

[Hexirp]

left の枝は f を使えば良く、 right の枝も恐らく恒等射で良い。では、 path の枝は、どうなるだろうか？

function i A Q X f (Push_out.path _ _ _ _ _ _ x i) = goal_0

[Hexirp]

うーん、これはかなり難しい。その前に、実際に余帰納法の原理を記述することを考えよう。

Bool -> P が (x : Bool) -> P x になるのである。これは即ち Bool -> Dependent_Type_Wrapper i (Bool i) P であり display を合成すると id になる。

同様に Codependent_Type_Wrapper i (Stream i A) Q -> Stream i A であり codisplay を合成すると id になる。

[Hexirp]

どうやら、 x : A で「限定」する方向性は上手く行かなさそうである。余帰納法の原理における分解子の枝の書き方は、どうなのだろうか？ 余依存型を使った時の。

それは、帰納法の原理の書き方を裏返せばよい。つまり、 これ を裏返せばよい。この中での f は Nat.succ の構築子の枝に該当する。これを裏返して分解子に対するものを与えることは容易である。

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAAUB+EAX1PUy58hFAEZyVWoxZsuvfiAzY8BImVGT6zVohAAdPQFs6OABYAjc8AByPeQOXCi4jdS0zdB42cs27PSRgoAHN4IlAAMwAnCEMkMhAcCCRxKW02CPsQaNj46iSkACY3aR1FLJy4xFSCxABmEvTdNAqYquLE5PrGjxAEAJ4gA
\begin{tikzcd}
P? \arrow[r, "f"] \arrow[d, "p"] & P? \arrow[d, "p"] \\
\mathbb{N} \arrow[r, "s"]        & \mathbb{N}       
\end{tikzcd}

[Hexirp]

この書き方は帰納型を定義する時にも広げられるのである。

define inductive type Is_True : Dependent_Type Bool where
  proof : Unit -> Dependent_Type_Wrapper Is_True
  proof_value : (lambda x : Unit => display (proof x)) = (lambda x : Unit => true)

こういう風に。これと同じ構文で余依存型を余帰納的に定義できるのではないだろうか？

[Hexirp]

inductive type を定義する時の primitive operator として Type と Dependent_Type と Dependent_Type_Wrapper と display と Path を認める。

coinductive type を定義する時の primitive operator として Type と Codependent_Type と Codependent_Type_Wrapper と codisplay と Path を認める。

[Hexirp]

(P : Bool & 0 -> Type) -> P true -> P false は「真」でなければならない。少なくとも「偽」ではあってはいけない。こう考えると、おのずからと Path の多重度に制約がかかる。つまり、 Path.id は 0 以上でなければならない。

いや、普通に多重度に関して多相にすれば良いだけなのでは……？

[Hexirp]

初心に戻って余帰納法の原理を型なしラムダ計算で記述してみよう。

Stream.coinduction A destructor_head destructor_tail x
  =
    Stream.comatching
      A
      (destructor_head x)
      (Stream.coinduction A destructor_head destructor_tail (destructor_tail x))

[Hexirp]

Stream.comatching は次のような型を持つんだよね。

Stream.comatching
    (A : Type)
    (P : Type)
    (destructor_head : P -> A)
    (destructor_tail : P -> Stream A)
  : P -> Stream A

[Hexirp]

そんで、 Codependent_Type_Wrapper を使えば、こういう型に出来る。

Stream.comatching
    (A : Type)
    (P : Codependent_Type (Stream A))
    (destructor_head : Codependent_Type_Wrapper (Stream A) P -> A)
    (destructor_tail : Codependent_Type_Wrapper (Stream A) P -> Stream A)
  : Codependent_Type_Wrapper (Stream A) P -> Stream A

ここで、これのような可換図式を満たす。

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAGUAKAQQEoQAvqXSZc+QigCM5KrUYs23QcJAZseAkWmTZ9Zq0Qce-ISPXiiZHdT0LDARUGyYUAObwioAGYAnCAFskMhAcCCRpOX02AAtlbz9AxGDQpABmG3kDEABHEGoGOgAjGAYABVENCRAfLFdonDiQXwC06hTEACYMqMMvTigAfWBooUHgHAF+fKKS8vNNQxq6htMmhKQukLDECNss2OnisoqLRdr6pwEgA
\begin{tikzcd}
S(A) \arrow[r, "h"] \arrow[d, "q"'] & A                    \\
Q \arrow[r, "{f(d_{h},d_{t})}"']    & S(A) \arrow[u, "h"']
\end{tikzcd}

[Hexirp]

また、これも。

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAGUAKAQQEoQAvqXSZc+QigCM5KrUYs2XPoOEgM2PASLTJs+s1aIOPfkJEbxRMrur6FRgIqDZMKAHN4RUADMAThABbJDIQHAgkaTkDNhwVH38gxBCwpABmW3lDEABHEGoGOgAjGAYABVFNCRBfLDcAC1izED9AtOoUxAAmDOijb04oAH1gOqEh4BwBfnyikvKLLSMa+sbVFsTu0PDESLss2JnisorLJdqG5wEgA
\begin{tikzcd}
S(A) \arrow[r, "t"] \arrow[d, "q"'] & S(A)                 \\
Q \arrow[r, "{f(d_{h},d_{t})}"']    & S(A) \arrow[u, "t"']
\end{tikzcd}

[Hexirp]

inductive type と coinductive type の定義で Dependent_Type と Dependent_Type_Wrapper を使えるようにする意味は殆どない。なぜならば、 Path による条件を加えることで代替できるから。

では、 Codependent_Type と Codependent_Type_Wrapper を使えるようにする意味は？ これもまた何らかの道具で代替可能であるように思う。今は coinduction の表現だけを考えよう。

[Hexirp]

Stream.coinduction は以下の二つの可換図式を満たす。

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAEUQBfU9TXfIRQBGclVqMWbAILdeIDNjwEiZYePrNWiEAGUAFNICU3cTCgBzeEVAAzAE4QAtkjIgcEJKIla2wKFwA+sAAFlxydo4uiG4eSABM1JpSOrb6-kGhPBnBOFwm1Ax0AEYwDAAK-MpCIPZYFiE4ESAOzgnUcYjeydogISCFJWWVSoJsdQ1NXBRcQA
\begin{tikzcd}
Q \arrow[r, "{d}_{h}"] \arrow[d, "{f({d}_{h},{d}_{t})}"'] & A \\
S(A) \arrow[ru, "h"']                                     &  
\end{tikzcd}

% https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAEUQBfU9TXfIRQBGclVqMWbTjz7Y8BImWHj6zVohABlABQBBAJTdeIDPMFFRK6mqmbdh7uJhQA5vCKgAZgCcIAWyQyEBwIJFEJdTZgKC4AfWAcLmNvP0DEYNCkACYbSQ0QLx0Y+OAAC1lYhKSjagY6ACMYBgAFfgUhEB8sVzKcFMK0nOosxABmPKjNftlBgPCRsPHJu0LiqvLK0pqnLiA
\begin{tikzcd}
Q \arrow[r, "{d}_{t}"] \arrow[d, "{f({d}_{h},{d}_{t})}"'] & Q \arrow[d, "{f({d}_{h},{d}_{t})}"] \\
S(A) \arrow[r, "t"]                                       & S(A)                               
\end{tikzcd}

[Hexirp]

つまり、 Codependent_Type と Codependent_Type_Wrapper と codisplay の存在を認めたら corecursion を拡張することで coinduction を実装できるということである。それは、 P : Type を Codependent_Type_Wrapper _ P : Type で置き換えることによる。

その計算規則は圏論的な考察により描写できる。すなわち、 comatching を計算した結果を参考にして coinduction を計算できる。

[Hexirp]

Codependent_Type_Wrapper を含めて書き直す。

Stream.coinduction A P destructor_head destructor_tail x
  =
    Stream.comatching
      A
      P
      destructor_head
      (lambda x => Stream.coinduction A P destructor_head destructor_tail (destructor_tail x))

[Hexirp]

ここで、 P を具体的に与えるには、どうすればいいのか、つまりは Codependent_Type と Codependent_Type_Wrapper と codisplay は何であるのか、それが問題になる。

先にも書いたように、その仮説を私は既に持っている。しかし、正しいかどうかは確かめられていない。

[Hexirp]

inductive type には matching と induction が天下り的に与えられ、 coinductive type には comatching と coinduction が天下り的に与えられるとする方が、筋が通っているのではないか。また、それぞれの計算規則も組み込まれる。

[Hexirp]

define inductive type Is_True : Dependent_Type Bool where
  proof : Unit -> Dependent_Type_Wrapper Is_True
  proof_value : (lambda x : Unit => display (proof x)) = (lambda x : Unit => true)

これと higher inductive type は非常に似ている。すなわち、 Interval -> A を包んでやり proof_value と同じ方法で末端を指定したものが。

ああ、 Interval -> A が Path であるなら Interval × A は Copath なのではあるまいな？ いや、その通りだ。

[Hexirp]

Dependent_Type_Wrapper は、こういうことだよなあ。

P -> P
(n : Nat) -> P n -> P
(n : Nat) -> P n -> P (n + 1)