[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