[TYPES] Statement of structural induction

[Paolo Giarrusso]

Thanks! Meanwhile, it has been suggested to me (by Dan Doel on ##dependent) that W-types relate to both ordinals and inductive types, so they probably answer my question (even though W-types are not equivalent to inductive types without further extensionality assumptions).

Paolo Giarrusso
-- 
Sent from my iPad

> On 10 Jan 2018, at 17:37, Pierre Courtieu <pierre.courtieu at gmail.com> wrote:
> 
> I don't know exactly if this can be useful but Pierre Castéran (with
> parts also done by Évelyne Contejean) formalized ordinals and proved
> the termination of hydra's problem usinng them there:
> 
> http://www.labri.fr/perso/casteran/hydra-ludica/index.html
> 
> This is work in progress but the proofs for hydra is finished as far as I know.
> 
> Best regards,
> Pierre Courtieu
> 
> 
> 2018-01-10 16:45 GMT+01:00 Paolo Giarrusso <p.giarrusso at gmail.com>:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>> 
>> Since I (and maybe others) understand structural induction better than transfinite induction, I now wonder if one can use structural induction to understand better both specific uses of transfinite induction and proof-theoretic ordinal analysis.
>> 
>> Has anybody written, say, an introduction to ordinals for the Coq programmer or some such thing? Googling found little,* maybe because this seems pointless to people who do understand ordinals. But maybe such a presentation would be more accessible to computer scientists used to proof assistants?
>> 
>> For instance:
>> 
>> (1) can one define the proof-theoretic strength of an inductive datatype, such as Richard’s example?
>> (2) Gentzen’s proof of consistency for PA translates derivations in PA to infinitary derivations in PA_\omega [1], and then requires transfinite induction up to \epsilon_0. Could one just use as structural induction on an inductive type of PA_\omega infinitary derivations?
>> 
>> (2b) In fact, if I try to encode PA_\omega derivations in Coq (pseudocode) naively, the result looks similar to Richard’s datatype (though more indexed) — there’s one premise with an argument per natural:
>> 
>> Inductive derivation Gamma Delta :=
>> | omegaR : forall F Gamma Delta, (forall n, derivation Gamma (F n : Delta)) -> derivation Gamma ((Forall x, F x) : Delta)
>> | omegaL :
>> forall F Gamma Delta, (forall n, derivation (F n : Gamma) Delta) ->
>> derivation ((Exists x, F x) : Gamma) Delta
>> 
>> * Forall x, F x
>> 
>> *The best answer seems to be Emil Jeřábek at https://mathoverflow.net/a/61045/36016, saying (IIUC) that ordinals can be understood as trees, but pointing out those trees are more complex. But some still prefer structural recursion even when it can be translated to induction on naturals, so maybe the same applies here.
>> 
>> [1] I’m following the presentation in https://www1.maths.leeds.ac.uk/~rathjen/Sepp-chiemsee.pdf.
>> 
>>>>> On Wed, 10 Jan 2018 at 11:45, Frédéric Blanqui <frederic.blanqui at inria.fr> wrote:
>>> 
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>> 
>>> Hello.
>>> 
>>> Well, it is if you define the height as a transfinite ordinal. In case
>>> of an infinitely branching constructor like Mk : (nat -> ty) -> ty,
>>> height(Mk f) = sup{height(f n) | n in nat} + 1.
>>> 
>>> Frédéric.
>>> 
>>> 
>>>> Le 09/01/2018 à 17:14, Xavier Leroy a écrit :
>>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>>> 
>>>>> On 07/01/2018 17:41, Xavier Leroy wrote:
>>>>> 
>>>>> As your example shows, the tree can contain infinitely-branching nodes, hence the size can be infinite, but all paths are finite, hence the height is finite.
>>>> I was confused.  All paths in this tree are finite indeed, and that's why it induces a well-founded ordering.  But in the presence of infinitely-branching nodes, the height can still be infinite and is not an appropriate justification for structural induction.
>>>> 
>>>> Sorry for the noise,
>>>> 
>>>> - Xavier Leroy
>>>