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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.