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?
SNat_Succ
doesn't usez
. That can't be right. – Daniel WagnerS2 = ...
on the 6th line? – Arthur Azevedo De AmorimO(1)
predecessor function, but I can't find a reference... – Arthur Azevedo De Amorimλ n s z . (s n)
so it, too, doesn't usez
. – MaiaVictor