Coinduction incompatible with univalence [WAS: Structural termination order incompatible with univalence] #1023
Comments
|
Attached my version of --without-K (as discussed in issue #865) if you want to try (and break) it. Original comment by Attachments: |
|
Here is an adaption of Maxime Denes coinduction version (from the coq list): open import Common.Coinduction
open import Common.Equality
prop = Set
data False : prop where
data CoFalse : prop where
CF : False → CoFalse
data Pandora : prop where
C : ∞ CoFalse → Pandora
postulate
ext : (CoFalse → Pandora) → (Pandora → CoFalse) → CoFalse ≡ Pandora
out : CoFalse → False
out (CF f) = f
foo : CoFalse ≡ Pandora
foo = ext (λ{ (CF ()) })
(λ{ (C c) → CF (out (♭ c))})
loop : CoFalse
loop rewrite foo = C (♯ loop)
false : False
false = out loop
Original comment by
|
|
Simplified version: open import Common.Coinduction
open import Common.Equality
prop = Set
data False : prop where
data Pandora : prop where
C : ∞ False → Pandora
postulate
ext : (False → Pandora) → (Pandora → False) → False ≡ Pandora
foo : False ≡ Pandora
foo = ext (λ()) (λ{ (C c) → ♭ c })
loop : False
loop rewrite foo = C (♯ loop)
Original comment by |
|
The coinduction version doesn't seem to have anything to do with coinduction, open import Relation.Binary.PropositionalEquality
data Zero : Set where
data WOne : Set where wrap : (Zero → WOne) → WOne
FOne = Zero → WOne
postulate
iso : WOne ≡ FOne
foo : WOne → Zero
foo (wrap f) rewrite (sym iso) = foo f
BOOM : Zero
BOOM = foo (wrap (λ ()))It seems that 'rewrite' also relies implicitly on K. Actually this is not very surprising because it doesn't look at the contents of the equality proof, so it just assumes they are all Original comment by |
open import Common.Equality
data Zero : Set where
mutual
data WOne : Set where wrap : FOne → WOne
FOne = Zero → WOne
postulate
iso : WOne ≡ FOne
foo : WOne → Zero
foo (wrap f) = aux FOne iso f
where
aux : (A : Set) → (WOne ≡ A) → A → Zero
aux .WOne refl f = foo f
BOOM : Zero
BOOM = foo (wrap (λ ()))
Is this rejected by your version of --without-K?Original comment by |
Original comment by |
|
Rewrite is not desugared in the termination checker since the fix of issue #59 (which is a recent one, therefore not yet released officially). See Agda.Termination.TermCheck: -- | Extract recursive calls from one clause.
termClause :: Clause -> TerM Calls
termClause clause = do
name <- terGetCurrent
ifM (isJust <$> do isWithFunction name) (return mempty) $ do
mapM' termClause' =<< do liftTCM $ inlineWithClauses name clause
termClause' :: Clause -> TerM CallsYou can simply skip the inlining in your version of --without-K and see if you obtain the desired results then. Original comment by |
Original comment by |
|
As I see from your patch, you simply mask out all patterns which are not obviously of a data (or record) type. However, this might be too simplistic in the presence of large eliminations, e.g. T : Bool -> Set
T true = Nat
T false = List Nat
f : (x : Bool) -> T x -> Set
f true zero = Nat
f true (suc x) = f true x
f false nil = Nat
f false (x :: xs) = f false xsHere, the second argument is of type "T x" which is not detectable as data type without instantiating x. Maybe we rather want the following: Type check patterns again, but without doing any kind of unification. Only do reduction. (This might actually be a (rather) simple left-to-right traversal through the patterns, because it means that dot-pattern values can never contribute to reducing types.) Every pattern and subpattern which then gets a data or record type is eligible to contribute to termination, the others are not. We will lose the following function then: f : (x : Bool) -> T x -> x \equiv false -> Set
f .false zero refl = Nat
f .false (suc n) refl = f false n reflIs it justified to reject this function with --new-without-K? Original comment by |
|
I'm not sure I understand what you mean by "type check patterns again without unification". Can you explain how this would help in the (first) definition of f? Alternatively, we could define f as f : (x : Bool) -> T x -> Set
f true = ftrue
where
ftrue : Nat -> Set
ftrue zero = Nat
ftrue (suc x) = ftrue x
f false = ffalse
where
ffalse : List Nat -> Set
ffalse nil = Nat
ffalse (x :: xs) = ffalse xsThis is accepted by my patch because it makes it clear to the termination checker that there are actually two separate functions here, and each one is doing recursion on a different type. Maybe there is some way to automatically desugar the original definition of f into this one? The second definition of f (let's call it g) can also be desugared to g : (x : Bool) -> T x -> x ≡ true -> Set
g .true n refl = gtrue n
where
gtrue : Nat -> Set
gtrue zero = Nat
gtrue (suc n) = gtrue nOriginal comment by |
|
I meant when you type check say the second clause of f from left to right you can do completely without unification, and you get out that all patterns For g, without unification, you would derive Your desugaring can also be applied to foo: foo : WOne → Zero
foo (wrap f) = aux FOne iso f
where
aux : (A : Set) → (WOne ≡ A) → A → Zero
aux .WOne refl f = aux2 f
where
aux2 : WOne -> Zero
aux2 f = foo fUnless you mark pattern f in aux unusable, you do not reject foo. Original comment by |
|
You treatment of g should actually work, I was mistaken. So you seem to suggest maybe Agda's termination checker should work on a compiled form of pattern matching, something like the case trees, instead. A more or less straightforward translation from deep to shallow pattern matching would turn g into g : (x : Bool) -> T x -> x ≡ true -> Set
g .true n refl = gtrue n
where
gtrue : Nat -> Set
gtrue zero = Nat
gtrue (suc n) = g true n reflTo arrive at your form, one would have to "tighten the loop" and see that "g Original comment by |
|
|
The main problem with my patch seems to be that it is too restrictive. Since it is better to have a restrictive solution than having none, I propose to enable it anyway for the release of 2.3.4, but only when --without-K is enabled (if you have K then there is no problem). I'm attaching a patch against the current darcs version that does this. This will give us some time to work out a more principled solution (hopefully). Original comment by Attachments: |
|
Pushed this. Needs entry in ChangeLog! Original comment by
|
|
Original comment by
|
On a personal branch of the standard library using the --without-K option, I needed to add the Original comment by |
|
Original comment by
|
|
I'm a little unclear about what the status of this one is. Do we know what needs to be done to the termination checker to make it less restrictive together with --without-K? I'm a little reluctant to tag issues with specific I'll remove the milestone for now. Original comment by
|
|
The original issue has been fixed, the remainder is an enhancement request for a more liberal fix. Original comment by
|
|
After fixing issue #1259, the problem with coinduction (comment 3) is back. This problem was only accidentially fixed since the termination checker did something random for with functions and --without-K. (This includes rewrite.) Also, nothing in Jesper's code addresses the guardedness check done for coinduction. I redeclare this as Defect, please open a new Enhancement issue for making the termination checker more liberal --without-K. Original comment by
|
|
Here's an adaptation of (comment 3) without 'with' or 'rewrite' (even without any mutual stuff) that exposes the problem: {-# OPTIONS --without-K #-}
open import Level
open import Common.Coinduction
open import Common.Equality
prop = Set
data False : prop where
data Pandora : prop where
C : ∞ False → Pandora
postulate
ext : (False → Pandora) → (Pandora → False) → False ≡ Pandora
f : False → Pandora
f ()
g : Pandora → False
g (C x) = ♭ x
foo : False ≡ Pandora
foo = ext f g
loop-aux : (A : Set) → A ≡ Pandora → A
loop-aux .Pandora refl = C (♯ (loop-aux False foo))
loop : False
loop = loop-aux False fooThe main problem is that AFAIK there hasn't been done any work yet on coinduction in the presence of univalence. Clearly, we need something stronger than guardedness, but it's not yet clear what it should be. I'll think about it. Original comment by |
|
Fixed by Jesper, maybe you can add (comment 22) to the test suite, in case it is not in yet. (comment 3) is in there as CoinductionAndUnivalence.agda. Original comment by
|
|
It seems that the check for the original problem can be circumvented by the identity type former as a datatype. The following proof of false typechecks on Agda version 2.6.2-c857009 {-# OPTIONS --without-K #-}
-- An empty type.
data Zero : Set where
-- A unit type as W-type.
mutual
data WOne : Set where wrap : FOne -> WOne
FOne = Zero -> WOne
-- Type equality.
data _<->_ (X : Set) : Set -> Set₁ where
Refl : X <-> X
-- This postulate is compatible with univalence:
postulate
iso : WOne <-> FOne
-- But accepting that is incompatible with univalence:
data Id (X : Set) : Set where
i : X → Id X
noo : (X : Set) -> (WOne <-> X) -> Id X -> Zero
noo .WOne Refl (i (wrap f)) = noo FOne iso (i f)
absurd : Zero
absurd = noo FOne iso (i \ ())
|
|
It seems I do not understand how the termination checker works, as I would not have expected this definition to pass the termination checker. Why is it fine to consider |
|
I re-checked our papers on pattern matching without K, and I'm pretty sure there's no way this example would be accepted by the (rather simplistic) termination criterion we're using there. So this seems to be caused by insufficient integration between the theories supporting the different features of Agda (in this case: pattern matching and termination checking). |
|
I was also a bit surprised by {-# OPTIONS --without-K #-}
data Zero : Set where
data Id (X : Set) : Set where
i : X → Id X
mutual
data WOne : Set where wrap : Id FOne -> WOne
FOne = Zero -> WOne
data _<->_ (X : Set) : Set -> Set₁ where
Refl : X <-> X
postulate
iso : WOne <-> FOne
mutual
noo : (X : Set) -> (WOne <-> X) -> Id X -> Zero
noo .WOne Refl (i (wrap f)) = noo FOne iso f
absurd : Zero
absurd = noo FOne iso (i \ ()) |
|
Do we know how this problem was addressed in Coq? |
|
I believe in Coq, constructor arguments are marked as either "recursive" or "non-recursive", and the termination checker only accepts recursive calls on arguments that come from a recursive position. In this example the argument of However, adopting such a criterion in Agda might also rule out a lot of "good" use cases, e.g. where one first defines a (non-recursive) functor and then uses a separate fixpoint construction, e.g. data Maybe (A : Set) : Set where
just : A → Maybe A
nothing : Maybe A
data Nat : Set where
inj : Maybe Nat → Nat
id : Nat → Nat
id (inj (just x)) = inj (just (id x))
id (inj nothing) = inj nothingThis is something we probably still want to accept, but (I presume) would be rejected by Coq's approach because the argument to |
|
Is their fix for the original problem of this issue also similar to what we do in Agda? Since that definition of |
|
I tried porting the example to Coq, but it seems it's not accepted: Inductive Zero : Prop := .
Inductive Id (X : Type) : Type :=
| i : X -> Id X.
Inductive One : Type :=
| wrap : Id (Zero -> One) -> One.
Inductive Equiv (X : Type) : Type -> Type :=
| Refl : Equiv X X.
Axiom iso : Equiv One (Zero -> One).
Fixpoint noo (X : Type) (eq : Equiv One X) (x : Id X) : Zero :=
(match eq in Equiv _ X return Id X -> Zero with
| Refl _ => fun x =>
match (x : Id One) with
| i _ o =>
match o with
| wrap f => noo (Zero -> One) iso f
end
end
end) x.Error message: I'm not sure what Coq exactly does here to reject the example, it seems that it somehow cares about the first argument of the recursive call to |
|
Thinking a bit more about it, the reason why Coq rejects the example is because I had to abstract over In other words, it seems that the Coq criterion can be summarized as "the type of the argument on which the function is structurally recursive cannot be refined by any pattern matches." Or perhaps a bit more refined: "the type of the argument on which the function is structurally recursive must be informative enough to access the argument used in the recursive call without any refinements from (other) pattern matches." |
|
Another way to approach the problem is by saying that we can compute in advance an infinite tree of all valid recursive calls from the type of the argument on which we are recursing. The way we construct this infinite tree is just by repeatedly case splitting on a fresh variable of this type and collecting all the possible recursive arguments generated by this process. Crucially, this should be done using the type before any refinements. Some examples:
However, using this process naively to check the validity of recursive calls could be prohibitively expensive. Maybe we can devise a cheaper way to approximate it? |
|
Oh, I see, I was under the impression Coq also had this problem, but maybe it actually was only discussed on coq-club. Unfortunately I can't seem to find the coq-club thread. |
|
Meta-comment: Please do not reopen issues whose fix has been shipped. Rather, open a new issue linking to the old one: |
Following discussions on the coq-club it was discovered that Agda's current
--without-K does not guarantee compatibility with univalence. My version of
--without-K DOES rule out the bad use of Refl in the following test case, an
argument for accepting my patch (see issue 865).
Original issue reported on code.google.com by
andreas....@gmail.comon 10 Jan 2014 at 8:27The text was updated successfully, but these errors were encountered: