<div dir="ltr"><div><div><div><div>Conor: I think it is not fair to say that noo is not structurally recursive; it should be totally fine according to definition 6 in "Eliminating Dependent Pattern Matching". <br>
</div><div><br>Looking at the proof of theorem 24 in the same paper, I see one implicit assumption that is not mentioned in the statement of the theorem itself and also currently not checked by Agda. The extra condition is that the type of the argument on which the function is structurally recursive should be a data type D vs. The definition of noo fails this condition, since it is structurally recursive on its third argument, whose type X is not a data type (at least not before pattern matching). <br>
<br></div><div>So an easy approach would be to require that the type on which we do induction is already a data type in the type of the whole function, not just in the type of each clause. Of course, this only works for functions that don't use fancy termination criteria like sized types. For those, it would probably be best to do something like explained by Bruno. But we don't know yet how to translate those to eliminators anyway. <br>
<br></div><div>Jesper<br></div></div></div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Wed, Jan 8, 2014 at 11:35 AM, Jesper Cockx <span dir="ltr"><<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div dir="ltr"><div><div><div><div>I'm trying to get a better understanding of the problem by manually translating the definition down to eliminators. First, here's a version of Conor's example without mutual induction:<div>
<br>
<br>noo : (X : Set) -> (WOne <-> X) -> X -> Zero<br></div>noo .WOne Refl (wrap f) = noo (Zero → WOne) myIso f<br><br></div>And here are the standard eliminators for WOne and <->:<br><br>WOne-elim : (P : WOne -> Set) -><br>
(m : (f : Zero -> WOne) <br> (h : (z : Zero) -> P (f z)) -> <br> P (wrap f)) -> <br> (x : WOne) -> P x<br>WOne-elim P m (wrap f) = m f (λ z → WOne-elim P m (f z)) <br>
<br><->-elim : (X : Set) (P : (Y : Set) -> X <-> Y -> Set) -><br> (m : P X Refl) -><br> (Y : Set) (E : X <-> Y) -> P Y E<br><->-elim X P m .X Refl = m<br><br></div>
Now I try to write noo using only these eliminators, to see what goes wrong:<div><br><br>noo' : (X : Set) -> (WOne <-> X) -> X -> Zero<br></div>noo' X E x = <->-elim WOne (λ Y _ → Y → Zero) subgoal X E x<br>
where<br> subgoal : WOne -> Zero<br> subgoal = (WOne-elim (λ _ → Zero) (λ f h → h {!!}))<br><br></div>What I understand of it, is that the order in which we apply the eliminators is important here. We start with x : X, so we cannot apply WOne-elim directly. So we first apply <->-elim instead, leaving the subgoal ? : WOne -> Zero. Now we can apply WOne-elim, however we are only allowed to make recursive calls to the subgoal, not to noo' itself. In particular, we cannot supply myIso as the argument for WOne <-> X, as it is already fixed to be Refl. I wonder if this problem was already present in 'Eliminating Dependent Pattern Matching', or was introduced later by the termination checker of Agda? This is certainly all very interesting...<span><font color="#888888"><br>
<br></font></span></div><span><font color="#888888">Jesper<br><div><div><div><br><br></div></div></div></font></span></div><div><div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Wed, Jan 8, 2014 at 11:05 AM, Altenkirch Thorsten <span dir="ltr"><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">P.S. An attempt at a summary:<br>
<br>
We already knew that pattern matching is incompatible with univalence<br>
because we can prove K.<br>
<br>
Now, due to the example by Maxime (and Conor) there is another<br>
incompatibilty which arises from pattern matching making things appear<br>
structurally recursive which shouldn't be.<br>
<br>
This one is not covered by K and it is another example where pattern<br>
matching is non-conservative over the standard eliminators (I guess we<br>
could invent a version of combinators which allow us to use propositional<br>
equality of types during recursion).<br>
<br>
As a consequence it also affects Coq, which always ruled out K but not<br>
this one.<br>
<br>
This is clearly a bug (has anybody filed a bug report) which should be<br>
fixed as a matter of urgency. Any proposals?<br>
<br>
Thorsten<br>
<br>
<br>
On 08/01/2014 09:52, "Altenkirch Thorsten"<br>
<div><div><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>> wrote:<br>
<br>
>On 07/01/2014 23:03, "Conor McBride" <<a href="mailto:conor@strictlypositive.org" target="_blank">conor@strictlypositive.org</a>> wrote:<br>
><br>
>><br>
>>On 7 Jan 2014, at 22:47, Altenkirch Thorsten<br>
>><<a href="mailto:psztxa@exmail.nottingham.ac.uk" target="_blank">psztxa@exmail.nottingham.ac.uk</a>> wrote:<br>
>><br>
>>> Hi Conor,<br>
>>><br>
>>> I am sure this must be a stupid question but why is this not covered<br>
>>> by your result that pattern matching can be reduced to eliminators + K?<br>
>><br>
>>The recursive call isn't covered by the inductive hypothesis. The direct<br>
>>version<br>
>>gives no account of the inductive hypothesis *at all*, hence the whole<br>
>>mess.<br>
>><br>
>>>>>> moo (wrap f) = noo (Zero -> WOne) myIso f<br>
>>>>>> noo .WOne Refl x = moo x<br>
>><br>
>>The recursive call<br>
>><br>
>> moo x<br>
>><br>
>>is really a recursive call<br>
>><br>
>> moo (subst myIso ... f)<br>
>><br>
>>but the inductive hypothesis tells us just that we can call moo on<br>
>>outputs of f.<br>
>><br>
>>Bottom line: it's not structurally recursive.<br>
><br>
>I know this - this was precisely the comment I made in my reply to Maxime.<br>
><br>
>However, it seems I am a victim of my own propaganda: I was always<br>
>thinking that Conor's result tells us that we can replace pattern matching<br>
>(with guarded recursion) by elimination constants.<br>
><br>
>However, this example shows that this is not true. Once we perform the<br>
>unification required by pattern matching we obtain a a term which "looks"<br>
>as if it is structurally smaller even though it isn't.<br>
><br>
>One obvious question is how we can recognize good instances of pattern<br>
>matching from bad ones.<br>
><br>
>This also increases the argument in favour of a safe version of pattern<br>
>matching which is evidence producing. One of my new students, Gabe<br>
>Dijkstra, is working on this - mainly triggered by the without-K issue.<br>
>However, as we see now there are other issues which went unnoticed.<br>
><br>
>Cheers,<br>
>Thorsten<br>
><br>
>><br>
>>Cheers<br>
>><br>
>>Conor<br>
>><br>
>><br>
>>>><br>
>>>> moo's input is bigger than the third argument in its noo call<br>
>>>> noo's third input is the same as the argument in its moo call<br>
>>>><br>
>>>> Size-change termination, how are ye?<br>
>>>><br>
>>>> When you do the translation to eliminators, you're obliged to<br>
>>>> show how recursive calls correspond to invocations of the<br>
>>>> inductive hypothesis: here that's just not going to happen.<br>
>>>> Transporting f across myIso does indeed give an element of<br>
>>>> WOne (your Box), but that does not make a nullary inductive<br>
>>>> hypothesis any easier to invoke.<br>
>>>><br>
>>>> I'd quite like to see us defining a type theory in which the<br>
>>>> only checking is type checking, then using it as a target for<br>
>>>> elaboration. Eliminators are one candidate, but there are<br>
>>>> others. Sized types are certainly another strong candidate.<br>
>>>> I'm also interested to see whether there are "locally clocked"<br>
>>>> explanations for termination, as there seem to be for<br>
>>>> productivity.<br>
>>>><br>
>>>> Interesting times<br>
>>>><br>
>>>> Conor<br>
>>>><br>
>>>><br>
>>>>>><br>
>>>>>> bad : Zero<br>
>>>>>> bad = moo (wrap \ ())<br>
>>>>>><br>
>>>>>><br>
>>>>>><br>
>>>>>>> T.<br>
>>>>>>><br>
>>>>>>>> I am also not sure how specific the problem is to univalence. As<br>
>>>>>>>>Cody<br>
>>>>>>>> said, I would expect to find some set-theoretical models where the<br>
>>>>>>>> equality holds. So being able to prove the negation is disturbing.<br>
>>>>>>>><br>
>>>>>>>> Maxime.<br>
>>>>>>>><br>
>>>>>>>> On 01/06/2014 07:23 PM, Abhishek Anand wrote:<br>
>>>>>>>>> It is known that UIP is inconsistent with univalence.<br>
>>>>>>>>> Does this typecheck even after disabling UIP(==K axiom?) ?<br>
>>>>>>>>> I might be wrong, but I think that UIP is baked into the<br>
>>>>>>>>>typechecker<br>
>>>>>>>>> of Agda.<br>
>>>>>>>>> But, UIP can be disabled somehow?<br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> -- Abhishek<br>
>>>>>>>>> <a href="http://www.cs.cornell.edu/~aa755/" target="_blank">http://www.cs.cornell.edu/~aa755/</a><br>
>>>>>>>>> <<a href="http://www.cs.cornell.edu/%7Eaa755/" target="_blank">http://www.cs.cornell.edu/%7Eaa755/</a>><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès <<a href="mailto:mail@maximedenes.fr" target="_blank">mail@maximedenes.fr</a><br>
>>>>>>>>> <mailto:<a href="mailto:mail@maximedenes.fr" target="_blank">mail@maximedenes.fr</a>>> wrote:<br>
>>>>>>>>><br>
>>>>>>>>> Bingo, Agda seems to have the same problem:<br>
>>>>>>>>><br>
>>>>>>>>> module Termination where<br>
>>>>>>>>><br>
>>>>>>>>> open import Relation.Binary.Core<br>
>>>>>>>>><br>
>>>>>>>>> data Empty : Set where<br>
>>>>>>>>><br>
>>>>>>>>> data Box : Set where<br>
>>>>>>>>> wrap : (Empty → Box) → Box<br>
>>>>>>>>><br>
>>>>>>>>> postulate<br>
>>>>>>>>> iso : (Empty → Box) ≡ Box<br>
>>>>>>>>><br>
>>>>>>>>> loop : Box -> Empty<br>
>>>>>>>>> loop (wrap x) rewrite iso = loop x<br>
>>>>>>>>><br>
>>>>>>>>> gift : Empty → Box<br>
>>>>>>>>> gift ()<br>
>>>>>>>>><br>
>>>>>>>>> bug : Empty<br>
>>>>>>>>> bug = loop (wrap gift)<br>
>>>>>>>>><br>
>>>>>>>>> However, I may be missing something due to my ignorance of Agda.<br>
>>>>>>>>> It may be well known that the axiom I introduced is<br>
>>>>>>>>>inconsistent.<br>
>>>>>>>>> Forgive me if it is the case.<br>
>>>>>>>>><br>
>>>>>>>>> Maxime.<br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> On 01/06/2014 01:15 PM, Maxime Dénès wrote:<br>
>>>>>>>>><br>
>>>>>>>>> The anti-extensionality bug is indeed related to<br>
>>>>>>>>>termination.<br>
>>>>>>>>> More precisely, it is the subterm relation used by the guard<br>
>>>>>>>>> checker which is not defined quite the right way on<br>
>>>>>>>>>dependent<br>
>>>>>>>>> pattern matching.<br>
>>>>>>>>><br>
>>>>>>>>> It is not too hard to fix (we have a patch), but doing so<br>
>>>>>>>>> without ruling out any interesting legitimate example<br>
>>>>>>>>>(dealing<br>
>>>>>>>>> with recursion on dependently typed data structures) is more<br>
>>>>>>>>> challenging.<br>
>>>>>>>>><br>
>>>>>>>>> I am also curious as to whether Agda is impacted. Let's try<br>
>>>>>>>>>it<br>
>>>>>>>>> :)<br>
>>>>>>>>><br>
>>>>>>>>> Maxime.<br>
>>>>>>>>><br>
>>>>>>>>> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:<br>
>>>>>>>>><br>
>>>>>>>>> Which bug was this?<br>
>>>>>>>>><br>
>>>>>>>>> I only saw the one which allowed you to prove<br>
>>>>>>>>> anti-extensionality? But<br>
>>>>>>>>> this wasn't related to termination, or?<br>
>>>>>>>>><br>
>>>>>>>>> Thorsten<br>
>>>>>>>>><br>
>>>>>>>>> On 06/01/2014 16:54, "Cody Roux"<br>
>>>>>>>>><<a href="mailto:cody.roux@andrew.cmu.edu" target="_blank">cody.roux@andrew.cmu.edu</a><br>
>>>>>>>>> <mailto:<a href="mailto:cody.roux@andrew.cmu.edu" target="_blank">cody.roux@andrew.cmu.edu</a>>> wrote:<br>
>>>>>>>>><br>
>>>>>>>>> Nice summary!<br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:<br>
>>>>>>>>><br>
>>>>>>>>> Agda enforces termination via a termination<br>
>>>>>>>>> checker which is more<br>
>>>>>>>>> flexible but I think less principled than Coq's<br>
>>>>>>>>> approach.<br>
>>>>>>>>><br>
>>>>>>>>> That's a bit scary given that there was an<br>
>>>>>>>>> inconsistency found in<br>
>>>>>>>>> the Coq termination checker just a couple of weeks<br>
>>>>>>>>>ago<br>
>>>>>>>>> :)<br>
>>>>>>>>><br>
>>>>>>>>> BTW, has anyone tried reproducing the bug in Agda?<br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> Cody<br>
>>>>>>>>><br>
>>>>>>>>> This message and any attachment are intended solely for<br>
>>>>>>>>> the addressee and may contain confidential information.<br>
>>>>>>>>>If<br>
>>>>>>>>> you have received this message in error, please send it<br>
>>>>>>>>> back to me, and immediately delete it. Please do not<br>
>>>>>>>>>use,<br>
>>>>>>>>> copy or disclose the information contained in this<br>
>>>>>>>>>message<br>
>>>>>>>>> or in any attachment. Any views or opinions expressed by<br>
>>>>>>>>> the author of this email do not necessarily reflect the<br>
>>>>>>>>> views of the University of Nottingham.<br>
>>>>>>>>><br>
>>>>>>>>> This message has been checked for viruses but the<br>
>>>>>>>>>contents<br>
>>>>>>>>> of an attachment<br>
>>>>>>>>> may still contain software viruses which could damage<br>
>>>>>>>>>your<br>
>>>>>>>>> computer system, you are advised to perform your own<br>
>>>>>>>>> checks. Email communications with the University of<br>
>>>>>>>>> Nottingham may be monitored as permitted by UK<br>
>>>>>>>>> legislation.<br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> _______________________________________________<br>
>>>>>>>>> Agda mailing list<br>
>>>>>>>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>>>>>>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>>> _______________________________________________<br>
>>>>>>>>> Agda mailing list<br>
>>>>>>>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>>>>>>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>>>>>>>><br>
>>>>>>>>><br>
>>>>>>>> _______________________________________________<br>
>>>>>>>> Agda mailing list<br>
>>>>>>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>>>>>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>>>>>> _______________________________________________<br>
>>>>>>> Agda mailing list<br>
>>>>>>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>>>>>>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>>>>><br>
>>>><br>
>>><br>
>><br>
><br>
><br>
<br>
</div></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div></div>