[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[email protected]>: >> [ 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 >>>>> <[email protected]> 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 >>>
