1
votes

I always assumed it had been proven that pred wasn't expressible in constant time on the Calculus of Constructions for any encoding of datatypes. Now, mind this encoding for 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))))

That's just the Scott encoding, except I'm actually typing the whole term instead of using recursion. What I noticed is, under this seemingly stupid encoding, I'm actually able to define not only Zero and Succ, but also 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: I just translated this by eye from another syntax. In case something is wrong, this is correct. You can run it by cloning this repo and typing:

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

Is this possible because my implementation has some kind of bug, or was I mistaken about the existence of said proof?

1
Your SNat_Succ doesn't use z. That can't be right.Daniel Wagner
Did you mean to have S2 = ... on the 6th line?Arthur Azevedo De Amorim
I also vaguely remember that there is an encoding of the natural numbers in the pure lambda calculus that does allow one to program an O(1) predecessor function, but I can't find a reference...Arthur Azevedo De Amorim
@DanielWagner How so? The Scott-encoded Succ is just λ n s z . (s n) so it, too, doesn't use z.MaiaVictor
@ArthurAzevedoDeAmorim yes, thanks.MaiaVictor

1 Answers

8
votes

I cannot understand very well what your encoding is trying to do. But your repository seems to have the following definitions (translated in Coq-like syntax from the files Nat.coc and SNat.coc):

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

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

If I understand correctly, the definition of SNat is using the natural number n to iterate a function of type * -> *. This doesn't seem well-typed, because n takes as an argument something of type *, thus requiring * : *, which is not valid in CoC.