-
Notifications
You must be signed in to change notification settings - Fork 339
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Termination checking with --prop: change in 2.6.4 compared with 2.6.3 #6930
Comments
I think this PR is responsible for this change: @plt-amy wrote:
In other words, you cannot recurse on inductive propositions. Amelia, could you have a look? |
Here is an analysis of 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 Thus, I think that the unsized Acc-in-Prop should also be accepted, and this is a real regression in 2.6.4. |
Having an accessibility predicate in |
@jesper: can you elaborate that thought? (something from the recent literature on proof irrelevant types of proposition in Type Theory, perhaps?) |
We actually have a counterexample in section 2.3 of our paper on |
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? |
There was indeed a bug in 2.6.3 that caused the termination checker to erroneously consider Basically |
@jespercockx: I will add the example in the OP #6639 to the testsuite. Could you spell out the counterexample from your paper in Agda? 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
|
Thinking about this a bit more, the problem only seems to be when we use induction on 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 So my hypothesis at the moment is that recursion on inductive |
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. While we do not have impredicativity for |
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
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. |
@plt-amy wrote:
Couldn't something similar be said about pattern matching on proofs? If all proofs are the same, how can you match on one? Why wouldn't this principle carry over to recursion?
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 |
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!).
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. |
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:
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. |
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
This is a very good point. |
@amp12: Thanks for the alert, we will revert the behavior here to the one of Agda 2.6.3. |
The following code contains two modules:
wf-Set
: a standard definition of well-founded induction using elements ofSet
as propositionswf-Prop
: a standard definition of well-founded induction using elements ofProp
as propositionswf-Set
checks with Agda 2.6.3 and with Adga 2.6.4wf-Prop
checks with Agda 2.6.3, but fails with Agda 2.6.4 (the functionAcc→B
fails the termination checker).I know 2.6.4 is not backwards compatible with 2.6.3, but I can't work out which new feature, if any, is causing the failure of termination checking.
The text was updated successfully, but these errors were encountered: