S'il est impossible d'avoir O (1) pred sur CoC, alors pourquoi cela fonctionne-t-il?

Question

J'ai toujours supposé qu'il avait été prouvé que pred n'était pas exprimable en temps constant sur le Calcul des Constructions pour tout codage de types de données. Maintenant, l'esprit ce codage pour 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)))) 

C'est juste l'encodage Scott, sauf que je tape en fait toute la durée au lieu d'utiliser la récursivité. Ce que je remarque est, sous ce codage apparemment stupide, je suis en fait capable de définir non seulement zéro et Succ, mais aussi 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))) 

Note: Je viens traduisit par l'œil d'une autre syntaxe. Au cas où quelque chose ne va pas, this est correct. Vous pouvez l'exécuter en clonant cette prise en pension et en tapant:

cd calculus-of-constructions 
npm i -g 
cd lib 
coc type SNat_Pred 
coc norm SNat_Pred 

Est-ce possible parce que ma mise en œuvre a une sorte de bug, ou étais-je trompé sur l'existence de cette preuve?

Answer 1

Je ne comprends pas très bien ce que votre encodage essaie de faire. Mais votre dépôt semble avoir les définitions suivantes (traduites dans la syntaxe Coq comme des fichiers Nat.coc et SNat.coc):

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

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

Si je comprends bien, la définition de SNat utilise le nombre naturel n pour itérer une fonction de type * -> *. Cela ne semble pas bien typé, car n prend comme argument quelque chose de type *, nécessitant ainsi * : *, ce qui n'est pas valide dans CoC.