我按照这篇文章的思路实现了依赖类型的λ演算:http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf该演算法可用,我还尝试了一些扩展:多个宇宙,硬编码归纳公理。然而,我想添加归纳类型以做更复杂的事情。
我正在考虑两种方式:
那怎么做呢?Coq、Agda和Idris等现有系统如何实现类型?
我正在考虑两种方式:
- 引入Fin-N、Product和W类型,并用它们表示归纳类型。
- 生成归纳和递归公理。
那怎么做呢?Coq、Agda和Idris等现有系统如何实现类型?
_rect
、_rec
和_ind
这些术语,它们是该语言的术语。这些方案的“正确性”涉及到理解fix
绑定器和保护条件,但我认为它们不是公理。 - Vinz