6
$\begingroup$

In https://dl.acm.org/doi/10.1145/3290316 section 4 (which I believe is a standard reference), the authors claimed that Voevodsky's propositional resizing rule justifies the consistency of an impredicative strict Prop. This is also how it is implemented in Coq. Then, in section 6.5, Agda said the termination checker assumes predicativity and hence it's problematic to be impredicative. I don't understand that. I don't see the relation between termination checking and predicativity.

So, how does that affect predicativity?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
7
$\begingroup$

After some research I have found a counterexample by Jesper Cockx:

data ⊥ : Prop where

data Bad : Prop where
  b : ((P : Prop) → P → P) → Bad

bad : Bad
bad = b (λ P p → p)

no-bad : Bad → ⊥
no-bad (b x) = no-bad (x Bad bad)

very-bad : ⊥
very-bad = no-bad bad

It looks like the recursion no-bad (x _) should be forbidden.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I love this counter-example! I wonder where it originated (I remember seeing a similar one long ago...) $\endgroup$
    – cody
    Commented Oct 26, 2022 at 18:33
  • 2
    $\begingroup$ @cody The example is in A Predicative Analysis of Structural Recursion by Abel and Altenkirch, which I think Agda's checker is based on. Just before, they cite Pattern Matching with Dependent Types by T. Coquand from 1992, so that might be the actual origin. I can't find a copy of the latter, though. $\endgroup$
    – Dan Doel
    Commented Oct 26, 2022 at 21:46
  • 1
    $\begingroup$ Thanks @DanDoel! Looks like the Coquand paper (wonks.github.io/type-theory-reading-group/papers/…) actually does contain the counter-example on Page 4. $\endgroup$
    – cody
    Commented Oct 28, 2022 at 21:09

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