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

<pre><code>Γ |- µ x . a : *    Γ |- b : *    Γ |- a [a/x] == b
---------------------------------------------------
Γ |- a == b
</code></pre>

<p>And such that applying a recursive term to an argument unrolled it:</p>

<pre><code>((µ x . a : T) q) ~&gt; (a[a/x] q)
</code></pre>

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

<pre><code>NAT =
  ∀ (P : *) -&gt;
  ∀ (Zero : P) -&gt;
  ∀ (Succ : NAT -&gt; P) -&gt;
  P

Zero =
  λ (P : *) -&gt;
  λ (Zero : P) -&gt;
  λ (Succ : NAT -&gt; P) -&gt;
  Zero

Succ =
  λ (n : NAT) -&gt;
  λ (P : *) -&gt;
  λ (Zero : P) -&gt;
  λ (Succ : NAT -&gt; P) -&gt;
  Succ n

induction =
  λ (P : NAT -&gt; *) -&gt;
  λ (Z : P Zero) -&gt;
  λ (S : ∀ (n : NAT) -&gt; P n -&gt; P (Succ n)) -&gt;
  λ (n : NAT) -&gt;
  n (P n) Z (λ (pred : NAT) -&gt; S n (induction P Z S pred))
</code></pre>

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

<pre><code>Z : P Zero
</code></pre>

<p>But should be:</p>

<pre><code>Z : P n
</code></pre>

<p>And, on the second case,</p>

<pre><code>(λ (p : NAT) -&gt; S p (induction P Z S p)) : ∀ (p : NAT) -&gt; P (Succ p)
</code></pre>

<p>But should be:</p>

<pre><code>(λ (p : NAT) -&gt; S p (induction P Z S p)) : ∀ (x : NAT) -&gt; P n
</code></pre>

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

<pre><code>case n of
  Zero   -&gt; ... here, n == Zero   ...
  Succ p -&gt; ... here, n == Succ p ...
</code></pre>

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

CC BY-SA 3.0
2018-01-05T02:33:51.430Z
[Related discussion](https://i.imgur.com/HjMeklb.png) on #coq at Freenode.
MaiaVictor
CC BY-SA 3.0
2018-01-05T07:30:19.737Z
The trouble you’re facing is with implementing dependent pattern matching; Aaron Stump’s recent papers discuss this and related problems; in particular this is discussed in “Self Types for Dependently Typed Lambda Encodings”, Sec. 2.1.
Blaisorblade
CC BY-SA 3.0
2018-01-05T07:37:56.870Z
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
CC BY-SA 3.0
2018-01-05T07:39:22.937Z
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
CC BY-SA 3.0
2018-01-05T07:39:57.477Z
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
CC BY-SA 3.0
2018-01-05T09:33:32.300Z
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
CC BY-SA 3.0
2018-01-05T13:12:07.503Z
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
<type-theory><lambda-calculus><functional-programming><automated-theorem-proving>
Is it possible to derive induction by extending CoC with recursion?
MaiaVictor
# Is it possible to derive induction by extending CoC with recursion?

(Asked by: username_0 on 2018-01-05)

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?

**Tags:** type-theory, lambda-calculus, functional-programming, automated-theorem-proving
> **Comments:**
> **username_0**: [Related discussion](https://i.imgur.com/HjMeklb.png) on #coq at Freenode.  
> **username_1**: The trouble you’re facing is with implementing dependent pattern matching; Aaron Stump’s recent papers discuss this and related problems; in particular this is discussed in “Self Types for Dependently Typed Lambda Encodings”, Sec. 2.1.  
> **username_2**: It would help if you said that you're adding *recursive types*, not just any kind of recursion. Or did I misunderstand you?  
> **username_2**: 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.  
> **username_1**: 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?  
> **username_0**: 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.  
> **username_3**: 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.  

---

## 0 answers

