3
$\begingroup$

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a Functor):

Fix : (* -> *) -> *
in  : ∀F. F (Fix F) -> Fix F
out : ∀F. Fix F -> F (Fix F)

We can then write down the type of case discrimination and folding:

case : ∀F T. (F (Fix F) -> T) -> Fix F -> T
fold : ∀F T. (F T -> T) -> Fix F -> T

But what is the type of induction (if there is one)? I've gotten this far:

ind : ∀F T (P : Fix F -> *). (∀(h : Fix F). P h -> P ???) -> (x : Fix F) -> P x

Assuming the rest is correct, what should be in the place of ???? Alternatively, what is the type of dependent case discrimination?

$\endgroup$
  • 1
    $\begingroup$ The word induction is used when we construct an inductive type, i.e., the smallest or initial fixed point of a type constructor $F$. However, a general type constructor need not have an initial or smallest fixed point, and therefore no reasonable induction principle can be stated in general. $\endgroup$ – Andrej Bauer Jan 28 at 17:42
  • 1
    $\begingroup$ If we let $F(X) = X \to \mathsf{Empty}$, what is $\mathsf{Fix}(F)$? $\endgroup$ – Andrej Bauer Jan 28 at 17:43
  • 1
    $\begingroup$ If we constrain F in some way (for example strictly positive occurrences of X), can we then state a induction principle? $\endgroup$ – Labbekak Jan 28 at 17:53
  • 1
    $\begingroup$ I think you need an additional constraint over $F$, namely that it is behaves well over "fibrations", i.e. that there is some function lift_fiber : forall A : *, (A -> *) -> (F A -> *). This is certainly enough to express what you need. $\endgroup$ – cody Jan 28 at 20:37
  • 2
    $\begingroup$ @cody: right, and we don't need any strict positivity, just covariance, in order to phraase the induction principle. $\endgroup$ – Andrej Bauer Jan 28 at 20:45
2
$\begingroup$

To answer my own question, the paper Generic derivation of induction for impredicative encodings in Cedille shows a type for induction on a fixpoint type. It can look like:

ind : ∀F T (P : Fix F -> *). ((h : F (Σ (Fix F) P)) -> P (in (map fst h))) -> (x : Fix F) -> P x

With Σ being the dependent product and map the functor map of F.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Just a note, having this Fix type is not enough to derive induction for inductive datatypes like Nat or List. You'd also need an induction principle for F. If F is constructed from unit, sums and products then you'd need induction principles for those. $\endgroup$ – Labbekak Feb 11 at 11:34

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.