Termination checking with --prop: change in 2.6.4 compared with 2.6.3

[amp12]

Termination checking with --prop: change in 2.6.4 compared with 2.6.3

[jespercockx]

Thinking about this a bit more, the problem only seems to be when we use induction on Prop to define something in Set, which is indeed already not allowed. Since we never need to reduce things in Prop, it should be fine to allow recursion on Prop types as long as the target is also in Prop. So maybe I was a bit too quick to close this issue.

There is a different problem with this when we add impredicative prop as the example by @plt-amy shows. But since we have not (yet) implemented impredicative Prop in Agda this is only a hypothetical problem.

So my hypothesis at the moment is that recursion on inductive Props is consistent but a non-conservative extension, which happens to be inconsistent with impredicativity. Perhaps we could allow this under a flag.

[nad]

I think users should be allowed to disable principles that would be incompatible with impredicativity.

I think the default should be that they are disabled, unless this breaks too much code.

[andreasabel]

I think this PR is responsible for this change:

• #6639

@plt-amy wrote:

This change makes it so that DontCare is always assigned the unknown ordering in the termination checker. This means that irrelevant and propositional arguments are never considered structurally smaller than their corresponding patterns.

In other words, you cannot recurse on inductive propositions.
If I think about it, this sounds quite radical.

Amelia, could you have a look?

[andreasabel]

Here is an analysis of Acc-in-Prop via sized types, which is accepted by the termination checker:

module wf-Prop-Sized {l : Level}{A : Set l}(R : A → A → Prop l) where

  -- Accessibility predicate
  data Acc (i : Size) (x : A) : Prop l where
    acc : (j : Size< i) (α : ∀ y → R y x → Acc j y) → Acc i x

  -- Well-foundedness
  iswf : Prop l
  iswf = ∀ x → Acc ∞ x

  -- Well-founded induction
  ind :
    {n : Level}
    (w : iswf)
    (B : A → Prop n)
    (b : ∀ x → (∀ y → R y x → B y) → B x)
    → -----------------------------------
    ∀ x → B x
  ind w B b x = Acc→B ∞ x (w x)
    where
    Acc→B : ∀ i x → Acc i x → B x
    Acc→B i x (acc j α) = b x (λ y r → Acc→B j y (α y r))

So the intuition is that Acc can be sliced into layers Acc i each of which is a strict proposition, but the layering still justifies well-founded induction.

Thus, I think that the unsized Acc-in-Prop should also be accepted, and this is a real regression in 2.6.4.

[jespercockx]

Having an accessibility predicate in Prop that you can recurse on leads to undecidable typechecking, doesn't it?

[amp12]

@jesper: can you elaborate that thought? (something from the recent literature on proof irrelevant types of proposition in Type Theory, perhaps?)

[jespercockx]

We actually have a counterexample in section 2.3 of our paper on sProp: https://dl.acm.org/doi/pdf/10.1145/3290316

[amp12]

I don't understand. I thought Agda's Prop implemented the suggestions in your paper that you cite. The example I mentioned in my bug report conforms to restrictions on how Props can be eliminated, in that it type checks in 2.6.3. The change from 2.6.3 to 2.6.4 that is causing this example to be rejected was not made in order to repair undecidability of type checking in 2.6.3 was it?

[jespercockx]

There was indeed a bug in 2.6.3 that caused the termination checker to erroneously consider Prop arguments which it shouldn't, and this got fixed by Amy in #6639. There is also an example of why this needed fixing in that PR (though it seems it was not added to the test suite @plt-amy).

Basically Prop is not the right tool for aiding Agda's termination checker. You can either use sized types as Andreas suggests, or use an accessibility predicate in Set (possibly with an @0 annotation so it gets erased from the compiled code).

[andreasabel]

@jespercockx: I will add the example in the OP #6639 to the testsuite.

Could you spell out the counterexample from your paper in Agda?
I am looking at the Acc_rect example (p7), but this is already forbidden in Agda due to missing singleton-elimination:

module wf-Prop {l : Level}{A : Set l}(R : A → A → Prop l) where

  -- Accessibility predicate
  data Acc (x : A) : Prop l where
    acc : (∀ y → R y x → Acc y) → Acc x

  inv : ∀ {x} (a : Acc x) y (lt : R y x) → Acc y
  inv (acc α) = α

  -- Well-foundedness
  iswf : Prop l
  iswf = ∀ x → Acc x

  -- Well-founded induction
  module WF
    {n : Level}
    (w : iswf)
    (B : A → Set n)
    (b : ∀ x → (∀ y → R y x → B y) → B x)
    where

    {-# TERMINATING #-}
    Acc-rect : ∀ x → Acc x → B x
    Acc-rect x (acc α) = b x (λ y r → Acc-rect  y (α y r))

Agda complains about Acc-rect:

Cannot split on datatype in Prop unless target is in Prop
when checking that the pattern acc α has type Acc x

[andreasabel]

I think #6639 was too eager in the sense that it disallows all recursion on proofs, not just those recursion schemes that would be incompatible with impredicativity.
A sufficient restriction for impredicativity would be to remove c h > h args from the structural ordering of proofs. This would remove Acc-induction as well, though. There are restrictions that would allow impredicativity and Acc-induction (as I demonstrate by the analysis using sized types), but these criteria are not as easy to implement.

While we do not have impredicativity for Prop, I would simply revert #6639.
Don't cross your bridges before you come to them.

[plt-amy]

It does not make sense to use the untyped structural order we use for sets to decide whether a recursive function on props is acceptable. If two props have the same type, how can one be said to be less than the other, when they're definitionally equal? However, in the accessibility case above, this is actually justified by the elimination principle, but the termination checker detects this essentially by accident. Hotfixes like

A sufficient restriction for impredicativity would be to remove c h > h args from the structural ordering of proofs

simply add yet more patchwork onto the ever-increasing pile we have to maintain to relate the structural-smallness relation to what is actually allowed by the induction principles. Of course having precise termination checking would necessarily be more conservative than what we have today; so it might make sense to keep the old behaviour under a flag. But it should not be the default.

[andreasabel]

@plt-amy wrote:

If two props have the same type, how can one be said to be less than the other, when they're definitionally equal?

Couldn't something similar be said about pattern matching on proofs? If all proofs are the same, how can you match on one?
The justification here is that in the end it does not matter which proof you had, because the result is proof-irrelevant again (as Prop can only be eliminated into Prop).

Why wouldn't this principle carry over to recursion?

• in pattern matching, you are using a distinction between constructors that "isn't really there" (because all proof are equal)
• in recursion, you are using the inductive structure that "isn't really there either" (because all proofs are equal)

So, the justification is, I'd say, that it is fine to be more intensional than definitional equality (for pattern matching and recursion), if you never violate the quotienting induced by the definitional equality.

What flags are concerned, I'd rather wait for the --impredicative-prop and bundle the changes needed for this feature under this flag.

[plt-amy]

Couldn't something similar be said about pattern matching on proofs? If all proofs are the same, how can you match on one?

Sure, I think that defining any sort of inductive Prop is a bit silly. But we can define those, and they do make sense, and they have induction principles, which, at least in theory, and, in my understanding, we're trying to capture. The coverage checker accurately does its job to make sure that a definition by cases would provide enough to fill in the arguments to the induction principle, so I'm not proposing we remove that entirely.

But the termination checker inaccurately does its job, and only accidentally guarantees that we make justifiable recursive calls — as evidenced by its failure when we introduce impredicativity. In my understanding, if the termination checker was correct about the base theory, then it would still be correct after passing to a consistent extensions (like impredicativity!).

What flags are concerned, I'd rather wait for the --impredicative-prop and bundle the changes needed for this feature under this flag.

So maybe it's fine if we don't by default implement a theory of "Prop + inductives" that is being gestured towards (which would be compatible with impredicativity), but I think users should be able to control this.
In the same way that --without-K was implemented before univalence became a theorem, I think users should be allowed to disable principles that would be incompatible with impredicativity. (It's possible today to postulate propositional resizing, even definitionally, using rewrite rules.)

[andreasabel]

Ok, then what's the flag name? --prop-recursion?

[andreasabel]

I think users should be allowed to disable principles that would be incompatible with impredicativity.

I think the default should be that they are disabled, unless this breaks too much code.

I presented the problem in today's ProgLog meeting. Some outcomes of the discussion:

1. The deeper problem in the termination checker that it does not distinguish between recursive constructor arguments (those contain subtrees in the same type or one of the mutual types and thus can be used as termination argument) and non-recursive ones (those that contain subtrees in unrelated types). If we keep track of this distinction, the impredicativity counterexample goes away (and maybe some other dubious recursion schemes).
2. The usual eliminators for inductive data should be definable without flags. They are part of the core type theory and compatible with all models. In particular, Acc-induction is the standard eliminator for inductive Acc in Prop, so it should be definable without extensions.

These arguments lead me back to my old position: Revert to 2.6.3's behavior, do not require a flag for recursion on proofs.

We should still think of an implementation of the separation between recursive and non-recursive arguments (point 1). This is done in Coq's termination checker, e.g.
The we can allow impredicative Prop without further modification to termination checking.

[plt-amy]

This is something I'm interested in researching, but I think it's an open problem. In particular, I'm not aware of any schema in the literature for translating structural pattern matching on higher inductive(-inductive) types to eliminators; such a schema would IMO be necessary to inform a correct implementation of termination checking.

It's also very fiddly even before we get that far into the weeds:

data List (A : Set) : Set where
  [] : List A
  cons : ((b : Bool) → if b then A else List A) → List A

I won't be able to write map before I have to log into the meeting, but we investigated this in the last AIM and found that Agda does accept it (and I find it hard to disagree with it here!). So if we want more precise termination checking, either it has to be very fancy indeed, or it'll cut down the space of types we can express; this might be a pretty significant restriction, but in fairness, it's possible that it's fine.

The usual eliminators for inductive data should be definable without flags.

This is a very good point.

[andreasabel]

@amp12: Thanks for the alert, we will revert the behavior here to the one of Agda 2.6.3.