[Agda] list equality decision procedure fails termination check
with Agda 2.4.0.1?
Dan Licata
drl at cs.cmu.edu
Tue Jul 15 03:09:49 CEST 2014
Regarding the differences between what I'm writing by hand and what with desugars to, one funny thing is that if I move exactly the same function outside of a 'where' then it checks, but if I put it in a where, it doesn't.
Doesn't check:
<=-to-+ : ∀ {n m} -> tlp n <=tl tlp m -> Σ \ k -> tlp (n +pn k) ≃ tlp m
<=-to-+ {n}{m} (Inr p) = 0 , p ∘ ap tlp (+pn-rh-Z n)
<=-to-+ {One} {One} (Inl (ltSR (ltSR (ltSR ()))))
<=-to-+ {S n} {One} (Inl lt) = Sums.abort( pos-not-<=0 n (Inl (lt-unS lt)))
<=-to-+ {n} {S n'} (Inl lt) = <=-to-+-cases {n}{n'} (lt-unS-right lt) (<=-to-+ {n} {n'}) where
-- FIXME: needed to move this outside to work around without-K termination restriction
<=-to-+-cases : ∀ {n n'} →
(tlp n <=tl tlp n') →
( (tlp n <=tl tlp n') → Σe Nat (λ k → Id (tlp (n +pn k)) (tlp n'))) →
Σe Nat (λ k → Id (tlp (n +pn k)) (S (tlp n')))
<=-to-+-cases {n}{n'}(Inr eq) f = S Z , (ap S eq) ∘ ap (S o tlp) (+pn-rh-Z n) ∘ ap tlp (+pn-rh-S n Z)
<=-to-+-cases {n} (Inl lt') f with f (Inl lt')
... | (n'' , eq''') = S n'' , ap S eq''' ∘ ap tlp (+pn-rh-S n n'')
Checks:
<=-to-+-cases : ∀ {n n'} →
(tlp n <=tl tlp n') →
( (tlp n <=tl tlp n') → Σe Nat (λ k → Id (tlp (n +pn k)) (tlp n'))) →
Σe Nat (λ k → Id (tlp (n +pn k)) (S (tlp n')))
<=-to-+-cases {n}{n'}(Inr eq) f = S Z , (ap S eq) ∘ ap (S o tlp) (+pn-rh-Z n) ∘ ap tlp (+pn-rh-S n Z)
<=-to-+-cases {n} (Inl lt') f with f (Inl lt')
... | (n'' , eq''') = S n'' , ap S eq''' ∘ ap tlp (+pn-rh-S n n'')
<=-to-+ : ∀ {n m} -> tlp n <=tl tlp m -> Σ \ k -> tlp (n +pn k) ≃ tlp m
<=-to-+ {n}{m} (Inr p) = 0 , p ∘ ap tlp (+pn-rh-Z n)
<=-to-+ {One} {One} (Inl (ltSR (ltSR (ltSR ()))))
<=-to-+ {S n} {One} (Inl lt) = Sums.abort( pos-not-<=0 n (Inl (lt-unS lt)))
<=-to-+ {n} {S n'} (Inl lt) = <=-to-+-cases {n}{n'} (lt-unS-right lt) (<=-to-+ {n} {n'})
-Dan
On Jul 13, 2014, at 11:37 AM, Andreas Abel <abela at chalmers.se> wrote:
> Jesper,
>
> Concerning the "looking into Agda's desugaring of with", you could try and play around with {-# OPTIONS -v tc.with:40 #-}. Not sure whether this gives enough information. You could insert suitable reportSDoc statements into TypeChecking/Rules/Def.hs and TypeChecking/With.hs to get more information.
>
> --Andreas
>
> On 13.07.2014 15:35, Jesper Cockx wrote:
>> Maxime: To be honest, I'm not sure what the intuition behind my fix is
>> either. However, it is exactly what I need in order to apply structural
>> recursion in my translation of pattern matching to eliminators (see
>> http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf).
>> I'm afraid I don't really understand your criterion for Coq either. I
>> thought univalence was only proven sound in combination with the
>> standard eliminators, and not with sized types?
>>
>> Dan: Your examples are instances of issue 59
>> (https://code.google.com/p/agda/issues/detail?id=59), which was fixed by
>> inlining "with" and "rewrite" for the purpose of termination checking.
>> However, at least for "rewrite" this inlining actually did bad things
>> when --without-K was enabled. For example, the following was accepted in
>> 2.3.2:
>>
>> ==================================================
>> {-# OPTIONS --without-K #-}
>> 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 (λ ()))
>> ==================================================
>>
>> I'm not sure if the inlining of "with" also causes problems, but on the
>> other hand I don't have a proof that it is sound either. So I decided to
>> disable the inlining entirely (when --without-K is enabled). It would be
>> interesting to take a look at the desuraging of "with" by Agda to see
>> how they differ from your manual desugaring. Does anyone know if this is
>> possible?
>>
>> Jesper
>>
>>
>> On Wed, Jul 9, 2014 at 11:43 PM, Dan Licata <drl at cs.cmu.edu
>> <mailto:drl at cs.cmu.edu>> wrote:
>>
>> Hi Jesper,
>>
>> Today I got the development version of Agda. There are some
>> examples that I think should work. They termination-check with
>> without-K turned off but not with it on.
>>
>> See the functions tagged with
>> NO_TERMINATION_CHECK
>>
>> in
>>
>> https://github.com/dlicata335/hott-agda/blob/master/lib/Int.agda
>> https://github.com/dlicata335/hott-agda/blob/master/lib/loopspace/Truncation.agda
>>
>> One issue seems to have to do with absurd patterns; for example, if
>> I do something like this (TLevel's are like natural numbers, with -2
>> being like 0, so S - is not less than it)
>>
>> foo : {C : _} (x y : TLevel) -> x <tl y -> C
>> foo (S x) (S y) lt = foo x y {!!}
>> foo (S y) -2 lt with lt
>> foo (S y) -2 lt | ()
>> foo _ _ _ = {!!}
>>
>> then the clause with the absurd pattern fails the termination
>> checker (?).
>>
>> Another seems to have something to do with 'with'; e.g. a function
>>
>> 1<=pos : (p : Positive) → tl 1 <=tl (tlp p)
>> 1<=pos One = Inr id
>> 1<=pos (S n) with 1<=pos n
>> ... | Inl lt = Inl (ltSR lt)
>> ... | Inr eq = transport (λ x → tl 1 <=tl S x) eq (Inl ltS)
>>
>> which is clearly structural recursive on p fails. But if I write
>> out the 'with' explicitly it's fine.
>>
>> I think I could get all of these to pass by writing out the 'with's
>> explicitly, but perhaps there is a way to change the termination
>> checker so that it accepts them?
>>
>> -Dan
>>
>> On Jul 1, 2014, at 12:59 PM, Dan Licata <dlicata at wesleyan.edu
>> <mailto:dlicata at wesleyan.edu>> wrote:
>>
>> > Hi Jesper,
>> >
>> > Thanks for the nice explanation! I don't think this restriction
>> should be much of an issue for HoTT, because we tend to stick closer
>> to the eliminators (e.g. for higher inductives that's all we know
>> how to do), so in the examples I can think of ftrue/ffalse are
>> already applications of eliminators, rather than direct recursive calls.
>> >
>> > I'll try my library on it next time I have a chance to upgrade agda.
>> >
>> > -Dan
>> >
>> >
>> > On Jul 1, 2014, at 12:00 AM, Jesper Cockx <Jesper at sikanda.be
>> <mailto:Jesper at sikanda.be>> wrote:
>> >
>> >> The current restriction is quite simple: for a function to be
>> >> structurally recursive on an argument x of type T, the type T
>> must be
>> >> a data type *before* any matching has been done. In particular, this
>> >> prohibits structural recursion on 'deep' arguments and universe-like
>> >> constructions such as the one in my previous mail. I don't know what
>> >> the current situation is on the Coq side of things, maybe
>> someone else
>> >> can clarify?
>> >>
>> >> Jesper
>> >>
>> >> On 6/30/14, Dan Licata <dlicata at wesleyan.edu
>> <mailto:dlicata at wesleyan.edu>> wrote:
>> >>> great! is there a way to explain what the restriction is? Has
>> Coq fixed
>> >>> this bug yet, and if so, how does your solution compare to theirs?
>> >>>
>> >>> -Dan
>> >>>
>> >>> On Jun 27, 2014, at 12:26 PM, Jesper Cockx <Jesper at sikanda.be
>> <mailto:Jesper at sikanda.be>> wrote:
>> >>>
>> >>>> Yes, this restriction is to address the incompatibility of the
>> termination
>> >>>> checker with univalence. As a side-effect, many functions on
>> universes no
>> >>>> longer pass the termination check, for example (by Andreas):
>> >>>> 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 xs
>> >>>> For the moment, such definitions have to be unfolded manually:
>> >>>> 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 xs
>> >>>> However, due to a mistake I made in the fix, the termination
>> checker a
>> >>>> complains much more than necessary when --without-K is
>> enabled. This has
>> >>>> now been fixed in the development version:
>> >>>> https://code.google.com/p/agda/issues/detail?id=1214&can=1.
>> I'll check the
>> >>>> other errors in Nils' library later. If you have any specific
>> examples
>> >>>> that you think should be accepted, please send them to me and
>> I'll see
>> >>>> what I can do.
>> >>>>
>> >>>> Jesper
>> >>>>
>> >>>>
>> >>>> On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata
>> <dlicata at wesleyan.edu <mailto:dlicata at wesleyan.edu>> wrote:
>> >>>> Is this restriction addressing the "termination checker +
>> propositional
>> >>>> univalence inconsistency" issue, or something else?
>> >>>>
>> >>>> -Dan
>> >>>>
>> >>>> On Jun 21, 2014, at 1:44 PM, Jesper Cockx <Jesper at sikanda.be
>> <mailto:Jesper at sikanda.be>> wrote:
>> >>>>
>> >>>>> I suppose by 'people working on this issue', you mean Andreas
>> and me? I'm
>> >>>>> not currently working on this problem, but I could be
>> convinced to if the
>> >>>>> current hack turns out to be too inconvenient. However, I
>> have two
>> >>>>> problems before I can start working on a fix:
>> >>>>>
>> >>>>> - The current theory of pattern matching doesn't allow
>> induction on
>> >>>>> 'deep' arguments, i.e. ones that only get an inductive type
>> after pattern
>> >>>>> matching on some other arguments. So the theory would have to be
>> >>>>> extended.
>> >>>>>
>> >>>>> - I don't have a lot of experience with the termination
>> checker, so I'm
>> >>>>> not confident to mess with it. It seems that in order to fix this
>> >>>>> problem, the termination checker would need some type
>> information, as
>> >>>>> well as information about the substitutions performed by the
>> previous
>> >>>>> case splits.
>> >>>>>
>> >>>>> If anyone can help me with (one of) these problems, I'd like
>> to work
>> >>>>> together on it. Otherwise I'll try to get a better
>> understanding by
>> >>>>> myself, but then it might take a long time.
>> >>>>>
>> >>>>> Jesper
>> >>>>>
>> >>>>>
>> >>>>> On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez
>> <asr at eafit.edu.co <mailto:asr at eafit.edu.co>>
>> >>>>> wrote:
>> >>>>>
>> >>>>> On 20 June 2014 09:07, Brent Yorgey <byorgey at seas.upenn.edu
>> <mailto:byorgey at seas.upenn.edu>> wrote:
>> >>>>> but is the code I linked now expected to
>> >>>>> fail termination checking?
>> >>>>>
>> >>>>> Using the --without-K option? I don't know. This is an open
>> issue and
>> >>>>> people working on this issue know that the current behaviour
>> is too
>> >>>>> restrictive. I don't know if they are working in a better
>> solution
>> >>>>> right now.
>> >>>>>
>> >>>>> --
>> >>>>> Andrés
>> >>>>>
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list