CoCにO（1）predを付けることが不可能な場合、なぜこれが機能しますか？

Question

私はいつも、predは、データ型のコード化のための計算の微積分で一定の時間に表現できないことが証明されていると仮定しました。私は実際に全体の用語を入力の代わりに、再帰を使用してい除き、ちょうどスコットエンコーディングです

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)))) 

：今、NATのためにこのエンコーディングを気に。私が気づいた何、この一見愚かなエンコーディングの下で​​、私は実際にゼロと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))) 

注：私はちょうど別の構文から目でこれを翻訳します。何かが間違っている場合、thisが正しいです。私の実装では、バグのいくつかの種類を持っているので

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では無効です。