[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Frédéric Blanqui]

Le 07/01/2014 20:43, Maxime Dénès a écrit :
> Hello Conor,
>
> In fact, I was wondering why the call to subst (which is defined by
> pattern matching) destroys the proper subterm status, while it is not
> the case for pattern matching. It does not seem very uniform, does it?
>
> In Coq, a reduction step would replace subst by its body before
> computing the size information.
>
> I agree that elaboration is nice. However, sometimes you don't want to
> pay the price for encoding things. In an ideal world, you could prove
> the elaboration process correct, and extract a checker that is correct
> by construction with respect to the target type theory you mention. Is
> there any existing work in that direction?
>
> Maxime.
>
Hello.

Some time ago, for proving the termination of higher-order rewrite 
systems, I formalized in Coq the notion of computability closure which 
is based on an extension of Girard's notion of reductibility. For the 
moment, it only considers simple types and the syntactic subterm 
relation in recursive calls. So, there is still quite some work to 
extend it to richer type disciplines and to size-based termination, but 
all the basic ingredients are already here (including the semantics of 
positive inductive types on which size-based termination is based). See 
http://color.inria.fr/ for downloading the CoLoR library, 
http://color.inria.fr/doc/CoLoR.Term.Lambda.LCompClos.html for having a 
look at the development without the proofs, and 
http://color.inria.fr/doc/CoLoR.Term.Lambda.LSystemT.html to see the 
example of Gödel' system T.

Best regards,

Frédéric.

> On 01/07/2014 12:25 PM, Conor McBride 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