Induction-recursion in Impredicative Type Theory

When building universes in a type theory, the standard technique relies on induction-recursion, but Kovács points out that the logical consistency of induction-recursion and induction-induction in the context of impredicative type theory is an open question.

Lastly, we do not handle impredicative universes. The main reason for this is that we do not know the consistency of having induction-recursion and impredicative function space together in the same universe, and modeling impredicativity seems to require this assumption in the metatheory.

Here I will not be providing a mechanized proof, as that is still a work in progress, but two techniques to justify mutual definitions in type theories. The running example will be the following mutual definition, where N depends on the value of x.

x : A;
y : B;

x = M;
y = N;

A transformation that almost works

By ignoring the types, mutual recursion can always be reduced to simple recursion while preserving positivity and erasability, as in the following.

x : A;
x =
  y : B;
  y = N;
  M;

y : B;
y = N;

The main issue with this is that it fails to type-check if N depends on x being M, which is a common situation in induction-recursion.

Can we type that?

By making the fixpoint stronger, such that the value is known while typing the fixpoint, the transformation above is well typed.

My general argument is that many(all?) occurrences of mutual recursion are just a decomposition of the derivation tree of this fixpoint.

// this acts like a hypothesis
Γ, x == M |- M : A  Γ, x == M |- N : B
------------------------------------------
Γ |- (x : A; x = M; N) : (x : A; x = M; B)

// then the following is well typed
// even if N depends on x being M
x : A;
x =
  y : B;
  y = N;
  M;

y : B;
y = N;

Is such a fixpoint logically consistent?

While I think typing with such a fixpoint is undecidable, I believe it is logically consistent.

One way to justify it is that, if we limit ourselves to CoC, there is a normalization preserving erasure to System Fω with fixpoints where the fixpoint no longer has the dependency. This should work because the hypothesis provided by the fixpoint is used only in erasable ways.

Another way is that self types with normal fixpoints seem to allow the insanely dependent fixpoint to be rebuilt, but that may be a big transformation.

A third justification, which I have not explored in depth, is that equality reflection seems to allow this fixpoint to be rebuilt from the weak one.

An alternative way

There is also another transformation that works here without relying on this fixpoint, but instead by relying on self types directly. These self types are similar to the ones used in the original self types paper.

While the original self types are Curry-style, here I will be using a Church-style presentation, but the proof of normalization should remain essentially the same.

This transformation makes it hard to check positivity, but this can be worked around in many ways it acts more as a way of justifying the fixpoint above.

Γ, x : @(x) -> T |- T : Prop
---------------------------- // self
Γ |- @(x) -> T : Prop

Γ, x : @(x) -> T |- M : T
-------------------------- // fix / fold
Γ |- @(x) => M : @(x) -> T

Γ |- M : @(x) -> T
------------------- // unfold
Γ |- @M : T[x := M]

// this is well typed
m_x : @(m_x) -> (m_y : @(m_y) -> (x = @m_x(m_y); B)) -> A
  = @(m_x) => (m_y) => (x = @m_x(m_y); y = @m_y(m_x); M);

m_y : @(m_y) -> (x = @m_x(m_y); B)
  = @(m_y) => (x = @m_x(m_y); y = @m_y(m_x); N);

x : A = @m_x(m_y);
x : B = @m_y;

Conclusion

I want this to be quite short, so I did not go into more detail, but there is more to explore. My guess is that equality reflection may also be enough with a simple fixpoint.

EduardoRFS/impredicative_induction.md