Type theory里的coinduction怎样理解( 二 )
都可能是无限类型，并且如果这两个类型是product，则它们的子类型也可以是无限类型 ，因此co-inductive可以包含无穷数据类型。
inductive type的范畴语义是自函子上的initial algebra，co-inductive的范畴语义是自函子上的terminal co-algebra。范畴这部分内容可以参考https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctor和https://ncatlab.org/nlab/show/terminal+coalgebra+for+an+endofunctor
如果是有限类型类型的话，关于其性质的证明就可以用前面的principle of induction，也就是归纳的方法；而对于无限类型的情况就要用principle of co-induction，因为我们不清楚它是怎么构造出来的，只能有观察的方法证明。
关于induction和co-induction还有更多的例子，比如对于自然数的generating function
通过inductive定义得到的是自然数集合
，而co-inductive定义得到的是?
；再比如list和co-list（也被称作stream），这两种结构都是用nil和cons表示，不过list是inductive定义的，就是长度有限的列表，而stream是co-induction方式定义的，就可以表示无限长度。（Haskell中因为默认惰性求值，最大不动点和最小不动点重合，于是list和stream就没有区分了）
关于包含无穷的自然数集合可以参考extended natural number in nLab
希望有所帮助。
■网友
Inductive就是符合类型递归式的最小类型。
Coinductive就是符合类型递归式的最大类型。
例如，同样写X = A * X。如果是inductive type的话，那么X是空集。如果是coinductive type的话 X = stream A。
推荐阅读
- 边城满洲里，冬日里的温暖
- 汽车知识|冬日里的追光者——诺马迪森“征途者B”
- 轮胎|暖暖的冬日，想和这里的花儿一起怒放！
- |邢台车主反映：行驶里程2600公里的新车，积碳竟像跑了10万公里
- 怎么样将家里的液晶电视和笔记本电脑连接
- 汽车知识|“大五座”SUV里的杰出代表 实拍本田UR-V
- 思域|2022款本田思域Type R路试谍照，多处搭载运动套件
- |全网好评的吉利星瑞，真这么好？为此，我们做了2000公里的长测
- 有谁知道关于 厂子里的一些信息 或介绍一些只有进了厂子才能知道的经历
- 关于图片里的文本识别，哪些特征相对有效