我一直认为已经证明，pred对于任何数据类型编码，都不能在构造演算的恒定时间内表达。现在，请注意 nats 的这种编码：
S0 : ∀ (r : *) . (r -> r) -> r -> r
S0 = λ s z . z
S1 : ∀ (r : *) (((∀ (r : *) . (r -> r) -> r -> r) -> a) -> (a -> a)))
S1 = λ s z . (s (λ s z . z))
S2 : (∀ (r : *) . ((∀ (r : *) . ((∀ (r : *) . (r -> r) -> r -> r) -> a) -> a -> a) -> a) -> a -> a)
S1 = λ s z . (s (λ s z . (s (λ s z . z))))
这只是 Scott 编码，除了我实际上是输入整个术语而不是使用递归。我注意到的是，在这种看似愚蠢的编码下，我实际上不仅可以定义 Zero 和 Succ，还可以定义O(1)Pred：
SNat
= λ (n : Nat)
-> (n *
(λ (p:*) -> (∀ (r:*) . (p -> r) -> r -> r))
(∀ (r:*) -> (r -> r) -> r -> r))
SNat_Zero
= λ (r : *)
-> λ (s : r -> r)
-> λ (z : r)
z
SNat_Succ
= λ (k : Nat)
-> λ (n : SNat k)
-> λ (r : *)
-> λ (s : (SNat k) -> r)
-> λ (z : r)
(s n)
SNat_Pred
= λ (k : Nat)
-> λ (n : SNat (Succ k))
-> λ (n (Maybe (SNat k))
(p:(SNat k) (Maybe_Just (SNat k) p))
(Maybe_Nothing (SNat k)))
注意：我只是从另一种语法中通过眼睛翻译了这个。如果出现问题，这是正确的。您可以通过克隆此 repo 并键入以下内容来运行它：
cd calculus-of-constructions
npm i -g
cd lib
coc type SNat_Pred
coc norm SNat_Pred
这是可能的，因为我的实现有某种错误，还是我误解了所述证明的存在？
我不能很好地理解你的编码试图做什么。但是您的存储库似乎具有以下定义（从文件Nat.coc和 中以类似 Coq 的语法翻译SNat.coc）：
Definition Nat :=
forall X : *, (X -> X) -> X -> X.
Definition SNat :=
fun n : Nat => n * (* Some more stuff *).
如果我理解正确， 的定义SNat是使用自然数n来迭代类型为 的函数* -> *。这似乎不是很好的类型，因为n将 type 的东西作为参数*，因此需要* : *，这在 CoC 中是无效的。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句