4
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ It would help if you said that you're adding recursive types, not just any kind of recursion. Or did I misunderstand you? $\endgroup$ – Andrej Bauer Jan 5 '18 at 7:37
  • 3
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jan 5 '18 at 7:39
  • 4
    $\begingroup$ 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? $\endgroup$ – Blaisorblade Jan 5 '18 at 7:39
  • 1
    $\begingroup$ 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. $\endgroup$ – MaiaVictor Jan 5 '18 at 9:33
  • 2
    $\begingroup$ 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. $\endgroup$ – Sebastian Graf Jan 5 '18 at 13:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.