C. *_*ann 17
他们并不陌生,他们只是coinductive土黄.抛开⊥的问题,我们可以将此处的自然数类型定义为由其组成Zero,或Succ应用于自然数.归纳定义将假设一个明确定义的结束,即任何数字都从Zero构造函数开始.coinductive定义只是说,给定任何自然数,它将是Zero或者我们可以移除外部Succ以获得另一个自然数.
看似微妙的区别在于,共同定义包括无穷无尽的一系列Succ构造函数,它们实际上是无限的真实表现.这是有意义的,因为虽然归纳定义是关于确保递归将达到明确定义的基本情况,但是共同定义是关于确保总是有明确定义的下一步可用.
由于数据构造函数是懒惰的,因此在Haskell中,coinductive解释很方便并且在某些方面是强制性的.
所以,这个无穷大的数字实际上是无穷大,或ω,如果你需要指定哪个无限,正如Daniel Fischer所说.它只是一个共鸣无限,就像更常见的无限列表一样.
如果你通过他们的教会编码来考虑自然数,有限数字意味着"迭代这个函数N次"; ω表示"无限期地迭代此函数".
Dan*_*her 10
好吧,有Succ _|_,Succ (Succ _|_)等等.你可能已经包含了那些"底层价值".inf = Succ inf通常被称为infinity或omega(作为自然数的序数).