如果不可能在CoC上使用O(1)pred,那么为什么这样做呢？

Question

我一直认为已经证明,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))))

这只是斯科特编码,除了我实际上键入整个术语而不是使用递归.我注意到的是,在这个看似愚蠢的编码下,我实际上不仅可以定义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

这是可能的,因为我的实现有某种错误,或者我错误地认为存在所述证据？

Answer 1

我无法理解你的编码尝试做什么.但是,你的资料库似乎有以下定义(翻译从文件勒柯克的语法Nat.coc和SNat.coc):

Definition Nat :=
  forall X : *, (X -> X) -> X -> X.

Definition SNat :=
  fun n : Nat => n * (* Some more stuff *).

如果我理解正确,定义SNat是使用自然数n来迭代类型的函数* -> *.这似乎不是很好的类型,因为n作为一个类型的参数*,因此需要* : *,这在CoC中是无效的.