Type theory里的coinduction怎样理解
structural induction 能用来证明 lambda calculus (也算是 infinite data structure 吧) 的定理。 【Type theory里的coinduction怎样理解】 从这句话可以看出题主对 induction（或者说 lambda calculus）的理解有问题。structural induction 可以理解为【对于任意大小的数据，我们可以归纳定义它上面的运算】，注意这里是【对于任意大小的】——【对于任意】是因为你的函数是 total 的。这并不意味着数据的无限与有限，因为 induction 只是解构的方式，而你在构造的时候只能构造出有限大小的数据（这是因为有 termination check。或者说你使用 eliminator 的时候就不可能存在无限的递归）。举个例子，给定一个由Zero和Succ两个构造器产生的一进制自然数，你写不出这样的代码：mugen = Succ mugen因为你不能无限地递归构造。注意我们现在没有讨论 induction，而是在讨论构造。
而假设我们的自然数类型是 coinductive 的，你就能够写出上面那样的代码，而且你写出的任何一个【构造】自然数的函数，都必须在被解构成更小部分时，递归调用自己（而在 induction 里面，你是【在构造更大的东西时，递归调用自己】）。
■网友
昨天刚刚听了P大胡振江老师的PL课讲recursive type今天就看到了这个问题，下面来勉强回答一下。
首先，我觉得structural induction的本质也是TaPL这本书上284页的principle of induction:
，因此用induction方法证明的lambda calculus的性质都是有穷次应用lambda calculus的syntax rule得到的表达式。
至于怎么理解co-induction，可以先考虑考虑怎么理解induction，这两个概念之间的关联性非常强，而因为在高中便熟知各种归纳法，使得induction在我们的大脑里先入为主，从而不是很好接收co-induction的概念。以TaPL中recursive type这一章的subtyping relation为例，书中给出的定义是：
可以看到generating function的形式基本一致，而且根据generating function写出的inference rule也是完全一样的。不同之处在于：finite subtyping关系集合通过取generating function的最小不动点得到，叫做inductively defined；infinite subtyping关系集合通过取generating function的最大不动点得到，叫做co-inductively defined。inductive是构造性的，比如我可以由
是
的子类和
是
的子类构造出
是
的子类，这样构造的结果不会包含无穷数据类型；而co-inductive是deconstruct的，与构造的过程刚好相反，可以理解作“观察性”的，我可以直接观察到
是
的子类，其中
和
推荐阅读
![[结对]中天金融结对帮扶团结村三年间：花开在眼前](https://p0.ssl.qhimgs4.com/t01b6de3abbdb96b907.jpg)
![[戴安娜王妃]威廉王子真柔情！本来开心纪念戴安娜忽然泪流不止，凯特不知所措](http://img88.010lm.com/img.php?https://image.uc.cn/s/wemedia/s/upload/2020/7754129187927f96deeb591e11f75cdd.jpg)
- 边城满洲里，冬日里的温暖
- 汽车知识|冬日里的追光者——诺马迪森“征途者B”
- 轮胎|暖暖的冬日，想和这里的花儿一起怒放！
- |邢台车主反映：行驶里程2600公里的新车，积碳竟像跑了10万公里
- 怎么样将家里的液晶电视和笔记本电脑连接
- 汽车知识|“大五座”SUV里的杰出代表 实拍本田UR-V
- 思域|2022款本田思域Type R路试谍照，多处搭载运动套件
- |全网好评的吉利星瑞，真这么好？为此，我们做了2000公里的长测
- 有谁知道关于 厂子里的一些信息 或介绍一些只有进了厂子才能知道的经历
- 关于图片里的文本识别，哪些特征相对有效