如何解决马尔可夫原理在伊德里斯中是可证明的吗?
Idris 是编程语言中一个有趣的例子,虽然它不是图灵完备的(不包括偏性注释或 assert_total
),但正如追随者有时喜欢说的那样:“吃豆子完备”——也就是说,它提供了足够的计算能力来开发人们真正关心的“实用”程序——比如吃豆子。
Idris 所处的这个有趣的位置让我就其计算能力提出了许多不同的问题。如果它不是图灵完备的,我们在哪里划线?为了避免这成为一个单一的问题,我决定将这些问题作为单独的堆栈交换问题进行提问。
我对这个堆栈交换帖子的问题是:Markov's principle 是否可以在 Idris 中证明?更具体地说,伊德里斯的以下类型是否适合居住?
(p : Nat -> Type) -> ((n : Nat) -> Dec (p n)) -> (((n : Nat) -> p n) -> Void) -> (n : Nat ** p n -> Void)
对于不熟悉马尔可夫原理的人来说,这种类型的命题作为类型的直观含义是:
For all decidable predicates on the natural numbers,if a predicate is not true for all n,then there exists a n that makes it false.
这是一个有趣的问题,因为该定理无法在纯直觉主义逻辑中证明,但一些构造性数学流派(例如俄罗斯学派)认为它有效。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。