coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strict positivity description in CIC spec

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strict positivity description in CIC spec
Date: Mon, 26 Aug 2019 15:10:22 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-phdr: 9a23:uMfR1RRBJURPKP4SdGA1RBcSvtpsv+yvbD5Q0YIujvd0So/mwa6ybBKN2/xhgRfzUJnB7Loc0qyK6vqmADFcqs/a6zgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrswndrNQajIttJ6o+1xfErHVFcPlKyG11Il6egwzy7dqq8p559CRQtfMh98peXqj/Yq81U79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+76puVRTlhjsLOyI//WrKkcF7kr5Vrwy9qBx+247UYZ+aNPxifqPGYNgWQXNNUttNWyBdB4+xaZYEAegcMuZCt4Tzp0UAowa9CwmiCu3gyDFHiXDq0qAhz+QtDRvL0BA8E98UrHjZqsj+OqcIUeCyyanF1SjNb+9I1jfz8ofIdA0qr/aLXbJ2d8rRyFcgFxnYhViXrIzlODWV1uIMs2eF9eptTuOvi3Qgqw1rvzivw8Asio/VhoIP1F/L7yF5zJwpKtKiUUN2Z8OvHpVXtyGfLYR2Q8UiTnlruCkk0b0GpYS7czYOyJg92RHQduGHfo6V6RzgTOacOSp0iXx7dL6lmRq+7UetxvfiWsS0ylpHrjZJnsHRun0JyRDf8NWLR/9/80u7xDqDyR3f5vtFLE07k6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk//Kn6+XjYrX9upCTLYl0igfgPaQ0gMC/AP44Mg8UU2iG/OS807vj/VHjQLpUlPI2lrPVv4zAKsgDp665BRFa0po75hqiATqqzs4UkWcbIF9KYh6LkYjkN0vOLfzkFfu/hk6jkDZvx/DIJL3hBZDNI2DGkLfme7Z97U9cxxQpzd1E5pJUELYBLOjuWk/0s9zYCAM5MxaqzOn9DNVxzJ8RVniXDq+DLKzSqUOI5v4oI+SUeIAVvy/9J+E56P7qkH82gkQQfbKp3JsScHC3BO5qI0SfYXr2g9cOC30GvgQkTL+itFrXfjfQe3+0F4094js2Ep7uWYjKS5ykhvqO3SOxE4dKTntFG0uPEHLtep/CXfoQPnG8OMhkxwcYWLaoTccE0heotQLgg+5iKezS+yACnZP5055o4urViQs//DgyBM3LgDLFdH19gm5dH2x+56t4u0Eojw7bifEk0cwdLsRa4rZyail/LYTVlrwoCsr1HB/EedGVUluvRpOtCGNpF49j85o1e094Xu6aoFXD0i6tWOdHkrWKAIc/+6Ta0mK3Jtx6jWvD0689lVQvRo1EPD/+3/8tx03oH4fM1n6hueOvfKUY0jTK8T7Tn2uUuwdFVQl2Tb/IVHRZbUKE9Nk=

>> This leaves open the question of what should happen with "nested"
>> types, like:
> I would say it's more a question about non recursively uniform parameters
> than about nesting

I never really understood why, but AFAIK such "non recursively uniform
parameters" are sometimes called "nested datatypes" or "non-regular
datatypes".
E.g.
https://www.kestrel.edu/home/people/meertens/publications/papers/Nested_datatypes.pdf

Stefan

[Coq-Club] Strict positivity description in CIC spec, William J. Bowman, 08/07/2019
- Re: [Coq-Club] Strict positivity description in CIC spec, roux cody, 08/07/2019
- Re: [Coq-Club] Strict positivity description in CIC spec, Hans Jacob Fehrmann Rojas, 08/07/2019
  - Re: [Coq-Club] Strict positivity description in CIC spec, William J. Bowman, 08/13/2019
    - Re: [Coq-Club] Strict positivity description in CIC spec, Valentin Robert, 08/13/2019
  - Re: [Coq-Club] Strict positivity description in CIC spec, Stefan Monnier, 08/26/2019
    - Re: [Coq-Club] Strict positivity description in CIC spec, Gaëtan Gilbert, 08/26/2019
      - Re: [Coq-Club] Strict positivity description in CIC spec, Stefan Monnier, 08/26/2019