# Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms:

Γ |- µ x . a : *    Γ |- b : *    Γ |- a [a/x] == b
---------------------------------------------------
Γ |- a == b


And such that applying a recursive term to an argument unrolled it:

((µ x . a : T) q) ~> (a[a/x] q)


It seems that even that way, deriving induction wouldn't be possible. I've attempted the following (using Morteish syntax):

NAT =
∀ (P : *) ->
∀ (Zero : P) ->
∀ (Succ : NAT -> P) ->
P

Zero =
λ (P : *) ->
λ (Zero : P) ->
λ (Succ : NAT -> P) ->
Zero

Succ =
λ (n : NAT) ->
λ (P : *) ->
λ (Zero : P) ->
λ (Succ : NAT -> P) ->
Succ n

induction =
λ (P : NAT -> *) ->
λ (Z : P Zero) ->
λ (S : ∀ (n : NAT) -> P n -> P (Succ n)) ->
λ (n : NAT) ->
n (P n) Z (λ (pred : NAT) -> S n (induction P Z S pred))


The problem here is that, when pattern-matching n on the definition of induction, we need to specify a return type. By specifying it to be P n, we get an error because, on the first case,

Z : P Zero


But should be:

Z : P n


And, on the second case,

(λ (p : NAT) -> S p (induction P Z S p)) : ∀ (p : NAT) -> P (Succ p)


But should be:

(λ (p : NAT) -> S p (induction P Z S p)) : ∀ (x : NAT) -> P n


The source of the problem seems to be that the system doesn't recognize that the following holds:

case n of
Zero   -> ... here, n == Zero   ...
Succ p -> ... here, n == Succ p ...


Or, in other words, after pattern matching a variable n : NAT as Zero, the system doesn't understand that n equals Zero. Similarly, it doesn't understand that Succ (pred n) == n. Is there any inherent reason for that, and is there any further extension that would allow this to check?

• It would help if you said that you're adding recursive types, not just any kind of recursion. Or did I misunderstand you? – Andrej Bauer Jan 5 '18 at 7:37
• If you allow unrestricted recursive types, I would imagine you can cook up some sort of a "paradox" that allows you to inhabit every type. – Andrej Bauer Jan 5 '18 at 7:39
• Note what you added is not a correct version of the fixpoint operator $\mu$: instead of $a [a/x]$ you’d need $a [\mu x.a/x]$! Also, it’s only at the level of proper types (because you use it at type *). But then, it seems not to be “primitive recursion”, because there’s no termination checking. The more I look at it, the more it looks like an incorrect version of Stump’s paper I just cited; you’re learning why careless variants of what Stump does don’t work, unlike what he does. Maybe that’s a step to understanding his work? – Blaisorblade Jan 5 '18 at 7:39
• Well in fact I got to this situation by trying to understand the CDLE paper (a follow up to the Self-types paper), and what justifies the things he did. I still don't get why all his primitives would be necessary for that, though, nor how a type being able to refer to its typed value helps here, but I'm making progress, I guess. I'll think more about that tomorrow when I'm less tired. – MaiaVictor Jan 5 '18 at 9:33
• As per TAPL, fix = λf:T→T. (λx:(µA.A→T). f (x x)) (λx:(µA.A→T). f (x x)) is well-typed, so as @Andrej Bauer pointed out, this has far-reaching consequences. – Sebastian Graf Jan 5 '18 at 13:12