5
$\begingroup$

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions.

If we assumed indNat as an axiom, is there an untyped term that would have the semantics of the induction function? What if we had Scott-encoded natural numbers and fix?

Can induction be inhabited in CoC + fix (such that the function would have the proper semantics, not an infinite loop)?

$\endgroup$
  • $\begingroup$ What type would you give to fix? $\endgroup$ – cody Jul 9 at 15:30
  • $\begingroup$ fix : (t : *) -> (t -> t) -> t $\endgroup$ – Labbekak Jul 10 at 12:12
  • $\begingroup$ The indNat would have the same erasure as the recnat right? $\endgroup$ – user833970 Sep 9 at 17:53
  • $\begingroup$ I think so yes (if you mean iteration on nats with recnat) $\endgroup$ – Labbekak Sep 9 at 20:11
5
$\begingroup$

Yes, there is such an untyped function, and it turns out that it is equivalent to the untyped erasure of iteration for church numerals.

The Cedille project has been doing lots to give types to these functions, and the core concept there is the dependent intersection, which provides a limited form of self reference that is enough to derive induction principles. This paper will probably interest you.

If you have $fix$ you can definitely implement induction principles, using structural recursion on the natural number. This is how they do it in CiC and Coq, with an extra restriction that the recursive calls must be on a structurally smaller value. Without this condition, you can write induction, but you also can write nonterminating terms with the same type as an induction principle.

$\endgroup$
  • 1
    $\begingroup$ I'm not convinced about that second comment about fix: in Coq they add a fixpoint for dependent types, not the one Labbekak seems to have in mind. I'm not sure the non-dependent one is sufficient. $\endgroup$ – cody Jul 10 at 15:32
  • 1
    $\begingroup$ However, non-dependent fix + dependent match for naturals seems to be sufficient, so now I'm not sure... $\endgroup$ – cody Jul 10 at 15:45

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.