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

[Matthieu Sozeau]

Hi,

  I can’t speak for Andrej, but my point was not to disqualify sized-types,
they are a fine, evidence-based foundation, just like wellfounded relations,
to define recursive definitions. The nice thing about wellfounded relations
is that they are readily available, supposing we have at least eliminators. 
I’m curious about the respective expressive power of both, my gut feeling is
that w.f. relations are most general but this is not backed up by anything
formal. My question about sized types is how do you justify definitions
on big ordinals defined *in* the type theory using the metatheoretical ordinals.
It might reduce to Bruno’s [… and the fact that those ordinals are not used in the
process you iterate…] and be a solved question. Then Andrej might be worried that
the metatheory has to be classical if you use ordinals (?) (but for wfs it wouldn’t
be??). I’m no expert on ordinals or the models of sized-types so please take this 
as another newbie question :)

  About the preservation by reduction, indeed that’s an advantage, and I can’t
see another way than to use a measure function to (in general, ordinal?) numbers 
and the associated well-founded order to encode it.

Cheers,
— Matthieu

On 9 janv. 2014, at 09:50, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:

> Hi.
> 
> Sorry but I don't really understand Andrej and Mathieu's last mails. In size-based termination, there is no ordinal in the type system     itself. Ordinals are just used in the meta-theory to justify that, indeed, every well typed term terminates. In fact, ordinals were already used before in the meta-theory of CIC (see Altenkirch and Werner's PhDs) to justify the fact that functions defined by structural induction indeed terminates. Size-based termination simply extends the syntax of CIC by making explicit something that was implicit in the interpretation of types as Girard's reducibility candidates. The nice thing is that it brings extra power to prove the termination of functions because, in contrast to the notion of "structurally smaller", size is invariant by reduction.
> 
> Best regards,
> 
> Frédéric.
> 
> Le 09/01/2014 00:25, Matthieu Sozeau a écrit :
>> I agree with you Andrej, and the (well founded) transitive closure of the subterm relation can easily be defined for computational inductive families (all inductive types if you remove prop), avoiding the computation of ordinals. That's precisely the "semantic" (maybe "evidence-based"?) explanation that C. Paulin used in her habilitation thesis to justify recursive definitions and the most general one for users (it does not even need to be attached to an inductive type). Equations can derive this subterm relation automatically for (non-mutual, non-nested) inductive families, and prove its wellfoundedness. Extending this to the other cases is a matter of thinking and engineering. The Below predicate of Epigram gives you similar access to every subterm you can recurse on "logically". The only culprit is reduction behavior/efficiency using this machinery, but that should be optimizable.
>> 
>> Best,
>> -- Matthieu
>> 
>> Le mercredi 8 janvier 2014, Andrej Bauer a écrit :
>> I would just like to point out that ordinals are an inherently
>> classical notion. The correct constructive and computationally
>> meaningful replacement is that of a well-founded relation, i.e., a
>> relation < on a set X satisfying, for all properties P,
>> 
>>  (forall y, ((forall x < y, P x) -> P y)) -> forall z, P z.
>> 
>> This is all well known, and of course you can recognize the
>> recursor/eliminator in the above formula. So if we are to take
>> computation seriously, we ought to think about inductive definitions
>> which are justified by a more general notion of well foundedness, not
>> just ordinals. The ordinals are bound to go wrong when we push them a
>> little bit.
>> 
>> Also, the HoTT experience has thought us (at least me) the value of
>> semantic notions over syntactic ones. I am referring to HoTT hProp vs.
>> CiC Prop. The former delineates the concept of "proposition" with a
>> semantic condition, while the latter does it formalistically. It would
>> seem sensible to me to go the same route with inductive definitions,
>> namely, rely on semantic justifications rather than syntactic ones. [I
>> may be misusing the words "semantic" and "syntactic" here, but I
>> cannot think of better ones.]
>> 
>> With kind regards,
>> 
>> Andrej
>> 
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
>> For more options, visit https://groups.google.com/groups/opt_out.
>> 
>> 
>> -- 
>> -- Matthieu
>> -- 
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
>> For more options, visit https://groups.google.com/groups/opt_out.
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe at googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.