The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi.

Le 08/01/2014 22:19, Matthieu Sozeau a écrit :

I have the same question, when I looked into it it seemed like measuring every data type like this would involve representing ordinals not just naturals... and then which ones... Maybe you can translate a (nat -> I) -> I constructor to (nat -> I i) -> I (^ i) ? Right. Andreas gave us a similar example on the HoTT list in his extension of Agda with size annotations. But, for proving termination, you just need the successor symbol ^ and the subterm relation ^x > x. There is no need to represent ordinals.

Then you'd want an (implicit?) subtyping from I i to I j for j > i ?
This is indeed necessary for typing a match whose branches have different sizes. But there is no subtyping in Coq (except on universes)...

Note also that size decreasingness is not sufficient for having termination. When defining f:I i->T, where T may depend on i in general, you need T(i) to satisfy additional conditions of monotony or continuity wrt i. See Andreas' work on this subject.

Best regards,

Frédéric.

-- Matthieu

Le mercredi 8 janvier 2014, Frédéric Blanqui a écrit :

Le 08/01/2014 19:18, Cody Roux a écrit :
> On 01/08/2014 12:49 PM, Jean Goubault-Larrecq wrote:
>> That sounds fair. A couple years ago, I tried seeing if there was
>> a straightforward way to perform this translation (with Jorge
>> Sacchini). It's not trivial, and in particular I found that I would
>> probably need some form of proof-irrelevance, even for
>> "first-order" datatypes, which seems ironic. However in this case
>> we would only need it on "h-level 0" so it doesn't seem hopeless.
>>
>> Higher-order datatypes are a bit more difficult, and I admit I
>> never worked it out. I believe it's possible though.
>>
>>>> The eliminators are like axioms in set theory and it is
>>>> worthwhile to translate any extension by reducing them to the
>>>> axiom instead of adding new ones even though they may be
>>>> semantically justified.
>>> That's fair, but I don't see why eliminators have a more powerful
>>> ontological status than sized-types. They require work to be
>>> derived as well, and the correctness proofs for them are quite
>>> similar to that for sized types. This seems like a matter of
>>> preference. Obviously I'm not neutral in this matter though.
>> I'm no Coq expert, but wasn't this idea of translating
>> pattern-matching to eliminators (recursors) already
>> the core of Cristina Cornes' PhD thesis, back in the
>> time where Coq only had recursors and no pattern-matching?
>>   I seem to recall she had already realized the difficulty
>> of the task, and the importance of axiom K, at least.
> I'm afraid I'm not aware of Cristina's work. I'll try to read up on this.
>
> Here is the situation as I understand it. As with most falls from grace,
> Coq started from a place without sin, namely with a rather hard to use
> guard system based on Gimenez's (hard to find) paper "Codifying guarded
> definitions with recursive schemes", in which every definition could (in
> principle) be translated back into the recursors from whence they came.
> Over time, the guard condition was relaxed to allow for more flexible
> definition, and the direct correspondence was lost.
>
> What I was referring to was more specific to sized-types. In principle
> it is possible to take this powerful extension of the guard condition,
> and use it to translate back into a system with only recursors. However,
> this requires a change to the definition of the inductive types, so it
> isn't as straightforward as the Gimenez translation. In particular,
> Lists would become size-indexed lists (vectors), and any fixpoint
> definition over lists would actually involve the fix-point combinator,
> definable in terms of recursors/eliminators:
>
> Fix : (forall n, (forall m < n, List m -> T) -> (List n -> T)) -> forall
> n, List n -> T
>
> Where n, m are natural numbers (the "skeleton" of List). I think I can
> define such a modified inductive type for every instance of inductive
> definitions in Coq. This would certainly revert us back to the sinless
> state desired by Thorsten and Vladimir, while preserving the paradise
> offered by the relaxed guard condition.
Including strictly positive inductive types, that is, with constructors
taking functions as recursive arguments?

> About K: Coq has managed to describe a pattern-match which does not
> allow it (by making less unification information available in the
> branches), and I don't think it's that relevant to the problem at hand,
> which is mostly concerned about when a term is a subterm of another.
>
> Best,
>
>
> Cody
>
>> All the best,
>>
>> - -- Jean.
>>
>>
>> -----BEGIN PGP SIGNATURE-----
>> Version: GnuPG/MacGPG2 v2.0.18 (Darwin)
>> Comment: GPGTools - http://gpgtools.org
>> Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/
>>
>> iQEcBAEBAgAGBQJSzY/DAAoJEBO3J6HB7Rh1WyUH/3uim2ZTsfzddH0gbCngNeFu
>> vqnvXmd8VPKNoH4LE9Ydhi2J4ibCmnyPH2sFi1ee6t5Kt9Oz8GhOc7HzRdlB2qsq
>> GpD+lxDE8I9HdokfDyYnP2RP2ZiUs2/2m1bcAJkWVZLwlcKyKiwr/yzY/lNdSIRS
>> J/YYIXMI/wCw1b38ZoFXvaa0okOS8IDDde2W1lybvRSO0F1ZO6qMzWwas5hD78mC
>> FU8MeU7xYvWOv30GRyYEl0PaUswCmmGhvVqZDH0Ttum2ONnQpQ9JhMKB6AaVZQu/
>> hB7/PE8vOXCFLBUMkBTfn/R655VHbs87tytgMLKE5Q+eMs5hA7u3lfEMIzzP+io=
>> =JLKR
>> -----END PGP SIGNATURE-----

--
-- Matthieu