<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:<br>
<br>noo : (X : Set) -> (WOne <-> X) -> X -> Zero<br>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:<br><br>noo' : (X : Set) -> (WOne <-> X) -> X -> Zero<br>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...<br>
<br></div>Jesper<br><div><div><div><br><br></div></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:0 0 0 .8ex;border-left:1px #ccc solid;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 class="HOEnZb"><div class="h5"><<a href="mailto:psztxa@exmail.nottingham.ac.uk">psztxa@exmail.nottingham.ac.uk</a>> wrote:<br>
<br>
>On 07/01/2014 23:03, "Conor McBride" <<a href="mailto:conor@strictlypositive.org">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">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">mail@maximedenes.fr</a><br>
>>>>>>>>> <mailto:<a href="mailto:mail@maximedenes.fr">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">cody.roux@andrew.cmu.edu</a><br>
>>>>>>>>> <mailto:<a href="mailto:cody.roux@andrew.cmu.edu">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">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">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">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se">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">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">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">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>