The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

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.

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-----