为什么初始代数对应于数据和最终的余代数？

Question

如果我理解正确的话,我们可以将归纳数据类型建模为初始F-代数和共感应数据类型作为最终的F-余代数(对于适当的endofunctor F)[ 1 ].据我所知,根据Lambek的引理,初始代数(和最终的余代数)是同构的不动点解T ? F T,但我不明白为什么初始代数是最不固定的点,而最终的代数是最大的固定点.(同构现象T ? F T有明显的解决方案吗？)

另外,我还不清楚类型理论中如何定义归纳和共感数据类型.是否有关于此主题的推荐资源,以及它们与类别理论的关系？

谢谢!

Answer 1

我的理解是，原则上，定点方程可能有很多解T \xe2\x89\x85 F T。根据兰贝克引理，初始代数（如果存在）就是这些不动点之一。事实上它是最小不动点。

\n\n

有一个通用条件定义了最小不动点的通用条件，沿着满足某些交换条件的任何其他不动点存在唯一态射的思路。

\n\n

换句话说，并非每个不动点都定义初始代数。

\n\n

同样的论点也适用于最终余代数和最大不动点。

\n\n

例如，参见函子的最小不动点。

\n