Stream: Miscellaneous

Topic: mutual ind vs nested ind


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Jun 01 2023 at 14:43):

under the right conditions indexed can also be translated to non indexed with an identity type.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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: May 18 2024 at 08:40 UTC