walker (May 23 2023 at 09:28): walker (May 23 2023 at 09:28):I hope I didn't ask this question before, does mutual induction as language feature offer any logical power over nested induction ? or is it just for convenience ?
James Wood (Jun 01 2023 at 12:40):IIRC, mutual induction can be translated into indexed induction. For example, mutually defined Even and Odd can be translated to Parity : nat -> bool -> Prop. I guess this indexed induction is not too far from nested (but otherwise unindexed) induction.
Ali Caglayan (Jun 01 2023 at 14:43):under the right conditions indexed can also be translated to non indexed with an identity type.
Ali Caglayan (Jun 01 2023 at 14:44):nested induction however is probably strictly stronger, but i dont remember where in the literature it is claimed. @Pierre-Marie Pédrot might be able to say more.
Gaëtan Gilbert (Jun 01 2023 at 14:54):Ali Caglayan said:
under the right conditions indexed can also be translated to non indexed with an identity type.
"under the right conditions" = the type is non recursive OR you accept using non recursively uniform parameters in the translation result
Of course this leaves you needing the identity type to bootstrap
Gaëtan Gilbert (Jun 01 2023 at 14:56):BTW do you all mean "nested/mutual inductives" or do you really refer to induction, and if the later is that different from recursion?
Gaëtan Gilbert (Jun 01 2023 at 14:59):nested inductives can be translated to mutual AFAIK, eg Inductive rose := Rose (_ : list rose) becomes Inductive rose := Rose (_ : list_rose) with list_rose := nil | cons (_:rose) (_:list_rose)
However translating mutual to single is unclear or maybe impossible when they live in different universes. OTOH I don't know any interesting examples of mutual inductives in different universes.
Last updated: Nov 29 2023 at 21:01 UTC