[Agda] list equality decision procedure fails termination check
with Agda 2.4.0.1?
Andreas Abel
abela at chalmers.se
Sun Jul 13 17:37:53 CEST 2014
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