The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

Hi Conor,

I am sure this must be a stupid question but why is this not covered
by your result that pattern matching can be reduced to eliminators + K?

Cheers,
Thorsten

On 07/01/2014 17:25, "Conor McBride" 
<conor AT strictlypositive.org>
 wrote:

>Hi Maxime
>
>On 7 Jan 2014, at 16:56, Maxime Dénès 
><mail AT maximedenes.fr>
> wrote:
>
>> Still, I don't understand why replacing the pattern matching in my
>> example by a call to subst makes the termination check fail.
>
>A call to subst destroys the "proper subterm" status, whereas
>pattern matching naively preserves it.
>
>> 
>> Maxime.
>
>>> {-# OPTIONS --without-K #-}
>>> 
>>> module BadWithoutK where
>>> 
>>> data Zero : Set where
>>> 
>>> data WOne : Set where
>>>  wrap : (Zero -> WOne) -> WOne
>>> 
>>> data _<->_ (X : Set) : Set -> Set where
>>>  Refl : X <-> X
>>> 
>>> postulate
>>>  myIso : WOne <-> (Zero -> WOne)
>>> 
>>> moo : WOne -> Zero
>>> noo : (X : Set) -> (WOne <-> X) -> X -> Zero
>>> 
>>> moo (wrap f) = noo (Zero -> WOne) myIso f
>>> noo .WOne Refl x = moo x
>
>moo's input is bigger than the third argument in its noo call
>noo's third input is the same as the argument in its moo call
>
>Size-change termination, how are ye?
>
>When you do the translation to eliminators, you're obliged to
>show how recursive calls correspond to invocations of the
>inductive hypothesis: here that's just not going to happen.
>Transporting f across myIso does indeed give an element of
>WOne (your Box), but that does not make a nullary inductive
>hypothesis any easier to invoke.
>
>I'd quite like to see us defining a type theory in which the
>only checking is type checking, then using it as a target for
>elaboration. Eliminators are one candidate, but there are
>others. Sized types are certainly another strong candidate.
>I'm also interested to see whether there are "locally clocked"
>explanations for termination, as there seem to be for
>productivity.
>
>Interesting times
>
>Conor
>
>
>>> 
>>> bad : Zero
>>> bad = moo (wrap \ ())
>>> 
>>> 
>>> 
>>>> T.
>>>> 
>>>>> I am also not sure how specific the problem is to univalence. As Cody
>>>>> said, I would expect to find some set-theoretical models where the
>>>>> equality holds. So being able to prove the negation is disturbing.
>>>>> 
>>>>> Maxime.
>>>>> 
>>>>> On 01/06/2014 07:23 PM, Abhishek Anand wrote:
>>>>>> It is known that UIP is inconsistent with univalence.
>>>>>> Does this typecheck even after disabling UIP(==K axiom?) ?
>>>>>> I might be wrong, but I think that UIP is baked into the typechecker
>>>>>> of Agda.
>>>>>> But, UIP can be disabled somehow?
>>>>>> 
>>>>>> 
>>>>>> -- Abhishek
>>>>>> http://www.cs.cornell.edu/~aa755/
>>>>>><http://www.cs.cornell.edu/%7Eaa755/>
>>>>>> 
>>>>>> 
>>>>>> On Mon, Jan 6, 2014 at 3:42 PM, Maxime Dénès 
>>>>>> <mail AT maximedenes.fr
>>>>>> <mailto:mail AT maximedenes.fr>>
>>>>>>  wrote:
>>>>>> 
>>>>>>   Bingo, Agda seems to have the same problem:
>>>>>> 
>>>>>>   module Termination where
>>>>>> 
>>>>>>   open import Relation.Binary.Core
>>>>>> 
>>>>>>   data Empty : Set where
>>>>>> 
>>>>>>   data Box : Set where
>>>>>>   wrap : (Empty → Box) → Box
>>>>>> 
>>>>>>   postulate
>>>>>>   iso : (Empty → Box) ≡ Box
>>>>>> 
>>>>>>   loop : Box -> Empty
>>>>>>   loop (wrap x) rewrite iso = loop x
>>>>>> 
>>>>>>   gift : Empty → Box
>>>>>>   gift ()
>>>>>> 
>>>>>>   bug : Empty
>>>>>>   bug = loop (wrap gift)
>>>>>> 
>>>>>>   However, I may be missing something due to my ignorance of Agda.
>>>>>>   It may be well known that the axiom I introduced is inconsistent.
>>>>>>   Forgive me if it is the case.
>>>>>> 
>>>>>>   Maxime.
>>>>>> 
>>>>>> 
>>>>>>   On 01/06/2014 01:15 PM, Maxime Dénès wrote:
>>>>>> 
>>>>>>       The anti-extensionality bug is indeed related to termination.
>>>>>>       More precisely, it is the subterm relation used by the guard
>>>>>>       checker which is not defined quite the right way on dependent
>>>>>>       pattern matching.
>>>>>> 
>>>>>>       It is not too hard to fix (we have a patch), but doing so
>>>>>>       without ruling out any interesting legitimate example (dealing
>>>>>>       with recursion on dependently typed data structures) is more
>>>>>>       challenging.
>>>>>> 
>>>>>>       I am also curious as to whether Agda is impacted. Let's try it
>>>>>> :)
>>>>>> 
>>>>>>       Maxime.
>>>>>> 
>>>>>>       On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
>>>>>> 
>>>>>>           Which bug was this?
>>>>>> 
>>>>>>           I only saw the one which allowed you to prove
>>>>>>           anti-extensionality? But
>>>>>>           this wasn't related to termination, or?
>>>>>> 
>>>>>>           Thorsten
>>>>>> 
>>>>>>           On 06/01/2014 16:54, "Cody Roux" 
>>>>>> <cody.roux AT andrew.cmu.edu
>>>>>>           
>>>>>> <mailto:cody.roux AT andrew.cmu.edu>>
>>>>>>  wrote:
>>>>>> 
>>>>>>               Nice summary!
>>>>>> 
>>>>>> 
>>>>>>               On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
>>>>>> 
>>>>>>                   Agda enforces termination via a termination
>>>>>>                   checker which is more
>>>>>>                   flexible but I think less principled than Coq's
>>>>>>                   approach.
>>>>>> 
>>>>>>               That's a bit scary given that there was an
>>>>>>               inconsistency found in
>>>>>>               the Coq termination checker just a couple of weeks ago
>>>>>> :)
>>>>>> 
>>>>>>               BTW, has anyone tried reproducing the bug in Agda?
>>>>>> 
>>>>>> 
>>>>>>               Cody
>>>>>> 
>>>>>>           This message and any attachment are intended solely for
>>>>>>           the addressee and may contain confidential information. If
>>>>>>           you have received this message in error, please send it
>>>>>>           back to me, and immediately delete it. Please do not use,
>>>>>>           copy or disclose the information contained in this message
>>>>>>           or in any attachment. Any views or opinions expressed by
>>>>>>           the author of this email do not necessarily reflect the
>>>>>>           views of the University of Nottingham.
>>>>>> 
>>>>>>           This message has been checked for viruses but the contents
>>>>>>           of an attachment
>>>>>>           may still contain software viruses which could damage your
>>>>>>           computer system, you are advised to perform your own
>>>>>>           checks. Email communications with the University of
>>>>>>           Nottingham may be monitored as permitted by UK
>>>>>>legislation.
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>>       _______________________________________________
>>>>>>       Agda mailing list
>>>>>>       
>>>>>> Agda AT lists.chalmers.se
>>>>>>  
>>>>>> <mailto:Agda AT lists.chalmers.se>
>>>>>>       https://lists.chalmers.se/mailman/listinfo/agda
>>>>>> 
>>>>>> 
>>>>>>   _______________________________________________
>>>>>>   Agda mailing list
>>>>>>   
>>>>>> Agda AT lists.chalmers.se
>>>>>>  
>>>>>> <mailto:Agda AT lists.chalmers.se>
>>>>>>   https://lists.chalmers.se/mailman/listinfo/agda
>>>>>> 
>>>>>> 
>>>>> _______________________________________________
>>>>> Agda mailing list
>>>>> Agda AT lists.chalmers.se
>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda AT lists.chalmers.se
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
>